Step | Hyp | Ref
| Expression |
1 | | cnfcom.1 |
. 2
โข (๐ โ ๐ผ โ dom ๐บ) |
2 | | cnfcom.s |
. . . . . 6
โข ๐ = dom (ฯ CNF ๐ด) |
3 | | omelon 9587 |
. . . . . . 7
โข ฯ
โ On |
4 | 3 | a1i 11 |
. . . . . 6
โข (๐ โ ฯ โ
On) |
5 | | cnfcom.a |
. . . . . 6
โข (๐ โ ๐ด โ On) |
6 | | cnfcom.g |
. . . . . 6
โข ๐บ = OrdIso( E , (๐น supp โ
)) |
7 | | cnfcom.f |
. . . . . . 7
โข ๐น = (โก(ฯ CNF ๐ด)โ๐ต) |
8 | 2, 4, 5 | cantnff1o 9637 |
. . . . . . . . 9
โข (๐ โ (ฯ CNF ๐ด):๐โ1-1-ontoโ(ฯ โo ๐ด)) |
9 | | f1ocnv 6797 |
. . . . . . . . 9
โข ((ฯ
CNF ๐ด):๐โ1-1-ontoโ(ฯ โo ๐ด) โ โก(ฯ CNF ๐ด):(ฯ โo ๐ด)โ1-1-ontoโ๐) |
10 | | f1of 6785 |
. . . . . . . . 9
โข (โก(ฯ CNF ๐ด):(ฯ โo ๐ด)โ1-1-ontoโ๐ โ โก(ฯ CNF ๐ด):(ฯ โo ๐ด)โถ๐) |
11 | 8, 9, 10 | 3syl 18 |
. . . . . . . 8
โข (๐ โ โก(ฯ CNF ๐ด):(ฯ โo ๐ด)โถ๐) |
12 | | cnfcom.b |
. . . . . . . 8
โข (๐ โ ๐ต โ (ฯ โo ๐ด)) |
13 | 11, 12 | ffvelcdmd 7037 |
. . . . . . 7
โข (๐ โ (โก(ฯ CNF ๐ด)โ๐ต) โ ๐) |
14 | 7, 13 | eqeltrid 2838 |
. . . . . 6
โข (๐ โ ๐น โ ๐) |
15 | 2, 4, 5, 6, 14 | cantnfcl 9608 |
. . . . 5
โข (๐ โ ( E We (๐น supp โ
) โง dom ๐บ โ ฯ)) |
16 | 15 | simprd 497 |
. . . 4
โข (๐ โ dom ๐บ โ ฯ) |
17 | | elnn 7814 |
. . . 4
โข ((๐ผ โ dom ๐บ โง dom ๐บ โ ฯ) โ ๐ผ โ ฯ) |
18 | 1, 16, 17 | syl2anc 585 |
. . 3
โข (๐ โ ๐ผ โ ฯ) |
19 | | eleq1 2822 |
. . . . . 6
โข (๐ค = ๐ผ โ (๐ค โ dom ๐บ โ ๐ผ โ dom ๐บ)) |
20 | | suceq 6384 |
. . . . . . . 8
โข (๐ค = ๐ผ โ suc ๐ค = suc ๐ผ) |
21 | 20 | fveq2d 6847 |
. . . . . . 7
โข (๐ค = ๐ผ โ (๐โsuc ๐ค) = (๐โsuc ๐ผ)) |
22 | 20 | fveq2d 6847 |
. . . . . . 7
โข (๐ค = ๐ผ โ (๐ปโsuc ๐ค) = (๐ปโsuc ๐ผ)) |
23 | | fveq2 6843 |
. . . . . . . . 9
โข (๐ค = ๐ผ โ (๐บโ๐ค) = (๐บโ๐ผ)) |
24 | 23 | oveq2d 7374 |
. . . . . . . 8
โข (๐ค = ๐ผ โ (ฯ โo (๐บโ๐ค)) = (ฯ โo (๐บโ๐ผ))) |
25 | | 2fveq3 6848 |
. . . . . . . 8
โข (๐ค = ๐ผ โ (๐นโ(๐บโ๐ค)) = (๐นโ(๐บโ๐ผ))) |
26 | 24, 25 | oveq12d 7376 |
. . . . . . 7
โข (๐ค = ๐ผ โ ((ฯ โo (๐บโ๐ค)) ยทo (๐นโ(๐บโ๐ค))) = ((ฯ โo (๐บโ๐ผ)) ยทo (๐นโ(๐บโ๐ผ)))) |
27 | 21, 22, 26 | f1oeq123d 6779 |
. . . . . 6
โข (๐ค = ๐ผ โ ((๐โsuc ๐ค):(๐ปโsuc ๐ค)โ1-1-ontoโ((ฯ โo (๐บโ๐ค)) ยทo (๐นโ(๐บโ๐ค))) โ (๐โsuc ๐ผ):(๐ปโsuc ๐ผ)โ1-1-ontoโ((ฯ โo (๐บโ๐ผ)) ยทo (๐นโ(๐บโ๐ผ))))) |
28 | 19, 27 | imbi12d 345 |
. . . . 5
โข (๐ค = ๐ผ โ ((๐ค โ dom ๐บ โ (๐โsuc ๐ค):(๐ปโsuc ๐ค)โ1-1-ontoโ((ฯ โo (๐บโ๐ค)) ยทo (๐นโ(๐บโ๐ค)))) โ (๐ผ โ dom ๐บ โ (๐โsuc ๐ผ):(๐ปโsuc ๐ผ)โ1-1-ontoโ((ฯ โo (๐บโ๐ผ)) ยทo (๐นโ(๐บโ๐ผ)))))) |
29 | 28 | imbi2d 341 |
. . . 4
โข (๐ค = ๐ผ โ ((๐ โ (๐ค โ dom ๐บ โ (๐โsuc ๐ค):(๐ปโsuc ๐ค)โ1-1-ontoโ((ฯ โo (๐บโ๐ค)) ยทo (๐นโ(๐บโ๐ค))))) โ (๐ โ (๐ผ โ dom ๐บ โ (๐โsuc ๐ผ):(๐ปโsuc ๐ผ)โ1-1-ontoโ((ฯ โo (๐บโ๐ผ)) ยทo (๐นโ(๐บโ๐ผ))))))) |
30 | | eleq1 2822 |
. . . . . 6
โข (๐ค = โ
โ (๐ค โ dom ๐บ โ โ
โ dom ๐บ)) |
31 | | suceq 6384 |
. . . . . . . 8
โข (๐ค = โ
โ suc ๐ค = suc โ
) |
32 | 31 | fveq2d 6847 |
. . . . . . 7
โข (๐ค = โ
โ (๐โsuc ๐ค) = (๐โsuc โ
)) |
33 | 31 | fveq2d 6847 |
. . . . . . 7
โข (๐ค = โ
โ (๐ปโsuc ๐ค) = (๐ปโsuc โ
)) |
34 | | fveq2 6843 |
. . . . . . . . 9
โข (๐ค = โ
โ (๐บโ๐ค) = (๐บโโ
)) |
35 | 34 | oveq2d 7374 |
. . . . . . . 8
โข (๐ค = โ
โ (ฯ
โo (๐บโ๐ค)) = (ฯ โo (๐บโโ
))) |
36 | | 2fveq3 6848 |
. . . . . . . 8
โข (๐ค = โ
โ (๐นโ(๐บโ๐ค)) = (๐นโ(๐บโโ
))) |
37 | 35, 36 | oveq12d 7376 |
. . . . . . 7
โข (๐ค = โ
โ ((ฯ
โo (๐บโ๐ค)) ยทo (๐นโ(๐บโ๐ค))) = ((ฯ โo (๐บโโ
))
ยทo (๐นโ(๐บโโ
)))) |
38 | 32, 33, 37 | f1oeq123d 6779 |
. . . . . 6
โข (๐ค = โ
โ ((๐โsuc ๐ค):(๐ปโsuc ๐ค)โ1-1-ontoโ((ฯ โo (๐บโ๐ค)) ยทo (๐นโ(๐บโ๐ค))) โ (๐โsuc โ
):(๐ปโsuc โ
)โ1-1-ontoโ((ฯ โo (๐บโโ
))
ยทo (๐นโ(๐บโโ
))))) |
39 | 30, 38 | imbi12d 345 |
. . . . 5
โข (๐ค = โ
โ ((๐ค โ dom ๐บ โ (๐โsuc ๐ค):(๐ปโsuc ๐ค)โ1-1-ontoโ((ฯ โo (๐บโ๐ค)) ยทo (๐นโ(๐บโ๐ค)))) โ (โ
โ dom ๐บ โ (๐โsuc โ
):(๐ปโsuc โ
)โ1-1-ontoโ((ฯ โo (๐บโโ
))
ยทo (๐นโ(๐บโโ
)))))) |
40 | | eleq1 2822 |
. . . . . 6
โข (๐ค = ๐ฆ โ (๐ค โ dom ๐บ โ ๐ฆ โ dom ๐บ)) |
41 | | suceq 6384 |
. . . . . . . 8
โข (๐ค = ๐ฆ โ suc ๐ค = suc ๐ฆ) |
42 | 41 | fveq2d 6847 |
. . . . . . 7
โข (๐ค = ๐ฆ โ (๐โsuc ๐ค) = (๐โsuc ๐ฆ)) |
43 | 41 | fveq2d 6847 |
. . . . . . 7
โข (๐ค = ๐ฆ โ (๐ปโsuc ๐ค) = (๐ปโsuc ๐ฆ)) |
44 | | fveq2 6843 |
. . . . . . . . 9
โข (๐ค = ๐ฆ โ (๐บโ๐ค) = (๐บโ๐ฆ)) |
45 | 44 | oveq2d 7374 |
. . . . . . . 8
โข (๐ค = ๐ฆ โ (ฯ โo (๐บโ๐ค)) = (ฯ โo (๐บโ๐ฆ))) |
46 | | 2fveq3 6848 |
. . . . . . . 8
โข (๐ค = ๐ฆ โ (๐นโ(๐บโ๐ค)) = (๐นโ(๐บโ๐ฆ))) |
47 | 45, 46 | oveq12d 7376 |
. . . . . . 7
โข (๐ค = ๐ฆ โ ((ฯ โo (๐บโ๐ค)) ยทo (๐นโ(๐บโ๐ค))) = ((ฯ โo (๐บโ๐ฆ)) ยทo (๐นโ(๐บโ๐ฆ)))) |
48 | 42, 43, 47 | f1oeq123d 6779 |
. . . . . 6
โข (๐ค = ๐ฆ โ ((๐โsuc ๐ค):(๐ปโsuc ๐ค)โ1-1-ontoโ((ฯ โo (๐บโ๐ค)) ยทo (๐นโ(๐บโ๐ค))) โ (๐โsuc ๐ฆ):(๐ปโsuc ๐ฆ)โ1-1-ontoโ((ฯ โo (๐บโ๐ฆ)) ยทo (๐นโ(๐บโ๐ฆ))))) |
49 | 40, 48 | imbi12d 345 |
. . . . 5
โข (๐ค = ๐ฆ โ ((๐ค โ dom ๐บ โ (๐โsuc ๐ค):(๐ปโsuc ๐ค)โ1-1-ontoโ((ฯ โo (๐บโ๐ค)) ยทo (๐นโ(๐บโ๐ค)))) โ (๐ฆ โ dom ๐บ โ (๐โsuc ๐ฆ):(๐ปโsuc ๐ฆ)โ1-1-ontoโ((ฯ โo (๐บโ๐ฆ)) ยทo (๐นโ(๐บโ๐ฆ)))))) |
50 | | eleq1 2822 |
. . . . . 6
โข (๐ค = suc ๐ฆ โ (๐ค โ dom ๐บ โ suc ๐ฆ โ dom ๐บ)) |
51 | | suceq 6384 |
. . . . . . . 8
โข (๐ค = suc ๐ฆ โ suc ๐ค = suc suc ๐ฆ) |
52 | 51 | fveq2d 6847 |
. . . . . . 7
โข (๐ค = suc ๐ฆ โ (๐โsuc ๐ค) = (๐โsuc suc ๐ฆ)) |
53 | 51 | fveq2d 6847 |
. . . . . . 7
โข (๐ค = suc ๐ฆ โ (๐ปโsuc ๐ค) = (๐ปโsuc suc ๐ฆ)) |
54 | | fveq2 6843 |
. . . . . . . . 9
โข (๐ค = suc ๐ฆ โ (๐บโ๐ค) = (๐บโsuc ๐ฆ)) |
55 | 54 | oveq2d 7374 |
. . . . . . . 8
โข (๐ค = suc ๐ฆ โ (ฯ โo (๐บโ๐ค)) = (ฯ โo (๐บโsuc ๐ฆ))) |
56 | | 2fveq3 6848 |
. . . . . . . 8
โข (๐ค = suc ๐ฆ โ (๐นโ(๐บโ๐ค)) = (๐นโ(๐บโsuc ๐ฆ))) |
57 | 55, 56 | oveq12d 7376 |
. . . . . . 7
โข (๐ค = suc ๐ฆ โ ((ฯ โo (๐บโ๐ค)) ยทo (๐นโ(๐บโ๐ค))) = ((ฯ โo (๐บโsuc ๐ฆ)) ยทo (๐นโ(๐บโsuc ๐ฆ)))) |
58 | 52, 53, 57 | f1oeq123d 6779 |
. . . . . 6
โข (๐ค = suc ๐ฆ โ ((๐โsuc ๐ค):(๐ปโsuc ๐ค)โ1-1-ontoโ((ฯ โo (๐บโ๐ค)) ยทo (๐นโ(๐บโ๐ค))) โ (๐โsuc suc ๐ฆ):(๐ปโsuc suc ๐ฆ)โ1-1-ontoโ((ฯ โo (๐บโsuc ๐ฆ)) ยทo (๐นโ(๐บโsuc ๐ฆ))))) |
59 | 50, 58 | imbi12d 345 |
. . . . 5
โข (๐ค = suc ๐ฆ โ ((๐ค โ dom ๐บ โ (๐โsuc ๐ค):(๐ปโsuc ๐ค)โ1-1-ontoโ((ฯ โo (๐บโ๐ค)) ยทo (๐นโ(๐บโ๐ค)))) โ (suc ๐ฆ โ dom ๐บ โ (๐โsuc suc ๐ฆ):(๐ปโsuc suc ๐ฆ)โ1-1-ontoโ((ฯ โo (๐บโsuc ๐ฆ)) ยทo (๐นโ(๐บโsuc ๐ฆ)))))) |
60 | 5 | adantr 482 |
. . . . . . 7
โข ((๐ โง โ
โ dom ๐บ) โ ๐ด โ On) |
61 | 12 | adantr 482 |
. . . . . . 7
โข ((๐ โง โ
โ dom ๐บ) โ ๐ต โ (ฯ โo ๐ด)) |
62 | | cnfcom.h |
. . . . . . 7
โข ๐ป = seqฯ((๐ โ V, ๐ง โ V โฆ (๐ +o ๐ง)), โ
) |
63 | | cnfcom.t |
. . . . . . 7
โข ๐ = seqฯ((๐ โ V, ๐ โ V โฆ ๐พ), โ
) |
64 | | cnfcom.m |
. . . . . . 7
โข ๐ = ((ฯ โo
(๐บโ๐)) ยทo (๐นโ(๐บโ๐))) |
65 | | cnfcom.k |
. . . . . . 7
โข ๐พ = ((๐ฅ โ ๐ โฆ (dom ๐ +o ๐ฅ)) โช โก(๐ฅ โ dom ๐ โฆ (๐ +o ๐ฅ))) |
66 | | simpr 486 |
. . . . . . 7
โข ((๐ โง โ
โ dom ๐บ) โ โ
โ dom
๐บ) |
67 | 3 | a1i 11 |
. . . . . . . 8
โข ((๐ โง โ
โ dom ๐บ) โ ฯ โ
On) |
68 | | suppssdm 8109 |
. . . . . . . . . . 11
โข (๐น supp โ
) โ dom ๐น |
69 | 2, 4, 5 | cantnfs 9607 |
. . . . . . . . . . . . 13
โข (๐ โ (๐น โ ๐ โ (๐น:๐ดโถฯ โง ๐น finSupp โ
))) |
70 | 14, 69 | mpbid 231 |
. . . . . . . . . . . 12
โข (๐ โ (๐น:๐ดโถฯ โง ๐น finSupp โ
)) |
71 | 70 | simpld 496 |
. . . . . . . . . . 11
โข (๐ โ ๐น:๐ดโถฯ) |
72 | 68, 71 | fssdm 6689 |
. . . . . . . . . 10
โข (๐ โ (๐น supp โ
) โ ๐ด) |
73 | | onss 7720 |
. . . . . . . . . . 11
โข (๐ด โ On โ ๐ด โ On) |
74 | 5, 73 | syl 17 |
. . . . . . . . . 10
โข (๐ โ ๐ด โ On) |
75 | 72, 74 | sstrd 3955 |
. . . . . . . . 9
โข (๐ โ (๐น supp โ
) โ On) |
76 | 6 | oif 9471 |
. . . . . . . . . 10
โข ๐บ:dom ๐บโถ(๐น supp โ
) |
77 | 76 | ffvelcdmi 7035 |
. . . . . . . . 9
โข (โ
โ dom ๐บ โ (๐บโโ
) โ (๐น supp โ
)) |
78 | | ssel2 3940 |
. . . . . . . . 9
โข (((๐น supp โ
) โ On โง
(๐บโโ
) โ
(๐น supp โ
)) โ
(๐บโโ
) โ
On) |
79 | 75, 77, 78 | syl2an 597 |
. . . . . . . 8
โข ((๐ โง โ
โ dom ๐บ) โ (๐บโโ
) โ On) |
80 | | peano1 7826 |
. . . . . . . . 9
โข โ
โ ฯ |
81 | 80 | a1i 11 |
. . . . . . . 8
โข ((๐ โง โ
โ dom ๐บ) โ โ
โ
ฯ) |
82 | | oen0 8534 |
. . . . . . . 8
โข
(((ฯ โ On โง (๐บโโ
) โ On) โง โ
โ ฯ) โ โ
โ (ฯ โo (๐บโโ
))) |
83 | 67, 79, 81, 82 | syl21anc 837 |
. . . . . . 7
โข ((๐ โง โ
โ dom ๐บ) โ โ
โ (ฯ
โo (๐บโโ
))) |
84 | | 0ex 5265 |
. . . . . . . . 9
โข โ
โ V |
85 | 63 | seqom0g 8403 |
. . . . . . . . 9
โข (โ
โ V โ (๐โโ
) = โ
) |
86 | 84, 85 | ax-mp 5 |
. . . . . . . 8
โข (๐โโ
) =
โ
|
87 | | f1o0 6822 |
. . . . . . . . . 10
โข
โ
:โ
โ1-1-ontoโโ
|
88 | 62 | seqom0g 8403 |
. . . . . . . . . . 11
โข (โ
โ V โ (๐ปโโ
) = โ
) |
89 | | f1oeq2 6774 |
. . . . . . . . . . 11
โข ((๐ปโโ
) = โ
โ
(โ
:(๐ปโโ
)โ1-1-ontoโโ
โ โ
:โ
โ1-1-ontoโโ
)) |
90 | 84, 88, 89 | mp2b 10 |
. . . . . . . . . 10
โข
(โ
:(๐ปโโ
)โ1-1-ontoโโ
โ โ
:โ
โ1-1-ontoโโ
) |
91 | 87, 90 | mpbir 230 |
. . . . . . . . 9
โข
โ
:(๐ปโโ
)โ1-1-ontoโโ
|
92 | | f1oeq1 6773 |
. . . . . . . . 9
โข ((๐โโ
) = โ
โ
((๐โโ
):(๐ปโโ
)โ1-1-ontoโโ
โ โ
:(๐ปโโ
)โ1-1-ontoโโ
)) |
93 | 91, 92 | mpbiri 258 |
. . . . . . . 8
โข ((๐โโ
) = โ
โ
(๐โโ
):(๐ปโโ
)โ1-1-ontoโโ
) |
94 | 86, 93 | mp1i 13 |
. . . . . . 7
โข ((๐ โง โ
โ dom ๐บ) โ (๐โโ
):(๐ปโโ
)โ1-1-ontoโโ
) |
95 | 2, 60, 61, 7, 6, 62, 63, 64, 65, 66, 83, 94 | cnfcomlem 9640 |
. . . . . 6
โข ((๐ โง โ
โ dom ๐บ) โ (๐โsuc โ
):(๐ปโsuc โ
)โ1-1-ontoโ((ฯ โo (๐บโโ
))
ยทo (๐นโ(๐บโโ
)))) |
96 | 95 | ex 414 |
. . . . 5
โข (๐ โ (โ
โ dom ๐บ โ (๐โsuc โ
):(๐ปโsuc โ
)โ1-1-ontoโ((ฯ โo (๐บโโ
))
ยทo (๐นโ(๐บโโ
))))) |
97 | 6 | oicl 9470 |
. . . . . . . . . 10
โข Ord dom
๐บ |
98 | | ordtr 6332 |
. . . . . . . . . 10
โข (Ord dom
๐บ โ Tr dom ๐บ) |
99 | 97, 98 | ax-mp 5 |
. . . . . . . . 9
โข Tr dom
๐บ |
100 | | trsuc 6405 |
. . . . . . . . 9
โข ((Tr dom
๐บ โง suc ๐ฆ โ dom ๐บ) โ ๐ฆ โ dom ๐บ) |
101 | 99, 100 | mpan 689 |
. . . . . . . 8
โข (suc
๐ฆ โ dom ๐บ โ ๐ฆ โ dom ๐บ) |
102 | 101 | imim1i 63 |
. . . . . . 7
โข ((๐ฆ โ dom ๐บ โ (๐โsuc ๐ฆ):(๐ปโsuc ๐ฆ)โ1-1-ontoโ((ฯ โo (๐บโ๐ฆ)) ยทo (๐นโ(๐บโ๐ฆ)))) โ (suc ๐ฆ โ dom ๐บ โ (๐โsuc ๐ฆ):(๐ปโsuc ๐ฆ)โ1-1-ontoโ((ฯ โo (๐บโ๐ฆ)) ยทo (๐นโ(๐บโ๐ฆ))))) |
103 | 5 | ad2antrr 725 |
. . . . . . . . . 10
โข (((๐ โง ๐ฆ โ ฯ) โง (suc ๐ฆ โ dom ๐บ โง (๐โsuc ๐ฆ):(๐ปโsuc ๐ฆ)โ1-1-ontoโ((ฯ โo (๐บโ๐ฆ)) ยทo (๐นโ(๐บโ๐ฆ))))) โ ๐ด โ On) |
104 | 12 | ad2antrr 725 |
. . . . . . . . . 10
โข (((๐ โง ๐ฆ โ ฯ) โง (suc ๐ฆ โ dom ๐บ โง (๐โsuc ๐ฆ):(๐ปโsuc ๐ฆ)โ1-1-ontoโ((ฯ โo (๐บโ๐ฆ)) ยทo (๐นโ(๐บโ๐ฆ))))) โ ๐ต โ (ฯ โo ๐ด)) |
105 | | simprl 770 |
. . . . . . . . . 10
โข (((๐ โง ๐ฆ โ ฯ) โง (suc ๐ฆ โ dom ๐บ โง (๐โsuc ๐ฆ):(๐ปโsuc ๐ฆ)โ1-1-ontoโ((ฯ โo (๐บโ๐ฆ)) ยทo (๐นโ(๐บโ๐ฆ))))) โ suc ๐ฆ โ dom ๐บ) |
106 | 74 | ad2antrr 725 |
. . . . . . . . . . . . . . 15
โข (((๐ โง ๐ฆ โ ฯ) โง (suc ๐ฆ โ dom ๐บ โง (๐โsuc ๐ฆ):(๐ปโsuc ๐ฆ)โ1-1-ontoโ((ฯ โo (๐บโ๐ฆ)) ยทo (๐นโ(๐บโ๐ฆ))))) โ ๐ด โ On) |
107 | 72 | ad2antrr 725 |
. . . . . . . . . . . . . . . 16
โข (((๐ โง ๐ฆ โ ฯ) โง (suc ๐ฆ โ dom ๐บ โง (๐โsuc ๐ฆ):(๐ปโsuc ๐ฆ)โ1-1-ontoโ((ฯ โo (๐บโ๐ฆ)) ยทo (๐นโ(๐บโ๐ฆ))))) โ (๐น supp โ
) โ ๐ด) |
108 | 76 | ffvelcdmi 7035 |
. . . . . . . . . . . . . . . . 17
โข (suc
๐ฆ โ dom ๐บ โ (๐บโsuc ๐ฆ) โ (๐น supp โ
)) |
109 | 108 | ad2antrl 727 |
. . . . . . . . . . . . . . . 16
โข (((๐ โง ๐ฆ โ ฯ) โง (suc ๐ฆ โ dom ๐บ โง (๐โsuc ๐ฆ):(๐ปโsuc ๐ฆ)โ1-1-ontoโ((ฯ โo (๐บโ๐ฆ)) ยทo (๐นโ(๐บโ๐ฆ))))) โ (๐บโsuc ๐ฆ) โ (๐น supp โ
)) |
110 | 107, 109 | sseldd 3946 |
. . . . . . . . . . . . . . 15
โข (((๐ โง ๐ฆ โ ฯ) โง (suc ๐ฆ โ dom ๐บ โง (๐โsuc ๐ฆ):(๐ปโsuc ๐ฆ)โ1-1-ontoโ((ฯ โo (๐บโ๐ฆ)) ยทo (๐นโ(๐บโ๐ฆ))))) โ (๐บโsuc ๐ฆ) โ ๐ด) |
111 | 106, 110 | sseldd 3946 |
. . . . . . . . . . . . . 14
โข (((๐ โง ๐ฆ โ ฯ) โง (suc ๐ฆ โ dom ๐บ โง (๐โsuc ๐ฆ):(๐ปโsuc ๐ฆ)โ1-1-ontoโ((ฯ โo (๐บโ๐ฆ)) ยทo (๐นโ(๐บโ๐ฆ))))) โ (๐บโsuc ๐ฆ) โ On) |
112 | | eloni 6328 |
. . . . . . . . . . . . . 14
โข ((๐บโsuc ๐ฆ) โ On โ Ord (๐บโsuc ๐ฆ)) |
113 | 111, 112 | syl 17 |
. . . . . . . . . . . . 13
โข (((๐ โง ๐ฆ โ ฯ) โง (suc ๐ฆ โ dom ๐บ โง (๐โsuc ๐ฆ):(๐ปโsuc ๐ฆ)โ1-1-ontoโ((ฯ โo (๐บโ๐ฆ)) ยทo (๐นโ(๐บโ๐ฆ))))) โ Ord (๐บโsuc ๐ฆ)) |
114 | | vex 3448 |
. . . . . . . . . . . . . . 15
โข ๐ฆ โ V |
115 | 114 | sucid 6400 |
. . . . . . . . . . . . . 14
โข ๐ฆ โ suc ๐ฆ |
116 | | ovexd 7393 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ (๐น supp โ
) โ V) |
117 | 15 | simpld 496 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ E We (๐น supp โ
)) |
118 | 6 | oiiso 9478 |
. . . . . . . . . . . . . . . . . 18
โข (((๐น supp โ
) โ V โง E
We (๐น supp โ
)) โ
๐บ Isom E , E (dom ๐บ, (๐น supp โ
))) |
119 | 116, 117,
118 | syl2anc 585 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ ๐บ Isom E , E (dom ๐บ, (๐น supp โ
))) |
120 | 119 | ad2antrr 725 |
. . . . . . . . . . . . . . . 16
โข (((๐ โง ๐ฆ โ ฯ) โง (suc ๐ฆ โ dom ๐บ โง (๐โsuc ๐ฆ):(๐ปโsuc ๐ฆ)โ1-1-ontoโ((ฯ โo (๐บโ๐ฆ)) ยทo (๐นโ(๐บโ๐ฆ))))) โ ๐บ Isom E , E (dom ๐บ, (๐น supp โ
))) |
121 | 101 | ad2antrl 727 |
. . . . . . . . . . . . . . . 16
โข (((๐ โง ๐ฆ โ ฯ) โง (suc ๐ฆ โ dom ๐บ โง (๐โsuc ๐ฆ):(๐ปโsuc ๐ฆ)โ1-1-ontoโ((ฯ โo (๐บโ๐ฆ)) ยทo (๐นโ(๐บโ๐ฆ))))) โ ๐ฆ โ dom ๐บ) |
122 | | isorel 7272 |
. . . . . . . . . . . . . . . 16
โข ((๐บ Isom E , E (dom ๐บ, (๐น supp โ
)) โง (๐ฆ โ dom ๐บ โง suc ๐ฆ โ dom ๐บ)) โ (๐ฆ E suc ๐ฆ โ (๐บโ๐ฆ) E (๐บโsuc ๐ฆ))) |
123 | 120, 121,
105, 122 | syl12anc 836 |
. . . . . . . . . . . . . . 15
โข (((๐ โง ๐ฆ โ ฯ) โง (suc ๐ฆ โ dom ๐บ โง (๐โsuc ๐ฆ):(๐ปโsuc ๐ฆ)โ1-1-ontoโ((ฯ โo (๐บโ๐ฆ)) ยทo (๐นโ(๐บโ๐ฆ))))) โ (๐ฆ E suc ๐ฆ โ (๐บโ๐ฆ) E (๐บโsuc ๐ฆ))) |
124 | 114 | sucex 7742 |
. . . . . . . . . . . . . . . 16
โข suc ๐ฆ โ V |
125 | 124 | epeli 5540 |
. . . . . . . . . . . . . . 15
โข (๐ฆ E suc ๐ฆ โ ๐ฆ โ suc ๐ฆ) |
126 | | fvex 6856 |
. . . . . . . . . . . . . . . 16
โข (๐บโsuc ๐ฆ) โ V |
127 | 126 | epeli 5540 |
. . . . . . . . . . . . . . 15
โข ((๐บโ๐ฆ) E (๐บโsuc ๐ฆ) โ (๐บโ๐ฆ) โ (๐บโsuc ๐ฆ)) |
128 | 123, 125,
127 | 3bitr3g 313 |
. . . . . . . . . . . . . 14
โข (((๐ โง ๐ฆ โ ฯ) โง (suc ๐ฆ โ dom ๐บ โง (๐โsuc ๐ฆ):(๐ปโsuc ๐ฆ)โ1-1-ontoโ((ฯ โo (๐บโ๐ฆ)) ยทo (๐นโ(๐บโ๐ฆ))))) โ (๐ฆ โ suc ๐ฆ โ (๐บโ๐ฆ) โ (๐บโsuc ๐ฆ))) |
129 | 115, 128 | mpbii 232 |
. . . . . . . . . . . . 13
โข (((๐ โง ๐ฆ โ ฯ) โง (suc ๐ฆ โ dom ๐บ โง (๐โsuc ๐ฆ):(๐ปโsuc ๐ฆ)โ1-1-ontoโ((ฯ โo (๐บโ๐ฆ)) ยทo (๐นโ(๐บโ๐ฆ))))) โ (๐บโ๐ฆ) โ (๐บโsuc ๐ฆ)) |
130 | | ordsucss 7754 |
. . . . . . . . . . . . 13
โข (Ord
(๐บโsuc ๐ฆ) โ ((๐บโ๐ฆ) โ (๐บโsuc ๐ฆ) โ suc (๐บโ๐ฆ) โ (๐บโsuc ๐ฆ))) |
131 | 113, 129,
130 | sylc 65 |
. . . . . . . . . . . 12
โข (((๐ โง ๐ฆ โ ฯ) โง (suc ๐ฆ โ dom ๐บ โง (๐โsuc ๐ฆ):(๐ปโsuc ๐ฆ)โ1-1-ontoโ((ฯ โo (๐บโ๐ฆ)) ยทo (๐นโ(๐บโ๐ฆ))))) โ suc (๐บโ๐ฆ) โ (๐บโsuc ๐ฆ)) |
132 | 76 | ffvelcdmi 7035 |
. . . . . . . . . . . . . . . . 17
โข (๐ฆ โ dom ๐บ โ (๐บโ๐ฆ) โ (๐น supp โ
)) |
133 | 121, 132 | syl 17 |
. . . . . . . . . . . . . . . 16
โข (((๐ โง ๐ฆ โ ฯ) โง (suc ๐ฆ โ dom ๐บ โง (๐โsuc ๐ฆ):(๐ปโsuc ๐ฆ)โ1-1-ontoโ((ฯ โo (๐บโ๐ฆ)) ยทo (๐นโ(๐บโ๐ฆ))))) โ (๐บโ๐ฆ) โ (๐น supp โ
)) |
134 | 107, 133 | sseldd 3946 |
. . . . . . . . . . . . . . 15
โข (((๐ โง ๐ฆ โ ฯ) โง (suc ๐ฆ โ dom ๐บ โง (๐โsuc ๐ฆ):(๐ปโsuc ๐ฆ)โ1-1-ontoโ((ฯ โo (๐บโ๐ฆ)) ยทo (๐นโ(๐บโ๐ฆ))))) โ (๐บโ๐ฆ) โ ๐ด) |
135 | 106, 134 | sseldd 3946 |
. . . . . . . . . . . . . 14
โข (((๐ โง ๐ฆ โ ฯ) โง (suc ๐ฆ โ dom ๐บ โง (๐โsuc ๐ฆ):(๐ปโsuc ๐ฆ)โ1-1-ontoโ((ฯ โo (๐บโ๐ฆ)) ยทo (๐นโ(๐บโ๐ฆ))))) โ (๐บโ๐ฆ) โ On) |
136 | | onsuc 7747 |
. . . . . . . . . . . . . 14
โข ((๐บโ๐ฆ) โ On โ suc (๐บโ๐ฆ) โ On) |
137 | 135, 136 | syl 17 |
. . . . . . . . . . . . 13
โข (((๐ โง ๐ฆ โ ฯ) โง (suc ๐ฆ โ dom ๐บ โง (๐โsuc ๐ฆ):(๐ปโsuc ๐ฆ)โ1-1-ontoโ((ฯ โo (๐บโ๐ฆ)) ยทo (๐นโ(๐บโ๐ฆ))))) โ suc (๐บโ๐ฆ) โ On) |
138 | 3 | a1i 11 |
. . . . . . . . . . . . 13
โข (((๐ โง ๐ฆ โ ฯ) โง (suc ๐ฆ โ dom ๐บ โง (๐โsuc ๐ฆ):(๐ปโsuc ๐ฆ)โ1-1-ontoโ((ฯ โo (๐บโ๐ฆ)) ยทo (๐นโ(๐บโ๐ฆ))))) โ ฯ โ
On) |
139 | 80 | a1i 11 |
. . . . . . . . . . . . 13
โข (((๐ โง ๐ฆ โ ฯ) โง (suc ๐ฆ โ dom ๐บ โง (๐โsuc ๐ฆ):(๐ปโsuc ๐ฆ)โ1-1-ontoโ((ฯ โo (๐บโ๐ฆ)) ยทo (๐นโ(๐บโ๐ฆ))))) โ โ
โ
ฯ) |
140 | | oewordi 8539 |
. . . . . . . . . . . . 13
โข (((suc
(๐บโ๐ฆ) โ On โง (๐บโsuc ๐ฆ) โ On โง ฯ โ On) โง
โ
โ ฯ) โ (suc (๐บโ๐ฆ) โ (๐บโsuc ๐ฆ) โ (ฯ โo suc
(๐บโ๐ฆ)) โ (ฯ โo (๐บโsuc ๐ฆ)))) |
141 | 137, 111,
138, 139, 140 | syl31anc 1374 |
. . . . . . . . . . . 12
โข (((๐ โง ๐ฆ โ ฯ) โง (suc ๐ฆ โ dom ๐บ โง (๐โsuc ๐ฆ):(๐ปโsuc ๐ฆ)โ1-1-ontoโ((ฯ โo (๐บโ๐ฆ)) ยทo (๐นโ(๐บโ๐ฆ))))) โ (suc (๐บโ๐ฆ) โ (๐บโsuc ๐ฆ) โ (ฯ โo suc
(๐บโ๐ฆ)) โ (ฯ โo (๐บโsuc ๐ฆ)))) |
142 | 131, 141 | mpd 15 |
. . . . . . . . . . 11
โข (((๐ โง ๐ฆ โ ฯ) โง (suc ๐ฆ โ dom ๐บ โง (๐โsuc ๐ฆ):(๐ปโsuc ๐ฆ)โ1-1-ontoโ((ฯ โo (๐บโ๐ฆ)) ยทo (๐นโ(๐บโ๐ฆ))))) โ (ฯ โo suc
(๐บโ๐ฆ)) โ (ฯ โo (๐บโsuc ๐ฆ))) |
143 | 71 | ad2antrr 725 |
. . . . . . . . . . . . . 14
โข (((๐ โง ๐ฆ โ ฯ) โง (suc ๐ฆ โ dom ๐บ โง (๐โsuc ๐ฆ):(๐ปโsuc ๐ฆ)โ1-1-ontoโ((ฯ โo (๐บโ๐ฆ)) ยทo (๐นโ(๐บโ๐ฆ))))) โ ๐น:๐ดโถฯ) |
144 | 143, 134 | ffvelcdmd 7037 |
. . . . . . . . . . . . 13
โข (((๐ โง ๐ฆ โ ฯ) โง (suc ๐ฆ โ dom ๐บ โง (๐โsuc ๐ฆ):(๐ปโsuc ๐ฆ)โ1-1-ontoโ((ฯ โo (๐บโ๐ฆ)) ยทo (๐นโ(๐บโ๐ฆ))))) โ (๐นโ(๐บโ๐ฆ)) โ ฯ) |
145 | | nnon 7809 |
. . . . . . . . . . . . . . 15
โข ((๐นโ(๐บโ๐ฆ)) โ ฯ โ (๐นโ(๐บโ๐ฆ)) โ On) |
146 | 144, 145 | syl 17 |
. . . . . . . . . . . . . 14
โข (((๐ โง ๐ฆ โ ฯ) โง (suc ๐ฆ โ dom ๐บ โง (๐โsuc ๐ฆ):(๐ปโsuc ๐ฆ)โ1-1-ontoโ((ฯ โo (๐บโ๐ฆ)) ยทo (๐นโ(๐บโ๐ฆ))))) โ (๐นโ(๐บโ๐ฆ)) โ On) |
147 | | oecl 8484 |
. . . . . . . . . . . . . . 15
โข ((ฯ
โ On โง (๐บโ๐ฆ) โ On) โ (ฯ
โo (๐บโ๐ฆ)) โ On) |
148 | 138, 135,
147 | syl2anc 585 |
. . . . . . . . . . . . . 14
โข (((๐ โง ๐ฆ โ ฯ) โง (suc ๐ฆ โ dom ๐บ โง (๐โsuc ๐ฆ):(๐ปโsuc ๐ฆ)โ1-1-ontoโ((ฯ โo (๐บโ๐ฆ)) ยทo (๐นโ(๐บโ๐ฆ))))) โ (ฯ โo
(๐บโ๐ฆ)) โ On) |
149 | | oen0 8534 |
. . . . . . . . . . . . . . 15
โข
(((ฯ โ On โง (๐บโ๐ฆ) โ On) โง โ
โ ฯ)
โ โ
โ (ฯ โo (๐บโ๐ฆ))) |
150 | 138, 135,
139, 149 | syl21anc 837 |
. . . . . . . . . . . . . 14
โข (((๐ โง ๐ฆ โ ฯ) โง (suc ๐ฆ โ dom ๐บ โง (๐โsuc ๐ฆ):(๐ปโsuc ๐ฆ)โ1-1-ontoโ((ฯ โo (๐บโ๐ฆ)) ยทo (๐นโ(๐บโ๐ฆ))))) โ โ
โ (ฯ
โo (๐บโ๐ฆ))) |
151 | | omord2 8515 |
. . . . . . . . . . . . . 14
โข ((((๐นโ(๐บโ๐ฆ)) โ On โง ฯ โ On โง
(ฯ โo (๐บโ๐ฆ)) โ On) โง โ
โ (ฯ
โo (๐บโ๐ฆ))) โ ((๐นโ(๐บโ๐ฆ)) โ ฯ โ ((ฯ
โo (๐บโ๐ฆ)) ยทo (๐นโ(๐บโ๐ฆ))) โ ((ฯ โo
(๐บโ๐ฆ)) ยทo
ฯ))) |
152 | 146, 138,
148, 150, 151 | syl31anc 1374 |
. . . . . . . . . . . . 13
โข (((๐ โง ๐ฆ โ ฯ) โง (suc ๐ฆ โ dom ๐บ โง (๐โsuc ๐ฆ):(๐ปโsuc ๐ฆ)โ1-1-ontoโ((ฯ โo (๐บโ๐ฆ)) ยทo (๐นโ(๐บโ๐ฆ))))) โ ((๐นโ(๐บโ๐ฆ)) โ ฯ โ ((ฯ
โo (๐บโ๐ฆ)) ยทo (๐นโ(๐บโ๐ฆ))) โ ((ฯ โo
(๐บโ๐ฆ)) ยทo
ฯ))) |
153 | 144, 152 | mpbid 231 |
. . . . . . . . . . . 12
โข (((๐ โง ๐ฆ โ ฯ) โง (suc ๐ฆ โ dom ๐บ โง (๐โsuc ๐ฆ):(๐ปโsuc ๐ฆ)โ1-1-ontoโ((ฯ โo (๐บโ๐ฆ)) ยทo (๐นโ(๐บโ๐ฆ))))) โ ((ฯ โo
(๐บโ๐ฆ)) ยทo (๐นโ(๐บโ๐ฆ))) โ ((ฯ โo
(๐บโ๐ฆ)) ยทo
ฯ)) |
154 | | oesuc 8474 |
. . . . . . . . . . . . 13
โข ((ฯ
โ On โง (๐บโ๐ฆ) โ On) โ (ฯ
โo suc (๐บโ๐ฆ)) = ((ฯ โo (๐บโ๐ฆ)) ยทo
ฯ)) |
155 | 138, 135,
154 | syl2anc 585 |
. . . . . . . . . . . 12
โข (((๐ โง ๐ฆ โ ฯ) โง (suc ๐ฆ โ dom ๐บ โง (๐โsuc ๐ฆ):(๐ปโsuc ๐ฆ)โ1-1-ontoโ((ฯ โo (๐บโ๐ฆ)) ยทo (๐นโ(๐บโ๐ฆ))))) โ (ฯ โo suc
(๐บโ๐ฆ)) = ((ฯ โo (๐บโ๐ฆ)) ยทo
ฯ)) |
156 | 153, 155 | eleqtrrd 2837 |
. . . . . . . . . . 11
โข (((๐ โง ๐ฆ โ ฯ) โง (suc ๐ฆ โ dom ๐บ โง (๐โsuc ๐ฆ):(๐ปโsuc ๐ฆ)โ1-1-ontoโ((ฯ โo (๐บโ๐ฆ)) ยทo (๐นโ(๐บโ๐ฆ))))) โ ((ฯ โo
(๐บโ๐ฆ)) ยทo (๐นโ(๐บโ๐ฆ))) โ (ฯ โo suc
(๐บโ๐ฆ))) |
157 | 142, 156 | sseldd 3946 |
. . . . . . . . . 10
โข (((๐ โง ๐ฆ โ ฯ) โง (suc ๐ฆ โ dom ๐บ โง (๐โsuc ๐ฆ):(๐ปโsuc ๐ฆ)โ1-1-ontoโ((ฯ โo (๐บโ๐ฆ)) ยทo (๐นโ(๐บโ๐ฆ))))) โ ((ฯ โo
(๐บโ๐ฆ)) ยทo (๐นโ(๐บโ๐ฆ))) โ (ฯ โo (๐บโsuc ๐ฆ))) |
158 | | simprr 772 |
. . . . . . . . . 10
โข (((๐ โง ๐ฆ โ ฯ) โง (suc ๐ฆ โ dom ๐บ โง (๐โsuc ๐ฆ):(๐ปโsuc ๐ฆ)โ1-1-ontoโ((ฯ โo (๐บโ๐ฆ)) ยทo (๐นโ(๐บโ๐ฆ))))) โ (๐โsuc ๐ฆ):(๐ปโsuc ๐ฆ)โ1-1-ontoโ((ฯ โo (๐บโ๐ฆ)) ยทo (๐นโ(๐บโ๐ฆ)))) |
159 | 2, 103, 104, 7, 6, 62, 63, 64, 65, 105, 157, 158 | cnfcomlem 9640 |
. . . . . . . . 9
โข (((๐ โง ๐ฆ โ ฯ) โง (suc ๐ฆ โ dom ๐บ โง (๐โsuc ๐ฆ):(๐ปโsuc ๐ฆ)โ1-1-ontoโ((ฯ โo (๐บโ๐ฆ)) ยทo (๐นโ(๐บโ๐ฆ))))) โ (๐โsuc suc ๐ฆ):(๐ปโsuc suc ๐ฆ)โ1-1-ontoโ((ฯ โo (๐บโsuc ๐ฆ)) ยทo (๐นโ(๐บโsuc ๐ฆ)))) |
160 | 159 | exp32 422 |
. . . . . . . 8
โข ((๐ โง ๐ฆ โ ฯ) โ (suc ๐ฆ โ dom ๐บ โ ((๐โsuc ๐ฆ):(๐ปโsuc ๐ฆ)โ1-1-ontoโ((ฯ โo (๐บโ๐ฆ)) ยทo (๐นโ(๐บโ๐ฆ))) โ (๐โsuc suc ๐ฆ):(๐ปโsuc suc ๐ฆ)โ1-1-ontoโ((ฯ โo (๐บโsuc ๐ฆ)) ยทo (๐นโ(๐บโsuc ๐ฆ)))))) |
161 | 160 | a2d 29 |
. . . . . . 7
โข ((๐ โง ๐ฆ โ ฯ) โ ((suc ๐ฆ โ dom ๐บ โ (๐โsuc ๐ฆ):(๐ปโsuc ๐ฆ)โ1-1-ontoโ((ฯ โo (๐บโ๐ฆ)) ยทo (๐นโ(๐บโ๐ฆ)))) โ (suc ๐ฆ โ dom ๐บ โ (๐โsuc suc ๐ฆ):(๐ปโsuc suc ๐ฆ)โ1-1-ontoโ((ฯ โo (๐บโsuc ๐ฆ)) ยทo (๐นโ(๐บโsuc ๐ฆ)))))) |
162 | 102, 161 | syl5 34 |
. . . . . 6
โข ((๐ โง ๐ฆ โ ฯ) โ ((๐ฆ โ dom ๐บ โ (๐โsuc ๐ฆ):(๐ปโsuc ๐ฆ)โ1-1-ontoโ((ฯ โo (๐บโ๐ฆ)) ยทo (๐นโ(๐บโ๐ฆ)))) โ (suc ๐ฆ โ dom ๐บ โ (๐โsuc suc ๐ฆ):(๐ปโsuc suc ๐ฆ)โ1-1-ontoโ((ฯ โo (๐บโsuc ๐ฆ)) ยทo (๐นโ(๐บโsuc ๐ฆ)))))) |
163 | 162 | expcom 415 |
. . . . 5
โข (๐ฆ โ ฯ โ (๐ โ ((๐ฆ โ dom ๐บ โ (๐โsuc ๐ฆ):(๐ปโsuc ๐ฆ)โ1-1-ontoโ((ฯ โo (๐บโ๐ฆ)) ยทo (๐นโ(๐บโ๐ฆ)))) โ (suc ๐ฆ โ dom ๐บ โ (๐โsuc suc ๐ฆ):(๐ปโsuc suc ๐ฆ)โ1-1-ontoโ((ฯ โo (๐บโsuc ๐ฆ)) ยทo (๐นโ(๐บโsuc ๐ฆ))))))) |
164 | 39, 49, 59, 96, 163 | finds2 7838 |
. . . 4
โข (๐ค โ ฯ โ (๐ โ (๐ค โ dom ๐บ โ (๐โsuc ๐ค):(๐ปโsuc ๐ค)โ1-1-ontoโ((ฯ โo (๐บโ๐ค)) ยทo (๐นโ(๐บโ๐ค)))))) |
165 | 29, 164 | vtoclga 3533 |
. . 3
โข (๐ผ โ ฯ โ (๐ โ (๐ผ โ dom ๐บ โ (๐โsuc ๐ผ):(๐ปโsuc ๐ผ)โ1-1-ontoโ((ฯ โo (๐บโ๐ผ)) ยทo (๐นโ(๐บโ๐ผ)))))) |
166 | 18, 165 | mpcom 38 |
. 2
โข (๐ โ (๐ผ โ dom ๐บ โ (๐โsuc ๐ผ):(๐ปโsuc ๐ผ)โ1-1-ontoโ((ฯ โo (๐บโ๐ผ)) ยทo (๐นโ(๐บโ๐ผ))))) |
167 | 1, 166 | mpd 15 |
1
โข (๐ โ (๐โsuc ๐ผ):(๐ปโsuc ๐ผ)โ1-1-ontoโ((ฯ โo (๐บโ๐ผ)) ยทo (๐นโ(๐บโ๐ผ)))) |