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