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 syl6ib ( ( 𝐴 ∈ 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 syl6ibr ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ¬ 𝐴𝐵𝐵𝐴 ) )
25 24 con1d ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ¬ 𝐵𝐴𝐴𝐵 ) )
26 7 25 impbid ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴𝐵 ↔ ¬ 𝐵𝐴 ) )