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	⊢ ( 𝐴 ∈ On → ( ℵ ‘ suc 𝐴 ) = { 𝑥 ∈ On ∣ 𝑥 ≼ ( ℵ ‘ 𝐴 ) } )

Proof

Step	Hyp	Ref	Expression
1		alephon	⊢ ( ℵ ‘ suc 𝐴 ) ∈ On
2	1	oneli	⊢ ( 𝑦 ∈ ( ℵ ‘ suc 𝐴 ) → 𝑦 ∈ On )
3		alephcard	⊢ ( card ‘ ( ℵ ‘ suc 𝐴 ) ) = ( ℵ ‘ suc 𝐴 )
4		iscard	⊢ ( ( card ‘ ( ℵ ‘ suc 𝐴 ) ) = ( ℵ ‘ suc 𝐴 ) ↔ ( ( ℵ ‘ suc 𝐴 ) ∈ On ∧ ∀ 𝑦 ∈ ( ℵ ‘ suc 𝐴 ) 𝑦 ≺ ( ℵ ‘ suc 𝐴 ) ) )
5	3 4	mpbi	⊢ ( ( ℵ ‘ suc 𝐴 ) ∈ On ∧ ∀ 𝑦 ∈ ( ℵ ‘ suc 𝐴 ) 𝑦 ≺ ( ℵ ‘ suc 𝐴 ) )
6	5	simpri	⊢ ∀ 𝑦 ∈ ( ℵ ‘ suc 𝐴 ) 𝑦 ≺ ( ℵ ‘ suc 𝐴 )
7	6	rspec	⊢ ( 𝑦 ∈ ( ℵ ‘ suc 𝐴 ) → 𝑦 ≺ ( ℵ ‘ suc 𝐴 ) )
8	2 7	jca	⊢ ( 𝑦 ∈ ( ℵ ‘ suc 𝐴 ) → ( 𝑦 ∈ On ∧ 𝑦 ≺ ( ℵ ‘ suc 𝐴 ) ) )
9		sdomel	⊢ ( ( 𝑦 ∈ On ∧ ( ℵ ‘ suc 𝐴 ) ∈ On ) → ( 𝑦 ≺ ( ℵ ‘ suc 𝐴 ) → 𝑦 ∈ ( ℵ ‘ suc 𝐴 ) ) )
10	1 9	mpan2	⊢ ( 𝑦 ∈ On → ( 𝑦 ≺ ( ℵ ‘ suc 𝐴 ) → 𝑦 ∈ ( ℵ ‘ suc 𝐴 ) ) )
11	10	imp	⊢ ( ( 𝑦 ∈ On ∧ 𝑦 ≺ ( ℵ ‘ suc 𝐴 ) ) → 𝑦 ∈ ( ℵ ‘ suc 𝐴 ) )
12	8 11	impbii	⊢ ( 𝑦 ∈ ( ℵ ‘ suc 𝐴 ) ↔ ( 𝑦 ∈ On ∧ 𝑦 ≺ ( ℵ ‘ suc 𝐴 ) ) )
13		breq1	⊢ ( 𝑥 = 𝑦 → ( 𝑥 ≺ ( ℵ ‘ suc 𝐴 ) ↔ 𝑦 ≺ ( ℵ ‘ suc 𝐴 ) ) )
14	13	elrab	⊢ ( 𝑦 ∈ { 𝑥 ∈ On ∣ 𝑥 ≺ ( ℵ ‘ suc 𝐴 ) } ↔ ( 𝑦 ∈ On ∧ 𝑦 ≺ ( ℵ ‘ suc 𝐴 ) ) )
15	12 14	bitr4i	⊢ ( 𝑦 ∈ ( ℵ ‘ suc 𝐴 ) ↔ 𝑦 ∈ { 𝑥 ∈ On ∣ 𝑥 ≺ ( ℵ ‘ suc 𝐴 ) } )
16	15	eqriv	⊢ ( ℵ ‘ suc 𝐴 ) = { 𝑥 ∈ On ∣ 𝑥 ≺ ( ℵ ‘ suc 𝐴 ) }
17		alephsucdom	⊢ ( 𝐴 ∈ On → ( 𝑥 ≼ ( ℵ ‘ 𝐴 ) ↔ 𝑥 ≺ ( ℵ ‘ suc 𝐴 ) ) )
18	17	rabbidv	⊢ ( 𝐴 ∈ On → { 𝑥 ∈ On ∣ 𝑥 ≼ ( ℵ ‘ 𝐴 ) } = { 𝑥 ∈ On ∣ 𝑥 ≺ ( ℵ ‘ suc 𝐴 ) } )
19	16 18	eqtr4id	⊢ ( 𝐴 ∈ On → ( ℵ ‘ suc 𝐴 ) = { 𝑥 ∈ On ∣ 𝑥 ≼ ( ℵ ‘ 𝐴 ) } )