Metamath Proof Explorer

Theorem aleph11

Description: The aleph function is one-to-one. (Contributed by NM, 3-Aug-2004)

Ref Expression
Assertion aleph11 ⊢ A ∈ On ∧ B ∈ On → ℵ ⁡ A = ℵ ⁡ B ↔ A = B

Proof

Step Hyp Ref Expression
1 alephord3 ⊢ A ∈ On ∧ B ∈ On → A ⊆ B ↔ ℵ ⁡ A ⊆ ℵ ⁡ B
2 alephord3 ⊢ B ∈ On ∧ A ∈ On → B ⊆ A ↔ ℵ ⁡ B ⊆ ℵ ⁡ A
3 2 ancoms ⊢ A ∈ On ∧ B ∈ On → B ⊆ A ↔ ℵ ⁡ B ⊆ ℵ ⁡ A
4 1 3 anbi12d ⊢ A ∈ On ∧ B ∈ On → A ⊆ B ∧ B ⊆ A ↔ ℵ ⁡ A ⊆ ℵ ⁡ B ∧ ℵ ⁡ B ⊆ ℵ ⁡ A
5 eqss ⊢ A = B ↔ A ⊆ B ∧ B ⊆ A
6 eqss ⊢ ℵ ⁡ A = ℵ ⁡ B ↔ ℵ ⁡ A ⊆ ℵ ⁡ B ∧ ℵ ⁡ B ⊆ ℵ ⁡ A
7 4 5 6 3bitr4g ⊢ A ∈ On ∧ B ∈ On → A = B ↔ ℵ ⁡ A = ℵ ⁡ B
8 7 bicomd ⊢ A ∈ On ∧ B ∈ On → ℵ ⁡ A = ℵ ⁡ B ↔ A = B