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