Step | Hyp | Ref
| Expression |
1 | | cantnfs.a |
. . . 4
β’ (π β π΄ β On) |
2 | | cantnflt.c |
. . . 4
β’ (π β πΆ β On) |
3 | | cantnflt.a |
. . . 4
β’ (π β β
β π΄) |
4 | | oen0 8537 |
. . . 4
β’ (((π΄ β On β§ πΆ β On) β§ β
β
π΄) β β
β
(π΄ βo πΆ)) |
5 | 1, 2, 3, 4 | syl21anc 837 |
. . 3
β’ (π β β
β (π΄ βo πΆ)) |
6 | | fveq2 6846 |
. . . . 5
β’ (πΎ = β
β (π»βπΎ) = (π»ββ
)) |
7 | | 0ex 5268 |
. . . . . 6
β’ β
β V |
8 | | cantnfval.h |
. . . . . . 7
β’ π» = seqΟ((π β V, π§ β V β¦ (((π΄ βo (πΊβπ)) Β·o (πΉβ(πΊβπ))) +o π§)), β
) |
9 | 8 | seqom0g 8406 |
. . . . . 6
β’ (β
β V β (π»ββ
) = β
) |
10 | 7, 9 | ax-mp 5 |
. . . . 5
β’ (π»ββ
) =
β
|
11 | 6, 10 | eqtrdi 2789 |
. . . 4
β’ (πΎ = β
β (π»βπΎ) = β
) |
12 | 11 | eleq1d 2819 |
. . 3
β’ (πΎ = β
β ((π»βπΎ) β (π΄ βo πΆ) β β
β (π΄ βo πΆ))) |
13 | 5, 12 | syl5ibrcom 247 |
. 2
β’ (π β (πΎ = β
β (π»βπΎ) β (π΄ βo πΆ))) |
14 | 2 | adantr 482 |
. . . . . . 7
β’ ((π β§ (π₯ β Ο β§ πΎ = suc π₯)) β πΆ β On) |
15 | | eloni 6331 |
. . . . . . 7
β’ (πΆ β On β Ord πΆ) |
16 | 14, 15 | syl 17 |
. . . . . 6
β’ ((π β§ (π₯ β Ο β§ πΎ = suc π₯)) β Ord πΆ) |
17 | | cantnflt.s |
. . . . . . . 8
β’ (π β (πΊ β πΎ) β πΆ) |
18 | 17 | adantr 482 |
. . . . . . 7
β’ ((π β§ (π₯ β Ο β§ πΎ = suc π₯)) β (πΊ β πΎ) β πΆ) |
19 | | cantnfcl.g |
. . . . . . . . . 10
β’ πΊ = OrdIso( E , (πΉ supp β
)) |
20 | 19 | oif 9474 |
. . . . . . . . 9
β’ πΊ:dom πΊβΆ(πΉ supp β
) |
21 | | ffn 6672 |
. . . . . . . . 9
β’ (πΊ:dom πΊβΆ(πΉ supp β
) β πΊ Fn dom πΊ) |
22 | 20, 21 | mp1i 13 |
. . . . . . . 8
β’ ((π β§ (π₯ β Ο β§ πΎ = suc π₯)) β πΊ Fn dom πΊ) |
23 | | cantnflt.k |
. . . . . . . . . 10
β’ (π β πΎ β suc dom πΊ) |
24 | 19 | oicl 9473 |
. . . . . . . . . . . . 13
β’ Ord dom
πΊ |
25 | | ordsuc 7752 |
. . . . . . . . . . . . 13
β’ (Ord dom
πΊ β Ord suc dom πΊ) |
26 | 24, 25 | mpbi 229 |
. . . . . . . . . . . 12
β’ Ord suc
dom πΊ |
27 | | ordelon 6345 |
. . . . . . . . . . . 12
β’ ((Ord suc
dom πΊ β§ πΎ β suc dom πΊ) β πΎ β On) |
28 | 26, 23, 27 | sylancr 588 |
. . . . . . . . . . 11
β’ (π β πΎ β On) |
29 | | ordsssuc 6410 |
. . . . . . . . . . 11
β’ ((πΎ β On β§ Ord dom πΊ) β (πΎ β dom πΊ β πΎ β suc dom πΊ)) |
30 | 28, 24, 29 | sylancl 587 |
. . . . . . . . . 10
β’ (π β (πΎ β dom πΊ β πΎ β suc dom πΊ)) |
31 | 23, 30 | mpbird 257 |
. . . . . . . . 9
β’ (π β πΎ β dom πΊ) |
32 | 31 | adantr 482 |
. . . . . . . 8
β’ ((π β§ (π₯ β Ο β§ πΎ = suc π₯)) β πΎ β dom πΊ) |
33 | | vex 3451 |
. . . . . . . . . 10
β’ π₯ β V |
34 | 33 | sucid 6403 |
. . . . . . . . 9
β’ π₯ β suc π₯ |
35 | | simprr 772 |
. . . . . . . . 9
β’ ((π β§ (π₯ β Ο β§ πΎ = suc π₯)) β πΎ = suc π₯) |
36 | 34, 35 | eleqtrrid 2841 |
. . . . . . . 8
β’ ((π β§ (π₯ β Ο β§ πΎ = suc π₯)) β π₯ β πΎ) |
37 | | fnfvima 7187 |
. . . . . . . 8
β’ ((πΊ Fn dom πΊ β§ πΎ β dom πΊ β§ π₯ β πΎ) β (πΊβπ₯) β (πΊ β πΎ)) |
38 | 22, 32, 36, 37 | syl3anc 1372 |
. . . . . . 7
β’ ((π β§ (π₯ β Ο β§ πΎ = suc π₯)) β (πΊβπ₯) β (πΊ β πΎ)) |
39 | 18, 38 | sseldd 3949 |
. . . . . 6
β’ ((π β§ (π₯ β Ο β§ πΎ = suc π₯)) β (πΊβπ₯) β πΆ) |
40 | | ordsucss 7757 |
. . . . . 6
β’ (Ord
πΆ β ((πΊβπ₯) β πΆ β suc (πΊβπ₯) β πΆ)) |
41 | 16, 39, 40 | sylc 65 |
. . . . 5
β’ ((π β§ (π₯ β Ο β§ πΎ = suc π₯)) β suc (πΊβπ₯) β πΆ) |
42 | | suppssdm 8112 |
. . . . . . . . . . 11
β’ (πΉ supp β
) β dom πΉ |
43 | | cantnfcl.f |
. . . . . . . . . . . . 13
β’ (π β πΉ β π) |
44 | | cantnfs.s |
. . . . . . . . . . . . . 14
β’ π = dom (π΄ CNF π΅) |
45 | | cantnfs.b |
. . . . . . . . . . . . . 14
β’ (π β π΅ β On) |
46 | 44, 1, 45 | cantnfs 9610 |
. . . . . . . . . . . . 13
β’ (π β (πΉ β π β (πΉ:π΅βΆπ΄ β§ πΉ finSupp β
))) |
47 | 43, 46 | mpbid 231 |
. . . . . . . . . . . 12
β’ (π β (πΉ:π΅βΆπ΄ β§ πΉ finSupp β
)) |
48 | 47 | simpld 496 |
. . . . . . . . . . 11
β’ (π β πΉ:π΅βΆπ΄) |
49 | 42, 48 | fssdm 6692 |
. . . . . . . . . 10
β’ (π β (πΉ supp β
) β π΅) |
50 | | onss 7723 |
. . . . . . . . . . 11
β’ (π΅ β On β π΅ β On) |
51 | 45, 50 | syl 17 |
. . . . . . . . . 10
β’ (π β π΅ β On) |
52 | 49, 51 | sstrd 3958 |
. . . . . . . . 9
β’ (π β (πΉ supp β
) β On) |
53 | 52 | adantr 482 |
. . . . . . . 8
β’ ((π β§ (π₯ β Ο β§ πΎ = suc π₯)) β (πΉ supp β
) β On) |
54 | 23 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ (π₯ β Ο β§ πΎ = suc π₯)) β πΎ β suc dom πΊ) |
55 | 35, 54 | eqeltrrd 2835 |
. . . . . . . . . 10
β’ ((π β§ (π₯ β Ο β§ πΎ = suc π₯)) β suc π₯ β suc dom πΊ) |
56 | | ordsucelsuc 7761 |
. . . . . . . . . . 11
β’ (Ord dom
πΊ β (π₯ β dom πΊ β suc π₯ β suc dom πΊ)) |
57 | 24, 56 | ax-mp 5 |
. . . . . . . . . 10
β’ (π₯ β dom πΊ β suc π₯ β suc dom πΊ) |
58 | 55, 57 | sylibr 233 |
. . . . . . . . 9
β’ ((π β§ (π₯ β Ο β§ πΎ = suc π₯)) β π₯ β dom πΊ) |
59 | 20 | ffvelcdmi 7038 |
. . . . . . . . 9
β’ (π₯ β dom πΊ β (πΊβπ₯) β (πΉ supp β
)) |
60 | 58, 59 | syl 17 |
. . . . . . . 8
β’ ((π β§ (π₯ β Ο β§ πΎ = suc π₯)) β (πΊβπ₯) β (πΉ supp β
)) |
61 | 53, 60 | sseldd 3949 |
. . . . . . 7
β’ ((π β§ (π₯ β Ο β§ πΎ = suc π₯)) β (πΊβπ₯) β On) |
62 | | onsuc 7750 |
. . . . . . 7
β’ ((πΊβπ₯) β On β suc (πΊβπ₯) β On) |
63 | 61, 62 | syl 17 |
. . . . . 6
β’ ((π β§ (π₯ β Ο β§ πΎ = suc π₯)) β suc (πΊβπ₯) β On) |
64 | 1 | adantr 482 |
. . . . . 6
β’ ((π β§ (π₯ β Ο β§ πΎ = suc π₯)) β π΄ β On) |
65 | 3 | adantr 482 |
. . . . . 6
β’ ((π β§ (π₯ β Ο β§ πΎ = suc π₯)) β β
β π΄) |
66 | | oewordi 8542 |
. . . . . 6
β’ (((suc
(πΊβπ₯) β On β§ πΆ β On β§ π΄ β On) β§ β
β π΄) β (suc (πΊβπ₯) β πΆ β (π΄ βo suc (πΊβπ₯)) β (π΄ βo πΆ))) |
67 | 63, 14, 64, 65, 66 | syl31anc 1374 |
. . . . 5
β’ ((π β§ (π₯ β Ο β§ πΎ = suc π₯)) β (suc (πΊβπ₯) β πΆ β (π΄ βo suc (πΊβπ₯)) β (π΄ βo πΆ))) |
68 | 41, 67 | mpd 15 |
. . . 4
β’ ((π β§ (π₯ β Ο β§ πΎ = suc π₯)) β (π΄ βo suc (πΊβπ₯)) β (π΄ βo πΆ)) |
69 | 35 | fveq2d 6850 |
. . . . 5
β’ ((π β§ (π₯ β Ο β§ πΎ = suc π₯)) β (π»βπΎ) = (π»βsuc π₯)) |
70 | | simprl 770 |
. . . . . 6
β’ ((π β§ (π₯ β Ο β§ πΎ = suc π₯)) β π₯ β Ο) |
71 | | simpl 484 |
. . . . . 6
β’ ((π β§ (π₯ β Ο β§ πΎ = suc π₯)) β π) |
72 | | eleq1 2822 |
. . . . . . . 8
β’ (π₯ = β
β (π₯ β dom πΊ β β
β dom πΊ)) |
73 | | suceq 6387 |
. . . . . . . . . 10
β’ (π₯ = β
β suc π₯ = suc β
) |
74 | 73 | fveq2d 6850 |
. . . . . . . . 9
β’ (π₯ = β
β (π»βsuc π₯) = (π»βsuc β
)) |
75 | | fveq2 6846 |
. . . . . . . . . . 11
β’ (π₯ = β
β (πΊβπ₯) = (πΊββ
)) |
76 | | suceq 6387 |
. . . . . . . . . . 11
β’ ((πΊβπ₯) = (πΊββ
) β suc (πΊβπ₯) = suc (πΊββ
)) |
77 | 75, 76 | syl 17 |
. . . . . . . . . 10
β’ (π₯ = β
β suc (πΊβπ₯) = suc (πΊββ
)) |
78 | 77 | oveq2d 7377 |
. . . . . . . . 9
β’ (π₯ = β
β (π΄ βo suc (πΊβπ₯)) = (π΄ βo suc (πΊββ
))) |
79 | 74, 78 | eleq12d 2828 |
. . . . . . . 8
β’ (π₯ = β
β ((π»βsuc π₯) β (π΄ βo suc (πΊβπ₯)) β (π»βsuc β
) β (π΄ βo suc (πΊββ
)))) |
80 | 72, 79 | imbi12d 345 |
. . . . . . 7
β’ (π₯ = β
β ((π₯ β dom πΊ β (π»βsuc π₯) β (π΄ βo suc (πΊβπ₯))) β (β
β dom πΊ β (π»βsuc β
) β (π΄ βo suc (πΊββ
))))) |
81 | | eleq1 2822 |
. . . . . . . 8
β’ (π₯ = π¦ β (π₯ β dom πΊ β π¦ β dom πΊ)) |
82 | | suceq 6387 |
. . . . . . . . . 10
β’ (π₯ = π¦ β suc π₯ = suc π¦) |
83 | 82 | fveq2d 6850 |
. . . . . . . . 9
β’ (π₯ = π¦ β (π»βsuc π₯) = (π»βsuc π¦)) |
84 | | fveq2 6846 |
. . . . . . . . . . 11
β’ (π₯ = π¦ β (πΊβπ₯) = (πΊβπ¦)) |
85 | | suceq 6387 |
. . . . . . . . . . 11
β’ ((πΊβπ₯) = (πΊβπ¦) β suc (πΊβπ₯) = suc (πΊβπ¦)) |
86 | 84, 85 | syl 17 |
. . . . . . . . . 10
β’ (π₯ = π¦ β suc (πΊβπ₯) = suc (πΊβπ¦)) |
87 | 86 | oveq2d 7377 |
. . . . . . . . 9
β’ (π₯ = π¦ β (π΄ βo suc (πΊβπ₯)) = (π΄ βo suc (πΊβπ¦))) |
88 | 83, 87 | eleq12d 2828 |
. . . . . . . 8
β’ (π₯ = π¦ β ((π»βsuc π₯) β (π΄ βo suc (πΊβπ₯)) β (π»βsuc π¦) β (π΄ βo suc (πΊβπ¦)))) |
89 | 81, 88 | imbi12d 345 |
. . . . . . 7
β’ (π₯ = π¦ β ((π₯ β dom πΊ β (π»βsuc π₯) β (π΄ βo suc (πΊβπ₯))) β (π¦ β dom πΊ β (π»βsuc π¦) β (π΄ βo suc (πΊβπ¦))))) |
90 | | eleq1 2822 |
. . . . . . . 8
β’ (π₯ = suc π¦ β (π₯ β dom πΊ β suc π¦ β dom πΊ)) |
91 | | suceq 6387 |
. . . . . . . . . 10
β’ (π₯ = suc π¦ β suc π₯ = suc suc π¦) |
92 | 91 | fveq2d 6850 |
. . . . . . . . 9
β’ (π₯ = suc π¦ β (π»βsuc π₯) = (π»βsuc suc π¦)) |
93 | | fveq2 6846 |
. . . . . . . . . . 11
β’ (π₯ = suc π¦ β (πΊβπ₯) = (πΊβsuc π¦)) |
94 | | suceq 6387 |
. . . . . . . . . . 11
β’ ((πΊβπ₯) = (πΊβsuc π¦) β suc (πΊβπ₯) = suc (πΊβsuc π¦)) |
95 | 93, 94 | syl 17 |
. . . . . . . . . 10
β’ (π₯ = suc π¦ β suc (πΊβπ₯) = suc (πΊβsuc π¦)) |
96 | 95 | oveq2d 7377 |
. . . . . . . . 9
β’ (π₯ = suc π¦ β (π΄ βo suc (πΊβπ₯)) = (π΄ βo suc (πΊβsuc π¦))) |
97 | 92, 96 | eleq12d 2828 |
. . . . . . . 8
β’ (π₯ = suc π¦ β ((π»βsuc π₯) β (π΄ βo suc (πΊβπ₯)) β (π»βsuc suc π¦) β (π΄ βo suc (πΊβsuc π¦)))) |
98 | 90, 97 | imbi12d 345 |
. . . . . . 7
β’ (π₯ = suc π¦ β ((π₯ β dom πΊ β (π»βsuc π₯) β (π΄ βo suc (πΊβπ₯))) β (suc π¦ β dom πΊ β (π»βsuc suc π¦) β (π΄ βo suc (πΊβsuc π¦))))) |
99 | 48 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ β
β dom πΊ) β πΉ:π΅βΆπ΄) |
100 | 20 | ffvelcdmi 7038 |
. . . . . . . . . . . 12
β’ (β
β dom πΊ β (πΊββ
) β (πΉ supp β
)) |
101 | 49 | sselda 3948 |
. . . . . . . . . . . 12
β’ ((π β§ (πΊββ
) β (πΉ supp β
)) β (πΊββ
) β π΅) |
102 | 100, 101 | sylan2 594 |
. . . . . . . . . . 11
β’ ((π β§ β
β dom πΊ) β (πΊββ
) β π΅) |
103 | 99, 102 | ffvelcdmd 7040 |
. . . . . . . . . 10
β’ ((π β§ β
β dom πΊ) β (πΉβ(πΊββ
)) β π΄) |
104 | 1 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ β
β dom πΊ) β π΄ β On) |
105 | | onelon 6346 |
. . . . . . . . . . . 12
β’ ((π΄ β On β§ (πΉβ(πΊββ
)) β π΄) β (πΉβ(πΊββ
)) β On) |
106 | 104, 103,
105 | syl2anc 585 |
. . . . . . . . . . 11
β’ ((π β§ β
β dom πΊ) β (πΉβ(πΊββ
)) β On) |
107 | 52 | sselda 3948 |
. . . . . . . . . . . . 13
β’ ((π β§ (πΊββ
) β (πΉ supp β
)) β (πΊββ
) β On) |
108 | 100, 107 | sylan2 594 |
. . . . . . . . . . . 12
β’ ((π β§ β
β dom πΊ) β (πΊββ
) β On) |
109 | | oecl 8487 |
. . . . . . . . . . . 12
β’ ((π΄ β On β§ (πΊββ
) β On)
β (π΄
βo (πΊββ
)) β On) |
110 | 104, 108,
109 | syl2anc 585 |
. . . . . . . . . . 11
β’ ((π β§ β
β dom πΊ) β (π΄ βo (πΊββ
)) β On) |
111 | 3 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ β
β dom πΊ) β β
β π΄) |
112 | | oen0 8537 |
. . . . . . . . . . . 12
β’ (((π΄ β On β§ (πΊββ
) β On) β§
β
β π΄) β
β
β (π΄
βo (πΊββ
))) |
113 | 104, 108,
111, 112 | syl21anc 837 |
. . . . . . . . . . 11
β’ ((π β§ β
β dom πΊ) β β
β (π΄ βo (πΊββ
))) |
114 | | omord2 8518 |
. . . . . . . . . . 11
β’ ((((πΉβ(πΊββ
)) β On β§ π΄ β On β§ (π΄ βo (πΊββ
)) β On)
β§ β
β (π΄
βo (πΊββ
))) β ((πΉβ(πΊββ
)) β π΄ β ((π΄ βo (πΊββ
)) Β·o (πΉβ(πΊββ
))) β ((π΄ βo (πΊββ
)) Β·o π΄))) |
115 | 106, 104,
110, 113, 114 | syl31anc 1374 |
. . . . . . . . . 10
β’ ((π β§ β
β dom πΊ) β ((πΉβ(πΊββ
)) β π΄ β ((π΄ βo (πΊββ
)) Β·o (πΉβ(πΊββ
))) β ((π΄ βo (πΊββ
)) Β·o π΄))) |
116 | 103, 115 | mpbid 231 |
. . . . . . . . 9
β’ ((π β§ β
β dom πΊ) β ((π΄ βo (πΊββ
)) Β·o (πΉβ(πΊββ
))) β ((π΄ βo (πΊββ
)) Β·o π΄)) |
117 | | peano1 7829 |
. . . . . . . . . . . 12
β’ β
β Ο |
118 | 117 | a1i 11 |
. . . . . . . . . . 11
β’ (β
β dom πΊ β β
β Ο) |
119 | 44, 1, 45, 19, 43, 8 | cantnfsuc 9614 |
. . . . . . . . . . 11
β’ ((π β§ β
β Ο)
β (π»βsuc
β
) = (((π΄
βo (πΊββ
)) Β·o (πΉβ(πΊββ
))) +o (π»ββ
))) |
120 | 118, 119 | sylan2 594 |
. . . . . . . . . 10
β’ ((π β§ β
β dom πΊ) β (π»βsuc β
) = (((π΄ βo (πΊββ
)) Β·o (πΉβ(πΊββ
))) +o (π»ββ
))) |
121 | 10 | oveq2i 7372 |
. . . . . . . . . . 11
β’ (((π΄ βo (πΊββ
))
Β·o (πΉβ(πΊββ
))) +o (π»ββ
)) = (((π΄ βo (πΊββ
))
Β·o (πΉβ(πΊββ
))) +o
β
) |
122 | | omcl 8486 |
. . . . . . . . . . . . 13
β’ (((π΄ βo (πΊββ
)) β On β§
(πΉβ(πΊββ
)) β On) β ((π΄ βo (πΊββ
))
Β·o (πΉβ(πΊββ
))) β
On) |
123 | 110, 106,
122 | syl2anc 585 |
. . . . . . . . . . . 12
β’ ((π β§ β
β dom πΊ) β ((π΄ βo (πΊββ
)) Β·o (πΉβ(πΊββ
))) β
On) |
124 | | oa0 8466 |
. . . . . . . . . . . 12
β’ (((π΄ βo (πΊββ
))
Β·o (πΉβ(πΊββ
))) β On β (((π΄ βo (πΊββ
))
Β·o (πΉβ(πΊββ
))) +o β
) =
((π΄ βo
(πΊββ
))
Β·o (πΉβ(πΊββ
)))) |
125 | 123, 124 | syl 17 |
. . . . . . . . . . 11
β’ ((π β§ β
β dom πΊ) β (((π΄ βo (πΊββ
)) Β·o (πΉβ(πΊββ
))) +o β
) =
((π΄ βo
(πΊββ
))
Β·o (πΉβ(πΊββ
)))) |
126 | 121, 125 | eqtrid 2785 |
. . . . . . . . . 10
β’ ((π β§ β
β dom πΊ) β (((π΄ βo (πΊββ
)) Β·o (πΉβ(πΊββ
))) +o (π»ββ
)) = ((π΄ βo (πΊββ
))
Β·o (πΉβ(πΊββ
)))) |
127 | 120, 126 | eqtrd 2773 |
. . . . . . . . 9
β’ ((π β§ β
β dom πΊ) β (π»βsuc β
) = ((π΄ βo (πΊββ
)) Β·o (πΉβ(πΊββ
)))) |
128 | | oesuc 8477 |
. . . . . . . . . 10
β’ ((π΄ β On β§ (πΊββ
) β On)
β (π΄
βo suc (πΊββ
)) = ((π΄ βo (πΊββ
)) Β·o π΄)) |
129 | 104, 108,
128 | syl2anc 585 |
. . . . . . . . 9
β’ ((π β§ β
β dom πΊ) β (π΄ βo suc (πΊββ
)) = ((π΄ βo (πΊββ
)) Β·o π΄)) |
130 | 116, 127,
129 | 3eltr4d 2849 |
. . . . . . . 8
β’ ((π β§ β
β dom πΊ) β (π»βsuc β
) β (π΄ βo suc (πΊββ
))) |
131 | 130 | ex 414 |
. . . . . . 7
β’ (π β (β
β dom πΊ β (π»βsuc β
) β (π΄ βo suc (πΊββ
)))) |
132 | | ordtr 6335 |
. . . . . . . . . . . 12
β’ (Ord dom
πΊ β Tr dom πΊ) |
133 | 24, 132 | ax-mp 5 |
. . . . . . . . . . 11
β’ Tr dom
πΊ |
134 | | trsuc 6408 |
. . . . . . . . . . 11
β’ ((Tr dom
πΊ β§ suc π¦ β dom πΊ) β π¦ β dom πΊ) |
135 | 133, 134 | mpan 689 |
. . . . . . . . . 10
β’ (suc
π¦ β dom πΊ β π¦ β dom πΊ) |
136 | 135 | imim1i 63 |
. . . . . . . . 9
β’ ((π¦ β dom πΊ β (π»βsuc π¦) β (π΄ βo suc (πΊβπ¦))) β (suc π¦ β dom πΊ β (π»βsuc π¦) β (π΄ βo suc (πΊβπ¦)))) |
137 | 1 | ad2antrr 725 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π¦ β Ο) β§ (suc π¦ β dom πΊ β§ (π»βsuc π¦) β (π΄ βo suc (πΊβπ¦)))) β π΄ β On) |
138 | | eloni 6331 |
. . . . . . . . . . . . . . . 16
β’ (π΄ β On β Ord π΄) |
139 | 137, 138 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π¦ β Ο) β§ (suc π¦ β dom πΊ β§ (π»βsuc π¦) β (π΄ βo suc (πΊβπ¦)))) β Ord π΄) |
140 | 48 | ad2antrr 725 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π¦ β Ο) β§ (suc π¦ β dom πΊ β§ (π»βsuc π¦) β (π΄ βo suc (πΊβπ¦)))) β πΉ:π΅βΆπ΄) |
141 | 49 | ad2antrr 725 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π¦ β Ο) β§ (suc π¦ β dom πΊ β§ (π»βsuc π¦) β (π΄ βo suc (πΊβπ¦)))) β (πΉ supp β
) β π΅) |
142 | 20 | ffvelcdmi 7038 |
. . . . . . . . . . . . . . . . . 18
β’ (suc
π¦ β dom πΊ β (πΊβsuc π¦) β (πΉ supp β
)) |
143 | 142 | ad2antrl 727 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π¦ β Ο) β§ (suc π¦ β dom πΊ β§ (π»βsuc π¦) β (π΄ βo suc (πΊβπ¦)))) β (πΊβsuc π¦) β (πΉ supp β
)) |
144 | 141, 143 | sseldd 3949 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π¦ β Ο) β§ (suc π¦ β dom πΊ β§ (π»βsuc π¦) β (π΄ βo suc (πΊβπ¦)))) β (πΊβsuc π¦) β π΅) |
145 | 140, 144 | ffvelcdmd 7040 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π¦ β Ο) β§ (suc π¦ β dom πΊ β§ (π»βsuc π¦) β (π΄ βo suc (πΊβπ¦)))) β (πΉβ(πΊβsuc π¦)) β π΄) |
146 | | ordsucss 7757 |
. . . . . . . . . . . . . . 15
β’ (Ord
π΄ β ((πΉβ(πΊβsuc π¦)) β π΄ β suc (πΉβ(πΊβsuc π¦)) β π΄)) |
147 | 139, 145,
146 | sylc 65 |
. . . . . . . . . . . . . 14
β’ (((π β§ π¦ β Ο) β§ (suc π¦ β dom πΊ β§ (π»βsuc π¦) β (π΄ βo suc (πΊβπ¦)))) β suc (πΉβ(πΊβsuc π¦)) β π΄) |
148 | | onelon 6346 |
. . . . . . . . . . . . . . . . 17
β’ ((π΄ β On β§ (πΉβ(πΊβsuc π¦)) β π΄) β (πΉβ(πΊβsuc π¦)) β On) |
149 | 137, 145,
148 | syl2anc 585 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π¦ β Ο) β§ (suc π¦ β dom πΊ β§ (π»βsuc π¦) β (π΄ βo suc (πΊβπ¦)))) β (πΉβ(πΊβsuc π¦)) β On) |
150 | | onsuc 7750 |
. . . . . . . . . . . . . . . 16
β’ ((πΉβ(πΊβsuc π¦)) β On β suc (πΉβ(πΊβsuc π¦)) β On) |
151 | 149, 150 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π¦ β Ο) β§ (suc π¦ β dom πΊ β§ (π»βsuc π¦) β (π΄ βo suc (πΊβπ¦)))) β suc (πΉβ(πΊβsuc π¦)) β On) |
152 | 52 | ad2antrr 725 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π¦ β Ο) β§ (suc π¦ β dom πΊ β§ (π»βsuc π¦) β (π΄ βo suc (πΊβπ¦)))) β (πΉ supp β
) β On) |
153 | 152, 143 | sseldd 3949 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π¦ β Ο) β§ (suc π¦ β dom πΊ β§ (π»βsuc π¦) β (π΄ βo suc (πΊβπ¦)))) β (πΊβsuc π¦) β On) |
154 | | oecl 8487 |
. . . . . . . . . . . . . . . 16
β’ ((π΄ β On β§ (πΊβsuc π¦) β On) β (π΄ βo (πΊβsuc π¦)) β On) |
155 | 137, 153,
154 | syl2anc 585 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π¦ β Ο) β§ (suc π¦ β dom πΊ β§ (π»βsuc π¦) β (π΄ βo suc (πΊβπ¦)))) β (π΄ βo (πΊβsuc π¦)) β On) |
156 | | omwordi 8522 |
. . . . . . . . . . . . . . 15
β’ ((suc
(πΉβ(πΊβsuc π¦)) β On β§ π΄ β On β§ (π΄ βo (πΊβsuc π¦)) β On) β (suc (πΉβ(πΊβsuc π¦)) β π΄ β ((π΄ βo (πΊβsuc π¦)) Β·o suc (πΉβ(πΊβsuc π¦))) β ((π΄ βo (πΊβsuc π¦)) Β·o π΄))) |
157 | 151, 137,
155, 156 | syl3anc 1372 |
. . . . . . . . . . . . . 14
β’ (((π β§ π¦ β Ο) β§ (suc π¦ β dom πΊ β§ (π»βsuc π¦) β (π΄ βo suc (πΊβπ¦)))) β (suc (πΉβ(πΊβsuc π¦)) β π΄ β ((π΄ βo (πΊβsuc π¦)) Β·o suc (πΉβ(πΊβsuc π¦))) β ((π΄ βo (πΊβsuc π¦)) Β·o π΄))) |
158 | 147, 157 | mpd 15 |
. . . . . . . . . . . . 13
β’ (((π β§ π¦ β Ο) β§ (suc π¦ β dom πΊ β§ (π»βsuc π¦) β (π΄ βo suc (πΊβπ¦)))) β ((π΄ βo (πΊβsuc π¦)) Β·o suc (πΉβ(πΊβsuc π¦))) β ((π΄ βo (πΊβsuc π¦)) Β·o π΄)) |
159 | | oesuc 8477 |
. . . . . . . . . . . . . 14
β’ ((π΄ β On β§ (πΊβsuc π¦) β On) β (π΄ βo suc (πΊβsuc π¦)) = ((π΄ βo (πΊβsuc π¦)) Β·o π΄)) |
160 | 137, 153,
159 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ (((π β§ π¦ β Ο) β§ (suc π¦ β dom πΊ β§ (π»βsuc π¦) β (π΄ βo suc (πΊβπ¦)))) β (π΄ βo suc (πΊβsuc π¦)) = ((π΄ βo (πΊβsuc π¦)) Β·o π΄)) |
161 | 158, 160 | sseqtrrd 3989 |
. . . . . . . . . . . 12
β’ (((π β§ π¦ β Ο) β§ (suc π¦ β dom πΊ β§ (π»βsuc π¦) β (π΄ βo suc (πΊβπ¦)))) β ((π΄ βo (πΊβsuc π¦)) Β·o suc (πΉβ(πΊβsuc π¦))) β (π΄ βo suc (πΊβsuc π¦))) |
162 | | eloni 6331 |
. . . . . . . . . . . . . . . . . 18
β’ ((πΊβsuc π¦) β On β Ord (πΊβsuc π¦)) |
163 | 153, 162 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π¦ β Ο) β§ (suc π¦ β dom πΊ β§ (π»βsuc π¦) β (π΄ βo suc (πΊβπ¦)))) β Ord (πΊβsuc π¦)) |
164 | | vex 3451 |
. . . . . . . . . . . . . . . . . . . . 21
β’ π¦ β V |
165 | 164 | sucid 6403 |
. . . . . . . . . . . . . . . . . . . 20
β’ π¦ β suc π¦ |
166 | 164 | sucex 7745 |
. . . . . . . . . . . . . . . . . . . . 21
β’ suc π¦ β V |
167 | 166 | epeli 5543 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π¦ E suc π¦ β π¦ β suc π¦) |
168 | 165, 167 | mpbir 230 |
. . . . . . . . . . . . . . . . . . 19
β’ π¦ E suc π¦ |
169 | | ovexd 7396 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β (πΉ supp β
) β V) |
170 | 44, 1, 45, 19, 43 | cantnfcl 9611 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β ( E We (πΉ supp β
) β§ dom πΊ β Ο)) |
171 | 170 | simpld 496 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β E We (πΉ supp β
)) |
172 | 19 | oiiso 9481 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((πΉ supp β
) β V β§ E
We (πΉ supp β
)) β
πΊ Isom E , E (dom πΊ, (πΉ supp β
))) |
173 | 169, 171,
172 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β πΊ Isom E , E (dom πΊ, (πΉ supp β
))) |
174 | 173 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π¦ β Ο) β§ (suc π¦ β dom πΊ β§ (π»βsuc π¦) β (π΄ βo suc (πΊβπ¦)))) β πΊ Isom E , E (dom πΊ, (πΉ supp β
))) |
175 | 135 | ad2antrl 727 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π¦ β Ο) β§ (suc π¦ β dom πΊ β§ (π»βsuc π¦) β (π΄ βo suc (πΊβπ¦)))) β π¦ β dom πΊ) |
176 | | simprl 770 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π¦ β Ο) β§ (suc π¦ β dom πΊ β§ (π»βsuc π¦) β (π΄ βo suc (πΊβπ¦)))) β suc π¦ β dom πΊ) |
177 | | isorel 7275 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((πΊ Isom E , E (dom πΊ, (πΉ supp β
)) β§ (π¦ β dom πΊ β§ suc π¦ β dom πΊ)) β (π¦ E suc π¦ β (πΊβπ¦) E (πΊβsuc π¦))) |
178 | 174, 175,
176, 177 | syl12anc 836 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π¦ β Ο) β§ (suc π¦ β dom πΊ β§ (π»βsuc π¦) β (π΄ βo suc (πΊβπ¦)))) β (π¦ E suc π¦ β (πΊβπ¦) E (πΊβsuc π¦))) |
179 | 168, 178 | mpbii 232 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π¦ β Ο) β§ (suc π¦ β dom πΊ β§ (π»βsuc π¦) β (π΄ βo suc (πΊβπ¦)))) β (πΊβπ¦) E (πΊβsuc π¦)) |
180 | | fvex 6859 |
. . . . . . . . . . . . . . . . . . 19
β’ (πΊβsuc π¦) β V |
181 | 180 | epeli 5543 |
. . . . . . . . . . . . . . . . . 18
β’ ((πΊβπ¦) E (πΊβsuc π¦) β (πΊβπ¦) β (πΊβsuc π¦)) |
182 | 179, 181 | sylib 217 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π¦ β Ο) β§ (suc π¦ β dom πΊ β§ (π»βsuc π¦) β (π΄ βo suc (πΊβπ¦)))) β (πΊβπ¦) β (πΊβsuc π¦)) |
183 | | ordsucss 7757 |
. . . . . . . . . . . . . . . . 17
β’ (Ord
(πΊβsuc π¦) β ((πΊβπ¦) β (πΊβsuc π¦) β suc (πΊβπ¦) β (πΊβsuc π¦))) |
184 | 163, 182,
183 | sylc 65 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π¦ β Ο) β§ (suc π¦ β dom πΊ β§ (π»βsuc π¦) β (π΄ βo suc (πΊβπ¦)))) β suc (πΊβπ¦) β (πΊβsuc π¦)) |
185 | 20 | ffvelcdmi 7038 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π¦ β dom πΊ β (πΊβπ¦) β (πΉ supp β
)) |
186 | 175, 185 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π¦ β Ο) β§ (suc π¦ β dom πΊ β§ (π»βsuc π¦) β (π΄ βo suc (πΊβπ¦)))) β (πΊβπ¦) β (πΉ supp β
)) |
187 | 152, 186 | sseldd 3949 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π¦ β Ο) β§ (suc π¦ β dom πΊ β§ (π»βsuc π¦) β (π΄ βo suc (πΊβπ¦)))) β (πΊβπ¦) β On) |
188 | | onsuc 7750 |
. . . . . . . . . . . . . . . . . 18
β’ ((πΊβπ¦) β On β suc (πΊβπ¦) β On) |
189 | 187, 188 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π¦ β Ο) β§ (suc π¦ β dom πΊ β§ (π»βsuc π¦) β (π΄ βo suc (πΊβπ¦)))) β suc (πΊβπ¦) β On) |
190 | 3 | ad2antrr 725 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π¦ β Ο) β§ (suc π¦ β dom πΊ β§ (π»βsuc π¦) β (π΄ βo suc (πΊβπ¦)))) β β
β π΄) |
191 | | oewordi 8542 |
. . . . . . . . . . . . . . . . 17
β’ (((suc
(πΊβπ¦) β On β§ (πΊβsuc π¦) β On β§ π΄ β On) β§ β
β π΄) β (suc (πΊβπ¦) β (πΊβsuc π¦) β (π΄ βo suc (πΊβπ¦)) β (π΄ βo (πΊβsuc π¦)))) |
192 | 189, 153,
137, 190, 191 | syl31anc 1374 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π¦ β Ο) β§ (suc π¦ β dom πΊ β§ (π»βsuc π¦) β (π΄ βo suc (πΊβπ¦)))) β (suc (πΊβπ¦) β (πΊβsuc π¦) β (π΄ βo suc (πΊβπ¦)) β (π΄ βo (πΊβsuc π¦)))) |
193 | 184, 192 | mpd 15 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π¦ β Ο) β§ (suc π¦ β dom πΊ β§ (π»βsuc π¦) β (π΄ βo suc (πΊβπ¦)))) β (π΄ βo suc (πΊβπ¦)) β (π΄ βo (πΊβsuc π¦))) |
194 | | simprr 772 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π¦ β Ο) β§ (suc π¦ β dom πΊ β§ (π»βsuc π¦) β (π΄ βo suc (πΊβπ¦)))) β (π»βsuc π¦) β (π΄ βo suc (πΊβπ¦))) |
195 | 193, 194 | sseldd 3949 |
. . . . . . . . . . . . . 14
β’ (((π β§ π¦ β Ο) β§ (suc π¦ β dom πΊ β§ (π»βsuc π¦) β (π΄ βo suc (πΊβπ¦)))) β (π»βsuc π¦) β (π΄ βo (πΊβsuc π¦))) |
196 | | peano2 7831 |
. . . . . . . . . . . . . . . . 17
β’ (π¦ β Ο β suc π¦ β
Ο) |
197 | 196 | ad2antlr 726 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π¦ β Ο) β§ (suc π¦ β dom πΊ β§ (π»βsuc π¦) β (π΄ βo suc (πΊβπ¦)))) β suc π¦ β Ο) |
198 | 8 | cantnfvalf 9609 |
. . . . . . . . . . . . . . . . 17
β’ π»:ΟβΆOn |
199 | 198 | ffvelcdmi 7038 |
. . . . . . . . . . . . . . . 16
β’ (suc
π¦ β Ο β
(π»βsuc π¦) β On) |
200 | 197, 199 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π¦ β Ο) β§ (suc π¦ β dom πΊ β§ (π»βsuc π¦) β (π΄ βo suc (πΊβπ¦)))) β (π»βsuc π¦) β On) |
201 | | omcl 8486 |
. . . . . . . . . . . . . . . 16
β’ (((π΄ βo (πΊβsuc π¦)) β On β§ (πΉβ(πΊβsuc π¦)) β On) β ((π΄ βo (πΊβsuc π¦)) Β·o (πΉβ(πΊβsuc π¦))) β On) |
202 | 155, 149,
201 | syl2anc 585 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π¦ β Ο) β§ (suc π¦ β dom πΊ β§ (π»βsuc π¦) β (π΄ βo suc (πΊβπ¦)))) β ((π΄ βo (πΊβsuc π¦)) Β·o (πΉβ(πΊβsuc π¦))) β On) |
203 | | oaord 8498 |
. . . . . . . . . . . . . . 15
β’ (((π»βsuc π¦) β On β§ (π΄ βo (πΊβsuc π¦)) β On β§ ((π΄ βo (πΊβsuc π¦)) Β·o (πΉβ(πΊβsuc π¦))) β On) β ((π»βsuc π¦) β (π΄ βo (πΊβsuc π¦)) β (((π΄ βo (πΊβsuc π¦)) Β·o (πΉβ(πΊβsuc π¦))) +o (π»βsuc π¦)) β (((π΄ βo (πΊβsuc π¦)) Β·o (πΉβ(πΊβsuc π¦))) +o (π΄ βo (πΊβsuc π¦))))) |
204 | 200, 155,
202, 203 | syl3anc 1372 |
. . . . . . . . . . . . . 14
β’ (((π β§ π¦ β Ο) β§ (suc π¦ β dom πΊ β§ (π»βsuc π¦) β (π΄ βo suc (πΊβπ¦)))) β ((π»βsuc π¦) β (π΄ βo (πΊβsuc π¦)) β (((π΄ βo (πΊβsuc π¦)) Β·o (πΉβ(πΊβsuc π¦))) +o (π»βsuc π¦)) β (((π΄ βo (πΊβsuc π¦)) Β·o (πΉβ(πΊβsuc π¦))) +o (π΄ βo (πΊβsuc π¦))))) |
205 | 195, 204 | mpbid 231 |
. . . . . . . . . . . . 13
β’ (((π β§ π¦ β Ο) β§ (suc π¦ β dom πΊ β§ (π»βsuc π¦) β (π΄ βo suc (πΊβπ¦)))) β (((π΄ βo (πΊβsuc π¦)) Β·o (πΉβ(πΊβsuc π¦))) +o (π»βsuc π¦)) β (((π΄ βo (πΊβsuc π¦)) Β·o (πΉβ(πΊβsuc π¦))) +o (π΄ βo (πΊβsuc π¦)))) |
206 | 44, 1, 45, 19, 43, 8 | cantnfsuc 9614 |
. . . . . . . . . . . . . . 15
β’ ((π β§ suc π¦ β Ο) β (π»βsuc suc π¦) = (((π΄ βo (πΊβsuc π¦)) Β·o (πΉβ(πΊβsuc π¦))) +o (π»βsuc π¦))) |
207 | 196, 206 | sylan2 594 |
. . . . . . . . . . . . . 14
β’ ((π β§ π¦ β Ο) β (π»βsuc suc π¦) = (((π΄ βo (πΊβsuc π¦)) Β·o (πΉβ(πΊβsuc π¦))) +o (π»βsuc π¦))) |
208 | 207 | adantr 482 |
. . . . . . . . . . . . 13
β’ (((π β§ π¦ β Ο) β§ (suc π¦ β dom πΊ β§ (π»βsuc π¦) β (π΄ βo suc (πΊβπ¦)))) β (π»βsuc suc π¦) = (((π΄ βo (πΊβsuc π¦)) Β·o (πΉβ(πΊβsuc π¦))) +o (π»βsuc π¦))) |
209 | | omsuc 8476 |
. . . . . . . . . . . . . 14
β’ (((π΄ βo (πΊβsuc π¦)) β On β§ (πΉβ(πΊβsuc π¦)) β On) β ((π΄ βo (πΊβsuc π¦)) Β·o suc (πΉβ(πΊβsuc π¦))) = (((π΄ βo (πΊβsuc π¦)) Β·o (πΉβ(πΊβsuc π¦))) +o (π΄ βo (πΊβsuc π¦)))) |
210 | 155, 149,
209 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ (((π β§ π¦ β Ο) β§ (suc π¦ β dom πΊ β§ (π»βsuc π¦) β (π΄ βo suc (πΊβπ¦)))) β ((π΄ βo (πΊβsuc π¦)) Β·o suc (πΉβ(πΊβsuc π¦))) = (((π΄ βo (πΊβsuc π¦)) Β·o (πΉβ(πΊβsuc π¦))) +o (π΄ βo (πΊβsuc π¦)))) |
211 | 205, 208,
210 | 3eltr4d 2849 |
. . . . . . . . . . . 12
β’ (((π β§ π¦ β Ο) β§ (suc π¦ β dom πΊ β§ (π»βsuc π¦) β (π΄ βo suc (πΊβπ¦)))) β (π»βsuc suc π¦) β ((π΄ βo (πΊβsuc π¦)) Β·o suc (πΉβ(πΊβsuc π¦)))) |
212 | 161, 211 | sseldd 3949 |
. . . . . . . . . . 11
β’ (((π β§ π¦ β Ο) β§ (suc π¦ β dom πΊ β§ (π»βsuc π¦) β (π΄ βo suc (πΊβπ¦)))) β (π»βsuc suc π¦) β (π΄ βo suc (πΊβsuc π¦))) |
213 | 212 | exp32 422 |
. . . . . . . . . 10
β’ ((π β§ π¦ β Ο) β (suc π¦ β dom πΊ β ((π»βsuc π¦) β (π΄ βo suc (πΊβπ¦)) β (π»βsuc suc π¦) β (π΄ βo suc (πΊβsuc π¦))))) |
214 | 213 | a2d 29 |
. . . . . . . . 9
β’ ((π β§ π¦ β Ο) β ((suc π¦ β dom πΊ β (π»βsuc π¦) β (π΄ βo suc (πΊβπ¦))) β (suc π¦ β dom πΊ β (π»βsuc suc π¦) β (π΄ βo suc (πΊβsuc π¦))))) |
215 | 136, 214 | syl5 34 |
. . . . . . . 8
β’ ((π β§ π¦ β Ο) β ((π¦ β dom πΊ β (π»βsuc π¦) β (π΄ βo suc (πΊβπ¦))) β (suc π¦ β dom πΊ β (π»βsuc suc π¦) β (π΄ βo suc (πΊβsuc π¦))))) |
216 | 215 | expcom 415 |
. . . . . . 7
β’ (π¦ β Ο β (π β ((π¦ β dom πΊ β (π»βsuc π¦) β (π΄ βo suc (πΊβπ¦))) β (suc π¦ β dom πΊ β (π»βsuc suc π¦) β (π΄ βo suc (πΊβsuc π¦)))))) |
217 | 80, 89, 98, 131, 216 | finds2 7841 |
. . . . . 6
β’ (π₯ β Ο β (π β (π₯ β dom πΊ β (π»βsuc π₯) β (π΄ βo suc (πΊβπ₯))))) |
218 | 70, 71, 58, 217 | syl3c 66 |
. . . . 5
β’ ((π β§ (π₯ β Ο β§ πΎ = suc π₯)) β (π»βsuc π₯) β (π΄ βo suc (πΊβπ₯))) |
219 | 69, 218 | eqeltrd 2834 |
. . . 4
β’ ((π β§ (π₯ β Ο β§ πΎ = suc π₯)) β (π»βπΎ) β (π΄ βo suc (πΊβπ₯))) |
220 | 68, 219 | sseldd 3949 |
. . 3
β’ ((π β§ (π₯ β Ο β§ πΎ = suc π₯)) β (π»βπΎ) β (π΄ βo πΆ)) |
221 | 220 | rexlimdvaa 3150 |
. 2
β’ (π β (βπ₯ β Ο πΎ = suc π₯ β (π»βπΎ) β (π΄ βo πΆ))) |
222 | | peano2 7831 |
. . . . 5
β’ (dom
πΊ β Ο β suc
dom πΊ β
Ο) |
223 | 170, 222 | simpl2im 505 |
. . . 4
β’ (π β suc dom πΊ β Ο) |
224 | | elnn 7817 |
. . . 4
β’ ((πΎ β suc dom πΊ β§ suc dom πΊ β Ο) β πΎ β Ο) |
225 | 23, 223, 224 | syl2anc 585 |
. . 3
β’ (π β πΎ β Ο) |
226 | | nn0suc 7836 |
. . 3
β’ (πΎ β Ο β (πΎ = β
β¨ βπ₯ β Ο πΎ = suc π₯)) |
227 | 225, 226 | syl 17 |
. 2
β’ (π β (πΎ = β
β¨ βπ₯ β Ο πΎ = suc π₯)) |
228 | 13, 221, 227 | mpjaod 859 |
1
β’ (π β (π»βπΎ) β (π΄ βo πΆ)) |