Metamath Proof Explorer

Theorem alephord2

Description: Ordering property of the aleph function. Theorem 8A(a) of Enderton p. 213 and its converse. (Contributed by NM, 3-Nov-2003) (Revised by Mario Carneiro, 9-Feb-2013)

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

Proof

Step Hyp Ref Expression
1 alephord ⊢ A ∈ On ∧ B ∈ On → A ∈ B ↔ ℵ ⁡ A ≺ ℵ ⁡ B
2 alephon ⊢ ℵ ⁡ A ∈ On
3 alephon ⊢ ℵ ⁡ B ∈ On
4 onenon ⊢ ℵ ⁡ B ∈ On → ℵ ⁡ B ∈ dom ⁡ card
5 3 4 ax-mp ⊢ ℵ ⁡ B ∈ dom ⁡ card
6 cardsdomel ⊢ ℵ ⁡ A ∈ On ∧ ℵ ⁡ B ∈ dom ⁡ card → ℵ ⁡ A ≺ ℵ ⁡ B ↔ ℵ ⁡ A ∈ card ⁡ ℵ ⁡ B
7 2 5 6 mp2an ⊢ ℵ ⁡ A ≺ ℵ ⁡ B ↔ ℵ ⁡ A ∈ card ⁡ ℵ ⁡ B
8 alephcard ⊢ card ⁡ ℵ ⁡ B = ℵ ⁡ B
9 8 eleq2i ⊢ ℵ ⁡ A ∈ card ⁡ ℵ ⁡ B ↔ ℵ ⁡ A ∈ ℵ ⁡ B
10 7 9 bitri ⊢ ℵ ⁡ A ≺ ℵ ⁡ B ↔ ℵ ⁡ A ∈ ℵ ⁡ B
11 1 10 bitrdi ⊢ A ∈ On ∧ B ∈ On → A ∈ B ↔ ℵ ⁡ A ∈ ℵ ⁡ B