This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 ≼ 𝐵 ↔ ¬ 𝐵 ≺ 𝐴 ) )

Proof

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