Step | Hyp | Ref
| Expression |
1 | | cltq 7286 |
. 2
class
<Q |
2 | | vx |
. . . . . . 7
setvar ๐ฅ |
3 | 2 | cv 1352 |
. . . . . 6
class ๐ฅ |
4 | | cnq 7281 |
. . . . . 6
class
Q |
5 | 3, 4 | wcel 2148 |
. . . . 5
wff ๐ฅ โ
Q |
6 | | vy |
. . . . . . 7
setvar ๐ฆ |
7 | 6 | cv 1352 |
. . . . . 6
class ๐ฆ |
8 | 7, 4 | wcel 2148 |
. . . . 5
wff ๐ฆ โ
Q |
9 | 5, 8 | wa 104 |
. . . 4
wff (๐ฅ โ Q โง
๐ฆ โ
Q) |
10 | | vz |
. . . . . . . . . . . . . 14
setvar ๐ง |
11 | 10 | cv 1352 |
. . . . . . . . . . . . 13
class ๐ง |
12 | | vw |
. . . . . . . . . . . . . 14
setvar ๐ค |
13 | 12 | cv 1352 |
. . . . . . . . . . . . 13
class ๐ค |
14 | 11, 13 | cop 3597 |
. . . . . . . . . . . 12
class
โจ๐ง, ๐คโฉ |
15 | | ceq 7280 |
. . . . . . . . . . . 12
class
~Q |
16 | 14, 15 | cec 6535 |
. . . . . . . . . . 11
class
[โจ๐ง, ๐คโฉ]
~Q |
17 | 3, 16 | wceq 1353 |
. . . . . . . . . 10
wff ๐ฅ = [โจ๐ง, ๐คโฉ]
~Q |
18 | | vv |
. . . . . . . . . . . . . 14
setvar ๐ฃ |
19 | 18 | cv 1352 |
. . . . . . . . . . . . 13
class ๐ฃ |
20 | | vu |
. . . . . . . . . . . . . 14
setvar ๐ข |
21 | 20 | cv 1352 |
. . . . . . . . . . . . 13
class ๐ข |
22 | 19, 21 | cop 3597 |
. . . . . . . . . . . 12
class
โจ๐ฃ, ๐ขโฉ |
23 | 22, 15 | cec 6535 |
. . . . . . . . . . 11
class
[โจ๐ฃ, ๐ขโฉ]
~Q |
24 | 7, 23 | wceq 1353 |
. . . . . . . . . 10
wff ๐ฆ = [โจ๐ฃ, ๐ขโฉ]
~Q |
25 | 17, 24 | wa 104 |
. . . . . . . . 9
wff (๐ฅ = [โจ๐ง, ๐คโฉ] ~Q โง
๐ฆ = [โจ๐ฃ, ๐ขโฉ] ~Q
) |
26 | | cmi 7275 |
. . . . . . . . . . 11
class
ยทN |
27 | 11, 21, 26 | co 5877 |
. . . . . . . . . 10
class (๐ง
ยทN ๐ข) |
28 | 13, 19, 26 | co 5877 |
. . . . . . . . . 10
class (๐ค
ยทN ๐ฃ) |
29 | | clti 7276 |
. . . . . . . . . 10
class
<N |
30 | 27, 28, 29 | wbr 4005 |
. . . . . . . . 9
wff (๐ง
ยทN ๐ข) <N (๐ค
ยทN ๐ฃ) |
31 | 25, 30 | wa 104 |
. . . . . . . 8
wff ((๐ฅ = [โจ๐ง, ๐คโฉ] ~Q โง
๐ฆ = [โจ๐ฃ, ๐ขโฉ] ~Q ) โง
(๐ง
ยทN ๐ข) <N (๐ค
ยทN ๐ฃ)) |
32 | 31, 20 | wex 1492 |
. . . . . . 7
wff
โ๐ข((๐ฅ = [โจ๐ง, ๐คโฉ] ~Q โง
๐ฆ = [โจ๐ฃ, ๐ขโฉ] ~Q ) โง
(๐ง
ยทN ๐ข) <N (๐ค
ยทN ๐ฃ)) |
33 | 32, 18 | wex 1492 |
. . . . . 6
wff
โ๐ฃโ๐ข((๐ฅ = [โจ๐ง, ๐คโฉ] ~Q โง
๐ฆ = [โจ๐ฃ, ๐ขโฉ] ~Q ) โง
(๐ง
ยทN ๐ข) <N (๐ค
ยทN ๐ฃ)) |
34 | 33, 12 | wex 1492 |
. . . . 5
wff
โ๐คโ๐ฃโ๐ข((๐ฅ = [โจ๐ง, ๐คโฉ] ~Q โง
๐ฆ = [โจ๐ฃ, ๐ขโฉ] ~Q ) โง
(๐ง
ยทN ๐ข) <N (๐ค
ยทN ๐ฃ)) |
35 | 34, 10 | wex 1492 |
. . . 4
wff
โ๐งโ๐คโ๐ฃโ๐ข((๐ฅ = [โจ๐ง, ๐คโฉ] ~Q โง
๐ฆ = [โจ๐ฃ, ๐ขโฉ] ~Q ) โง
(๐ง
ยทN ๐ข) <N (๐ค
ยทN ๐ฃ)) |
36 | 9, 35 | wa 104 |
. . 3
wff ((๐ฅ โ Q โง
๐ฆ โ Q)
โง โ๐งโ๐คโ๐ฃโ๐ข((๐ฅ = [โจ๐ง, ๐คโฉ] ~Q โง
๐ฆ = [โจ๐ฃ, ๐ขโฉ] ~Q ) โง
(๐ง
ยทN ๐ข) <N (๐ค
ยทN ๐ฃ))) |
37 | 36, 2, 6 | copab 4065 |
. 2
class
{โจ๐ฅ, ๐ฆโฉ โฃ ((๐ฅ โ Q โง
๐ฆ โ Q)
โง โ๐งโ๐คโ๐ฃโ๐ข((๐ฅ = [โจ๐ง, ๐คโฉ] ~Q โง
๐ฆ = [โจ๐ฃ, ๐ขโฉ] ~Q ) โง
(๐ง
ยทN ๐ข) <N (๐ค
ยทN ๐ฃ)))} |
38 | 1, 37 | wceq 1353 |
1
wff
<Q = {โจ๐ฅ, ๐ฆโฉ โฃ ((๐ฅ โ Q โง ๐ฆ โ Q) โง
โ๐งโ๐คโ๐ฃโ๐ข((๐ฅ = [โจ๐ง, ๐คโฉ] ~Q โง
๐ฆ = [โจ๐ฃ, ๐ขโฉ] ~Q ) โง
(๐ง
ยทN ๐ข) <N (๐ค
ยทN ๐ฃ)))} |