Metamath Proof Explorer

Theorem alephord2i

Description: Ordering property of the aleph function. Theorem 66 of Suppes p. 229. (Contributed by NM, 25-Oct-2003)

Ref Expression
Assertion alephord2i ⊢ B ∈ On → A ∈ B → ℵ ⁡ A ∈ ℵ ⁡ B

Proof

Step Hyp Ref Expression
1 onelon ⊢ B ∈ On ∧ A ∈ B → A ∈ On
2 alephord2 ⊢ A ∈ On ∧ B ∈ On → A ∈ B ↔ ℵ ⁡ A ∈ ℵ ⁡ B
3 2 biimpd ⊢ A ∈ On ∧ B ∈ On → A ∈ B → ℵ ⁡ A ∈ ℵ ⁡ B
4 3 expimpd ⊢ A ∈ On → B ∈ On ∧ A ∈ B → ℵ ⁡ A ∈ ℵ ⁡ B
5 1 4 mpcom ⊢ B ∈ On ∧ A ∈ B → ℵ ⁡ A ∈ ℵ ⁡ B
6 5 ex ⊢ B ∈ On → A ∈ B → ℵ ⁡ A ∈ ℵ ⁡ B