Step | Hyp | Ref
| Expression |
1 | | omelon 9590 |
. . . . . . 7
β’ Ο
β On |
2 | | cnfcom.a |
. . . . . . . 8
β’ (π β π΄ β On) |
3 | | suppssdm 8112 |
. . . . . . . . . 10
β’ (πΉ supp β
) β dom πΉ |
4 | | cnfcom.f |
. . . . . . . . . . . . 13
β’ πΉ = (β‘(Ο CNF π΄)βπ΅) |
5 | | cnfcom.s |
. . . . . . . . . . . . . . . 16
β’ π = dom (Ο CNF π΄) |
6 | 1 | a1i 11 |
. . . . . . . . . . . . . . . 16
β’ (π β Ο β
On) |
7 | 5, 6, 2 | cantnff1o 9640 |
. . . . . . . . . . . . . . 15
β’ (π β (Ο CNF π΄):πβ1-1-ontoβ(Ο βo π΄)) |
8 | | f1ocnv 6800 |
. . . . . . . . . . . . . . 15
β’ ((Ο
CNF π΄):πβ1-1-ontoβ(Ο βo π΄) β β‘(Ο CNF π΄):(Ο βo π΄)β1-1-ontoβπ) |
9 | | f1of 6788 |
. . . . . . . . . . . . . . 15
β’ (β‘(Ο CNF π΄):(Ο βo π΄)β1-1-ontoβπ β β‘(Ο CNF π΄):(Ο βo π΄)βΆπ) |
10 | 7, 8, 9 | 3syl 18 |
. . . . . . . . . . . . . 14
β’ (π β β‘(Ο CNF π΄):(Ο βo π΄)βΆπ) |
11 | | cnfcom.b |
. . . . . . . . . . . . . 14
β’ (π β π΅ β (Ο βo π΄)) |
12 | 10, 11 | ffvelcdmd 7040 |
. . . . . . . . . . . . 13
β’ (π β (β‘(Ο CNF π΄)βπ΅) β π) |
13 | 4, 12 | eqeltrid 2838 |
. . . . . . . . . . . 12
β’ (π β πΉ β π) |
14 | 5, 6, 2 | cantnfs 9610 |
. . . . . . . . . . . 12
β’ (π β (πΉ β π β (πΉ:π΄βΆΟ β§ πΉ finSupp β
))) |
15 | 13, 14 | mpbid 231 |
. . . . . . . . . . 11
β’ (π β (πΉ:π΄βΆΟ β§ πΉ finSupp β
)) |
16 | 15 | simpld 496 |
. . . . . . . . . 10
β’ (π β πΉ:π΄βΆΟ) |
17 | 3, 16 | fssdm 6692 |
. . . . . . . . 9
β’ (π β (πΉ supp β
) β π΄) |
18 | | cnfcom.1 |
. . . . . . . . . 10
β’ (π β πΌ β dom πΊ) |
19 | | cnfcom.g |
. . . . . . . . . . . 12
β’ πΊ = OrdIso( E , (πΉ supp β
)) |
20 | 19 | oif 9474 |
. . . . . . . . . . 11
β’ πΊ:dom πΊβΆ(πΉ supp β
) |
21 | 20 | ffvelcdmi 7038 |
. . . . . . . . . 10
β’ (πΌ β dom πΊ β (πΊβπΌ) β (πΉ supp β
)) |
22 | 18, 21 | syl 17 |
. . . . . . . . 9
β’ (π β (πΊβπΌ) β (πΉ supp β
)) |
23 | 17, 22 | sseldd 3949 |
. . . . . . . 8
β’ (π β (πΊβπΌ) β π΄) |
24 | | onelon 6346 |
. . . . . . . 8
β’ ((π΄ β On β§ (πΊβπΌ) β π΄) β (πΊβπΌ) β On) |
25 | 2, 23, 24 | syl2anc 585 |
. . . . . . 7
β’ (π β (πΊβπΌ) β On) |
26 | | oecl 8487 |
. . . . . . 7
β’ ((Ο
β On β§ (πΊβπΌ) β On) β (Ο
βo (πΊβπΌ)) β On) |
27 | 1, 25, 26 | sylancr 588 |
. . . . . 6
β’ (π β (Ο
βo (πΊβπΌ)) β On) |
28 | 16, 23 | ffvelcdmd 7040 |
. . . . . . 7
β’ (π β (πΉβ(πΊβπΌ)) β Ο) |
29 | | nnon 7812 |
. . . . . . 7
β’ ((πΉβ(πΊβπΌ)) β Ο β (πΉβ(πΊβπΌ)) β On) |
30 | 28, 29 | syl 17 |
. . . . . 6
β’ (π β (πΉβ(πΊβπΌ)) β On) |
31 | | omcl 8486 |
. . . . . 6
β’
(((Ο βo (πΊβπΌ)) β On β§ (πΉβ(πΊβπΌ)) β On) β ((Ο
βo (πΊβπΌ)) Β·o (πΉβ(πΊβπΌ))) β On) |
32 | 27, 30, 31 | syl2anc 585 |
. . . . 5
β’ (π β ((Ο
βo (πΊβπΌ)) Β·o (πΉβ(πΊβπΌ))) β On) |
33 | 5, 6, 2, 19, 13 | cantnfcl 9611 |
. . . . . . . 8
β’ (π β ( E We (πΉ supp β
) β§ dom πΊ β Ο)) |
34 | 33 | simprd 497 |
. . . . . . 7
β’ (π β dom πΊ β Ο) |
35 | | elnn 7817 |
. . . . . . 7
β’ ((πΌ β dom πΊ β§ dom πΊ β Ο) β πΌ β Ο) |
36 | 18, 34, 35 | syl2anc 585 |
. . . . . 6
β’ (π β πΌ β Ο) |
37 | | cnfcom.h |
. . . . . . . 8
β’ π» = seqΟ((π β V, π§ β V β¦ (π +o π§)), β
) |
38 | 37 | cantnfvalf 9609 |
. . . . . . 7
β’ π»:ΟβΆOn |
39 | 38 | ffvelcdmi 7038 |
. . . . . 6
β’ (πΌ β Ο β (π»βπΌ) β On) |
40 | 36, 39 | syl 17 |
. . . . 5
β’ (π β (π»βπΌ) β On) |
41 | | eqid 2733 |
. . . . . 6
β’ ((π¦ β ((Ο
βo (πΊβπΌ)) Β·o (πΉβ(πΊβπΌ))) β¦ ((π»βπΌ) +o π¦)) βͺ β‘(π¦ β (π»βπΌ) β¦ (((Ο βo
(πΊβπΌ)) Β·o (πΉβ(πΊβπΌ))) +o π¦))) = ((π¦ β ((Ο βo (πΊβπΌ)) Β·o (πΉβ(πΊβπΌ))) β¦ ((π»βπΌ) +o π¦)) βͺ β‘(π¦ β (π»βπΌ) β¦ (((Ο βo
(πΊβπΌ)) Β·o (πΉβ(πΊβπΌ))) +o π¦))) |
42 | 41 | oacomf1o 8516 |
. . . . 5
β’
((((Ο βo (πΊβπΌ)) Β·o (πΉβ(πΊβπΌ))) β On β§ (π»βπΌ) β On) β ((π¦ β ((Ο βo (πΊβπΌ)) Β·o (πΉβ(πΊβπΌ))) β¦ ((π»βπΌ) +o π¦)) βͺ β‘(π¦ β (π»βπΌ) β¦ (((Ο βo
(πΊβπΌ)) Β·o (πΉβ(πΊβπΌ))) +o π¦))):(((Ο βo (πΊβπΌ)) Β·o (πΉβ(πΊβπΌ))) +o (π»βπΌ))β1-1-ontoβ((π»βπΌ) +o ((Ο βo
(πΊβπΌ)) Β·o (πΉβ(πΊβπΌ))))) |
43 | 32, 40, 42 | syl2anc 585 |
. . . 4
β’ (π β ((π¦ β ((Ο βo (πΊβπΌ)) Β·o (πΉβ(πΊβπΌ))) β¦ ((π»βπΌ) +o π¦)) βͺ β‘(π¦ β (π»βπΌ) β¦ (((Ο βo
(πΊβπΌ)) Β·o (πΉβ(πΊβπΌ))) +o π¦))):(((Ο βo (πΊβπΌ)) Β·o (πΉβ(πΊβπΌ))) +o (π»βπΌ))β1-1-ontoβ((π»βπΌ) +o ((Ο βo
(πΊβπΌ)) Β·o (πΉβ(πΊβπΌ))))) |
44 | | cnfcom.t |
. . . . . . . 8
β’ π = seqΟ((π β V, π β V β¦ πΎ), β
) |
45 | 44 | seqomsuc 8407 |
. . . . . . 7
β’ (πΌ β Ο β (πβsuc πΌ) = (πΌ(π β V, π β V β¦ πΎ)(πβπΌ))) |
46 | 36, 45 | syl 17 |
. . . . . 6
β’ (π β (πβsuc πΌ) = (πΌ(π β V, π β V β¦ πΎ)(πβπΌ))) |
47 | | nfcv 2904 |
. . . . . . . . 9
β’
β²π’πΎ |
48 | | nfcv 2904 |
. . . . . . . . 9
β’
β²π£πΎ |
49 | | nfcv 2904 |
. . . . . . . . 9
β’
β²π((π¦ β ((Ο βo (πΊβπ’)) Β·o (πΉβ(πΊβπ’))) β¦ (dom π£ +o π¦)) βͺ β‘(π¦ β dom π£ β¦ (((Ο βo (πΊβπ’)) Β·o (πΉβ(πΊβπ’))) +o π¦))) |
50 | | nfcv 2904 |
. . . . . . . . 9
β’
β²π((π¦ β ((Ο βo (πΊβπ’)) Β·o (πΉβ(πΊβπ’))) β¦ (dom π£ +o π¦)) βͺ β‘(π¦ β dom π£ β¦ (((Ο βo (πΊβπ’)) Β·o (πΉβ(πΊβπ’))) +o π¦))) |
51 | | cnfcom.k |
. . . . . . . . . 10
β’ πΎ = ((π₯ β π β¦ (dom π +o π₯)) βͺ β‘(π₯ β dom π β¦ (π +o π₯))) |
52 | | oveq2 7369 |
. . . . . . . . . . . . 13
β’ (π₯ = π¦ β (dom π +o π₯) = (dom π +o π¦)) |
53 | 52 | cbvmptv 5222 |
. . . . . . . . . . . 12
β’ (π₯ β π β¦ (dom π +o π₯)) = (π¦ β π β¦ (dom π +o π¦)) |
54 | | cnfcom.m |
. . . . . . . . . . . . . 14
β’ π = ((Ο βo
(πΊβπ)) Β·o (πΉβ(πΊβπ))) |
55 | | simpl 484 |
. . . . . . . . . . . . . . . . 17
β’ ((π = π’ β§ π = π£) β π = π’) |
56 | 55 | fveq2d 6850 |
. . . . . . . . . . . . . . . 16
β’ ((π = π’ β§ π = π£) β (πΊβπ) = (πΊβπ’)) |
57 | 56 | oveq2d 7377 |
. . . . . . . . . . . . . . 15
β’ ((π = π’ β§ π = π£) β (Ο βo (πΊβπ)) = (Ο βo (πΊβπ’))) |
58 | 56 | fveq2d 6850 |
. . . . . . . . . . . . . . 15
β’ ((π = π’ β§ π = π£) β (πΉβ(πΊβπ)) = (πΉβ(πΊβπ’))) |
59 | 57, 58 | oveq12d 7379 |
. . . . . . . . . . . . . 14
β’ ((π = π’ β§ π = π£) β ((Ο βo (πΊβπ)) Β·o (πΉβ(πΊβπ))) = ((Ο βo (πΊβπ’)) Β·o (πΉβ(πΊβπ’)))) |
60 | 54, 59 | eqtrid 2785 |
. . . . . . . . . . . . 13
β’ ((π = π’ β§ π = π£) β π = ((Ο βo (πΊβπ’)) Β·o (πΉβ(πΊβπ’)))) |
61 | | simpr 486 |
. . . . . . . . . . . . . . 15
β’ ((π = π’ β§ π = π£) β π = π£) |
62 | 61 | dmeqd 5865 |
. . . . . . . . . . . . . 14
β’ ((π = π’ β§ π = π£) β dom π = dom π£) |
63 | 62 | oveq1d 7376 |
. . . . . . . . . . . . 13
β’ ((π = π’ β§ π = π£) β (dom π +o π¦) = (dom π£ +o π¦)) |
64 | 60, 63 | mpteq12dv 5200 |
. . . . . . . . . . . 12
β’ ((π = π’ β§ π = π£) β (π¦ β π β¦ (dom π +o π¦)) = (π¦ β ((Ο βo (πΊβπ’)) Β·o (πΉβ(πΊβπ’))) β¦ (dom π£ +o π¦))) |
65 | 53, 64 | eqtrid 2785 |
. . . . . . . . . . 11
β’ ((π = π’ β§ π = π£) β (π₯ β π β¦ (dom π +o π₯)) = (π¦ β ((Ο βo (πΊβπ’)) Β·o (πΉβ(πΊβπ’))) β¦ (dom π£ +o π¦))) |
66 | | oveq2 7369 |
. . . . . . . . . . . . . 14
β’ (π₯ = π¦ β (π +o π₯) = (π +o π¦)) |
67 | 66 | cbvmptv 5222 |
. . . . . . . . . . . . 13
β’ (π₯ β dom π β¦ (π +o π₯)) = (π¦ β dom π β¦ (π +o π¦)) |
68 | 60 | oveq1d 7376 |
. . . . . . . . . . . . . 14
β’ ((π = π’ β§ π = π£) β (π +o π¦) = (((Ο βo (πΊβπ’)) Β·o (πΉβ(πΊβπ’))) +o π¦)) |
69 | 62, 68 | mpteq12dv 5200 |
. . . . . . . . . . . . 13
β’ ((π = π’ β§ π = π£) β (π¦ β dom π β¦ (π +o π¦)) = (π¦ β dom π£ β¦ (((Ο βo (πΊβπ’)) Β·o (πΉβ(πΊβπ’))) +o π¦))) |
70 | 67, 69 | eqtrid 2785 |
. . . . . . . . . . . 12
β’ ((π = π’ β§ π = π£) β (π₯ β dom π β¦ (π +o π₯)) = (π¦ β dom π£ β¦ (((Ο βo (πΊβπ’)) Β·o (πΉβ(πΊβπ’))) +o π¦))) |
71 | 70 | cnveqd 5835 |
. . . . . . . . . . 11
β’ ((π = π’ β§ π = π£) β β‘(π₯ β dom π β¦ (π +o π₯)) = β‘(π¦ β dom π£ β¦ (((Ο βo (πΊβπ’)) Β·o (πΉβ(πΊβπ’))) +o π¦))) |
72 | 65, 71 | uneq12d 4128 |
. . . . . . . . . 10
β’ ((π = π’ β§ π = π£) β ((π₯ β π β¦ (dom π +o π₯)) βͺ β‘(π₯ β dom π β¦ (π +o π₯))) = ((π¦ β ((Ο βo (πΊβπ’)) Β·o (πΉβ(πΊβπ’))) β¦ (dom π£ +o π¦)) βͺ β‘(π¦ β dom π£ β¦ (((Ο βo (πΊβπ’)) Β·o (πΉβ(πΊβπ’))) +o π¦)))) |
73 | 51, 72 | eqtrid 2785 |
. . . . . . . . 9
β’ ((π = π’ β§ π = π£) β πΎ = ((π¦ β ((Ο βo (πΊβπ’)) Β·o (πΉβ(πΊβπ’))) β¦ (dom π£ +o π¦)) βͺ β‘(π¦ β dom π£ β¦ (((Ο βo (πΊβπ’)) Β·o (πΉβ(πΊβπ’))) +o π¦)))) |
74 | 47, 48, 49, 50, 73 | cbvmpo 7455 |
. . . . . . . 8
β’ (π β V, π β V β¦ πΎ) = (π’ β V, π£ β V β¦ ((π¦ β ((Ο βo (πΊβπ’)) Β·o (πΉβ(πΊβπ’))) β¦ (dom π£ +o π¦)) βͺ β‘(π¦ β dom π£ β¦ (((Ο βo (πΊβπ’)) Β·o (πΉβ(πΊβπ’))) +o π¦)))) |
75 | 74 | a1i 11 |
. . . . . . 7
β’ (π β (π β V, π β V β¦ πΎ) = (π’ β V, π£ β V β¦ ((π¦ β ((Ο βo (πΊβπ’)) Β·o (πΉβ(πΊβπ’))) β¦ (dom π£ +o π¦)) βͺ β‘(π¦ β dom π£ β¦ (((Ο βo (πΊβπ’)) Β·o (πΉβ(πΊβπ’))) +o π¦))))) |
76 | | simprl 770 |
. . . . . . . . . . . 12
β’ ((π β§ (π’ = πΌ β§ π£ = (πβπΌ))) β π’ = πΌ) |
77 | 76 | fveq2d 6850 |
. . . . . . . . . . 11
β’ ((π β§ (π’ = πΌ β§ π£ = (πβπΌ))) β (πΊβπ’) = (πΊβπΌ)) |
78 | 77 | oveq2d 7377 |
. . . . . . . . . 10
β’ ((π β§ (π’ = πΌ β§ π£ = (πβπΌ))) β (Ο βo
(πΊβπ’)) = (Ο βo (πΊβπΌ))) |
79 | 77 | fveq2d 6850 |
. . . . . . . . . 10
β’ ((π β§ (π’ = πΌ β§ π£ = (πβπΌ))) β (πΉβ(πΊβπ’)) = (πΉβ(πΊβπΌ))) |
80 | 78, 79 | oveq12d 7379 |
. . . . . . . . 9
β’ ((π β§ (π’ = πΌ β§ π£ = (πβπΌ))) β ((Ο βo
(πΊβπ’)) Β·o (πΉβ(πΊβπ’))) = ((Ο βo (πΊβπΌ)) Β·o (πΉβ(πΊβπΌ)))) |
81 | | simpr 486 |
. . . . . . . . . . . 12
β’ ((π’ = πΌ β§ π£ = (πβπΌ)) β π£ = (πβπΌ)) |
82 | 81 | dmeqd 5865 |
. . . . . . . . . . 11
β’ ((π’ = πΌ β§ π£ = (πβπΌ)) β dom π£ = dom (πβπΌ)) |
83 | | cnfcom.3 |
. . . . . . . . . . . 12
β’ (π β (πβπΌ):(π»βπΌ)β1-1-ontoβπ) |
84 | | f1odm 6792 |
. . . . . . . . . . . 12
β’ ((πβπΌ):(π»βπΌ)β1-1-ontoβπ β dom (πβπΌ) = (π»βπΌ)) |
85 | 83, 84 | syl 17 |
. . . . . . . . . . 11
β’ (π β dom (πβπΌ) = (π»βπΌ)) |
86 | 82, 85 | sylan9eqr 2795 |
. . . . . . . . . 10
β’ ((π β§ (π’ = πΌ β§ π£ = (πβπΌ))) β dom π£ = (π»βπΌ)) |
87 | 86 | oveq1d 7376 |
. . . . . . . . 9
β’ ((π β§ (π’ = πΌ β§ π£ = (πβπΌ))) β (dom π£ +o π¦) = ((π»βπΌ) +o π¦)) |
88 | 80, 87 | mpteq12dv 5200 |
. . . . . . . 8
β’ ((π β§ (π’ = πΌ β§ π£ = (πβπΌ))) β (π¦ β ((Ο βo (πΊβπ’)) Β·o (πΉβ(πΊβπ’))) β¦ (dom π£ +o π¦)) = (π¦ β ((Ο βo (πΊβπΌ)) Β·o (πΉβ(πΊβπΌ))) β¦ ((π»βπΌ) +o π¦))) |
89 | 80 | oveq1d 7376 |
. . . . . . . . . 10
β’ ((π β§ (π’ = πΌ β§ π£ = (πβπΌ))) β (((Ο βo
(πΊβπ’)) Β·o (πΉβ(πΊβπ’))) +o π¦) = (((Ο βo (πΊβπΌ)) Β·o (πΉβ(πΊβπΌ))) +o π¦)) |
90 | 86, 89 | mpteq12dv 5200 |
. . . . . . . . 9
β’ ((π β§ (π’ = πΌ β§ π£ = (πβπΌ))) β (π¦ β dom π£ β¦ (((Ο βo (πΊβπ’)) Β·o (πΉβ(πΊβπ’))) +o π¦)) = (π¦ β (π»βπΌ) β¦ (((Ο βo
(πΊβπΌ)) Β·o (πΉβ(πΊβπΌ))) +o π¦))) |
91 | 90 | cnveqd 5835 |
. . . . . . . 8
β’ ((π β§ (π’ = πΌ β§ π£ = (πβπΌ))) β β‘(π¦ β dom π£ β¦ (((Ο βo (πΊβπ’)) Β·o (πΉβ(πΊβπ’))) +o π¦)) = β‘(π¦ β (π»βπΌ) β¦ (((Ο βo
(πΊβπΌ)) Β·o (πΉβ(πΊβπΌ))) +o π¦))) |
92 | 88, 91 | uneq12d 4128 |
. . . . . . 7
β’ ((π β§ (π’ = πΌ β§ π£ = (πβπΌ))) β ((π¦ β ((Ο βo (πΊβπ’)) Β·o (πΉβ(πΊβπ’))) β¦ (dom π£ +o π¦)) βͺ β‘(π¦ β dom π£ β¦ (((Ο βo (πΊβπ’)) Β·o (πΉβ(πΊβπ’))) +o π¦))) = ((π¦ β ((Ο βo (πΊβπΌ)) Β·o (πΉβ(πΊβπΌ))) β¦ ((π»βπΌ) +o π¦)) βͺ β‘(π¦ β (π»βπΌ) β¦ (((Ο βo
(πΊβπΌ)) Β·o (πΉβ(πΊβπΌ))) +o π¦)))) |
93 | 18 | elexd 3467 |
. . . . . . 7
β’ (π β πΌ β V) |
94 | | fvexd 6861 |
. . . . . . 7
β’ (π β (πβπΌ) β V) |
95 | | ovex 7394 |
. . . . . . . . . 10
β’ ((Ο
βo (πΊβπΌ)) Β·o (πΉβ(πΊβπΌ))) β V |
96 | 95 | mptex 7177 |
. . . . . . . . 9
β’ (π¦ β ((Ο
βo (πΊβπΌ)) Β·o (πΉβ(πΊβπΌ))) β¦ ((π»βπΌ) +o π¦)) β V |
97 | | fvex 6859 |
. . . . . . . . . . 11
β’ (π»βπΌ) β V |
98 | 97 | mptex 7177 |
. . . . . . . . . 10
β’ (π¦ β (π»βπΌ) β¦ (((Ο βo
(πΊβπΌ)) Β·o (πΉβ(πΊβπΌ))) +o π¦)) β V |
99 | 98 | cnvex 7866 |
. . . . . . . . 9
β’ β‘(π¦ β (π»βπΌ) β¦ (((Ο βo
(πΊβπΌ)) Β·o (πΉβ(πΊβπΌ))) +o π¦)) β V |
100 | 96, 99 | unex 7684 |
. . . . . . . 8
β’ ((π¦ β ((Ο
βo (πΊβπΌ)) Β·o (πΉβ(πΊβπΌ))) β¦ ((π»βπΌ) +o π¦)) βͺ β‘(π¦ β (π»βπΌ) β¦ (((Ο βo
(πΊβπΌ)) Β·o (πΉβ(πΊβπΌ))) +o π¦))) β V |
101 | 100 | a1i 11 |
. . . . . . 7
β’ (π β ((π¦ β ((Ο βo (πΊβπΌ)) Β·o (πΉβ(πΊβπΌ))) β¦ ((π»βπΌ) +o π¦)) βͺ β‘(π¦ β (π»βπΌ) β¦ (((Ο βo
(πΊβπΌ)) Β·o (πΉβ(πΊβπΌ))) +o π¦))) β V) |
102 | 75, 92, 93, 94, 101 | ovmpod 7511 |
. . . . . 6
β’ (π β (πΌ(π β V, π β V β¦ πΎ)(πβπΌ)) = ((π¦ β ((Ο βo (πΊβπΌ)) Β·o (πΉβ(πΊβπΌ))) β¦ ((π»βπΌ) +o π¦)) βͺ β‘(π¦ β (π»βπΌ) β¦ (((Ο βo
(πΊβπΌ)) Β·o (πΉβ(πΊβπΌ))) +o π¦)))) |
103 | 46, 102 | eqtrd 2773 |
. . . . 5
β’ (π β (πβsuc πΌ) = ((π¦ β ((Ο βo (πΊβπΌ)) Β·o (πΉβ(πΊβπΌ))) β¦ ((π»βπΌ) +o π¦)) βͺ β‘(π¦ β (π»βπΌ) β¦ (((Ο βo
(πΊβπΌ)) Β·o (πΉβ(πΊβπΌ))) +o π¦)))) |
104 | 103 | f1oeq1d 6783 |
. . . 4
β’ (π β ((πβsuc πΌ):(((Ο βo (πΊβπΌ)) Β·o (πΉβ(πΊβπΌ))) +o (π»βπΌ))β1-1-ontoβ((π»βπΌ) +o ((Ο βo
(πΊβπΌ)) Β·o (πΉβ(πΊβπΌ)))) β ((π¦ β ((Ο βo (πΊβπΌ)) Β·o (πΉβ(πΊβπΌ))) β¦ ((π»βπΌ) +o π¦)) βͺ β‘(π¦ β (π»βπΌ) β¦ (((Ο βo
(πΊβπΌ)) Β·o (πΉβ(πΊβπΌ))) +o π¦))):(((Ο βo (πΊβπΌ)) Β·o (πΉβ(πΊβπΌ))) +o (π»βπΌ))β1-1-ontoβ((π»βπΌ) +o ((Ο βo
(πΊβπΌ)) Β·o (πΉβ(πΊβπΌ)))))) |
105 | 43, 104 | mpbird 257 |
. . 3
β’ (π β (πβsuc πΌ):(((Ο βo (πΊβπΌ)) Β·o (πΉβ(πΊβπΌ))) +o (π»βπΌ))β1-1-ontoβ((π»βπΌ) +o ((Ο βo
(πΊβπΌ)) Β·o (πΉβ(πΊβπΌ))))) |
106 | 1 | a1i 11 |
. . . . . 6
β’ ((π΄ β On β§ πΉ β π) β Ο β On) |
107 | | simpl 484 |
. . . . . 6
β’ ((π΄ β On β§ πΉ β π) β π΄ β On) |
108 | | simpr 486 |
. . . . . 6
β’ ((π΄ β On β§ πΉ β π) β πΉ β π) |
109 | 54 | oveq1i 7371 |
. . . . . . . . . 10
β’ (π +o π§) = (((Ο
βo (πΊβπ)) Β·o (πΉβ(πΊβπ))) +o π§) |
110 | 109 | a1i 11 |
. . . . . . . . 9
β’ ((π β V β§ π§ β V) β (π +o π§) = (((Ο
βo (πΊβπ)) Β·o (πΉβ(πΊβπ))) +o π§)) |
111 | 110 | mpoeq3ia 7439 |
. . . . . . . 8
β’ (π β V, π§ β V β¦ (π +o π§)) = (π β V, π§ β V β¦ (((Ο
βo (πΊβπ)) Β·o (πΉβ(πΊβπ))) +o π§)) |
112 | | eqid 2733 |
. . . . . . . 8
β’ β
=
β
|
113 | | seqomeq12 8404 |
. . . . . . . 8
β’ (((π β V, π§ β V β¦ (π +o π§)) = (π β V, π§ β V β¦ (((Ο
βo (πΊβπ)) Β·o (πΉβ(πΊβπ))) +o π§)) β§ β
= β
) β
seqΟ((π
β V, π§ β V
β¦ (π +o
π§)), β
) =
seqΟ((π
β V, π§ β V
β¦ (((Ο βo (πΊβπ)) Β·o (πΉβ(πΊβπ))) +o π§)), β
)) |
114 | 111, 112,
113 | mp2an 691 |
. . . . . . 7
β’
seqΟ((π β V, π§ β V β¦ (π +o π§)), β
) = seqΟ((π β V, π§ β V β¦ (((Ο
βo (πΊβπ)) Β·o (πΉβ(πΊβπ))) +o π§)), β
) |
115 | 37, 114 | eqtri 2761 |
. . . . . 6
β’ π» = seqΟ((π β V, π§ β V β¦ (((Ο
βo (πΊβπ)) Β·o (πΉβ(πΊβπ))) +o π§)), β
) |
116 | 5, 106, 107, 19, 108, 115 | cantnfsuc 9614 |
. . . . 5
β’ (((π΄ β On β§ πΉ β π) β§ πΌ β Ο) β (π»βsuc πΌ) = (((Ο βo (πΊβπΌ)) Β·o (πΉβ(πΊβπΌ))) +o (π»βπΌ))) |
117 | 2, 13, 36, 116 | syl21anc 837 |
. . . 4
β’ (π β (π»βsuc πΌ) = (((Ο βo (πΊβπΌ)) Β·o (πΉβ(πΊβπΌ))) +o (π»βπΌ))) |
118 | 117 | f1oeq2d 6784 |
. . 3
β’ (π β ((πβsuc πΌ):(π»βsuc πΌ)β1-1-ontoβ((π»βπΌ) +o ((Ο βo
(πΊβπΌ)) Β·o (πΉβ(πΊβπΌ)))) β (πβsuc πΌ):(((Ο βo (πΊβπΌ)) Β·o (πΉβ(πΊβπΌ))) +o (π»βπΌ))β1-1-ontoβ((π»βπΌ) +o ((Ο βo
(πΊβπΌ)) Β·o (πΉβ(πΊβπΌ)))))) |
119 | 105, 118 | mpbird 257 |
. 2
β’ (π β (πβsuc πΌ):(π»βsuc πΌ)β1-1-ontoβ((π»βπΌ) +o ((Ο βo
(πΊβπΌ)) Β·o (πΉβ(πΊβπΌ))))) |
120 | | sssucid 6401 |
. . . . . 6
β’ dom πΊ β suc dom πΊ |
121 | 120, 18 | sselid 3946 |
. . . . 5
β’ (π β πΌ β suc dom πΊ) |
122 | | epelg 5542 |
. . . . . . . . . . 11
β’ (πΌ β dom πΊ β (π¦ E πΌ β π¦ β πΌ)) |
123 | 18, 122 | syl 17 |
. . . . . . . . . 10
β’ (π β (π¦ E πΌ β π¦ β πΌ)) |
124 | 123 | biimpar 479 |
. . . . . . . . 9
β’ ((π β§ π¦ β πΌ) β π¦ E πΌ) |
125 | | ovexd 7396 |
. . . . . . . . . . . 12
β’ (π β (πΉ supp β
) β V) |
126 | 33 | simpld 496 |
. . . . . . . . . . . 12
β’ (π β E We (πΉ supp β
)) |
127 | 19 | oiiso 9481 |
. . . . . . . . . . . 12
β’ (((πΉ supp β
) β V β§ E
We (πΉ supp β
)) β
πΊ Isom E , E (dom πΊ, (πΉ supp β
))) |
128 | 125, 126,
127 | syl2anc 585 |
. . . . . . . . . . 11
β’ (π β πΊ Isom E , E (dom πΊ, (πΉ supp β
))) |
129 | 128 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π¦ β πΌ) β πΊ Isom E , E (dom πΊ, (πΉ supp β
))) |
130 | 19 | oicl 9473 |
. . . . . . . . . . . 12
β’ Ord dom
πΊ |
131 | | ordelss 6337 |
. . . . . . . . . . . 12
β’ ((Ord dom
πΊ β§ πΌ β dom πΊ) β πΌ β dom πΊ) |
132 | 130, 18, 131 | sylancr 588 |
. . . . . . . . . . 11
β’ (π β πΌ β dom πΊ) |
133 | 132 | sselda 3948 |
. . . . . . . . . 10
β’ ((π β§ π¦ β πΌ) β π¦ β dom πΊ) |
134 | 18 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π¦ β πΌ) β πΌ β dom πΊ) |
135 | | isorel 7275 |
. . . . . . . . . 10
β’ ((πΊ Isom E , E (dom πΊ, (πΉ supp β
)) β§ (π¦ β dom πΊ β§ πΌ β dom πΊ)) β (π¦ E πΌ β (πΊβπ¦) E (πΊβπΌ))) |
136 | 129, 133,
134, 135 | syl12anc 836 |
. . . . . . . . 9
β’ ((π β§ π¦ β πΌ) β (π¦ E πΌ β (πΊβπ¦) E (πΊβπΌ))) |
137 | 124, 136 | mpbid 231 |
. . . . . . . 8
β’ ((π β§ π¦ β πΌ) β (πΊβπ¦) E (πΊβπΌ)) |
138 | | fvex 6859 |
. . . . . . . . 9
β’ (πΊβπΌ) β V |
139 | 138 | epeli 5543 |
. . . . . . . 8
β’ ((πΊβπ¦) E (πΊβπΌ) β (πΊβπ¦) β (πΊβπΌ)) |
140 | 137, 139 | sylib 217 |
. . . . . . 7
β’ ((π β§ π¦ β πΌ) β (πΊβπ¦) β (πΊβπΌ)) |
141 | 140 | ralrimiva 3140 |
. . . . . 6
β’ (π β βπ¦ β πΌ (πΊβπ¦) β (πΊβπΌ)) |
142 | | ffun 6675 |
. . . . . . . 8
β’ (πΊ:dom πΊβΆ(πΉ supp β
) β Fun πΊ) |
143 | 20, 142 | ax-mp 5 |
. . . . . . 7
β’ Fun πΊ |
144 | | funimass4 6911 |
. . . . . . 7
β’ ((Fun
πΊ β§ πΌ β dom πΊ) β ((πΊ β πΌ) β (πΊβπΌ) β βπ¦ β πΌ (πΊβπ¦) β (πΊβπΌ))) |
145 | 143, 132,
144 | sylancr 588 |
. . . . . 6
β’ (π β ((πΊ β πΌ) β (πΊβπΌ) β βπ¦ β πΌ (πΊβπ¦) β (πΊβπΌ))) |
146 | 141, 145 | mpbird 257 |
. . . . 5
β’ (π β (πΊ β πΌ) β (πΊβπΌ)) |
147 | 1 | a1i 11 |
. . . . . 6
β’ (((π΄ β On β§ πΉ β π) β§ (πΌ β suc dom πΊ β§ (πΊβπΌ) β On β§ (πΊ β πΌ) β (πΊβπΌ))) β Ο β
On) |
148 | | simpll 766 |
. . . . . 6
β’ (((π΄ β On β§ πΉ β π) β§ (πΌ β suc dom πΊ β§ (πΊβπΌ) β On β§ (πΊ β πΌ) β (πΊβπΌ))) β π΄ β On) |
149 | | simplr 768 |
. . . . . 6
β’ (((π΄ β On β§ πΉ β π) β§ (πΌ β suc dom πΊ β§ (πΊβπΌ) β On β§ (πΊ β πΌ) β (πΊβπΌ))) β πΉ β π) |
150 | | peano1 7829 |
. . . . . . 7
β’ β
β Ο |
151 | 150 | a1i 11 |
. . . . . 6
β’ (((π΄ β On β§ πΉ β π) β§ (πΌ β suc dom πΊ β§ (πΊβπΌ) β On β§ (πΊ β πΌ) β (πΊβπΌ))) β β
β
Ο) |
152 | | simpr1 1195 |
. . . . . 6
β’ (((π΄ β On β§ πΉ β π) β§ (πΌ β suc dom πΊ β§ (πΊβπΌ) β On β§ (πΊ β πΌ) β (πΊβπΌ))) β πΌ β suc dom πΊ) |
153 | | simpr2 1196 |
. . . . . 6
β’ (((π΄ β On β§ πΉ β π) β§ (πΌ β suc dom πΊ β§ (πΊβπΌ) β On β§ (πΊ β πΌ) β (πΊβπΌ))) β (πΊβπΌ) β On) |
154 | | simpr3 1197 |
. . . . . 6
β’ (((π΄ β On β§ πΉ β π) β§ (πΌ β suc dom πΊ β§ (πΊβπΌ) β On β§ (πΊ β πΌ) β (πΊβπΌ))) β (πΊ β πΌ) β (πΊβπΌ)) |
155 | 5, 147, 148, 19, 149, 115, 151, 152, 153, 154 | cantnflt 9616 |
. . . . 5
β’ (((π΄ β On β§ πΉ β π) β§ (πΌ β suc dom πΊ β§ (πΊβπΌ) β On β§ (πΊ β πΌ) β (πΊβπΌ))) β (π»βπΌ) β (Ο βo (πΊβπΌ))) |
156 | 2, 13, 121, 25, 146, 155 | syl23anc 1378 |
. . . 4
β’ (π β (π»βπΌ) β (Ο βo (πΊβπΌ))) |
157 | 16 | ffnd 6673 |
. . . . . . . . 9
β’ (π β πΉ Fn π΄) |
158 | | 0ex 5268 |
. . . . . . . . . 10
β’ β
β V |
159 | 158 | a1i 11 |
. . . . . . . . 9
β’ (π β β
β
V) |
160 | | elsuppfn 8106 |
. . . . . . . . 9
β’ ((πΉ Fn π΄ β§ π΄ β On β§ β
β V) β
((πΊβπΌ) β (πΉ supp β
) β ((πΊβπΌ) β π΄ β§ (πΉβ(πΊβπΌ)) β β
))) |
161 | 157, 2, 159, 160 | syl3anc 1372 |
. . . . . . . 8
β’ (π β ((πΊβπΌ) β (πΉ supp β
) β ((πΊβπΌ) β π΄ β§ (πΉβ(πΊβπΌ)) β β
))) |
162 | | simpr 486 |
. . . . . . . 8
β’ (((πΊβπΌ) β π΄ β§ (πΉβ(πΊβπΌ)) β β
) β (πΉβ(πΊβπΌ)) β β
) |
163 | 161, 162 | syl6bi 253 |
. . . . . . 7
β’ (π β ((πΊβπΌ) β (πΉ supp β
) β (πΉβ(πΊβπΌ)) β β
)) |
164 | 22, 163 | mpd 15 |
. . . . . 6
β’ (π β (πΉβ(πΊβπΌ)) β β
) |
165 | | on0eln0 6377 |
. . . . . . 7
β’ ((πΉβ(πΊβπΌ)) β On β (β
β (πΉβ(πΊβπΌ)) β (πΉβ(πΊβπΌ)) β β
)) |
166 | 30, 165 | syl 17 |
. . . . . 6
β’ (π β (β
β (πΉβ(πΊβπΌ)) β (πΉβ(πΊβπΌ)) β β
)) |
167 | 164, 166 | mpbird 257 |
. . . . 5
β’ (π β β
β (πΉβ(πΊβπΌ))) |
168 | | omword1 8524 |
. . . . 5
β’
((((Ο βo (πΊβπΌ)) β On β§ (πΉβ(πΊβπΌ)) β On) β§ β
β (πΉβ(πΊβπΌ))) β (Ο βo
(πΊβπΌ)) β ((Ο βo
(πΊβπΌ)) Β·o (πΉβ(πΊβπΌ)))) |
169 | 27, 30, 167, 168 | syl21anc 837 |
. . . 4
β’ (π β (Ο
βo (πΊβπΌ)) β ((Ο βo
(πΊβπΌ)) Β·o (πΉβ(πΊβπΌ)))) |
170 | | oaabs2 8599 |
. . . 4
β’ ((((π»βπΌ) β (Ο βo (πΊβπΌ)) β§ ((Ο βo (πΊβπΌ)) Β·o (πΉβ(πΊβπΌ))) β On) β§ (Ο
βo (πΊβπΌ)) β ((Ο βo
(πΊβπΌ)) Β·o (πΉβ(πΊβπΌ)))) β ((π»βπΌ) +o ((Ο βo
(πΊβπΌ)) Β·o (πΉβ(πΊβπΌ)))) = ((Ο βo (πΊβπΌ)) Β·o (πΉβ(πΊβπΌ)))) |
171 | 156, 32, 169, 170 | syl21anc 837 |
. . 3
β’ (π β ((π»βπΌ) +o ((Ο βo
(πΊβπΌ)) Β·o (πΉβ(πΊβπΌ)))) = ((Ο βo (πΊβπΌ)) Β·o (πΉβ(πΊβπΌ)))) |
172 | 171 | f1oeq3d 6785 |
. 2
β’ (π β ((πβsuc πΌ):(π»βsuc πΌ)β1-1-ontoβ((π»βπΌ) +o ((Ο βo
(πΊβπΌ)) Β·o (πΉβ(πΊβπΌ)))) β (πβsuc πΌ):(π»βsuc πΌ)β1-1-ontoβ((Ο βo (πΊβπΌ)) Β·o (πΉβ(πΊβπΌ))))) |
173 | 119, 172 | mpbid 231 |
1
β’ (π β (πβsuc πΌ):(π»βsuc πΌ)β1-1-ontoβ((Ο βo (πΊβπΌ)) Β·o (πΉβ(πΊβπΌ)))) |