Metamath Proof Explorer

Theorem alephdom2

Description: A dominated initial ordinal is included. (Contributed by Jeff Hankins, 24-Oct-2009)

Ref Expression
Assertion alephdom2 ⊢ A ∈ On ∧ B ∈ On → ℵ ⁡ A ⊆ B ↔ ℵ ⁡ A ≼ B

Proof

Step Hyp Ref Expression
1 alephsdom ⊢ B ∈ On ∧ A ∈ On → B ∈ ℵ ⁡ A ↔ B ≺ ℵ ⁡ A
2 1 ancoms ⊢ A ∈ On ∧ B ∈ On → B ∈ ℵ ⁡ A ↔ B ≺ ℵ ⁡ A
3 2 notbid ⊢ A ∈ On ∧ B ∈ On → ¬ B ∈ ℵ ⁡ A ↔ ¬ B ≺ ℵ ⁡ A
4 alephon ⊢ ℵ ⁡ A ∈ On
5 4 onordi ⊢ Ord ⁡ ℵ ⁡ A
6 eloni ⊢ B ∈ On → Ord ⁡ B
7 ordtri1 ⊢ Ord ⁡ ℵ ⁡ A ∧ Ord ⁡ B → ℵ ⁡ A ⊆ B ↔ ¬ B ∈ ℵ ⁡ A
8 5 6 7 sylancr ⊢ B ∈ On → ℵ ⁡ A ⊆ B ↔ ¬ B ∈ ℵ ⁡ A
9 8 adantl ⊢ A ∈ On ∧ B ∈ On → ℵ ⁡ A ⊆ B ↔ ¬ B ∈ ℵ ⁡ A
10 domtriord ⊢ ℵ ⁡ A ∈ On ∧ B ∈ On → ℵ ⁡ A ≼ B ↔ ¬ B ≺ ℵ ⁡ A
11 4 10 mpan ⊢ B ∈ On → ℵ ⁡ A ≼ B ↔ ¬ B ≺ ℵ ⁡ A
12 11 adantl ⊢ A ∈ On ∧ B ∈ On → ℵ ⁡ A ≼ B ↔ ¬ B ≺ ℵ ⁡ A
13 3 9 12 3bitr4d ⊢ A ∈ On ∧ B ∈ On → ℵ ⁡ A ⊆ B ↔ ℵ ⁡ A ≼ B