Metamath Proof Explorer

Theorem alephord3

Description: Ordering property of the aleph function. (Contributed by NM, 11-Nov-2003)

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

Proof

Step Hyp Ref Expression
1 alephord2 ⊢ ( ( 𝐵 ∈ On ∧ 𝐴 ∈ On ) → ( 𝐵 ∈ 𝐴 ↔ ( ℵ ‘ 𝐵 ) ∈ ( ℵ ‘ 𝐴 ) ) )
2 1 ancoms ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐵 ∈ 𝐴 ↔ ( ℵ ‘ 𝐵 ) ∈ ( ℵ ‘ 𝐴 ) ) )
3 2 notbid ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ¬ 𝐵 ∈ 𝐴 ↔ ¬ ( ℵ ‘ 𝐵 ) ∈ ( ℵ ‘ 𝐴 ) ) )
4 ontri1 ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 ⊆ 𝐵 ↔ ¬ 𝐵 ∈ 𝐴 ) )
5 alephon ⊢ ( ℵ ‘ 𝐴 ) ∈ On
6 alephon ⊢ ( ℵ ‘ 𝐵 ) ∈ On
7 ontri1 ⊢ ( ( ( ℵ ‘ 𝐴 ) ∈ On ∧ ( ℵ ‘ 𝐵 ) ∈ On ) → ( ( ℵ ‘ 𝐴 ) ⊆ ( ℵ ‘ 𝐵 ) ↔ ¬ ( ℵ ‘ 𝐵 ) ∈ ( ℵ ‘ 𝐴 ) ) )
8 5 6 7 mp2an ⊢ ( ( ℵ ‘ 𝐴 ) ⊆ ( ℵ ‘ 𝐵 ) ↔ ¬ ( ℵ ‘ 𝐵 ) ∈ ( ℵ ‘ 𝐴 ) )
9 8 a1i ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ( ℵ ‘ 𝐴 ) ⊆ ( ℵ ‘ 𝐵 ) ↔ ¬ ( ℵ ‘ 𝐵 ) ∈ ( ℵ ‘ 𝐴 ) ) )
10 3 4 9 3bitr4d ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 ⊆ 𝐵 ↔ ( ℵ ‘ 𝐴 ) ⊆ ( ℵ ‘ 𝐵 ) ) )