Step | Hyp | Ref
| Expression |
1 | | peano1 7829 |
. . . . . 6
β’ β
β Ο |
2 | | ne0i 4298 |
. . . . . 6
β’ (β
β Ο β Ο β β
) |
3 | | brwdomn0 9513 |
. . . . . 6
β’ (Ο
β β
β (Ο βΌ* π΄ β βπ π:π΄βontoβΟ)) |
4 | 1, 2, 3 | mp2b 10 |
. . . . 5
β’ (Ο
βΌ* π΄
β βπ π:π΄βontoβΟ) |
5 | | vex 3451 |
. . . . . . . . . 10
β’ π β V |
6 | | fof 6760 |
. . . . . . . . . 10
β’ (π:π΄βontoβΟ β π:π΄βΆΟ) |
7 | | dmfex 7848 |
. . . . . . . . . 10
β’ ((π β V β§ π:π΄βΆΟ) β π΄ β V) |
8 | 5, 6, 7 | sylancr 588 |
. . . . . . . . 9
β’ (π:π΄βontoβΟ β π΄ β V) |
9 | | cnvimass 6037 |
. . . . . . . . . 10
β’ (β‘π β ran πΈ) β dom π |
10 | 9, 6 | fssdm 6692 |
. . . . . . . . 9
β’ (π:π΄βontoβΟ β (β‘π β ran πΈ) β π΄) |
11 | 8, 10 | sselpwd 5287 |
. . . . . . . 8
β’ (π:π΄βontoβΟ β (β‘π β ran πΈ) β π« π΄) |
12 | | fin1a2lem.b |
. . . . . . . . . . . . . 14
β’ πΈ = (π₯ β Ο β¦ (2o
Β·o π₯)) |
13 | 12 | fin1a2lem4 10347 |
. . . . . . . . . . . . 13
β’ πΈ:Οβ1-1βΟ |
14 | | f1cnv 6812 |
. . . . . . . . . . . . 13
β’ (πΈ:Οβ1-1βΟ β β‘πΈ:ran πΈβ1-1-ontoβΟ) |
15 | | f1ofo 6795 |
. . . . . . . . . . . . 13
β’ (β‘πΈ:ran πΈβ1-1-ontoβΟ β β‘πΈ:ran πΈβontoβΟ) |
16 | 13, 14, 15 | mp2b 10 |
. . . . . . . . . . . 12
β’ β‘πΈ:ran πΈβontoβΟ |
17 | | fofun 6761 |
. . . . . . . . . . . 12
β’ (β‘πΈ:ran πΈβontoβΟ β Fun β‘πΈ) |
18 | 16, 17 | ax-mp 5 |
. . . . . . . . . . 11
β’ Fun β‘πΈ |
19 | 5 | resex 5989 |
. . . . . . . . . . 11
β’ (π βΎ (β‘π β ran πΈ)) β V |
20 | | cofunexg 7885 |
. . . . . . . . . . 11
β’ ((Fun
β‘πΈ β§ (π βΎ (β‘π β ran πΈ)) β V) β (β‘πΈ β (π βΎ (β‘π β ran πΈ))) β V) |
21 | 18, 19, 20 | mp2an 691 |
. . . . . . . . . 10
β’ (β‘πΈ β (π βΎ (β‘π β ran πΈ))) β V |
22 | | fofun 6761 |
. . . . . . . . . . . . 13
β’ (π:π΄βontoβΟ β Fun π) |
23 | | fores 6770 |
. . . . . . . . . . . . 13
β’ ((Fun
π β§ (β‘π β ran πΈ) β dom π) β (π βΎ (β‘π β ran πΈ)):(β‘π β ran πΈ)βontoβ(π β (β‘π β ran πΈ))) |
24 | 22, 9, 23 | sylancl 587 |
. . . . . . . . . . . 12
β’ (π:π΄βontoβΟ β (π βΎ (β‘π β ran πΈ)):(β‘π β ran πΈ)βontoβ(π β (β‘π β ran πΈ))) |
25 | | f1f 6742 |
. . . . . . . . . . . . . . 15
β’ (πΈ:Οβ1-1βΟ β πΈ:ΟβΆΟ) |
26 | | frn 6679 |
. . . . . . . . . . . . . . 15
β’ (πΈ:ΟβΆΟ β
ran πΈ β
Ο) |
27 | 13, 25, 26 | mp2b 10 |
. . . . . . . . . . . . . 14
β’ ran πΈ β
Ο |
28 | | foimacnv 6805 |
. . . . . . . . . . . . . 14
β’ ((π:π΄βontoβΟ β§ ran πΈ β Ο) β (π β (β‘π β ran πΈ)) = ran πΈ) |
29 | 27, 28 | mpan2 690 |
. . . . . . . . . . . . 13
β’ (π:π΄βontoβΟ β (π β (β‘π β ran πΈ)) = ran πΈ) |
30 | | foeq3 6758 |
. . . . . . . . . . . . 13
β’ ((π β (β‘π β ran πΈ)) = ran πΈ β ((π βΎ (β‘π β ran πΈ)):(β‘π β ran πΈ)βontoβ(π β (β‘π β ran πΈ)) β (π βΎ (β‘π β ran πΈ)):(β‘π β ran πΈ)βontoβran πΈ)) |
31 | 29, 30 | syl 17 |
. . . . . . . . . . . 12
β’ (π:π΄βontoβΟ β ((π βΎ (β‘π β ran πΈ)):(β‘π β ran πΈ)βontoβ(π β (β‘π β ran πΈ)) β (π βΎ (β‘π β ran πΈ)):(β‘π β ran πΈ)βontoβran πΈ)) |
32 | 24, 31 | mpbid 231 |
. . . . . . . . . . 11
β’ (π:π΄βontoβΟ β (π βΎ (β‘π β ran πΈ)):(β‘π β ran πΈ)βontoβran πΈ) |
33 | | foco 6774 |
. . . . . . . . . . 11
β’ ((β‘πΈ:ran πΈβontoβΟ β§ (π βΎ (β‘π β ran πΈ)):(β‘π β ran πΈ)βontoβran πΈ) β (β‘πΈ β (π βΎ (β‘π β ran πΈ))):(β‘π β ran πΈ)βontoβΟ) |
34 | 16, 32, 33 | sylancr 588 |
. . . . . . . . . 10
β’ (π:π΄βontoβΟ β (β‘πΈ β (π βΎ (β‘π β ran πΈ))):(β‘π β ran πΈ)βontoβΟ) |
35 | | fowdom 9515 |
. . . . . . . . . 10
β’ (((β‘πΈ β (π βΎ (β‘π β ran πΈ))) β V β§ (β‘πΈ β (π βΎ (β‘π β ran πΈ))):(β‘π β ran πΈ)βontoβΟ) β Ο βΌ*
(β‘π β ran πΈ)) |
36 | 21, 34, 35 | sylancr 588 |
. . . . . . . . 9
β’ (π:π΄βontoβΟ β Ο βΌ*
(β‘π β ran πΈ)) |
37 | 5 | cnvex 7866 |
. . . . . . . . . . . 12
β’ β‘π β V |
38 | 37 | imaex 7857 |
. . . . . . . . . . 11
β’ (β‘π β ran πΈ) β V |
39 | | isfin3-2 10311 |
. . . . . . . . . . 11
β’ ((β‘π β ran πΈ) β V β ((β‘π β ran πΈ) β FinIII β Β¬
Ο βΌ* (β‘π β ran πΈ))) |
40 | 38, 39 | ax-mp 5 |
. . . . . . . . . 10
β’ ((β‘π β ran πΈ) β FinIII β Β¬
Ο βΌ* (β‘π β ran πΈ)) |
41 | 40 | con2bii 358 |
. . . . . . . . 9
β’ (Ο
βΌ* (β‘π β ran πΈ) β Β¬ (β‘π β ran πΈ) β FinIII) |
42 | 36, 41 | sylib 217 |
. . . . . . . 8
β’ (π:π΄βontoβΟ β Β¬ (β‘π β ran πΈ) β FinIII) |
43 | | fin1a2lem.aa |
. . . . . . . . . . . . . . 15
β’ π = (π₯ β On β¦ suc π₯) |
44 | 12, 43 | fin1a2lem6 10349 |
. . . . . . . . . . . . . 14
β’ (π βΎ ran πΈ):ran πΈβ1-1-ontoβ(Ο β ran πΈ) |
45 | | f1ocnv 6800 |
. . . . . . . . . . . . . 14
β’ ((π βΎ ran πΈ):ran πΈβ1-1-ontoβ(Ο β ran πΈ) β β‘(π βΎ ran πΈ):(Ο β ran πΈ)β1-1-ontoβran
πΈ) |
46 | | f1ofo 6795 |
. . . . . . . . . . . . . 14
β’ (β‘(π βΎ ran πΈ):(Ο β ran πΈ)β1-1-ontoβran
πΈ β β‘(π βΎ ran πΈ):(Ο β ran πΈ)βontoβran πΈ) |
47 | 44, 45, 46 | mp2b 10 |
. . . . . . . . . . . . 13
β’ β‘(π βΎ ran πΈ):(Ο β ran πΈ)βontoβran πΈ |
48 | | foco 6774 |
. . . . . . . . . . . . 13
β’ ((β‘πΈ:ran πΈβontoβΟ β§ β‘(π βΎ ran πΈ):(Ο β ran πΈ)βontoβran πΈ) β (β‘πΈ β β‘(π βΎ ran πΈ)):(Ο β ran πΈ)βontoβΟ) |
49 | 16, 47, 48 | mp2an 691 |
. . . . . . . . . . . 12
β’ (β‘πΈ β β‘(π βΎ ran πΈ)):(Ο β ran πΈ)βontoβΟ |
50 | | fofun 6761 |
. . . . . . . . . . . 12
β’ ((β‘πΈ β β‘(π βΎ ran πΈ)):(Ο β ran πΈ)βontoβΟ β Fun (β‘πΈ β β‘(π βΎ ran πΈ))) |
51 | 49, 50 | ax-mp 5 |
. . . . . . . . . . 11
β’ Fun
(β‘πΈ β β‘(π βΎ ran πΈ)) |
52 | 5 | resex 5989 |
. . . . . . . . . . 11
β’ (π βΎ (π΄ β (β‘π β ran πΈ))) β V |
53 | | cofunexg 7885 |
. . . . . . . . . . 11
β’ ((Fun
(β‘πΈ β β‘(π βΎ ran πΈ)) β§ (π βΎ (π΄ β (β‘π β ran πΈ))) β V) β ((β‘πΈ β β‘(π βΎ ran πΈ)) β (π βΎ (π΄ β (β‘π β ran πΈ)))) β V) |
54 | 51, 52, 53 | mp2an 691 |
. . . . . . . . . 10
β’ ((β‘πΈ β β‘(π βΎ ran πΈ)) β (π βΎ (π΄ β (β‘π β ran πΈ)))) β V |
55 | | difss 4095 |
. . . . . . . . . . . . . 14
β’ (π΄ β (β‘π β ran πΈ)) β π΄ |
56 | 6 | fdmd 6683 |
. . . . . . . . . . . . . 14
β’ (π:π΄βontoβΟ β dom π = π΄) |
57 | 55, 56 | sseqtrrid 4001 |
. . . . . . . . . . . . 13
β’ (π:π΄βontoβΟ β (π΄ β (β‘π β ran πΈ)) β dom π) |
58 | | fores 6770 |
. . . . . . . . . . . . 13
β’ ((Fun
π β§ (π΄ β (β‘π β ran πΈ)) β dom π) β (π βΎ (π΄ β (β‘π β ran πΈ))):(π΄ β (β‘π β ran πΈ))βontoβ(π β (π΄ β (β‘π β ran πΈ)))) |
59 | 22, 57, 58 | syl2anc 585 |
. . . . . . . . . . . 12
β’ (π:π΄βontoβΟ β (π βΎ (π΄ β (β‘π β ran πΈ))):(π΄ β (β‘π β ran πΈ))βontoβ(π β (π΄ β (β‘π β ran πΈ)))) |
60 | | funcnvcnv 6572 |
. . . . . . . . . . . . . . . 16
β’ (Fun
π β Fun β‘β‘π) |
61 | | imadif 6589 |
. . . . . . . . . . . . . . . 16
β’ (Fun
β‘β‘π β (β‘π β (Ο β ran πΈ)) = ((β‘π β Ο) β (β‘π β ran πΈ))) |
62 | 22, 60, 61 | 3syl 18 |
. . . . . . . . . . . . . . 15
β’ (π:π΄βontoβΟ β (β‘π β (Ο β ran πΈ)) = ((β‘π β Ο) β (β‘π β ran πΈ))) |
63 | 62 | imaeq2d 6017 |
. . . . . . . . . . . . . 14
β’ (π:π΄βontoβΟ β (π β (β‘π β (Ο β ran πΈ))) = (π β ((β‘π β Ο) β (β‘π β ran πΈ)))) |
64 | | difss 4095 |
. . . . . . . . . . . . . . 15
β’ (Ο
β ran πΈ) β
Ο |
65 | | foimacnv 6805 |
. . . . . . . . . . . . . . 15
β’ ((π:π΄βontoβΟ β§ (Ο β ran πΈ) β Ο) β (π β (β‘π β (Ο β ran πΈ))) = (Ο β ran πΈ)) |
66 | 64, 65 | mpan2 690 |
. . . . . . . . . . . . . 14
β’ (π:π΄βontoβΟ β (π β (β‘π β (Ο β ran πΈ))) = (Ο β ran πΈ)) |
67 | | fimacnv 6694 |
. . . . . . . . . . . . . . . . 17
β’ (π:π΄βΆΟ β (β‘π β Ο) = π΄) |
68 | 6, 67 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ (π:π΄βontoβΟ β (β‘π β Ο) = π΄) |
69 | 68 | difeq1d 4085 |
. . . . . . . . . . . . . . 15
β’ (π:π΄βontoβΟ β ((β‘π β Ο) β (β‘π β ran πΈ)) = (π΄ β (β‘π β ran πΈ))) |
70 | 69 | imaeq2d 6017 |
. . . . . . . . . . . . . 14
β’ (π:π΄βontoβΟ β (π β ((β‘π β Ο) β (β‘π β ran πΈ))) = (π β (π΄ β (β‘π β ran πΈ)))) |
71 | 63, 66, 70 | 3eqtr3rd 2782 |
. . . . . . . . . . . . 13
β’ (π:π΄βontoβΟ β (π β (π΄ β (β‘π β ran πΈ))) = (Ο β ran πΈ)) |
72 | | foeq3 6758 |
. . . . . . . . . . . . 13
β’ ((π β (π΄ β (β‘π β ran πΈ))) = (Ο β ran πΈ) β ((π βΎ (π΄ β (β‘π β ran πΈ))):(π΄ β (β‘π β ran πΈ))βontoβ(π β (π΄ β (β‘π β ran πΈ))) β (π βΎ (π΄ β (β‘π β ran πΈ))):(π΄ β (β‘π β ran πΈ))βontoβ(Ο β ran πΈ))) |
73 | 71, 72 | syl 17 |
. . . . . . . . . . . 12
β’ (π:π΄βontoβΟ β ((π βΎ (π΄ β (β‘π β ran πΈ))):(π΄ β (β‘π β ran πΈ))βontoβ(π β (π΄ β (β‘π β ran πΈ))) β (π βΎ (π΄ β (β‘π β ran πΈ))):(π΄ β (β‘π β ran πΈ))βontoβ(Ο β ran πΈ))) |
74 | 59, 73 | mpbid 231 |
. . . . . . . . . . 11
β’ (π:π΄βontoβΟ β (π βΎ (π΄ β (β‘π β ran πΈ))):(π΄ β (β‘π β ran πΈ))βontoβ(Ο β ran πΈ)) |
75 | | foco 6774 |
. . . . . . . . . . 11
β’ (((β‘πΈ β β‘(π βΎ ran πΈ)):(Ο β ran πΈ)βontoβΟ β§ (π βΎ (π΄ β (β‘π β ran πΈ))):(π΄ β (β‘π β ran πΈ))βontoβ(Ο β ran πΈ)) β ((β‘πΈ β β‘(π βΎ ran πΈ)) β (π βΎ (π΄ β (β‘π β ran πΈ)))):(π΄ β (β‘π β ran πΈ))βontoβΟ) |
76 | 49, 74, 75 | sylancr 588 |
. . . . . . . . . 10
β’ (π:π΄βontoβΟ β ((β‘πΈ β β‘(π βΎ ran πΈ)) β (π βΎ (π΄ β (β‘π β ran πΈ)))):(π΄ β (β‘π β ran πΈ))βontoβΟ) |
77 | | fowdom 9515 |
. . . . . . . . . 10
β’ ((((β‘πΈ β β‘(π βΎ ran πΈ)) β (π βΎ (π΄ β (β‘π β ran πΈ)))) β V β§ ((β‘πΈ β β‘(π βΎ ran πΈ)) β (π βΎ (π΄ β (β‘π β ran πΈ)))):(π΄ β (β‘π β ran πΈ))βontoβΟ) β Ο βΌ*
(π΄ β (β‘π β ran πΈ))) |
78 | 54, 76, 77 | sylancr 588 |
. . . . . . . . 9
β’ (π:π΄βontoβΟ β Ο βΌ*
(π΄ β (β‘π β ran πΈ))) |
79 | | difexg 5288 |
. . . . . . . . . . 11
β’ (π΄ β V β (π΄ β (β‘π β ran πΈ)) β V) |
80 | | isfin3-2 10311 |
. . . . . . . . . . 11
β’ ((π΄ β (β‘π β ran πΈ)) β V β ((π΄ β (β‘π β ran πΈ)) β FinIII β Β¬
Ο βΌ* (π΄ β (β‘π β ran πΈ)))) |
81 | 8, 79, 80 | 3syl 18 |
. . . . . . . . . 10
β’ (π:π΄βontoβΟ β ((π΄ β (β‘π β ran πΈ)) β FinIII β Β¬
Ο βΌ* (π΄ β (β‘π β ran πΈ)))) |
82 | 81 | con2bid 355 |
. . . . . . . . 9
β’ (π:π΄βontoβΟ β (Ο βΌ*
(π΄ β (β‘π β ran πΈ)) β Β¬ (π΄ β (β‘π β ran πΈ)) β
FinIII)) |
83 | 78, 82 | mpbid 231 |
. . . . . . . 8
β’ (π:π΄βontoβΟ β Β¬ (π΄ β (β‘π β ran πΈ)) β
FinIII) |
84 | | eleq1 2822 |
. . . . . . . . . . . 12
β’ (π¦ = (β‘π β ran πΈ) β (π¦ β FinIII β (β‘π β ran πΈ) β
FinIII)) |
85 | | difeq2 4080 |
. . . . . . . . . . . . 13
β’ (π¦ = (β‘π β ran πΈ) β (π΄ β π¦) = (π΄ β (β‘π β ran πΈ))) |
86 | 85 | eleq1d 2819 |
. . . . . . . . . . . 12
β’ (π¦ = (β‘π β ran πΈ) β ((π΄ β π¦) β FinIII β (π΄ β (β‘π β ran πΈ)) β
FinIII)) |
87 | 84, 86 | orbi12d 918 |
. . . . . . . . . . 11
β’ (π¦ = (β‘π β ran πΈ) β ((π¦ β FinIII β¨ (π΄ β π¦) β FinIII) β ((β‘π β ran πΈ) β FinIII β¨ (π΄ β (β‘π β ran πΈ)) β
FinIII))) |
88 | 87 | notbid 318 |
. . . . . . . . . 10
β’ (π¦ = (β‘π β ran πΈ) β (Β¬ (π¦ β FinIII β¨ (π΄ β π¦) β FinIII) β Β¬
((β‘π β ran πΈ) β FinIII β¨ (π΄ β (β‘π β ran πΈ)) β
FinIII))) |
89 | | ioran 983 |
. . . . . . . . . 10
β’ (Β¬
((β‘π β ran πΈ) β FinIII β¨ (π΄ β (β‘π β ran πΈ)) β FinIII) β (Β¬
(β‘π β ran πΈ) β FinIII β§ Β¬
(π΄ β (β‘π β ran πΈ)) β
FinIII)) |
90 | 88, 89 | bitrdi 287 |
. . . . . . . . 9
β’ (π¦ = (β‘π β ran πΈ) β (Β¬ (π¦ β FinIII β¨ (π΄ β π¦) β FinIII) β (Β¬
(β‘π β ran πΈ) β FinIII β§ Β¬
(π΄ β (β‘π β ran πΈ)) β
FinIII))) |
91 | 90 | rspcev 3583 |
. . . . . . . 8
β’ (((β‘π β ran πΈ) β π« π΄ β§ (Β¬ (β‘π β ran πΈ) β FinIII β§ Β¬
(π΄ β (β‘π β ran πΈ)) β FinIII)) β
βπ¦ β π«
π΄ Β¬ (π¦ β FinIII β¨ (π΄ β π¦) β FinIII)) |
92 | 11, 42, 83, 91 | syl12anc 836 |
. . . . . . 7
β’ (π:π΄βontoβΟ β βπ¦ β π« π΄ Β¬ (π¦ β FinIII β¨ (π΄ β π¦) β FinIII)) |
93 | | rexnal 3100 |
. . . . . . 7
β’
(βπ¦ β
π« π΄ Β¬ (π¦ β FinIII β¨
(π΄ β π¦) β FinIII)
β Β¬ βπ¦
β π« π΄(π¦ β FinIII β¨
(π΄ β π¦) β
FinIII)) |
94 | 92, 93 | sylib 217 |
. . . . . 6
β’ (π:π΄βontoβΟ β Β¬ βπ¦ β π« π΄(π¦ β FinIII β¨ (π΄ β π¦) β FinIII)) |
95 | 94 | exlimiv 1934 |
. . . . 5
β’
(βπ π:π΄βontoβΟ β Β¬ βπ¦ β π« π΄(π¦ β FinIII β¨ (π΄ β π¦) β FinIII)) |
96 | 4, 95 | sylbi 216 |
. . . 4
β’ (Ο
βΌ* π΄
β Β¬ βπ¦
β π« π΄(π¦ β FinIII β¨
(π΄ β π¦) β
FinIII)) |
97 | 96 | con2i 139 |
. . 3
β’
(βπ¦ β
π« π΄(π¦ β FinIII β¨
(π΄ β π¦) β FinIII)
β Β¬ Ο βΌ* π΄) |
98 | | isfin3-2 10311 |
. . 3
β’ (π΄ β π β (π΄ β FinIII β Β¬
Ο βΌ* π΄)) |
99 | 97, 98 | imbitrrid 245 |
. 2
β’ (π΄ β π β (βπ¦ β π« π΄(π¦ β FinIII β¨ (π΄ β π¦) β FinIII) β π΄ β
FinIII)) |
100 | 99 | imp 408 |
1
β’ ((π΄ β π β§ βπ¦ β π« π΄(π¦ β FinIII β¨ (π΄ β π¦) β FinIII)) β π΄ β
FinIII) |