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∈On→ℵ⁡suc⁡A=x∈On|x≼ℵ⁡A

Proof

Step Hyp Ref Expression
1 alephon ⊢ℵ⁡suc⁡A∈On
2 1 oneli ⊢y∈ℵ⁡suc⁡A→y∈On
3 alephcard ⊢card⁡ℵ⁡suc⁡A=ℵ⁡suc⁡A
4 iscard ⊢card⁡ℵ⁡suc⁡A=ℵ⁡suc⁡A↔ℵ⁡suc⁡A∈On∧∀y∈ℵ⁡suc⁡Ay≺ℵ⁡suc⁡A
5 3 4 mpbi ⊢ℵ⁡suc⁡A∈On∧∀y∈ℵ⁡suc⁡Ay≺ℵ⁡suc⁡A
6 5 simpri ⊢∀y∈ℵ⁡suc⁡Ay≺ℵ⁡suc⁡A
7 6 rspec ⊢y∈ℵ⁡suc⁡A→y≺ℵ⁡suc⁡A
8 2 7 jca ⊢y∈ℵ⁡suc⁡A→y∈On∧y≺ℵ⁡suc⁡A
9 sdomel ⊢y∈On∧ℵ⁡suc⁡A∈On→y≺ℵ⁡suc⁡A→y∈ℵ⁡suc⁡A
10 1 9 mpan2 ⊢y∈On→y≺ℵ⁡suc⁡A→y∈ℵ⁡suc⁡A
11 10 imp ⊢y∈On∧y≺ℵ⁡suc⁡A→y∈ℵ⁡suc⁡A
12 8 11 impbii ⊢y∈ℵ⁡suc⁡A↔y∈On∧y≺ℵ⁡suc⁡A
13 breq1 ⊢x=y→x≺ℵ⁡suc⁡A↔y≺ℵ⁡suc⁡A
14 13 elrab ⊢y∈x∈On|x≺ℵ⁡suc⁡A↔y∈On∧y≺ℵ⁡suc⁡A
15 12 14 bitr4i ⊢y∈ℵ⁡suc⁡A↔y∈x∈On|x≺ℵ⁡suc⁡A
16 15 eqriv ⊢ℵ⁡suc⁡A=x∈On|x≺ℵ⁡suc⁡A
17 alephsucdom ⊢A∈On→x≼ℵ⁡A↔x≺ℵ⁡suc⁡A
18 17 rabbidv ⊢A∈On→x∈On|x≼ℵ⁡A=x∈On|x≺ℵ⁡suc⁡A
19 16 18 eqtr4id ⊢A∈On→ℵ⁡suc⁡A=x∈On|x≼ℵ⁡A