Step | Hyp | Ref
| Expression |
1 | | cardon 9936 |
. . . . . . . . 9
β’
(cardβπ΄)
β On |
2 | | eleq1 2822 |
. . . . . . . . 9
β’
((cardβπ΄) =
π΄ β ((cardβπ΄) β On β π΄ β On)) |
3 | 1, 2 | mpbii 232 |
. . . . . . . 8
β’
((cardβπ΄) =
π΄ β π΄ β On) |
4 | | alephle 10080 |
. . . . . . . . 9
β’ (π΄ β On β π΄ β (β΅βπ΄)) |
5 | | fveq2 6889 |
. . . . . . . . . . 11
β’ (π₯ = π΄ β (β΅βπ₯) = (β΅βπ΄)) |
6 | 5 | sseq2d 4014 |
. . . . . . . . . 10
β’ (π₯ = π΄ β (π΄ β (β΅βπ₯) β π΄ β (β΅βπ΄))) |
7 | 6 | rspcev 3613 |
. . . . . . . . 9
β’ ((π΄ β On β§ π΄ β (β΅βπ΄)) β βπ₯ β On π΄ β (β΅βπ₯)) |
8 | 4, 7 | mpdan 686 |
. . . . . . . 8
β’ (π΄ β On β βπ₯ β On π΄ β (β΅βπ₯)) |
9 | | nfcv 2904 |
. . . . . . . . . 10
β’
β²π₯π΄ |
10 | | nfcv 2904 |
. . . . . . . . . . 11
β’
β²π₯β΅ |
11 | | nfrab1 3452 |
. . . . . . . . . . . 12
β’
β²π₯{π₯ β On β£ π΄ β (β΅βπ₯)} |
12 | 11 | nfint 4960 |
. . . . . . . . . . 11
β’
β²π₯β© {π₯
β On β£ π΄ β
(β΅βπ₯)} |
13 | 10, 12 | nffv 6899 |
. . . . . . . . . 10
β’
β²π₯(β΅ββ©
{π₯ β On β£ π΄ β (β΅βπ₯)}) |
14 | 9, 13 | nfss 3974 |
. . . . . . . . 9
β’
β²π₯ π΄ β (β΅ββ© {π₯
β On β£ π΄ β
(β΅βπ₯)}) |
15 | | fveq2 6889 |
. . . . . . . . . 10
β’ (π₯ = β©
{π₯ β On β£ π΄ β (β΅βπ₯)} β (β΅βπ₯) = (β΅ββ© {π₯
β On β£ π΄ β
(β΅βπ₯)})) |
16 | 15 | sseq2d 4014 |
. . . . . . . . 9
β’ (π₯ = β©
{π₯ β On β£ π΄ β (β΅βπ₯)} β (π΄ β (β΅βπ₯) β π΄ β (β΅ββ© {π₯
β On β£ π΄ β
(β΅βπ₯)}))) |
17 | 14, 16 | onminsb 7779 |
. . . . . . . 8
β’
(βπ₯ β On
π΄ β
(β΅βπ₯) β
π΄ β
(β΅ββ© {π₯ β On β£ π΄ β (β΅βπ₯)})) |
18 | 3, 8, 17 | 3syl 18 |
. . . . . . 7
β’
((cardβπ΄) =
π΄ β π΄ β (β΅ββ© {π₯
β On β£ π΄ β
(β΅βπ₯)})) |
19 | 18 | a1i 11 |
. . . . . 6
β’ (β© {π₯
β On β£ π΄ β
(β΅βπ₯)} =
β
β ((cardβπ΄) = π΄ β π΄ β (β΅ββ© {π₯
β On β£ π΄ β
(β΅βπ₯)}))) |
20 | | fveq2 6889 |
. . . . . . . . 9
β’ (β© {π₯
β On β£ π΄ β
(β΅βπ₯)} =
β
β (β΅ββ© {π₯ β On β£ π΄ β (β΅βπ₯)}) =
(β΅ββ
)) |
21 | | aleph0 10058 |
. . . . . . . . 9
β’
(β΅ββ
) = Ο |
22 | 20, 21 | eqtrdi 2789 |
. . . . . . . 8
β’ (β© {π₯
β On β£ π΄ β
(β΅βπ₯)} =
β
β (β΅ββ© {π₯ β On β£ π΄ β (β΅βπ₯)}) = Ο) |
23 | 22 | sseq1d 4013 |
. . . . . . 7
β’ (β© {π₯
β On β£ π΄ β
(β΅βπ₯)} =
β
β ((β΅ββ© {π₯ β On β£ π΄ β (β΅βπ₯)}) β π΄ β Ο β π΄)) |
24 | 23 | biimprd 247 |
. . . . . 6
β’ (β© {π₯
β On β£ π΄ β
(β΅βπ₯)} =
β
β (Ο β π΄ β (β΅ββ© {π₯
β On β£ π΄ β
(β΅βπ₯)}) β
π΄)) |
25 | 19, 24 | anim12d 610 |
. . . . 5
β’ (β© {π₯
β On β£ π΄ β
(β΅βπ₯)} =
β
β (((cardβπ΄) = π΄ β§ Ο β π΄) β (π΄ β (β΅ββ© {π₯
β On β£ π΄ β
(β΅βπ₯)}) β§
(β΅ββ© {π₯ β On β£ π΄ β (β΅βπ₯)}) β π΄))) |
26 | | eqss 3997 |
. . . . 5
β’ (π΄ = (β΅ββ© {π₯
β On β£ π΄ β
(β΅βπ₯)}) β
(π΄ β
(β΅ββ© {π₯ β On β£ π΄ β (β΅βπ₯)}) β§ (β΅ββ© {π₯
β On β£ π΄ β
(β΅βπ₯)}) β
π΄)) |
27 | 25, 26 | syl6ibr 252 |
. . . 4
β’ (β© {π₯
β On β£ π΄ β
(β΅βπ₯)} =
β
β (((cardβπ΄) = π΄ β§ Ο β π΄) β π΄ = (β΅ββ© {π₯
β On β£ π΄ β
(β΅βπ₯)}))) |
28 | 27 | com12 32 |
. . 3
β’
(((cardβπ΄) =
π΄ β§ Ο β
π΄) β (β© {π₯
β On β£ π΄ β
(β΅βπ₯)} =
β
β π΄ =
(β΅ββ© {π₯ β On β£ π΄ β (β΅βπ₯)}))) |
29 | 28 | ancoms 460 |
. 2
β’ ((Ο
β π΄ β§
(cardβπ΄) = π΄) β (β© {π₯
β On β£ π΄ β
(β΅βπ₯)} =
β
β π΄ =
(β΅ββ© {π₯ β On β£ π΄ β (β΅βπ₯)}))) |
30 | | fveq2 6889 |
. . . . . . . . . . 11
β’ (π₯ = π¦ β (β΅βπ₯) = (β΅βπ¦)) |
31 | 30 | sseq2d 4014 |
. . . . . . . . . 10
β’ (π₯ = π¦ β (π΄ β (β΅βπ₯) β π΄ β (β΅βπ¦))) |
32 | 31 | onnminsb 7784 |
. . . . . . . . 9
β’ (π¦ β On β (π¦ β β© {π₯
β On β£ π΄ β
(β΅βπ₯)} β
Β¬ π΄ β
(β΅βπ¦))) |
33 | | vex 3479 |
. . . . . . . . . . 11
β’ π¦ β V |
34 | 33 | sucid 6444 |
. . . . . . . . . 10
β’ π¦ β suc π¦ |
35 | | eleq2 2823 |
. . . . . . . . . 10
β’ (β© {π₯
β On β£ π΄ β
(β΅βπ₯)} = suc
π¦ β (π¦ β β© {π₯
β On β£ π΄ β
(β΅βπ₯)} β
π¦ β suc π¦)) |
36 | 34, 35 | mpbiri 258 |
. . . . . . . . 9
β’ (β© {π₯
β On β£ π΄ β
(β΅βπ₯)} = suc
π¦ β π¦ β β© {π₯ β On β£ π΄ β (β΅βπ₯)}) |
37 | 32, 36 | impel 507 |
. . . . . . . 8
β’ ((π¦ β On β§ β© {π₯
β On β£ π΄ β
(β΅βπ₯)} = suc
π¦) β Β¬ π΄ β (β΅βπ¦)) |
38 | 37 | adantl 483 |
. . . . . . 7
β’
(((cardβπ΄) =
π΄ β§ (π¦ β On β§ β©
{π₯ β On β£ π΄ β (β΅βπ₯)} = suc π¦)) β Β¬ π΄ β (β΅βπ¦)) |
39 | | fveq2 6889 |
. . . . . . . . . . 11
β’ (β© {π₯
β On β£ π΄ β
(β΅βπ₯)} = suc
π¦ β
(β΅ββ© {π₯ β On β£ π΄ β (β΅βπ₯)}) = (β΅βsuc π¦)) |
40 | | alephsuc 10060 |
. . . . . . . . . . 11
β’ (π¦ β On β
(β΅βsuc π¦) =
(harβ(β΅βπ¦))) |
41 | 39, 40 | sylan9eqr 2795 |
. . . . . . . . . 10
β’ ((π¦ β On β§ β© {π₯
β On β£ π΄ β
(β΅βπ₯)} = suc
π¦) β
(β΅ββ© {π₯ β On β£ π΄ β (β΅βπ₯)}) = (harβ(β΅βπ¦))) |
42 | 41 | eleq2d 2820 |
. . . . . . . . 9
β’ ((π¦ β On β§ β© {π₯
β On β£ π΄ β
(β΅βπ₯)} = suc
π¦) β (π΄ β (β΅ββ© {π₯
β On β£ π΄ β
(β΅βπ₯)}) β
π΄ β
(harβ(β΅βπ¦)))) |
43 | 42 | biimpd 228 |
. . . . . . . 8
β’ ((π¦ β On β§ β© {π₯
β On β£ π΄ β
(β΅βπ₯)} = suc
π¦) β (π΄ β (β΅ββ© {π₯
β On β£ π΄ β
(β΅βπ₯)}) β
π΄ β
(harβ(β΅βπ¦)))) |
44 | | elharval 9553 |
. . . . . . . . . 10
β’ (π΄ β
(harβ(β΅βπ¦)) β (π΄ β On β§ π΄ βΌ (β΅βπ¦))) |
45 | 44 | simprbi 498 |
. . . . . . . . 9
β’ (π΄ β
(harβ(β΅βπ¦)) β π΄ βΌ (β΅βπ¦)) |
46 | | onenon 9941 |
. . . . . . . . . . . 12
β’ (π΄ β On β π΄ β dom
card) |
47 | 3, 46 | syl 17 |
. . . . . . . . . . 11
β’
((cardβπ΄) =
π΄ β π΄ β dom card) |
48 | | alephon 10061 |
. . . . . . . . . . . 12
β’
(β΅βπ¦)
β On |
49 | | onenon 9941 |
. . . . . . . . . . . 12
β’
((β΅βπ¦)
β On β (β΅βπ¦) β dom card) |
50 | 48, 49 | ax-mp 5 |
. . . . . . . . . . 11
β’
(β΅βπ¦)
β dom card |
51 | | carddom2 9969 |
. . . . . . . . . . 11
β’ ((π΄ β dom card β§
(β΅βπ¦) β
dom card) β ((cardβπ΄) β (cardβ(β΅βπ¦)) β π΄ βΌ (β΅βπ¦))) |
52 | 47, 50, 51 | sylancl 587 |
. . . . . . . . . 10
β’
((cardβπ΄) =
π΄ β ((cardβπ΄) β
(cardβ(β΅βπ¦)) β π΄ βΌ (β΅βπ¦))) |
53 | | sseq1 4007 |
. . . . . . . . . . 11
β’
((cardβπ΄) =
π΄ β ((cardβπ΄) β
(cardβ(β΅βπ¦)) β π΄ β (cardβ(β΅βπ¦)))) |
54 | | alephcard 10062 |
. . . . . . . . . . . 12
β’
(cardβ(β΅βπ¦)) = (β΅βπ¦) |
55 | 54 | sseq2i 4011 |
. . . . . . . . . . 11
β’ (π΄ β
(cardβ(β΅βπ¦)) β π΄ β (β΅βπ¦)) |
56 | 53, 55 | bitrdi 287 |
. . . . . . . . . 10
β’
((cardβπ΄) =
π΄ β ((cardβπ΄) β
(cardβ(β΅βπ¦)) β π΄ β (β΅βπ¦))) |
57 | 52, 56 | bitr3d 281 |
. . . . . . . . 9
β’
((cardβπ΄) =
π΄ β (π΄ βΌ (β΅βπ¦) β π΄ β (β΅βπ¦))) |
58 | 45, 57 | imbitrid 243 |
. . . . . . . 8
β’
((cardβπ΄) =
π΄ β (π΄ β (harβ(β΅βπ¦)) β π΄ β (β΅βπ¦))) |
59 | 43, 58 | sylan9r 510 |
. . . . . . 7
β’
(((cardβπ΄) =
π΄ β§ (π¦ β On β§ β©
{π₯ β On β£ π΄ β (β΅βπ₯)} = suc π¦)) β (π΄ β (β΅ββ© {π₯
β On β£ π΄ β
(β΅βπ₯)}) β
π΄ β
(β΅βπ¦))) |
60 | 38, 59 | mtod 197 |
. . . . . 6
β’
(((cardβπ΄) =
π΄ β§ (π¦ β On β§ β©
{π₯ β On β£ π΄ β (β΅βπ₯)} = suc π¦)) β Β¬ π΄ β (β΅ββ© {π₯
β On β£ π΄ β
(β΅βπ₯)})) |
61 | 60 | rexlimdvaa 3157 |
. . . . 5
β’
((cardβπ΄) =
π΄ β (βπ¦ β On β© {π₯
β On β£ π΄ β
(β΅βπ₯)} = suc
π¦ β Β¬ π΄ β (β΅ββ© {π₯
β On β£ π΄ β
(β΅βπ₯)}))) |
62 | | onintrab2 7782 |
. . . . . . . . . . . . . 14
β’
(βπ₯ β On
π΄ β
(β΅βπ₯) β
β© {π₯ β On β£ π΄ β (β΅βπ₯)} β On) |
63 | 8, 62 | sylib 217 |
. . . . . . . . . . . . 13
β’ (π΄ β On β β© {π₯
β On β£ π΄ β
(β΅βπ₯)} β
On) |
64 | | onelon 6387 |
. . . . . . . . . . . . 13
β’ ((β© {π₯
β On β£ π΄ β
(β΅βπ₯)} β
On β§ π¦ β β© {π₯
β On β£ π΄ β
(β΅βπ₯)}) β
π¦ β
On) |
65 | 63, 64 | sylan 581 |
. . . . . . . . . . . 12
β’ ((π΄ β On β§ π¦ β β© {π₯
β On β£ π΄ β
(β΅βπ₯)}) β
π¦ β
On) |
66 | 32 | adantld 492 |
. . . . . . . . . . . 12
β’ (π¦ β On β ((π΄ β On β§ π¦ β β© {π₯
β On β£ π΄ β
(β΅βπ₯)}) β
Β¬ π΄ β
(β΅βπ¦))) |
67 | 65, 66 | mpcom 38 |
. . . . . . . . . . 11
β’ ((π΄ β On β§ π¦ β β© {π₯
β On β£ π΄ β
(β΅βπ₯)}) β
Β¬ π΄ β
(β΅βπ¦)) |
68 | 48 | onelssi 6477 |
. . . . . . . . . . 11
β’ (π΄ β (β΅βπ¦) β π΄ β (β΅βπ¦)) |
69 | 67, 68 | nsyl 140 |
. . . . . . . . . 10
β’ ((π΄ β On β§ π¦ β β© {π₯
β On β£ π΄ β
(β΅βπ₯)}) β
Β¬ π΄ β
(β΅βπ¦)) |
70 | 69 | nrexdv 3150 |
. . . . . . . . 9
β’ (π΄ β On β Β¬
βπ¦ β β© {π₯
β On β£ π΄ β
(β΅βπ₯)}π΄ β (β΅βπ¦)) |
71 | 70 | adantr 482 |
. . . . . . . 8
β’ ((π΄ β On β§ Lim β© {π₯
β On β£ π΄ β
(β΅βπ₯)}) β
Β¬ βπ¦ β β© {π₯
β On β£ π΄ β
(β΅βπ₯)}π΄ β (β΅βπ¦)) |
72 | | alephlim 10059 |
. . . . . . . . . . 11
β’ ((β© {π₯
β On β£ π΄ β
(β΅βπ₯)} β
On β§ Lim β© {π₯ β On β£ π΄ β (β΅βπ₯)}) β (β΅ββ© {π₯
β On β£ π΄ β
(β΅βπ₯)}) =
βͺ π¦ β β© {π₯ β On β£ π΄ β (β΅βπ₯)} (β΅βπ¦)) |
73 | 63, 72 | sylan 581 |
. . . . . . . . . 10
β’ ((π΄ β On β§ Lim β© {π₯
β On β£ π΄ β
(β΅βπ₯)}) β
(β΅ββ© {π₯ β On β£ π΄ β (β΅βπ₯)}) = βͺ
π¦ β β© {π₯
β On β£ π΄ β
(β΅βπ₯)}
(β΅βπ¦)) |
74 | 73 | eleq2d 2820 |
. . . . . . . . 9
β’ ((π΄ β On β§ Lim β© {π₯
β On β£ π΄ β
(β΅βπ₯)}) β
(π΄ β
(β΅ββ© {π₯ β On β£ π΄ β (β΅βπ₯)}) β π΄ β βͺ
π¦ β β© {π₯
β On β£ π΄ β
(β΅βπ₯)}
(β΅βπ¦))) |
75 | | eliun 5001 |
. . . . . . . . 9
β’ (π΄ β βͺ π¦ β β© {π₯ β On β£ π΄ β (β΅βπ₯)} (β΅βπ¦) β βπ¦ β β© {π₯
β On β£ π΄ β
(β΅βπ₯)}π΄ β (β΅βπ¦)) |
76 | 74, 75 | bitrdi 287 |
. . . . . . . 8
β’ ((π΄ β On β§ Lim β© {π₯
β On β£ π΄ β
(β΅βπ₯)}) β
(π΄ β
(β΅ββ© {π₯ β On β£ π΄ β (β΅βπ₯)}) β βπ¦ β β© {π₯ β On β£ π΄ β (β΅βπ₯)}π΄ β (β΅βπ¦))) |
77 | 71, 76 | mtbird 325 |
. . . . . . 7
β’ ((π΄ β On β§ Lim β© {π₯
β On β£ π΄ β
(β΅βπ₯)}) β
Β¬ π΄ β
(β΅ββ© {π₯ β On β£ π΄ β (β΅βπ₯)})) |
78 | 77 | ex 414 |
. . . . . 6
β’ (π΄ β On β (Lim β© {π₯
β On β£ π΄ β
(β΅βπ₯)} β
Β¬ π΄ β
(β΅ββ© {π₯ β On β£ π΄ β (β΅βπ₯)}))) |
79 | 3, 78 | syl 17 |
. . . . 5
β’
((cardβπ΄) =
π΄ β (Lim β© {π₯
β On β£ π΄ β
(β΅βπ₯)} β
Β¬ π΄ β
(β΅ββ© {π₯ β On β£ π΄ β (β΅βπ₯)}))) |
80 | 61, 79 | jaod 858 |
. . . 4
β’
((cardβπ΄) =
π΄ β ((βπ¦ β On β© {π₯
β On β£ π΄ β
(β΅βπ₯)} = suc
π¦ β¨ Lim β© {π₯
β On β£ π΄ β
(β΅βπ₯)}) β
Β¬ π΄ β
(β΅ββ© {π₯ β On β£ π΄ β (β΅βπ₯)}))) |
81 | 8, 17 | syl 17 |
. . . . . 6
β’ (π΄ β On β π΄ β (β΅ββ© {π₯
β On β£ π΄ β
(β΅βπ₯)})) |
82 | | alephon 10061 |
. . . . . . 7
β’
(β΅ββ© {π₯ β On β£ π΄ β (β΅βπ₯)}) β On |
83 | | onsseleq 6403 |
. . . . . . 7
β’ ((π΄ β On β§
(β΅ββ© {π₯ β On β£ π΄ β (β΅βπ₯)}) β On) β (π΄ β (β΅ββ© {π₯
β On β£ π΄ β
(β΅βπ₯)}) β
(π΄ β
(β΅ββ© {π₯ β On β£ π΄ β (β΅βπ₯)}) β¨ π΄ = (β΅ββ© {π₯
β On β£ π΄ β
(β΅βπ₯)})))) |
84 | 82, 83 | mpan2 690 |
. . . . . 6
β’ (π΄ β On β (π΄ β (β΅ββ© {π₯
β On β£ π΄ β
(β΅βπ₯)}) β
(π΄ β
(β΅ββ© {π₯ β On β£ π΄ β (β΅βπ₯)}) β¨ π΄ = (β΅ββ© {π₯
β On β£ π΄ β
(β΅βπ₯)})))) |
85 | 81, 84 | mpbid 231 |
. . . . 5
β’ (π΄ β On β (π΄ β (β΅ββ© {π₯
β On β£ π΄ β
(β΅βπ₯)}) β¨
π΄ = (β΅ββ© {π₯
β On β£ π΄ β
(β΅βπ₯)}))) |
86 | 85 | ord 863 |
. . . 4
β’ (π΄ β On β (Β¬ π΄ β (β΅ββ© {π₯
β On β£ π΄ β
(β΅βπ₯)}) β
π΄ = (β΅ββ© {π₯
β On β£ π΄ β
(β΅βπ₯)}))) |
87 | 3, 80, 86 | sylsyld 61 |
. . 3
β’
((cardβπ΄) =
π΄ β ((βπ¦ β On β© {π₯
β On β£ π΄ β
(β΅βπ₯)} = suc
π¦ β¨ Lim β© {π₯
β On β£ π΄ β
(β΅βπ₯)}) β
π΄ = (β΅ββ© {π₯
β On β£ π΄ β
(β΅βπ₯)}))) |
88 | 87 | adantl 483 |
. 2
β’ ((Ο
β π΄ β§
(cardβπ΄) = π΄) β ((βπ¦ β On β© {π₯
β On β£ π΄ β
(β΅βπ₯)} = suc
π¦ β¨ Lim β© {π₯
β On β£ π΄ β
(β΅βπ₯)}) β
π΄ = (β΅ββ© {π₯
β On β£ π΄ β
(β΅βπ₯)}))) |
89 | | eloni 6372 |
. . . . 5
β’ (β© {π₯
β On β£ π΄ β
(β΅βπ₯)} β
On β Ord β© {π₯ β On β£ π΄ β (β΅βπ₯)}) |
90 | | ordzsl 7831 |
. . . . . 6
β’ (Ord
β© {π₯ β On β£ π΄ β (β΅βπ₯)} β (β©
{π₯ β On β£ π΄ β (β΅βπ₯)} = β
β¨ βπ¦ β On β© {π₯
β On β£ π΄ β
(β΅βπ₯)} = suc
π¦ β¨ Lim β© {π₯
β On β£ π΄ β
(β΅βπ₯)})) |
91 | | 3orass 1091 |
. . . . . 6
β’ ((β© {π₯
β On β£ π΄ β
(β΅βπ₯)} =
β
β¨ βπ¦
β On β© {π₯ β On β£ π΄ β (β΅βπ₯)} = suc π¦ β¨ Lim β© {π₯ β On β£ π΄ β (β΅βπ₯)}) β (β© {π₯
β On β£ π΄ β
(β΅βπ₯)} =
β
β¨ (βπ¦
β On β© {π₯ β On β£ π΄ β (β΅βπ₯)} = suc π¦ β¨ Lim β© {π₯ β On β£ π΄ β (β΅βπ₯)}))) |
92 | 90, 91 | bitri 275 |
. . . . 5
β’ (Ord
β© {π₯ β On β£ π΄ β (β΅βπ₯)} β (β©
{π₯ β On β£ π΄ β (β΅βπ₯)} = β
β¨ (βπ¦ β On β© {π₯
β On β£ π΄ β
(β΅βπ₯)} = suc
π¦ β¨ Lim β© {π₯
β On β£ π΄ β
(β΅βπ₯)}))) |
93 | 89, 92 | sylib 217 |
. . . 4
β’ (β© {π₯
β On β£ π΄ β
(β΅βπ₯)} β
On β (β© {π₯ β On β£ π΄ β (β΅βπ₯)} = β
β¨ (βπ¦ β On β©
{π₯ β On β£ π΄ β (β΅βπ₯)} = suc π¦ β¨ Lim β© {π₯ β On β£ π΄ β (β΅βπ₯)}))) |
94 | 3, 63, 93 | 3syl 18 |
. . 3
β’
((cardβπ΄) =
π΄ β (β© {π₯
β On β£ π΄ β
(β΅βπ₯)} =
β
β¨ (βπ¦
β On β© {π₯ β On β£ π΄ β (β΅βπ₯)} = suc π¦ β¨ Lim β© {π₯ β On β£ π΄ β (β΅βπ₯)}))) |
95 | 94 | adantl 483 |
. 2
β’ ((Ο
β π΄ β§
(cardβπ΄) = π΄) β (β© {π₯
β On β£ π΄ β
(β΅βπ₯)} =
β
β¨ (βπ¦
β On β© {π₯ β On β£ π΄ β (β΅βπ₯)} = suc π¦ β¨ Lim β© {π₯ β On β£ π΄ β (β΅βπ₯)}))) |
96 | 29, 88, 95 | mpjaod 859 |
1
β’ ((Ο
β π΄ β§
(cardβπ΄) = π΄) β π΄ = (β΅ββ© {π₯
β On β£ π΄ β
(β΅βπ₯)})) |