Step | Hyp | Ref
| Expression |
1 | | brdomi 8951 |
. 2
β’ (Ο
βΌ π΄ β
βπ π:Οβ1-1βπ΄) |
2 | | peano1 7873 |
. . . . . 6
β’ β
β Ο |
3 | | f1f1orn 6835 |
. . . . . . . . 9
β’ (π:Οβ1-1βπ΄ β π:Οβ1-1-ontoβran
π) |
4 | 3 | adantr 480 |
. . . . . . . 8
β’ ((π:Οβ1-1βπ΄ β§ π΄ = β
) β π:Οβ1-1-ontoβran
π) |
5 | | f1f 6778 |
. . . . . . . . . . 11
β’ (π:Οβ1-1βπ΄ β π:ΟβΆπ΄) |
6 | 5 | frnd 6716 |
. . . . . . . . . 10
β’ (π:Οβ1-1βπ΄ β ran π β π΄) |
7 | | sseq0 4392 |
. . . . . . . . . 10
β’ ((ran
π β π΄ β§ π΄ = β
) β ran π = β
) |
8 | 6, 7 | sylan 579 |
. . . . . . . . 9
β’ ((π:Οβ1-1βπ΄ β§ π΄ = β
) β ran π = β
) |
9 | 8 | f1oeq3d 6821 |
. . . . . . . 8
β’ ((π:Οβ1-1βπ΄ β§ π΄ = β
) β (π:Οβ1-1-ontoβran
π β π:Οβ1-1-ontoββ
)) |
10 | 4, 9 | mpbid 231 |
. . . . . . 7
β’ ((π:Οβ1-1βπ΄ β§ π΄ = β
) β π:Οβ1-1-ontoββ
) |
11 | | f1ocnv 6836 |
. . . . . . 7
β’ (π:Οβ1-1-ontoββ
β β‘π:β
β1-1-ontoβΟ) |
12 | | noel 4323 |
. . . . . . . 8
β’ Β¬
β
β β
|
13 | | f1o00 6859 |
. . . . . . . . . 10
β’ (β‘π:β
β1-1-ontoβΟ β (β‘π = β
β§ Ο =
β
)) |
14 | 13 | simprbi 496 |
. . . . . . . . 9
β’ (β‘π:β
β1-1-ontoβΟ β Ο =
β
) |
15 | 14 | eleq2d 2811 |
. . . . . . . 8
β’ (β‘π:β
β1-1-ontoβΟ β (β
β Ο β
β
β β
)) |
16 | 12, 15 | mtbiri 327 |
. . . . . . 7
β’ (β‘π:β
β1-1-ontoβΟ β Β¬ β
β
Ο) |
17 | 10, 11, 16 | 3syl 18 |
. . . . . 6
β’ ((π:Οβ1-1βπ΄ β§ π΄ = β
) β Β¬ β
β
Ο) |
18 | 2, 17 | mt2 199 |
. . . . 5
β’ Β¬
(π:Οβ1-1βπ΄ β§ π΄ = β
) |
19 | 18 | imnani 400 |
. . . 4
β’ (π:Οβ1-1βπ΄ β Β¬ π΄ = β
) |
20 | 19 | neqned 2939 |
. . 3
β’ (π:Οβ1-1βπ΄ β π΄ β β
) |
21 | 20 | exlimiv 1925 |
. 2
β’
(βπ π:Οβ1-1βπ΄ β π΄ β β
) |
22 | 1, 21 | syl 17 |
1
β’ (Ο
βΌ π΄ β π΄ β β
) |