This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem alephsuc2

Description: An alternate representation of a successor aleph. The aleph function is the function obtained from the hartogs function by transfinite recursion, starting from _om . Using this theorem we could define the aleph function with { z e. On | z ~<_ x } in place of |^| { z e. On | x ~< z } in df-aleph . (Contributed by NM, 3-Nov-2003) (Revised by Mario Carneiro, 2-Feb-2013)

Ref Expression
Assertion alephsuc2 
|- ( A e. On -> ( aleph ` suc A ) = { x e. On | x ~<_ ( aleph ` A ) } )

Proof

Step Hyp Ref Expression
1 alephon 
 |-  ( aleph ` suc A ) e. On
2 1 oneli 
 |-  ( y e. ( aleph ` suc A ) -> y e. On )
3 alephcard 
 |-  ( card ` ( aleph ` suc A ) ) = ( aleph ` suc A )
4 iscard 
 |-  ( ( card ` ( aleph ` suc A ) ) = ( aleph ` suc A ) <-> ( ( aleph ` suc A ) e. On /\ A. y e. ( aleph ` suc A ) y ~< ( aleph ` suc A ) ) )
5 3 4 mpbi 
 |-  ( ( aleph ` suc A ) e. On /\ A. y e. ( aleph ` suc A ) y ~< ( aleph ` suc A ) )
6 5 simpri 
 |-  A. y e. ( aleph ` suc A ) y ~< ( aleph ` suc A )
7 6 rspec 
 |-  ( y e. ( aleph ` suc A ) -> y ~< ( aleph ` suc A ) )
8 2 7 jca 
 |-  ( y e. ( aleph ` suc A ) -> ( y e. On /\ y ~< ( aleph ` suc A ) ) )
9 sdomel 
 |-  ( ( y e. On /\ ( aleph ` suc A ) e. On ) -> ( y ~< ( aleph ` suc A ) -> y e. ( aleph ` suc A ) ) )
10 1 9 mpan2 
 |-  ( y e. On -> ( y ~< ( aleph ` suc A ) -> y e. ( aleph ` suc A ) ) )
11 10 imp 
 |-  ( ( y e. On /\ y ~< ( aleph ` suc A ) ) -> y e. ( aleph ` suc A ) )
12 8 11 impbii 
 |-  ( y e. ( aleph ` suc A ) <-> ( y e. On /\ y ~< ( aleph ` suc A ) ) )
13 breq1 
 |-  ( x = y -> ( x ~< ( aleph ` suc A ) <-> y ~< ( aleph ` suc A ) ) )
14 13 elrab 
 |-  ( y e. { x e. On | x ~< ( aleph ` suc A ) } <-> ( y e. On /\ y ~< ( aleph ` suc A ) ) )
15 12 14 bitr4i 
 |-  ( y e. ( aleph ` suc A ) <-> y e. { x e. On | x ~< ( aleph ` suc A ) } )
16 15 eqriv 
 |-  ( aleph ` suc A ) = { x e. On | x ~< ( aleph ` suc A ) }
17 alephsucdom 
 |-  ( A e. On -> ( x ~<_ ( aleph ` A ) <-> x ~< ( aleph ` suc A ) ) )
18 17 rabbidv 
 |-  ( A e. On -> { x e. On | x ~<_ ( aleph ` A ) } = { x e. On | x ~< ( aleph ` suc A ) } )
19 16 18 eqtr4id 
 |-  ( A e. On -> ( aleph ` suc A ) = { x e. On | x ~<_ ( aleph ` A ) } )