Metamath Proof Explorer

Theorem alephsuc3

Description: An alternate representation of a successor aleph. Compare alephsuc and alephsuc2 . Equality can be obtained by taking the card of the right-hand side then using alephcard and carden . (Contributed by NM, 23-Oct-2004)

Ref Expression
Assertion alephsuc3 
|- ( A e. On -> ( aleph ` suc A ) ~~ { x e. On | x ~~ ( aleph ` A ) } )

Proof

Step Hyp Ref Expression
1 alephsuc2 
 |-  ( A e. On -> ( aleph ` suc A ) = { x e. On | x ~<_ ( aleph ` A ) } )
2 alephcard 
 |-  ( card ` ( aleph ` A ) ) = ( aleph ` A )
3 alephon 
 |-  ( aleph ` A ) e. On
4 onenon 
 |-  ( ( aleph ` A ) e. On -> ( aleph ` A ) e. dom card )
5 3 4 ax-mp 
 |-  ( aleph ` A ) e. dom card
6 cardval2 
 |-  ( ( aleph ` A ) e. dom card -> ( card ` ( aleph ` A ) ) = { x e. On | x ~< ( aleph ` A ) } )
7 5 6 ax-mp 
 |-  ( card ` ( aleph ` A ) ) = { x e. On | x ~< ( aleph ` A ) }
8 2 7 eqtr3i 
 |-  ( aleph ` A ) = { x e. On | x ~< ( aleph ` A ) }
9 8 a1i 
 |-  ( A e. On -> ( aleph ` A ) = { x e. On | x ~< ( aleph ` A ) } )
10 1 9 difeq12d 
 |-  ( A e. On -> ( ( aleph ` suc A ) \ ( aleph ` A ) ) = ( { x e. On | x ~<_ ( aleph ` A ) } \ { x e. On | x ~< ( aleph ` A ) } ) )
11 difrab 
 |-  ( { x e. On | x ~<_ ( aleph ` A ) } \ { x e. On | x ~< ( aleph ` A ) } ) = { x e. On | ( x ~<_ ( aleph ` A ) /\ -. x ~< ( aleph ` A ) ) }
12 bren2 
 |-  ( x ~~ ( aleph ` A ) <-> ( x ~<_ ( aleph ` A ) /\ -. x ~< ( aleph ` A ) ) )
13 12 rabbii 
 |-  { x e. On | x ~~ ( aleph ` A ) } = { x e. On | ( x ~<_ ( aleph ` A ) /\ -. x ~< ( aleph ` A ) ) }
14 11 13 eqtr4i 
 |-  ( { x e. On | x ~<_ ( aleph ` A ) } \ { x e. On | x ~< ( aleph ` A ) } ) = { x e. On | x ~~ ( aleph ` A ) }
15 10 14 eqtr2di 
 |-  ( A e. On -> { x e. On | x ~~ ( aleph ` A ) } = ( ( aleph ` suc A ) \ ( aleph ` A ) ) )
16 alephon 
 |-  ( aleph ` suc A ) e. On
17 onenon 
 |-  ( ( aleph ` suc A ) e. On -> ( aleph ` suc A ) e. dom card )
18 16 17 mp1i 
 |-  ( A e. On -> ( aleph ` suc A ) e. dom card )
19 sucelon 
 |-  ( A e. On <-> suc A e. On )
20 alephgeom 
 |-  ( suc A e. On <-> _om C_ ( aleph ` suc A ) )
21 19 20 bitri 
 |-  ( A e. On <-> _om C_ ( aleph ` suc A ) )
22 fvex 
 |-  ( aleph ` suc A ) e. _V
23 ssdomg 
 |-  ( ( aleph ` suc A ) e. _V -> ( _om C_ ( aleph ` suc A ) -> _om ~<_ ( aleph ` suc A ) ) )
24 22 23 ax-mp 
 |-  ( _om C_ ( aleph ` suc A ) -> _om ~<_ ( aleph ` suc A ) )
25 21 24 sylbi 
 |-  ( A e. On -> _om ~<_ ( aleph ` suc A ) )
26 alephordilem1 
 |-  ( A e. On -> ( aleph ` A ) ~< ( aleph ` suc A ) )
27 infdif 
 |-  ( ( ( aleph ` suc A ) e. dom card /\ _om ~<_ ( aleph ` suc A ) /\ ( aleph ` A ) ~< ( aleph ` suc A ) ) -> ( ( aleph ` suc A ) \ ( aleph ` A ) ) ~~ ( aleph ` suc A ) )
28 18 25 26 27 syl3anc 
 |-  ( A e. On -> ( ( aleph ` suc A ) \ ( aleph ` A ) ) ~~ ( aleph ` suc A ) )
29 15 28 eqbrtrd 
 |-  ( A e. On -> { x e. On | x ~~ ( aleph ` A ) } ~~ ( aleph ` suc A ) )
30 29 ensymd 
 |-  ( A e. On -> ( aleph ` suc A ) ~~ { x e. On | x ~~ ( aleph ` A ) } )