Step | Hyp | Ref
| Expression |
1 | | isf32lem.a |
. . . 4
β’ (π β πΉ:ΟβΆπ« πΊ) |
2 | | isf32lem.b |
. . . 4
β’ (π β βπ₯ β Ο (πΉβsuc π₯) β (πΉβπ₯)) |
3 | | isf32lem.c |
. . . 4
β’ (π β Β¬ β© ran πΉ β ran πΉ) |
4 | 1, 2, 3 | isf32lem2 10295 |
. . 3
β’ ((π β§ π β Ο) β βπ β Ο (π β π β§ (πΉβsuc π) β (πΉβπ))) |
5 | 4 | ralrimiva 3140 |
. 2
β’ (π β βπ β Ο βπ β Ο (π β π β§ (πΉβsuc π) β (πΉβπ))) |
6 | | isf32lem.d |
. . . . . . . 8
β’ π = {π¦ β Ο β£ (πΉβsuc π¦) β (πΉβπ¦)} |
7 | 6 | ssrab3 4041 |
. . . . . . 7
β’ π β
Ο |
8 | | nnunifi 9241 |
. . . . . . 7
β’ ((π β Ο β§ π β Fin) β βͺ π
β Ο) |
9 | 7, 8 | mpan 689 |
. . . . . 6
β’ (π β Fin β βͺ π
β Ο) |
10 | 9 | adantl 483 |
. . . . 5
β’ ((π β§ π β Fin) β βͺ π
β Ο) |
11 | | elssuni 4899 |
. . . . . . . . . . . . 13
β’ (π β π β π β βͺ π) |
12 | | nnon 7809 |
. . . . . . . . . . . . . 14
β’ (π β Ο β π β On) |
13 | | omsson 7807 |
. . . . . . . . . . . . . . 15
β’ Ο
β On |
14 | 13, 10 | sselid 3943 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β Fin) β βͺ π
β On) |
15 | | ontri1 6352 |
. . . . . . . . . . . . . 14
β’ ((π β On β§ βͺ π
β On) β (π
β βͺ π β Β¬ βͺ
π β π)) |
16 | 12, 14, 15 | syl2anr 598 |
. . . . . . . . . . . . 13
β’ (((π β§ π β Fin) β§ π β Ο) β (π β βͺ π β Β¬ βͺ π
β π)) |
17 | 11, 16 | imbitrid 243 |
. . . . . . . . . . . 12
β’ (((π β§ π β Fin) β§ π β Ο) β (π β π β Β¬ βͺ
π β π)) |
18 | 17 | con2d 134 |
. . . . . . . . . . 11
β’ (((π β§ π β Fin) β§ π β Ο) β (βͺ π
β π β Β¬ π β π)) |
19 | 18 | impr 456 |
. . . . . . . . . 10
β’ (((π β§ π β Fin) β§ (π β Ο β§ βͺ π
β π)) β Β¬
π β π) |
20 | 6 | eleq2i 2826 |
. . . . . . . . . 10
β’ (π β π β π β {π¦ β Ο β£ (πΉβsuc π¦) β (πΉβπ¦)}) |
21 | 19, 20 | sylnib 328 |
. . . . . . . . 9
β’ (((π β§ π β Fin) β§ (π β Ο β§ βͺ π
β π)) β Β¬
π β {π¦ β Ο β£ (πΉβsuc π¦) β (πΉβπ¦)}) |
22 | | suceq 6384 |
. . . . . . . . . . . . 13
β’ (π¦ = π β suc π¦ = suc π) |
23 | 22 | fveq2d 6847 |
. . . . . . . . . . . 12
β’ (π¦ = π β (πΉβsuc π¦) = (πΉβsuc π)) |
24 | | fveq2 6843 |
. . . . . . . . . . . 12
β’ (π¦ = π β (πΉβπ¦) = (πΉβπ)) |
25 | 23, 24 | psseq12d 4055 |
. . . . . . . . . . 11
β’ (π¦ = π β ((πΉβsuc π¦) β (πΉβπ¦) β (πΉβsuc π) β (πΉβπ))) |
26 | 25 | elrab3 3647 |
. . . . . . . . . 10
β’ (π β Ο β (π β {π¦ β Ο β£ (πΉβsuc π¦) β (πΉβπ¦)} β (πΉβsuc π) β (πΉβπ))) |
27 | 26 | ad2antrl 727 |
. . . . . . . . 9
β’ (((π β§ π β Fin) β§ (π β Ο β§ βͺ π
β π)) β (π β {π¦ β Ο β£ (πΉβsuc π¦) β (πΉβπ¦)} β (πΉβsuc π) β (πΉβπ))) |
28 | 21, 27 | mtbid 324 |
. . . . . . . 8
β’ (((π β§ π β Fin) β§ (π β Ο β§ βͺ π
β π)) β Β¬
(πΉβsuc π) β (πΉβπ)) |
29 | 28 | expr 458 |
. . . . . . 7
β’ (((π β§ π β Fin) β§ π β Ο) β (βͺ π
β π β Β¬
(πΉβsuc π) β (πΉβπ))) |
30 | | imnan 401 |
. . . . . . 7
β’ ((βͺ π
β π β Β¬
(πΉβsuc π) β (πΉβπ)) β Β¬ (βͺ
π β π β§ (πΉβsuc π) β (πΉβπ))) |
31 | 29, 30 | sylib 217 |
. . . . . 6
β’ (((π β§ π β Fin) β§ π β Ο) β Β¬ (βͺ π
β π β§ (πΉβsuc π) β (πΉβπ))) |
32 | 31 | nrexdv 3143 |
. . . . 5
β’ ((π β§ π β Fin) β Β¬ βπ β Ο (βͺ π
β π β§ (πΉβsuc π) β (πΉβπ))) |
33 | | eleq1 2822 |
. . . . . . . . 9
β’ (π = βͺ
π β (π β π β βͺ π β π)) |
34 | 33 | anbi1d 631 |
. . . . . . . 8
β’ (π = βͺ
π β ((π β π β§ (πΉβsuc π) β (πΉβπ)) β (βͺ π β π β§ (πΉβsuc π) β (πΉβπ)))) |
35 | 34 | rexbidv 3172 |
. . . . . . 7
β’ (π = βͺ
π β (βπ β Ο (π β π β§ (πΉβsuc π) β (πΉβπ)) β βπ β Ο (βͺ
π β π β§ (πΉβsuc π) β (πΉβπ)))) |
36 | 35 | notbid 318 |
. . . . . 6
β’ (π = βͺ
π β (Β¬
βπ β Ο
(π β π β§ (πΉβsuc π) β (πΉβπ)) β Β¬ βπ β Ο (βͺ
π β π β§ (πΉβsuc π) β (πΉβπ)))) |
37 | 36 | rspcev 3580 |
. . . . 5
β’ ((βͺ π
β Ο β§ Β¬ βπ β Ο (βͺ
π β π β§ (πΉβsuc π) β (πΉβπ))) β βπ β Ο Β¬ βπ β Ο (π β π β§ (πΉβsuc π) β (πΉβπ))) |
38 | 10, 32, 37 | syl2anc 585 |
. . . 4
β’ ((π β§ π β Fin) β βπ β Ο Β¬
βπ β Ο
(π β π β§ (πΉβsuc π) β (πΉβπ))) |
39 | | rexnal 3100 |
. . . 4
β’
(βπ β
Ο Β¬ βπ
β Ο (π β
π β§ (πΉβsuc π) β (πΉβπ)) β Β¬ βπ β Ο βπ β Ο (π β π β§ (πΉβsuc π) β (πΉβπ))) |
40 | 38, 39 | sylib 217 |
. . 3
β’ ((π β§ π β Fin) β Β¬ βπ β Ο βπ β Ο (π β π β§ (πΉβsuc π) β (πΉβπ))) |
41 | 40 | ex 414 |
. 2
β’ (π β (π β Fin β Β¬ βπ β Ο βπ β Ο (π β π β§ (πΉβsuc π) β (πΉβπ)))) |
42 | 5, 41 | mt2d 136 |
1
β’ (π β Β¬ π β Fin) |