Metamath Proof Explorer

Theorem alephord3

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

Ref Expression
Assertion alephord3 ⊢ A ∈ On ∧ B ∈ On → A ⊆ B ↔ ℵ ⁡ A ⊆ ℵ ⁡ B

Proof

Step Hyp Ref Expression
1 alephord2 ⊢ 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 ontri1 ⊢ A ∈ On ∧ B ∈ On → A ⊆ B ↔ ¬ B ∈ A
5 alephon ⊢ ℵ ⁡ A ∈ On
6 alephon ⊢ ℵ ⁡ B ∈ On
7 ontri1 ⊢ ℵ ⁡ A ∈ On ∧ ℵ ⁡ B ∈ On → ℵ ⁡ A ⊆ ℵ ⁡ B ↔ ¬ ℵ ⁡ B ∈ ℵ ⁡ A
8 5 6 7 mp2an ⊢ ℵ ⁡ A ⊆ ℵ ⁡ B ↔ ¬ ℵ ⁡ B ∈ ℵ ⁡ A
9 8 a1i ⊢ A ∈ On ∧ B ∈ On → ℵ ⁡ A ⊆ ℵ ⁡ B ↔ ¬ ℵ ⁡ B ∈ ℵ ⁡ A
10 3 4 9 3bitr4d ⊢ A ∈ On ∧ B ∈ On → A ⊆ B ↔ ℵ ⁡ A ⊆ ℵ ⁡ B