Metamath Proof Explorer

Theorem domtriord

Description: Dominance is trichotomous in the restricted case of ordinal numbers. (Contributed by Jeff Hankins, 24-Oct-2009)

Ref Expression
Assertion domtriord ⊢ A ∈ On ∧ B ∈ On → A ≼ B ↔ ¬ B ≺ A

Proof

Step Hyp Ref Expression
1 sbth ⊢ B ≼ A ∧ A ≼ B → B ≈ A
2 1 expcom ⊢ A ≼ B → B ≼ A → B ≈ A
3 2 a1i ⊢ A ∈ On ∧ B ∈ On → A ≼ B → B ≼ A → B ≈ A
4 iman ⊢ B ≼ A → B ≈ A ↔ ¬ B ≼ A ∧ ¬ B ≈ A
5 brsdom ⊢ B ≺ A ↔ B ≼ A ∧ ¬ B ≈ A
6 4 5 xchbinxr ⊢ B ≼ A → B ≈ A ↔ ¬ B ≺ A
7 3 6 syl6ib ⊢ A ∈ On ∧ B ∈ On → A ≼ B → ¬ B ≺ A
8 onelss ⊢ B ∈ On → A ∈ B → A ⊆ B
9 ssdomg ⊢ B ∈ On → A ⊆ B → A ≼ B
10 8 9 syld ⊢ B ∈ On → A ∈ B → A ≼ B
11 10 adantl ⊢ A ∈ On ∧ B ∈ On → A ∈ B → A ≼ B
12 11 con3d ⊢ A ∈ On ∧ B ∈ On → ¬ A ≼ B → ¬ A ∈ B
13 ontri1 ⊢ B ∈ On ∧ A ∈ On → B ⊆ A ↔ ¬ A ∈ B
14 13 ancoms ⊢ A ∈ On ∧ B ∈ On → B ⊆ A ↔ ¬ A ∈ B
15 12 14 sylibrd ⊢ A ∈ On ∧ B ∈ On → ¬ A ≼ B → B ⊆ A
16 ssdomg ⊢ A ∈ On → B ⊆ A → B ≼ A
17 16 adantr ⊢ A ∈ On ∧ B ∈ On → B ⊆ A → B ≼ A
18 15 17 syld ⊢ A ∈ On ∧ B ∈ On → ¬ A ≼ B → B ≼ A
19 ensym ⊢ B ≈ A → A ≈ B
20 endom ⊢ A ≈ B → A ≼ B
21 19 20 syl ⊢ B ≈ A → A ≼ B
22 21 con3i ⊢ ¬ A ≼ B → ¬ B ≈ A
23 18 22 jca2 ⊢ A ∈ On ∧ B ∈ On → ¬ A ≼ B → B ≼ A ∧ ¬ B ≈ A
24 23 5 syl6ibr ⊢ A ∈ On ∧ B ∈ On → ¬ A ≼ B → B ≺ A
25 24 con1d ⊢ A ∈ On ∧ B ∈ On → ¬ B ≺ A → A ≼ B
26 7 25 impbid ⊢ A ∈ On ∧ B ∈ On → A ≼ B ↔ ¬ B ≺ A