Step | Hyp | Ref
| Expression |
1 | | 2fveq3 6886 |
. . . 4
β’ (π₯ = β
β
(cardβ(β΅βπ₯)) =
(cardβ(β΅ββ
))) |
2 | | fveq2 6881 |
. . . 4
β’ (π₯ = β
β
(β΅βπ₯) =
(β΅ββ
)) |
3 | 1, 2 | eqeq12d 2740 |
. . 3
β’ (π₯ = β
β
((cardβ(β΅βπ₯)) = (β΅βπ₯) β (cardβ(β΅ββ
))
= (β΅ββ
))) |
4 | | 2fveq3 6886 |
. . . 4
β’ (π₯ = π¦ β (cardβ(β΅βπ₯)) =
(cardβ(β΅βπ¦))) |
5 | | fveq2 6881 |
. . . 4
β’ (π₯ = π¦ β (β΅βπ₯) = (β΅βπ¦)) |
6 | 4, 5 | eqeq12d 2740 |
. . 3
β’ (π₯ = π¦ β ((cardβ(β΅βπ₯)) = (β΅βπ₯) β
(cardβ(β΅βπ¦)) = (β΅βπ¦))) |
7 | | 2fveq3 6886 |
. . . 4
β’ (π₯ = suc π¦ β (cardβ(β΅βπ₯)) =
(cardβ(β΅βsuc π¦))) |
8 | | fveq2 6881 |
. . . 4
β’ (π₯ = suc π¦ β (β΅βπ₯) = (β΅βsuc π¦)) |
9 | 7, 8 | eqeq12d 2740 |
. . 3
β’ (π₯ = suc π¦ β ((cardβ(β΅βπ₯)) = (β΅βπ₯) β
(cardβ(β΅βsuc π¦)) = (β΅βsuc π¦))) |
10 | | 2fveq3 6886 |
. . . 4
β’ (π₯ = π΄ β (cardβ(β΅βπ₯)) =
(cardβ(β΅βπ΄))) |
11 | | fveq2 6881 |
. . . 4
β’ (π₯ = π΄ β (β΅βπ₯) = (β΅βπ΄)) |
12 | 10, 11 | eqeq12d 2740 |
. . 3
β’ (π₯ = π΄ β ((cardβ(β΅βπ₯)) = (β΅βπ₯) β
(cardβ(β΅βπ΄)) = (β΅βπ΄))) |
13 | | cardom 9976 |
. . . 4
β’
(cardβΟ) = Ο |
14 | | aleph0 10056 |
. . . . 5
β’
(β΅ββ
) = Ο |
15 | 14 | fveq2i 6884 |
. . . 4
β’
(cardβ(β΅ββ
)) =
(cardβΟ) |
16 | 13, 15, 14 | 3eqtr4i 2762 |
. . 3
β’
(cardβ(β΅ββ
)) =
(β΅ββ
) |
17 | | harcard 9968 |
. . . . 5
β’
(cardβ(harβ(β΅βπ¦))) = (harβ(β΅βπ¦)) |
18 | | alephsuc 10058 |
. . . . . 6
β’ (π¦ β On β
(β΅βsuc π¦) =
(harβ(β΅βπ¦))) |
19 | 18 | fveq2d 6885 |
. . . . 5
β’ (π¦ β On β
(cardβ(β΅βsuc π¦)) =
(cardβ(harβ(β΅βπ¦)))) |
20 | 17, 19, 18 | 3eqtr4a 2790 |
. . . 4
β’ (π¦ β On β
(cardβ(β΅βsuc π¦)) = (β΅βsuc π¦)) |
21 | 20 | a1d 25 |
. . 3
β’ (π¦ β On β
((cardβ(β΅βπ¦)) = (β΅βπ¦) β (cardβ(β΅βsuc π¦)) = (β΅βsuc π¦))) |
22 | | cardiun 9972 |
. . . . . . 7
β’ (π₯ β V β (βπ¦ β π₯ (cardβ(β΅βπ¦)) = (β΅βπ¦) β (cardββͺ π¦ β π₯ (β΅βπ¦)) = βͺ
π¦ β π₯ (β΅βπ¦))) |
23 | 22 | elv 3472 |
. . . . . 6
β’
(βπ¦ β
π₯
(cardβ(β΅βπ¦)) = (β΅βπ¦) β (cardββͺ π¦ β π₯ (β΅βπ¦)) = βͺ
π¦ β π₯ (β΅βπ¦)) |
24 | 23 | adantl 481 |
. . . . 5
β’ ((Lim
π₯ β§ βπ¦ β π₯ (cardβ(β΅βπ¦)) = (β΅βπ¦)) β (cardββͺ π¦ β π₯ (β΅βπ¦)) = βͺ
π¦ β π₯ (β΅βπ¦)) |
25 | | vex 3470 |
. . . . . . . 8
β’ π₯ β V |
26 | | alephlim 10057 |
. . . . . . . 8
β’ ((π₯ β V β§ Lim π₯) β (β΅βπ₯) = βͺ π¦ β π₯ (β΅βπ¦)) |
27 | 25, 26 | mpan 687 |
. . . . . . 7
β’ (Lim
π₯ β
(β΅βπ₯) =
βͺ π¦ β π₯ (β΅βπ¦)) |
28 | 27 | adantr 480 |
. . . . . 6
β’ ((Lim
π₯ β§ βπ¦ β π₯ (cardβ(β΅βπ¦)) = (β΅βπ¦)) β (β΅βπ₯) = βͺ π¦ β π₯ (β΅βπ¦)) |
29 | 28 | fveq2d 6885 |
. . . . 5
β’ ((Lim
π₯ β§ βπ¦ β π₯ (cardβ(β΅βπ¦)) = (β΅βπ¦)) β
(cardβ(β΅βπ₯)) = (cardββͺ π¦ β π₯ (β΅βπ¦))) |
30 | 24, 29, 28 | 3eqtr4d 2774 |
. . . 4
β’ ((Lim
π₯ β§ βπ¦ β π₯ (cardβ(β΅βπ¦)) = (β΅βπ¦)) β
(cardβ(β΅βπ₯)) = (β΅βπ₯)) |
31 | 30 | ex 412 |
. . 3
β’ (Lim
π₯ β (βπ¦ β π₯ (cardβ(β΅βπ¦)) = (β΅βπ¦) β
(cardβ(β΅βπ₯)) = (β΅βπ₯))) |
32 | 3, 6, 9, 12, 16, 21, 31 | tfinds 7842 |
. 2
β’ (π΄ β On β
(cardβ(β΅βπ΄)) = (β΅βπ΄)) |
33 | | card0 9948 |
. . 3
β’
(cardββ
) = β
|
34 | | alephfnon 10055 |
. . . . . . 7
β’ β΅
Fn On |
35 | 34 | fndmi 6643 |
. . . . . 6
β’ dom
β΅ = On |
36 | 35 | eleq2i 2817 |
. . . . 5
β’ (π΄ β dom β΅ β π΄ β On) |
37 | | ndmfv 6916 |
. . . . 5
β’ (Β¬
π΄ β dom β΅ β
(β΅βπ΄) =
β
) |
38 | 36, 37 | sylnbir 331 |
. . . 4
β’ (Β¬
π΄ β On β
(β΅βπ΄) =
β
) |
39 | 38 | fveq2d 6885 |
. . 3
β’ (Β¬
π΄ β On β
(cardβ(β΅βπ΄)) = (cardββ
)) |
40 | 33, 39, 38 | 3eqtr4a 2790 |
. 2
β’ (Β¬
π΄ β On β
(cardβ(β΅βπ΄)) = (β΅βπ΄)) |
41 | 32, 40 | pm2.61i 182 |
1
β’
(cardβ(β΅βπ΄)) = (β΅βπ΄) |