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 ⁡ A y ≺ ℵ ⁡ suc ⁡ A
5 3 4 mpbi ⊢ ℵ ⁡ suc ⁡ A ∈ On ∧ ∀ y ∈ ℵ ⁡ suc ⁡ A y ≺ ℵ ⁡ suc ⁡ A
6 5 simpri ⊢ ∀ y ∈ ℵ ⁡ suc ⁡ A y ≺ ℵ ⁡ 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