This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem alephdom2

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

Ref Expression
Assertion alephdom2 ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ( ℵ ‘ 𝐴 ) ⊆ 𝐵 ↔ ( ℵ ‘ 𝐴 ) ≼ 𝐵 ) )

Proof

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