Detailed syntax breakdown of Definition df-iltp
Step | Hyp | Ref
| Expression |
1 | | cltp 6393 |
. 2
class
<P |
2 | | vx |
. . . . . . 7
setvar 𝑥 |
3 | 2 | cv 1242 |
. . . . . 6
class 𝑥 |
4 | | cnp 6389 |
. . . . . 6
class
P |
5 | 3, 4 | wcel 1393 |
. . . . 5
wff 𝑥 ∈
P |
6 | | vy |
. . . . . . 7
setvar 𝑦 |
7 | 6 | cv 1242 |
. . . . . 6
class 𝑦 |
8 | 7, 4 | wcel 1393 |
. . . . 5
wff 𝑦 ∈
P |
9 | 5, 8 | wa 97 |
. . . 4
wff (𝑥 ∈ P ∧
𝑦 ∈
P) |
10 | | vq |
. . . . . . . 8
setvar 𝑞 |
11 | 10 | cv 1242 |
. . . . . . 7
class 𝑞 |
12 | | c2nd 5766 |
. . . . . . . 8
class
2nd |
13 | 3, 12 | cfv 4902 |
. . . . . . 7
class
(2nd ‘𝑥) |
14 | 11, 13 | wcel 1393 |
. . . . . 6
wff 𝑞 ∈ (2nd
‘𝑥) |
15 | | c1st 5765 |
. . . . . . . 8
class
1st |
16 | 7, 15 | cfv 4902 |
. . . . . . 7
class
(1st ‘𝑦) |
17 | 11, 16 | wcel 1393 |
. . . . . 6
wff 𝑞 ∈ (1st
‘𝑦) |
18 | 14, 17 | wa 97 |
. . . . 5
wff (𝑞 ∈ (2nd
‘𝑥) ∧ 𝑞 ∈ (1st
‘𝑦)) |
19 | | cnq 6378 |
. . . . 5
class
Q |
20 | 18, 10, 19 | wrex 2307 |
. . . 4
wff
∃𝑞 ∈
Q (𝑞 ∈
(2nd ‘𝑥)
∧ 𝑞 ∈
(1st ‘𝑦)) |
21 | 9, 20 | wa 97 |
. . 3
wff ((𝑥 ∈ P ∧
𝑦 ∈ P)
∧ ∃𝑞 ∈
Q (𝑞 ∈
(2nd ‘𝑥)
∧ 𝑞 ∈
(1st ‘𝑦))) |
22 | 21, 2, 6 | copab 3817 |
. 2
class
{〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ P ∧
𝑦 ∈ P)
∧ ∃𝑞 ∈
Q (𝑞 ∈
(2nd ‘𝑥)
∧ 𝑞 ∈
(1st ‘𝑦)))} |
23 | 1, 22 | wceq 1243 |
1
wff
<P = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ P ∧ 𝑦 ∈ P) ∧
∃𝑞 ∈
Q (𝑞 ∈
(2nd ‘𝑥)
∧ 𝑞 ∈
(1st ‘𝑦)))} |