Step | Hyp | Ref
| Expression |
1 | | ccnf 9605 |
. 2
class
CNF |
2 | | vx |
. . 3
setvar ๐ฅ |
3 | | vy |
. . 3
setvar ๐ฆ |
4 | | con0 6321 |
. . 3
class
On |
5 | | vf |
. . . 4
setvar ๐ |
6 | | vg |
. . . . . . 7
setvar ๐ |
7 | 6 | cv 1541 |
. . . . . 6
class ๐ |
8 | | c0 4286 |
. . . . . 6
class
โ
|
9 | | cfsupp 9311 |
. . . . . 6
class
finSupp |
10 | 7, 8, 9 | wbr 5109 |
. . . . 5
wff ๐ finSupp
โ
|
11 | 2 | cv 1541 |
. . . . . 6
class ๐ฅ |
12 | 3 | cv 1541 |
. . . . . 6
class ๐ฆ |
13 | | cmap 8771 |
. . . . . 6
class
โm |
14 | 11, 12, 13 | co 7361 |
. . . . 5
class (๐ฅ โm ๐ฆ) |
15 | 10, 6, 14 | crab 3406 |
. . . 4
class {๐ โ (๐ฅ โm ๐ฆ) โฃ ๐ finSupp โ
} |
16 | | vh |
. . . . 5
setvar โ |
17 | 5 | cv 1541 |
. . . . . . 7
class ๐ |
18 | | csupp 8096 |
. . . . . . 7
class
supp |
19 | 17, 8, 18 | co 7361 |
. . . . . 6
class (๐ supp โ
) |
20 | | cep 5540 |
. . . . . 6
class
E |
21 | 19, 20 | coi 9453 |
. . . . 5
class OrdIso( E
, (๐ supp
โ
)) |
22 | 16 | cv 1541 |
. . . . . . 7
class โ |
23 | 22 | cdm 5637 |
. . . . . 6
class dom โ |
24 | | vk |
. . . . . . . 8
setvar ๐ |
25 | | vz |
. . . . . . . 8
setvar ๐ง |
26 | | cvv 3447 |
. . . . . . . 8
class
V |
27 | 24 | cv 1541 |
. . . . . . . . . . . 12
class ๐ |
28 | 27, 22 | cfv 6500 |
. . . . . . . . . . 11
class (โโ๐) |
29 | | coe 8415 |
. . . . . . . . . . 11
class
โo |
30 | 11, 28, 29 | co 7361 |
. . . . . . . . . 10
class (๐ฅ โo (โโ๐)) |
31 | 28, 17 | cfv 6500 |
. . . . . . . . . 10
class (๐โ(โโ๐)) |
32 | | comu 8414 |
. . . . . . . . . 10
class
ยทo |
33 | 30, 31, 32 | co 7361 |
. . . . . . . . 9
class ((๐ฅ โo (โโ๐)) ยทo (๐โ(โโ๐))) |
34 | 25 | cv 1541 |
. . . . . . . . 9
class ๐ง |
35 | | coa 8413 |
. . . . . . . . 9
class
+o |
36 | 33, 34, 35 | co 7361 |
. . . . . . . 8
class (((๐ฅ โo (โโ๐)) ยทo (๐โ(โโ๐))) +o ๐ง) |
37 | 24, 25, 26, 26, 36 | cmpo 7363 |
. . . . . . 7
class (๐ โ V, ๐ง โ V โฆ (((๐ฅ โo (โโ๐)) ยทo (๐โ(โโ๐))) +o ๐ง)) |
38 | 37, 8 | cseqom 8397 |
. . . . . 6
class
seqฯ((๐ โ V, ๐ง โ V โฆ (((๐ฅ โo (โโ๐)) ยทo (๐โ(โโ๐))) +o ๐ง)), โ
) |
39 | 23, 38 | cfv 6500 |
. . . . 5
class
(seqฯ((๐ โ V, ๐ง โ V โฆ (((๐ฅ โo (โโ๐)) ยทo (๐โ(โโ๐))) +o ๐ง)), โ
)โdom โ) |
40 | 16, 21, 39 | csb 3859 |
. . . 4
class
โฆOrdIso( E , (๐ supp โ
)) / โโฆ(seqฯ((๐ โ V, ๐ง โ V โฆ (((๐ฅ โo (โโ๐)) ยทo (๐โ(โโ๐))) +o ๐ง)), โ
)โdom โ) |
41 | 5, 15, 40 | cmpt 5192 |
. . 3
class (๐ โ {๐ โ (๐ฅ โm ๐ฆ) โฃ ๐ finSupp โ
} โฆ
โฆOrdIso( E , (๐ supp โ
)) / โโฆ(seqฯ((๐ โ V, ๐ง โ V โฆ (((๐ฅ โo (โโ๐)) ยทo (๐โ(โโ๐))) +o ๐ง)), โ
)โdom โ)) |
42 | 2, 3, 4, 4, 41 | cmpo 7363 |
. 2
class (๐ฅ โ On, ๐ฆ โ On โฆ (๐ โ {๐ โ (๐ฅ โm ๐ฆ) โฃ ๐ finSupp โ
} โฆ
โฆOrdIso( E , (๐ supp โ
)) / โโฆ(seqฯ((๐ โ V, ๐ง โ V โฆ (((๐ฅ โo (โโ๐)) ยทo (๐โ(โโ๐))) +o ๐ง)), โ
)โdom โ))) |
43 | 1, 42 | wceq 1542 |
1
wff CNF =
(๐ฅ โ On, ๐ฆ โ On โฆ (๐ โ {๐ โ (๐ฅ โm ๐ฆ) โฃ ๐ finSupp โ
} โฆ
โฆOrdIso( E , (๐ supp โ
)) / โโฆ(seqฯ((๐ โ V, ๐ง โ V โฆ (((๐ฅ โo (โโ๐)) ยทo (๐โ(โโ๐))) +o ๐ง)), โ
)โdom โ))) |