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 ) } )