Metamath Proof Explorer

Theorem alephcard

Description: Every aleph is a cardinal number. Theorem 65 of Suppes p. 229. (Contributed by NM, 25-Oct-2003) (Revised by Mario Carneiro, 2-Feb-2013)

Ref Expression
Assertion alephcard 
|- ( card ` ( aleph ` A ) ) = ( aleph ` A )

Proof

Step Hyp Ref Expression
1 2fveq3 
 |-  ( x = (/) -> ( card ` ( aleph ` x ) ) = ( card ` ( aleph ` (/) ) ) )
2 fveq2 
 |-  ( x = (/) -> ( aleph ` x ) = ( aleph ` (/) ) )
3 1 2 eqeq12d 
 |-  ( x = (/) -> ( ( card ` ( aleph ` x ) ) = ( aleph ` x ) <-> ( card ` ( aleph ` (/) ) ) = ( aleph ` (/) ) ) )
4 2fveq3 
 |-  ( x = y -> ( card ` ( aleph ` x ) ) = ( card ` ( aleph ` y ) ) )
5 fveq2 
 |-  ( x = y -> ( aleph ` x ) = ( aleph ` y ) )
6 4 5 eqeq12d 
 |-  ( x = y -> ( ( card ` ( aleph ` x ) ) = ( aleph ` x ) <-> ( card ` ( aleph ` y ) ) = ( aleph ` y ) ) )
7 2fveq3 
 |-  ( x = suc y -> ( card ` ( aleph ` x ) ) = ( card ` ( aleph ` suc y ) ) )
8 fveq2 
 |-  ( x = suc y -> ( aleph ` x ) = ( aleph ` suc y ) )
9 7 8 eqeq12d 
 |-  ( x = suc y -> ( ( card ` ( aleph ` x ) ) = ( aleph ` x ) <-> ( card ` ( aleph ` suc y ) ) = ( aleph ` suc y ) ) )
10 2fveq3 
 |-  ( x = A -> ( card ` ( aleph ` x ) ) = ( card ` ( aleph ` A ) ) )
11 fveq2 
 |-  ( x = A -> ( aleph ` x ) = ( aleph ` A ) )
12 10 11 eqeq12d 
 |-  ( x = A -> ( ( card ` ( aleph ` x ) ) = ( aleph ` x ) <-> ( card ` ( aleph ` A ) ) = ( aleph ` A ) ) )
13 cardom 
 |-  ( card ` _om ) = _om
14 aleph0 
 |-  ( aleph ` (/) ) = _om
15 14 fveq2i 
 |-  ( card ` ( aleph ` (/) ) ) = ( card ` _om )
16 13 15 14 3eqtr4i 
 |-  ( card ` ( aleph ` (/) ) ) = ( aleph ` (/) )
17 harcard 
 |-  ( card ` ( har ` ( aleph ` y ) ) ) = ( har ` ( aleph ` y ) )
18 alephsuc 
 |-  ( y e. On -> ( aleph ` suc y ) = ( har ` ( aleph ` y ) ) )
19 18 fveq2d 
 |-  ( y e. On -> ( card ` ( aleph ` suc y ) ) = ( card ` ( har ` ( aleph ` y ) ) ) )
20 17 19 18 3eqtr4a 
 |-  ( y e. On -> ( card ` ( aleph ` suc y ) ) = ( aleph ` suc y ) )
21 20 a1d 
 |-  ( y e. On -> ( ( card ` ( aleph ` y ) ) = ( aleph ` y ) -> ( card ` ( aleph ` suc y ) ) = ( aleph ` suc y ) ) )
22 cardiun 
 |-  ( x e. _V -> ( A. y e. x ( card ` ( aleph ` y ) ) = ( aleph ` y ) -> ( card ` U_ y e. x ( aleph ` y ) ) = U_ y e. x ( aleph ` y ) ) )
23 22 elv 
 |-  ( A. y e. x ( card ` ( aleph ` y ) ) = ( aleph ` y ) -> ( card ` U_ y e. x ( aleph ` y ) ) = U_ y e. x ( aleph ` y ) )
24 23 adantl 
 |-  ( ( Lim x /\ A. y e. x ( card ` ( aleph ` y ) ) = ( aleph ` y ) ) -> ( card ` U_ y e. x ( aleph ` y ) ) = U_ y e. x ( aleph ` y ) )
25 vex 
 |-  x e. _V
26 alephlim 
 |-  ( ( x e. _V /\ Lim x ) -> ( aleph ` x ) = U_ y e. x ( aleph ` y ) )
27 25 26 mpan 
 |-  ( Lim x -> ( aleph ` x ) = U_ y e. x ( aleph ` y ) )
28 27 adantr 
 |-  ( ( Lim x /\ A. y e. x ( card ` ( aleph ` y ) ) = ( aleph ` y ) ) -> ( aleph ` x ) = U_ y e. x ( aleph ` y ) )
29 28 fveq2d 
 |-  ( ( Lim x /\ A. y e. x ( card ` ( aleph ` y ) ) = ( aleph ` y ) ) -> ( card ` ( aleph ` x ) ) = ( card ` U_ y e. x ( aleph ` y ) ) )
30 24 29 28 3eqtr4d 
 |-  ( ( Lim x /\ A. y e. x ( card ` ( aleph ` y ) ) = ( aleph ` y ) ) -> ( card ` ( aleph ` x ) ) = ( aleph ` x ) )
31 30 ex 
 |-  ( Lim x -> ( A. y e. x ( card ` ( aleph ` y ) ) = ( aleph ` y ) -> ( card ` ( aleph ` x ) ) = ( aleph ` x ) ) )
32 3 6 9 12 16 21 31 tfinds 
 |-  ( A e. On -> ( card ` ( aleph ` A ) ) = ( aleph ` A ) )
33 card0 
 |-  ( card ` (/) ) = (/)
34 alephfnon 
 |-  aleph Fn On
35 34 fndmi 
 |-  dom aleph = On
36 35 eleq2i 
 |-  ( A e. dom aleph <-> A e. On )
37 ndmfv 
 |-  ( -. A e. dom aleph -> ( aleph ` A ) = (/) )
38 36 37 sylnbir 
 |-  ( -. A e. On -> ( aleph ` A ) = (/) )
39 38 fveq2d 
 |-  ( -. A e. On -> ( card ` ( aleph ` A ) ) = ( card ` (/) ) )
40 33 39 38 3eqtr4a 
 |-  ( -. A e. On -> ( card ` ( aleph ` A ) ) = ( aleph ` A ) )
41 32 40 pm2.61i 
 |-  ( card ` ( aleph ` A ) ) = ( aleph ` A )