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