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 ) → ( ( ℵ ‘ 𝐴 ) ⊆ 𝐵 ↔ ( ℵ ‘ 𝐴 ) ≼ 𝐵 ) )