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