Step | Hyp | Ref
| Expression |
1 | | brdomi 8950 |
. 2
β’ (Ο
βΌ π΄ β
βπ π:Οβ1-1βπ΄) |
2 | | peano1 7875 |
. . . . . 6
β’ β
β Ο |
3 | | f1f1orn 6841 |
. . . . . . . . 9
β’ (π:Οβ1-1βπ΄ β π:Οβ1-1-ontoβran
π) |
4 | 3 | adantr 481 |
. . . . . . . 8
β’ ((π:Οβ1-1βπ΄ β§ π΄ = β
) β π:Οβ1-1-ontoβran
π) |
5 | | f1f 6784 |
. . . . . . . . . . 11
β’ (π:Οβ1-1βπ΄ β π:ΟβΆπ΄) |
6 | 5 | frnd 6722 |
. . . . . . . . . 10
β’ (π:Οβ1-1βπ΄ β ran π β π΄) |
7 | | sseq0 4398 |
. . . . . . . . . 10
β’ ((ran
π β π΄ β§ π΄ = β
) β ran π = β
) |
8 | 6, 7 | sylan 580 |
. . . . . . . . 9
β’ ((π:Οβ1-1βπ΄ β§ π΄ = β
) β ran π = β
) |
9 | 8 | f1oeq3d 6827 |
. . . . . . . 8
β’ ((π:Οβ1-1βπ΄ β§ π΄ = β
) β (π:Οβ1-1-ontoβran
π β π:Οβ1-1-ontoββ
)) |
10 | 4, 9 | mpbid 231 |
. . . . . . 7
β’ ((π:Οβ1-1βπ΄ β§ π΄ = β
) β π:Οβ1-1-ontoββ
) |
11 | | f1ocnv 6842 |
. . . . . . 7
β’ (π:Οβ1-1-ontoββ
β β‘π:β
β1-1-ontoβΟ) |
12 | | noel 4329 |
. . . . . . . 8
β’ Β¬
β
β β
|
13 | | f1o00 6865 |
. . . . . . . . . 10
β’ (β‘π:β
β1-1-ontoβΟ β (β‘π = β
β§ Ο =
β
)) |
14 | 13 | simprbi 497 |
. . . . . . . . 9
β’ (β‘π:β
β1-1-ontoβΟ β Ο =
β
) |
15 | 14 | eleq2d 2819 |
. . . . . . . 8
β’ (β‘π:β
β1-1-ontoβΟ β (β
β Ο β
β
β β
)) |
16 | 12, 15 | mtbiri 326 |
. . . . . . 7
β’ (β‘π:β
β1-1-ontoβΟ β Β¬ β
β
Ο) |
17 | 10, 11, 16 | 3syl 18 |
. . . . . 6
β’ ((π:Οβ1-1βπ΄ β§ π΄ = β
) β Β¬ β
β
Ο) |
18 | 2, 17 | mt2 199 |
. . . . 5
β’ Β¬
(π:Οβ1-1βπ΄ β§ π΄ = β
) |
19 | 18 | imnani 401 |
. . . 4
β’ (π:Οβ1-1βπ΄ β Β¬ π΄ = β
) |
20 | 19 | neqned 2947 |
. . 3
β’ (π:Οβ1-1βπ΄ β π΄ β β
) |
21 | 20 | exlimiv 1933 |
. 2
β’
(βπ π:Οβ1-1βπ΄ β π΄ β β
) |
22 | 1, 21 | syl 17 |
1
β’ (Ο
βΌ π΄ β π΄ β β
) |