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 ( 𝐴 ∈ 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 ∣ 𝑥 ≼ ( ℵ ‘ 𝐴 ) } )