Metamath Proof Explorer

Theorem alephord

Description: Ordering property of the aleph function. (Contributed by NM, 26-Oct-2003) (Revised by Mario Carneiro, 9-Feb-2013)

Ref Expression
Assertion alephord ⊢ A ∈ On ∧ B ∈ On → A ∈ B ↔ ℵ ⁡ A ≺ ℵ ⁡ B

Proof

Step Hyp Ref Expression
1 alephordi ⊢ B ∈ On → A ∈ B → ℵ ⁡ A ≺ ℵ ⁡ B
2 1 adantl ⊢ A ∈ On ∧ B ∈ On → A ∈ B → ℵ ⁡ A ≺ ℵ ⁡ B
3 brsdom ⊢ ℵ ⁡ A ≺ ℵ ⁡ B ↔ ℵ ⁡ A ≼ ℵ ⁡ B ∧ ¬ ℵ ⁡ A ≈ ℵ ⁡ B
4 alephon ⊢ ℵ ⁡ A ∈ On
5 alephon ⊢ ℵ ⁡ B ∈ On
6 domtriord ⊢ ℵ ⁡ A ∈ On ∧ ℵ ⁡ B ∈ On → ℵ ⁡ A ≼ ℵ ⁡ B ↔ ¬ ℵ ⁡ B ≺ ℵ ⁡ A
7 4 5 6 mp2an ⊢ ℵ ⁡ A ≼ ℵ ⁡ B ↔ ¬ ℵ ⁡ B ≺ ℵ ⁡ A
8 alephordi ⊢ A ∈ On → B ∈ A → ℵ ⁡ B ≺ ℵ ⁡ A
9 8 con3d ⊢ A ∈ On → ¬ ℵ ⁡ B ≺ ℵ ⁡ A → ¬ B ∈ A
10 7 9 syl5bi ⊢ A ∈ On → ℵ ⁡ A ≼ ℵ ⁡ B → ¬ B ∈ A
11 10 adantr ⊢ A ∈ On ∧ B ∈ On → ℵ ⁡ A ≼ ℵ ⁡ B → ¬ B ∈ A
12 ontri1 ⊢ A ∈ On ∧ B ∈ On → A ⊆ B ↔ ¬ B ∈ A
13 11 12 sylibrd ⊢ A ∈ On ∧ B ∈ On → ℵ ⁡ A ≼ ℵ ⁡ B → A ⊆ B
14 fveq2 ⊢ A = B → ℵ ⁡ A = ℵ ⁡ B
15 eqeng ⊢ ℵ ⁡ A ∈ On → ℵ ⁡ A = ℵ ⁡ B → ℵ ⁡ A ≈ ℵ ⁡ B
16 4 14 15 mpsyl ⊢ A = B → ℵ ⁡ A ≈ ℵ ⁡ B
17 16 necon3bi ⊢ ¬ ℵ ⁡ A ≈ ℵ ⁡ B → A ≠ B
18 13 17 anim12d1 ⊢ A ∈ On ∧ B ∈ On → ℵ ⁡ A ≼ ℵ ⁡ B ∧ ¬ ℵ ⁡ A ≈ ℵ ⁡ B → A ⊆ B ∧ A ≠ B
19 onelpss ⊢ A ∈ On ∧ B ∈ On → A ∈ B ↔ A ⊆ B ∧ A ≠ B
20 18 19 sylibrd ⊢ A ∈ On ∧ B ∈ On → ℵ ⁡ A ≼ ℵ ⁡ B ∧ ¬ ℵ ⁡ A ≈ ℵ ⁡ B → A ∈ B
21 3 20 syl5bi ⊢ A ∈ On ∧ B ∈ On → ℵ ⁡ A ≺ ℵ ⁡ B → A ∈ B
22 2 21 impbid ⊢ A ∈ On ∧ B ∈ On → A ∈ B ↔ ℵ ⁡ A ≺ ℵ ⁡ B