Step | Hyp | Ref
| Expression |
1 | | fin1a2lem.aa |
. . . 4
β’ π = (π₯ β On β¦ suc π₯) |
2 | 1 | fin1a2lem2 10345 |
. . 3
β’ π:Onβ1-1βOn |
3 | | fin1a2lem.b |
. . . . 5
β’ πΈ = (π₯ β Ο β¦ (2o
Β·o π₯)) |
4 | 3 | fin1a2lem4 10347 |
. . . 4
β’ πΈ:Οβ1-1βΟ |
5 | | f1f 6742 |
. . . 4
β’ (πΈ:Οβ1-1βΟ β πΈ:ΟβΆΟ) |
6 | | frn 6679 |
. . . . 5
β’ (πΈ:ΟβΆΟ β
ran πΈ β
Ο) |
7 | | omsson 7810 |
. . . . 5
β’ Ο
β On |
8 | 6, 7 | sstrdi 3960 |
. . . 4
β’ (πΈ:ΟβΆΟ β
ran πΈ β
On) |
9 | 4, 5, 8 | mp2b 10 |
. . 3
β’ ran πΈ β On |
10 | | f1ores 6802 |
. . 3
β’ ((π:Onβ1-1βOn β§ ran πΈ β On) β (π βΎ ran πΈ):ran πΈβ1-1-ontoβ(π β ran πΈ)) |
11 | 2, 9, 10 | mp2an 691 |
. 2
β’ (π βΎ ran πΈ):ran πΈβ1-1-ontoβ(π β ran πΈ) |
12 | 9 | sseli 3944 |
. . . . . . . . 9
β’ (π β ran πΈ β π β On) |
13 | 1 | fin1a2lem1 10344 |
. . . . . . . . 9
β’ (π β On β (πβπ) = suc π) |
14 | 12, 13 | syl 17 |
. . . . . . . 8
β’ (π β ran πΈ β (πβπ) = suc π) |
15 | 14 | eqeq1d 2735 |
. . . . . . 7
β’ (π β ran πΈ β ((πβπ) = π β suc π = π)) |
16 | 15 | rexbiia 3092 |
. . . . . 6
β’
(βπ β ran
πΈ(πβπ) = π β βπ β ran πΈ suc π = π) |
17 | 4, 5, 6 | mp2b 10 |
. . . . . . . . . . . 12
β’ ran πΈ β
Ο |
18 | 17 | sseli 3944 |
. . . . . . . . . . 11
β’ (π β ran πΈ β π β Ο) |
19 | | peano2 7831 |
. . . . . . . . . . 11
β’ (π β Ο β suc π β
Ο) |
20 | 18, 19 | syl 17 |
. . . . . . . . . 10
β’ (π β ran πΈ β suc π β Ο) |
21 | 3 | fin1a2lem5 10348 |
. . . . . . . . . . . 12
β’ (π β Ο β (π β ran πΈ β Β¬ suc π β ran πΈ)) |
22 | 21 | biimpd 228 |
. . . . . . . . . . 11
β’ (π β Ο β (π β ran πΈ β Β¬ suc π β ran πΈ)) |
23 | 18, 22 | mpcom 38 |
. . . . . . . . . 10
β’ (π β ran πΈ β Β¬ suc π β ran πΈ) |
24 | 20, 23 | jca 513 |
. . . . . . . . 9
β’ (π β ran πΈ β (suc π β Ο β§ Β¬ suc π β ran πΈ)) |
25 | | eleq1 2822 |
. . . . . . . . . 10
β’ (suc
π = π β (suc π β Ο β π β Ο)) |
26 | | eleq1 2822 |
. . . . . . . . . . 11
β’ (suc
π = π β (suc π β ran πΈ β π β ran πΈ)) |
27 | 26 | notbid 318 |
. . . . . . . . . 10
β’ (suc
π = π β (Β¬ suc π β ran πΈ β Β¬ π β ran πΈ)) |
28 | 25, 27 | anbi12d 632 |
. . . . . . . . 9
β’ (suc
π = π β ((suc π β Ο β§ Β¬ suc π β ran πΈ) β (π β Ο β§ Β¬ π β ran πΈ))) |
29 | 24, 28 | syl5ibcom 244 |
. . . . . . . 8
β’ (π β ran πΈ β (suc π = π β (π β Ο β§ Β¬ π β ran πΈ))) |
30 | 29 | rexlimiv 3142 |
. . . . . . 7
β’
(βπ β ran
πΈ suc π = π β (π β Ο β§ Β¬ π β ran πΈ)) |
31 | | peano1 7829 |
. . . . . . . . . . . . . 14
β’ β
β Ο |
32 | 3 | fin1a2lem3 10346 |
. . . . . . . . . . . . . 14
β’ (β
β Ο β (πΈββ
) = (2o
Β·o β
)) |
33 | 31, 32 | ax-mp 5 |
. . . . . . . . . . . . 13
β’ (πΈββ
) = (2o
Β·o β
) |
34 | | 2on 8430 |
. . . . . . . . . . . . . 14
β’
2o β On |
35 | | om0 8467 |
. . . . . . . . . . . . . 14
β’
(2o β On β (2o Β·o
β
) = β
) |
36 | 34, 35 | ax-mp 5 |
. . . . . . . . . . . . 13
β’
(2o Β·o β
) = β
|
37 | 33, 36 | eqtri 2761 |
. . . . . . . . . . . 12
β’ (πΈββ
) =
β
|
38 | | f1fun 6744 |
. . . . . . . . . . . . . 14
β’ (πΈ:Οβ1-1βΟ β Fun πΈ) |
39 | 4, 38 | ax-mp 5 |
. . . . . . . . . . . . 13
β’ Fun πΈ |
40 | | f1dm 6746 |
. . . . . . . . . . . . . . 15
β’ (πΈ:Οβ1-1βΟ β dom πΈ = Ο) |
41 | 4, 40 | ax-mp 5 |
. . . . . . . . . . . . . 14
β’ dom πΈ = Ο |
42 | 31, 41 | eleqtrri 2833 |
. . . . . . . . . . . . 13
β’ β
β dom πΈ |
43 | | fvelrn 7031 |
. . . . . . . . . . . . 13
β’ ((Fun
πΈ β§ β
β dom
πΈ) β (πΈββ
) β ran πΈ) |
44 | 39, 42, 43 | mp2an 691 |
. . . . . . . . . . . 12
β’ (πΈββ
) β ran πΈ |
45 | 37, 44 | eqeltrri 2831 |
. . . . . . . . . . 11
β’ β
β ran πΈ |
46 | | eleq1 2822 |
. . . . . . . . . . 11
β’ (π = β
β (π β ran πΈ β β
β ran πΈ)) |
47 | 45, 46 | mpbiri 258 |
. . . . . . . . . 10
β’ (π = β
β π β ran πΈ) |
48 | 47 | necon3bi 2967 |
. . . . . . . . 9
β’ (Β¬
π β ran πΈ β π β β
) |
49 | | nnsuc 7824 |
. . . . . . . . 9
β’ ((π β Ο β§ π β β
) β
βπ β Ο
π = suc π) |
50 | 48, 49 | sylan2 594 |
. . . . . . . 8
β’ ((π β Ο β§ Β¬
π β ran πΈ) β βπ β Ο π = suc π) |
51 | | eleq1 2822 |
. . . . . . . . . . . . 13
β’ (π = suc π β (π β Ο β suc π β Ο)) |
52 | | eleq1 2822 |
. . . . . . . . . . . . . 14
β’ (π = suc π β (π β ran πΈ β suc π β ran πΈ)) |
53 | 52 | notbid 318 |
. . . . . . . . . . . . 13
β’ (π = suc π β (Β¬ π β ran πΈ β Β¬ suc π β ran πΈ)) |
54 | 51, 53 | anbi12d 632 |
. . . . . . . . . . . 12
β’ (π = suc π β ((π β Ο β§ Β¬ π β ran πΈ) β (suc π β Ο β§ Β¬ suc π β ran πΈ))) |
55 | 54 | anbi1d 631 |
. . . . . . . . . . 11
β’ (π = suc π β (((π β Ο β§ Β¬ π β ran πΈ) β§ π β Ο) β ((suc π β Ο β§ Β¬ suc
π β ran πΈ) β§ π β Ο))) |
56 | | simplr 768 |
. . . . . . . . . . . 12
β’ (((suc
π β Ο β§
Β¬ suc π β ran
πΈ) β§ π β Ο) β Β¬ suc π β ran πΈ) |
57 | 21 | adantl 483 |
. . . . . . . . . . . 12
β’ (((suc
π β Ο β§
Β¬ suc π β ran
πΈ) β§ π β Ο) β (π β ran πΈ β Β¬ suc π β ran πΈ)) |
58 | 56, 57 | mpbird 257 |
. . . . . . . . . . 11
β’ (((suc
π β Ο β§
Β¬ suc π β ran
πΈ) β§ π β Ο) β π β ran πΈ) |
59 | 55, 58 | syl6bi 253 |
. . . . . . . . . 10
β’ (π = suc π β (((π β Ο β§ Β¬ π β ran πΈ) β§ π β Ο) β π β ran πΈ)) |
60 | 59 | com12 32 |
. . . . . . . . 9
β’ (((π β Ο β§ Β¬
π β ran πΈ) β§ π β Ο) β (π = suc π β π β ran πΈ)) |
61 | 60 | impr 456 |
. . . . . . . 8
β’ (((π β Ο β§ Β¬
π β ran πΈ) β§ (π β Ο β§ π = suc π)) β π β ran πΈ) |
62 | | simprr 772 |
. . . . . . . . 9
β’ (((π β Ο β§ Β¬
π β ran πΈ) β§ (π β Ο β§ π = suc π)) β π = suc π) |
63 | 62 | eqcomd 2739 |
. . . . . . . 8
β’ (((π β Ο β§ Β¬
π β ran πΈ) β§ (π β Ο β§ π = suc π)) β suc π = π) |
64 | 50, 61, 63 | reximssdv 3166 |
. . . . . . 7
β’ ((π β Ο β§ Β¬
π β ran πΈ) β βπ β ran πΈ suc π = π) |
65 | 30, 64 | impbii 208 |
. . . . . 6
β’
(βπ β ran
πΈ suc π = π β (π β Ο β§ Β¬ π β ran πΈ)) |
66 | 16, 65 | bitri 275 |
. . . . 5
β’
(βπ β ran
πΈ(πβπ) = π β (π β Ο β§ Β¬ π β ran πΈ)) |
67 | | f1fn 6743 |
. . . . . . 7
β’ (π:Onβ1-1βOn β π Fn On) |
68 | 2, 67 | ax-mp 5 |
. . . . . 6
β’ π Fn On |
69 | | fvelimab 6918 |
. . . . . 6
β’ ((π Fn On β§ ran πΈ β On) β (π β (π β ran πΈ) β βπ β ran πΈ(πβπ) = π)) |
70 | 68, 9, 69 | mp2an 691 |
. . . . 5
β’ (π β (π β ran πΈ) β βπ β ran πΈ(πβπ) = π) |
71 | | eldif 3924 |
. . . . 5
β’ (π β (Ο β ran
πΈ) β (π β Ο β§ Β¬
π β ran πΈ)) |
72 | 66, 70, 71 | 3bitr4i 303 |
. . . 4
β’ (π β (π β ran πΈ) β π β (Ο β ran πΈ)) |
73 | 72 | eqriv 2730 |
. . 3
β’ (π β ran πΈ) = (Ο β ran πΈ) |
74 | | f1oeq3 6778 |
. . 3
β’ ((π β ran πΈ) = (Ο β ran πΈ) β ((π βΎ ran πΈ):ran πΈβ1-1-ontoβ(π β ran πΈ) β (π βΎ ran πΈ):ran πΈβ1-1-ontoβ(Ο β ran πΈ))) |
75 | 73, 74 | ax-mp 5 |
. 2
β’ ((π βΎ ran πΈ):ran πΈβ1-1-ontoβ(π β ran πΈ) β (π βΎ ran πΈ):ran πΈβ1-1-ontoβ(Ο β ran πΈ)) |
76 | 11, 75 | mpbi 229 |
1
β’ (π βΎ ran πΈ):ran πΈβ1-1-ontoβ(Ο β ran πΈ) |