Step | Hyp | Ref
| Expression |
1 | | alephfplem.1 |
. . 3
β’ π» = (rec(β΅, Ο)
βΎ Ο) |
2 | 1 | alephfplem4 10043 |
. 2
β’ βͺ (π»
β Ο) β ran β΅ |
3 | | isinfcard 10028 |
. . 3
β’ ((Ο
β βͺ (π» β Ο) β§ (cardββͺ (π»
β Ο)) = βͺ (π» β Ο)) β βͺ (π»
β Ο) β ran β΅) |
4 | | cardalephex 10026 |
. . . 4
β’ (Ο
β βͺ (π» β Ο) β ((cardββͺ (π»
β Ο)) = βͺ (π» β Ο) β βπ§ β On βͺ (π»
β Ο) = (β΅βπ§))) |
5 | 4 | biimpa 477 |
. . 3
β’ ((Ο
β βͺ (π» β Ο) β§ (cardββͺ (π»
β Ο)) = βͺ (π» β Ο)) β βπ§ β On βͺ (π»
β Ο) = (β΅βπ§)) |
6 | 3, 5 | sylbir 234 |
. 2
β’ (βͺ (π»
β Ο) β ran β΅ β βπ§ β On βͺ
(π» β Ο) =
(β΅βπ§)) |
7 | | alephle 10024 |
. . . . . . . . 9
β’ (π§ β On β π§ β (β΅βπ§)) |
8 | | alephon 10005 |
. . . . . . . . . . 11
β’
(β΅βπ§)
β On |
9 | 8 | onirri 6430 |
. . . . . . . . . 10
β’ Β¬
(β΅βπ§) β
(β΅βπ§) |
10 | | frfnom 8381 |
. . . . . . . . . . . . . 14
β’
(rec(β΅, Ο) βΎ Ο) Fn Ο |
11 | 1 | fneq1i 6599 |
. . . . . . . . . . . . . 14
β’ (π» Fn Ο β (rec(β΅,
Ο) βΎ Ο) Fn Ο) |
12 | 10, 11 | mpbir 230 |
. . . . . . . . . . . . 13
β’ π» Fn Ο |
13 | | fnfun 6602 |
. . . . . . . . . . . . 13
β’ (π» Fn Ο β Fun π») |
14 | | eluniima 7197 |
. . . . . . . . . . . . 13
β’ (Fun
π» β (π§ β βͺ (π»
β Ο) β βπ£ β Ο π§ β (π»βπ£))) |
15 | 12, 13, 14 | mp2b 10 |
. . . . . . . . . . . 12
β’ (π§ β βͺ (π»
β Ο) β βπ£ β Ο π§ β (π»βπ£)) |
16 | | alephsson 10036 |
. . . . . . . . . . . . . . . 16
β’ ran
β΅ β On |
17 | 1 | alephfplem3 10042 |
. . . . . . . . . . . . . . . 16
β’ (π£ β Ο β (π»βπ£) β ran β΅) |
18 | 16, 17 | sselid 3942 |
. . . . . . . . . . . . . . 15
β’ (π£ β Ο β (π»βπ£) β On) |
19 | | alephord2i 10013 |
. . . . . . . . . . . . . . 15
β’ ((π»βπ£) β On β (π§ β (π»βπ£) β (β΅βπ§) β (β΅β(π»βπ£)))) |
20 | 18, 19 | syl 17 |
. . . . . . . . . . . . . 14
β’ (π£ β Ο β (π§ β (π»βπ£) β (β΅βπ§) β (β΅β(π»βπ£)))) |
21 | 1 | alephfplem2 10041 |
. . . . . . . . . . . . . . . . 17
β’ (π£ β Ο β (π»βsuc π£) = (β΅β(π»βπ£))) |
22 | | peano2 7827 |
. . . . . . . . . . . . . . . . . 18
β’ (π£ β Ο β suc π£ β
Ο) |
23 | | fnfvelrn 7031 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π» Fn Ο β§ suc π£ β Ο) β (π»βsuc π£) β ran π») |
24 | 12, 23 | mpan 688 |
. . . . . . . . . . . . . . . . . . 19
β’ (suc
π£ β Ο β
(π»βsuc π£) β ran π») |
25 | | fnima 6631 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π» Fn Ο β (π» β Ο) = ran π») |
26 | 12, 25 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
β’ (π» β Ο) = ran π» |
27 | 24, 26 | eleqtrrdi 2848 |
. . . . . . . . . . . . . . . . . 18
β’ (suc
π£ β Ο β
(π»βsuc π£) β (π» β Ο)) |
28 | 22, 27 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ (π£ β Ο β (π»βsuc π£) β (π» β Ο)) |
29 | 21, 28 | eqeltrrd 2838 |
. . . . . . . . . . . . . . . 16
β’ (π£ β Ο β
(β΅β(π»βπ£)) β (π» β Ο)) |
30 | | elssuni 4898 |
. . . . . . . . . . . . . . . 16
β’
((β΅β(π»βπ£)) β (π» β Ο) β
(β΅β(π»βπ£)) β βͺ
(π» β
Ο)) |
31 | 29, 30 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (π£ β Ο β
(β΅β(π»βπ£)) β βͺ
(π» β
Ο)) |
32 | 31 | sseld 3943 |
. . . . . . . . . . . . . 14
β’ (π£ β Ο β
((β΅βπ§) β
(β΅β(π»βπ£)) β (β΅βπ§) β βͺ (π» β
Ο))) |
33 | 20, 32 | syld 47 |
. . . . . . . . . . . . 13
β’ (π£ β Ο β (π§ β (π»βπ£) β (β΅βπ§) β βͺ (π» β
Ο))) |
34 | 33 | rexlimiv 3145 |
. . . . . . . . . . . 12
β’
(βπ£ β
Ο π§ β (π»βπ£) β (β΅βπ§) β βͺ (π» β
Ο)) |
35 | 15, 34 | sylbi 216 |
. . . . . . . . . . 11
β’ (π§ β βͺ (π»
β Ο) β (β΅βπ§) β βͺ (π» β
Ο)) |
36 | | eleq2 2826 |
. . . . . . . . . . . 12
β’ (βͺ (π»
β Ο) = (β΅βπ§) β (π§ β βͺ (π» β Ο) β π§ β (β΅βπ§))) |
37 | | eleq2 2826 |
. . . . . . . . . . . 12
β’ (βͺ (π»
β Ο) = (β΅βπ§) β ((β΅βπ§) β βͺ (π» β Ο) β
(β΅βπ§) β
(β΅βπ§))) |
38 | 36, 37 | imbi12d 344 |
. . . . . . . . . . 11
β’ (βͺ (π»
β Ο) = (β΅βπ§) β ((π§ β βͺ (π» β Ο) β
(β΅βπ§) β
βͺ (π» β Ο)) β (π§ β (β΅βπ§) β (β΅βπ§) β (β΅βπ§)))) |
39 | 35, 38 | mpbii 232 |
. . . . . . . . . 10
β’ (βͺ (π»
β Ο) = (β΅βπ§) β (π§ β (β΅βπ§) β (β΅βπ§) β (β΅βπ§))) |
40 | 9, 39 | mtoi 198 |
. . . . . . . . 9
β’ (βͺ (π»
β Ο) = (β΅βπ§) β Β¬ π§ β (β΅βπ§)) |
41 | 7, 40 | anim12i 613 |
. . . . . . . 8
β’ ((π§ β On β§ βͺ (π»
β Ο) = (β΅βπ§)) β (π§ β (β΅βπ§) β§ Β¬ π§ β (β΅βπ§))) |
42 | | eloni 6327 |
. . . . . . . . . 10
β’ (π§ β On β Ord π§) |
43 | 8 | onordi 6428 |
. . . . . . . . . 10
β’ Ord
(β΅βπ§) |
44 | | ordtri4 6354 |
. . . . . . . . . 10
β’ ((Ord
π§ β§ Ord
(β΅βπ§)) β
(π§ = (β΅βπ§) β (π§ β (β΅βπ§) β§ Β¬ π§ β (β΅βπ§)))) |
45 | 42, 43, 44 | sylancl 586 |
. . . . . . . . 9
β’ (π§ β On β (π§ = (β΅βπ§) β (π§ β (β΅βπ§) β§ Β¬ π§ β (β΅βπ§)))) |
46 | 45 | adantr 481 |
. . . . . . . 8
β’ ((π§ β On β§ βͺ (π»
β Ο) = (β΅βπ§)) β (π§ = (β΅βπ§) β (π§ β (β΅βπ§) β§ Β¬ π§ β (β΅βπ§)))) |
47 | 41, 46 | mpbird 256 |
. . . . . . 7
β’ ((π§ β On β§ βͺ (π»
β Ο) = (β΅βπ§)) β π§ = (β΅βπ§)) |
48 | | eqeq2 2748 |
. . . . . . . 8
β’ (βͺ (π»
β Ο) = (β΅βπ§) β (π§ = βͺ (π» β Ο) β π§ = (β΅βπ§))) |
49 | 48 | adantl 482 |
. . . . . . 7
β’ ((π§ β On β§ βͺ (π»
β Ο) = (β΅βπ§)) β (π§ = βͺ (π» β Ο) β π§ = (β΅βπ§))) |
50 | 47, 49 | mpbird 256 |
. . . . . 6
β’ ((π§ β On β§ βͺ (π»
β Ο) = (β΅βπ§)) β π§ = βͺ (π» β
Ο)) |
51 | 50 | eqcomd 2742 |
. . . . 5
β’ ((π§ β On β§ βͺ (π»
β Ο) = (β΅βπ§)) β βͺ (π» β Ο) = π§) |
52 | 51 | fveq2d 6846 |
. . . 4
β’ ((π§ β On β§ βͺ (π»
β Ο) = (β΅βπ§)) β (β΅ββͺ (π»
β Ο)) = (β΅βπ§)) |
53 | | eqeq2 2748 |
. . . . 5
β’ (βͺ (π»
β Ο) = (β΅βπ§) β ((β΅ββͺ (π»
β Ο)) = βͺ (π» β Ο) β
(β΅ββͺ (π» β Ο)) = (β΅βπ§))) |
54 | 53 | adantl 482 |
. . . 4
β’ ((π§ β On β§ βͺ (π»
β Ο) = (β΅βπ§)) β ((β΅ββͺ (π»
β Ο)) = βͺ (π» β Ο) β
(β΅ββͺ (π» β Ο)) = (β΅βπ§))) |
55 | 52, 54 | mpbird 256 |
. . 3
β’ ((π§ β On β§ βͺ (π»
β Ο) = (β΅βπ§)) β (β΅ββͺ (π»
β Ο)) = βͺ (π» β Ο)) |
56 | 55 | rexlimiva 3144 |
. 2
β’
(βπ§ β On
βͺ (π» β Ο) = (β΅βπ§) β (β΅ββͺ (π»
β Ο)) = βͺ (π» β Ο)) |
57 | 2, 6, 56 | mp2b 10 |
1
β’
(β΅ββͺ (π» β Ο)) = βͺ (π»
β Ο) |