Step | Hyp | Ref
| Expression |
1 | | epweon 7714 |
. . . . 5
β’ E We
On |
2 | | fveq2 6847 |
. . . . . . . . . . 11
β’ (π¦ = β
β (πΉβπ¦) = (πΉββ
)) |
3 | 2 | eleq1d 2823 |
. . . . . . . . . 10
β’ (π¦ = β
β ((πΉβπ¦) β On β (πΉββ
) β On)) |
4 | | fveq2 6847 |
. . . . . . . . . . 11
β’ (π¦ = π§ β (πΉβπ¦) = (πΉβπ§)) |
5 | 4 | eleq1d 2823 |
. . . . . . . . . 10
β’ (π¦ = π§ β ((πΉβπ¦) β On β (πΉβπ§) β On)) |
6 | | fveq2 6847 |
. . . . . . . . . . 11
β’ (π¦ = suc π§ β (πΉβπ¦) = (πΉβsuc π§)) |
7 | 6 | eleq1d 2823 |
. . . . . . . . . 10
β’ (π¦ = suc π§ β ((πΉβπ¦) β On β (πΉβsuc π§) β On)) |
8 | | simpl 484 |
. . . . . . . . . 10
β’ (((πΉββ
) β On β§
βπ₯ β Ο
(πΉβsuc π₯) β (πΉβπ₯)) β (πΉββ
) β On) |
9 | | suceq 6388 |
. . . . . . . . . . . . . . 15
β’ (π₯ = π§ β suc π₯ = suc π§) |
10 | 9 | fveq2d 6851 |
. . . . . . . . . . . . . 14
β’ (π₯ = π§ β (πΉβsuc π₯) = (πΉβsuc π§)) |
11 | | fveq2 6847 |
. . . . . . . . . . . . . 14
β’ (π₯ = π§ β (πΉβπ₯) = (πΉβπ§)) |
12 | 10, 11 | eleq12d 2832 |
. . . . . . . . . . . . 13
β’ (π₯ = π§ β ((πΉβsuc π₯) β (πΉβπ₯) β (πΉβsuc π§) β (πΉβπ§))) |
13 | 12 | rspcv 3580 |
. . . . . . . . . . . 12
β’ (π§ β Ο β
(βπ₯ β Ο
(πΉβsuc π₯) β (πΉβπ₯) β (πΉβsuc π§) β (πΉβπ§))) |
14 | | onelon 6347 |
. . . . . . . . . . . . 13
β’ (((πΉβπ§) β On β§ (πΉβsuc π§) β (πΉβπ§)) β (πΉβsuc π§) β On) |
15 | 14 | expcom 415 |
. . . . . . . . . . . 12
β’ ((πΉβsuc π§) β (πΉβπ§) β ((πΉβπ§) β On β (πΉβsuc π§) β On)) |
16 | 13, 15 | syl6 35 |
. . . . . . . . . . 11
β’ (π§ β Ο β
(βπ₯ β Ο
(πΉβsuc π₯) β (πΉβπ₯) β ((πΉβπ§) β On β (πΉβsuc π§) β On))) |
17 | 16 | adantld 492 |
. . . . . . . . . 10
β’ (π§ β Ο β (((πΉββ
) β On β§
βπ₯ β Ο
(πΉβsuc π₯) β (πΉβπ₯)) β ((πΉβπ§) β On β (πΉβsuc π§) β On))) |
18 | 3, 5, 7, 8, 17 | finds2 7842 |
. . . . . . . . 9
β’ (π¦ β Ο β (((πΉββ
) β On β§
βπ₯ β Ο
(πΉβsuc π₯) β (πΉβπ₯)) β (πΉβπ¦) β On)) |
19 | 18 | com12 32 |
. . . . . . . 8
β’ (((πΉββ
) β On β§
βπ₯ β Ο
(πΉβsuc π₯) β (πΉβπ₯)) β (π¦ β Ο β (πΉβπ¦) β On)) |
20 | 19 | ralrimiv 3143 |
. . . . . . 7
β’ (((πΉββ
) β On β§
βπ₯ β Ο
(πΉβsuc π₯) β (πΉβπ₯)) β βπ¦ β Ο (πΉβπ¦) β On) |
21 | | eqid 2737 |
. . . . . . . 8
β’ (π¦ β Ο β¦ (πΉβπ¦)) = (π¦ β Ο β¦ (πΉβπ¦)) |
22 | 21 | fmpt 7063 |
. . . . . . 7
β’
(βπ¦ β
Ο (πΉβπ¦) β On β (π¦ β Ο β¦ (πΉβπ¦)):ΟβΆOn) |
23 | 20, 22 | sylib 217 |
. . . . . 6
β’ (((πΉββ
) β On β§
βπ₯ β Ο
(πΉβsuc π₯) β (πΉβπ₯)) β (π¦ β Ο β¦ (πΉβπ¦)):ΟβΆOn) |
24 | 23 | frnd 6681 |
. . . . 5
β’ (((πΉββ
) β On β§
βπ₯ β Ο
(πΉβsuc π₯) β (πΉβπ₯)) β ran (π¦ β Ο β¦ (πΉβπ¦)) β On) |
25 | | peano1 7830 |
. . . . . . . 8
β’ β
β Ο |
26 | 23 | fdmd 6684 |
. . . . . . . 8
β’ (((πΉββ
) β On β§
βπ₯ β Ο
(πΉβsuc π₯) β (πΉβπ₯)) β dom (π¦ β Ο β¦ (πΉβπ¦)) = Ο) |
27 | 25, 26 | eleqtrrid 2845 |
. . . . . . 7
β’ (((πΉββ
) β On β§
βπ₯ β Ο
(πΉβsuc π₯) β (πΉβπ₯)) β β
β dom (π¦ β Ο β¦ (πΉβπ¦))) |
28 | 27 | ne0d 4300 |
. . . . . 6
β’ (((πΉββ
) β On β§
βπ₯ β Ο
(πΉβsuc π₯) β (πΉβπ₯)) β dom (π¦ β Ο β¦ (πΉβπ¦)) β β
) |
29 | | dm0rn0 5885 |
. . . . . . 7
β’ (dom
(π¦ β Ο β¦
(πΉβπ¦)) = β
β ran (π¦ β Ο β¦ (πΉβπ¦)) = β
) |
30 | 29 | necon3bii 2997 |
. . . . . 6
β’ (dom
(π¦ β Ο β¦
(πΉβπ¦)) β β
β ran (π¦ β Ο β¦ (πΉβπ¦)) β β
) |
31 | 28, 30 | sylib 217 |
. . . . 5
β’ (((πΉββ
) β On β§
βπ₯ β Ο
(πΉβsuc π₯) β (πΉβπ₯)) β ran (π¦ β Ο β¦ (πΉβπ¦)) β β
) |
32 | | wefrc 5632 |
. . . . 5
β’ (( E We
On β§ ran (π¦ β
Ο β¦ (πΉβπ¦)) β On β§ ran (π¦ β Ο β¦ (πΉβπ¦)) β β
) β βπ§ β ran (π¦ β Ο β¦ (πΉβπ¦))(ran (π¦ β Ο β¦ (πΉβπ¦)) β© π§) = β
) |
33 | 1, 24, 31, 32 | mp3an2i 1467 |
. . . 4
β’ (((πΉββ
) β On β§
βπ₯ β Ο
(πΉβsuc π₯) β (πΉβπ₯)) β βπ§ β ran (π¦ β Ο β¦ (πΉβπ¦))(ran (π¦ β Ο β¦ (πΉβπ¦)) β© π§) = β
) |
34 | | fvex 6860 |
. . . . . 6
β’ (πΉβπ€) β V |
35 | 34 | rgenw 3069 |
. . . . 5
β’
βπ€ β
Ο (πΉβπ€) β V |
36 | | fveq2 6847 |
. . . . . . 7
β’ (π¦ = π€ β (πΉβπ¦) = (πΉβπ€)) |
37 | 36 | cbvmptv 5223 |
. . . . . 6
β’ (π¦ β Ο β¦ (πΉβπ¦)) = (π€ β Ο β¦ (πΉβπ€)) |
38 | | ineq2 4171 |
. . . . . . 7
β’ (π§ = (πΉβπ€) β (ran (π¦ β Ο β¦ (πΉβπ¦)) β© π§) = (ran (π¦ β Ο β¦ (πΉβπ¦)) β© (πΉβπ€))) |
39 | 38 | eqeq1d 2739 |
. . . . . 6
β’ (π§ = (πΉβπ€) β ((ran (π¦ β Ο β¦ (πΉβπ¦)) β© π§) = β
β (ran (π¦ β Ο β¦ (πΉβπ¦)) β© (πΉβπ€)) = β
)) |
40 | 37, 39 | rexrnmptw 7050 |
. . . . 5
β’
(βπ€ β
Ο (πΉβπ€) β V β (βπ§ β ran (π¦ β Ο β¦ (πΉβπ¦))(ran (π¦ β Ο β¦ (πΉβπ¦)) β© π§) = β
β βπ€ β Ο (ran (π¦ β Ο β¦ (πΉβπ¦)) β© (πΉβπ€)) = β
)) |
41 | 35, 40 | ax-mp 5 |
. . . 4
β’
(βπ§ β ran
(π¦ β Ο β¦
(πΉβπ¦))(ran (π¦ β Ο β¦ (πΉβπ¦)) β© π§) = β
β βπ€ β Ο (ran (π¦ β Ο β¦ (πΉβπ¦)) β© (πΉβπ€)) = β
) |
42 | 33, 41 | sylib 217 |
. . 3
β’ (((πΉββ
) β On β§
βπ₯ β Ο
(πΉβsuc π₯) β (πΉβπ₯)) β βπ€ β Ο (ran (π¦ β Ο β¦ (πΉβπ¦)) β© (πΉβπ€)) = β
) |
43 | | peano2 7832 |
. . . . . . . . 9
β’ (π€ β Ο β suc π€ β
Ο) |
44 | 43 | adantl 483 |
. . . . . . . 8
β’ ((((πΉββ
) β On β§
βπ₯ β Ο
(πΉβsuc π₯) β (πΉβπ₯)) β§ π€ β Ο) β suc π€ β
Ο) |
45 | | eqid 2737 |
. . . . . . . 8
β’ (πΉβsuc π€) = (πΉβsuc π€) |
46 | | fveq2 6847 |
. . . . . . . . 9
β’ (π¦ = suc π€ β (πΉβπ¦) = (πΉβsuc π€)) |
47 | 46 | rspceeqv 3600 |
. . . . . . . 8
β’ ((suc
π€ β Ο β§
(πΉβsuc π€) = (πΉβsuc π€)) β βπ¦ β Ο (πΉβsuc π€) = (πΉβπ¦)) |
48 | 44, 45, 47 | sylancl 587 |
. . . . . . 7
β’ ((((πΉββ
) β On β§
βπ₯ β Ο
(πΉβsuc π₯) β (πΉβπ₯)) β§ π€ β Ο) β βπ¦ β Ο (πΉβsuc π€) = (πΉβπ¦)) |
49 | | fvex 6860 |
. . . . . . . 8
β’ (πΉβsuc π€) β V |
50 | 21 | elrnmpt 5916 |
. . . . . . . 8
β’ ((πΉβsuc π€) β V β ((πΉβsuc π€) β ran (π¦ β Ο β¦ (πΉβπ¦)) β βπ¦ β Ο (πΉβsuc π€) = (πΉβπ¦))) |
51 | 49, 50 | ax-mp 5 |
. . . . . . 7
β’ ((πΉβsuc π€) β ran (π¦ β Ο β¦ (πΉβπ¦)) β βπ¦ β Ο (πΉβsuc π€) = (πΉβπ¦)) |
52 | 48, 51 | sylibr 233 |
. . . . . 6
β’ ((((πΉββ
) β On β§
βπ₯ β Ο
(πΉβsuc π₯) β (πΉβπ₯)) β§ π€ β Ο) β (πΉβsuc π€) β ran (π¦ β Ο β¦ (πΉβπ¦))) |
53 | | suceq 6388 |
. . . . . . . . . 10
β’ (π₯ = π€ β suc π₯ = suc π€) |
54 | 53 | fveq2d 6851 |
. . . . . . . . 9
β’ (π₯ = π€ β (πΉβsuc π₯) = (πΉβsuc π€)) |
55 | | fveq2 6847 |
. . . . . . . . 9
β’ (π₯ = π€ β (πΉβπ₯) = (πΉβπ€)) |
56 | 54, 55 | eleq12d 2832 |
. . . . . . . 8
β’ (π₯ = π€ β ((πΉβsuc π₯) β (πΉβπ₯) β (πΉβsuc π€) β (πΉβπ€))) |
57 | 56 | rspccva 3583 |
. . . . . . 7
β’
((βπ₯ β
Ο (πΉβsuc π₯) β (πΉβπ₯) β§ π€ β Ο) β (πΉβsuc π€) β (πΉβπ€)) |
58 | 57 | adantll 713 |
. . . . . 6
β’ ((((πΉββ
) β On β§
βπ₯ β Ο
(πΉβsuc π₯) β (πΉβπ₯)) β§ π€ β Ο) β (πΉβsuc π€) β (πΉβπ€)) |
59 | | inelcm 4429 |
. . . . . 6
β’ (((πΉβsuc π€) β ran (π¦ β Ο β¦ (πΉβπ¦)) β§ (πΉβsuc π€) β (πΉβπ€)) β (ran (π¦ β Ο β¦ (πΉβπ¦)) β© (πΉβπ€)) β β
) |
60 | 52, 58, 59 | syl2anc 585 |
. . . . 5
β’ ((((πΉββ
) β On β§
βπ₯ β Ο
(πΉβsuc π₯) β (πΉβπ₯)) β§ π€ β Ο) β (ran (π¦ β Ο β¦ (πΉβπ¦)) β© (πΉβπ€)) β β
) |
61 | 60 | neneqd 2949 |
. . . 4
β’ ((((πΉββ
) β On β§
βπ₯ β Ο
(πΉβsuc π₯) β (πΉβπ₯)) β§ π€ β Ο) β Β¬ (ran (π¦ β Ο β¦ (πΉβπ¦)) β© (πΉβπ€)) = β
) |
62 | 61 | nrexdv 3147 |
. . 3
β’ (((πΉββ
) β On β§
βπ₯ β Ο
(πΉβsuc π₯) β (πΉβπ₯)) β Β¬ βπ€ β Ο (ran (π¦ β Ο β¦ (πΉβπ¦)) β© (πΉβπ€)) = β
) |
63 | 42, 62 | pm2.65da 816 |
. 2
β’ ((πΉββ
) β On β
Β¬ βπ₯ β
Ο (πΉβsuc π₯) β (πΉβπ₯)) |
64 | | rexnal 3104 |
. 2
β’
(βπ₯ β
Ο Β¬ (πΉβsuc
π₯) β (πΉβπ₯) β Β¬ βπ₯ β Ο (πΉβsuc π₯) β (πΉβπ₯)) |
65 | 63, 64 | sylibr 233 |
1
β’ ((πΉββ
) β On β
βπ₯ β Ο
Β¬ (πΉβsuc π₯) β (πΉβπ₯)) |