Theorem ordtri3or

Description: A trichotomy law for ordinals. Proposition 7.10 of TakeutiZaring p. 38. (Contributed by NM, 10-May-1994) (Proof shortened by Andrew Salmon, 25-Jul-2011)

	Ref	Expression
Assertion	ordtri3or	⊢ ( ( Ord 𝐴 ∧ Ord 𝐵 ) → ( 𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		ordin	⊢ ( ( Ord 𝐴 ∧ Ord 𝐵 ) → Ord ( 𝐴 ∩ 𝐵 ) )
2		ordirr	⊢ ( Ord ( 𝐴 ∩ 𝐵 ) → ¬ ( 𝐴 ∩ 𝐵 ) ∈ ( 𝐴 ∩ 𝐵 ) )
3	1 2	syl	⊢ ( ( Ord 𝐴 ∧ Ord 𝐵 ) → ¬ ( 𝐴 ∩ 𝐵 ) ∈ ( 𝐴 ∩ 𝐵 ) )
4		ianor	⊢ ( ¬ ( ( 𝐴 ∩ 𝐵 ) ∈ 𝐴 ∧ ( 𝐵 ∩ 𝐴 ) ∈ 𝐵 ) ↔ ( ¬ ( 𝐴 ∩ 𝐵 ) ∈ 𝐴 ∨ ¬ ( 𝐵 ∩ 𝐴 ) ∈ 𝐵 ) )
5		elin	⊢ ( ( 𝐴 ∩ 𝐵 ) ∈ ( 𝐴 ∩ 𝐵 ) ↔ ( ( 𝐴 ∩ 𝐵 ) ∈ 𝐴 ∧ ( 𝐴 ∩ 𝐵 ) ∈ 𝐵 ) )
6		incom	⊢ ( 𝐴 ∩ 𝐵 ) = ( 𝐵 ∩ 𝐴 )
7	6	eleq1i	⊢ ( ( 𝐴 ∩ 𝐵 ) ∈ 𝐵 ↔ ( 𝐵 ∩ 𝐴 ) ∈ 𝐵 )
8	7	anbi2i	⊢ ( ( ( 𝐴 ∩ 𝐵 ) ∈ 𝐴 ∧ ( 𝐴 ∩ 𝐵 ) ∈ 𝐵 ) ↔ ( ( 𝐴 ∩ 𝐵 ) ∈ 𝐴 ∧ ( 𝐵 ∩ 𝐴 ) ∈ 𝐵 ) )
9	5 8	bitri	⊢ ( ( 𝐴 ∩ 𝐵 ) ∈ ( 𝐴 ∩ 𝐵 ) ↔ ( ( 𝐴 ∩ 𝐵 ) ∈ 𝐴 ∧ ( 𝐵 ∩ 𝐴 ) ∈ 𝐵 ) )
10	4 9	xchnxbir	⊢ ( ¬ ( 𝐴 ∩ 𝐵 ) ∈ ( 𝐴 ∩ 𝐵 ) ↔ ( ¬ ( 𝐴 ∩ 𝐵 ) ∈ 𝐴 ∨ ¬ ( 𝐵 ∩ 𝐴 ) ∈ 𝐵 ) )
11	3 10	sylib	⊢ ( ( Ord 𝐴 ∧ Ord 𝐵 ) → ( ¬ ( 𝐴 ∩ 𝐵 ) ∈ 𝐴 ∨ ¬ ( 𝐵 ∩ 𝐴 ) ∈ 𝐵 ) )
12		inss1	⊢ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐴
13		ordsseleq	⊢ ( ( Ord ( 𝐴 ∩ 𝐵 ) ∧ Ord 𝐴 ) → ( ( 𝐴 ∩ 𝐵 ) ⊆ 𝐴 ↔ ( ( 𝐴 ∩ 𝐵 ) ∈ 𝐴 ∨ ( 𝐴 ∩ 𝐵 ) = 𝐴 ) ) )
14	12 13	mpbii	⊢ ( ( Ord ( 𝐴 ∩ 𝐵 ) ∧ Ord 𝐴 ) → ( ( 𝐴 ∩ 𝐵 ) ∈ 𝐴 ∨ ( 𝐴 ∩ 𝐵 ) = 𝐴 ) )
15	1 14	sylan	⊢ ( ( ( Ord 𝐴 ∧ Ord 𝐵 ) ∧ Ord 𝐴 ) → ( ( 𝐴 ∩ 𝐵 ) ∈ 𝐴 ∨ ( 𝐴 ∩ 𝐵 ) = 𝐴 ) )
16	15	anabss1	⊢ ( ( Ord 𝐴 ∧ Ord 𝐵 ) → ( ( 𝐴 ∩ 𝐵 ) ∈ 𝐴 ∨ ( 𝐴 ∩ 𝐵 ) = 𝐴 ) )
17	16	ord	⊢ ( ( Ord 𝐴 ∧ Ord 𝐵 ) → ( ¬ ( 𝐴 ∩ 𝐵 ) ∈ 𝐴 → ( 𝐴 ∩ 𝐵 ) = 𝐴 ) )
18		df-ss	⊢ ( 𝐴 ⊆ 𝐵 ↔ ( 𝐴 ∩ 𝐵 ) = 𝐴 )
19	17 18	syl6ibr	⊢ ( ( Ord 𝐴 ∧ Ord 𝐵 ) → ( ¬ ( 𝐴 ∩ 𝐵 ) ∈ 𝐴 → 𝐴 ⊆ 𝐵 ) )
20		ordin	⊢ ( ( Ord 𝐵 ∧ Ord 𝐴 ) → Ord ( 𝐵 ∩ 𝐴 ) )
21		inss1	⊢ ( 𝐵 ∩ 𝐴 ) ⊆ 𝐵
22		ordsseleq	⊢ ( ( Ord ( 𝐵 ∩ 𝐴 ) ∧ Ord 𝐵 ) → ( ( 𝐵 ∩ 𝐴 ) ⊆ 𝐵 ↔ ( ( 𝐵 ∩ 𝐴 ) ∈ 𝐵 ∨ ( 𝐵 ∩ 𝐴 ) = 𝐵 ) ) )
23	21 22	mpbii	⊢ ( ( Ord ( 𝐵 ∩ 𝐴 ) ∧ Ord 𝐵 ) → ( ( 𝐵 ∩ 𝐴 ) ∈ 𝐵 ∨ ( 𝐵 ∩ 𝐴 ) = 𝐵 ) )
24	20 23	sylan	⊢ ( ( ( Ord 𝐵 ∧ Ord 𝐴 ) ∧ Ord 𝐵 ) → ( ( 𝐵 ∩ 𝐴 ) ∈ 𝐵 ∨ ( 𝐵 ∩ 𝐴 ) = 𝐵 ) )
25	24	anabss4	⊢ ( ( Ord 𝐴 ∧ Ord 𝐵 ) → ( ( 𝐵 ∩ 𝐴 ) ∈ 𝐵 ∨ ( 𝐵 ∩ 𝐴 ) = 𝐵 ) )
26	25	ord	⊢ ( ( Ord 𝐴 ∧ Ord 𝐵 ) → ( ¬ ( 𝐵 ∩ 𝐴 ) ∈ 𝐵 → ( 𝐵 ∩ 𝐴 ) = 𝐵 ) )
27		df-ss	⊢ ( 𝐵 ⊆ 𝐴 ↔ ( 𝐵 ∩ 𝐴 ) = 𝐵 )
28	26 27	syl6ibr	⊢ ( ( Ord 𝐴 ∧ Ord 𝐵 ) → ( ¬ ( 𝐵 ∩ 𝐴 ) ∈ 𝐵 → 𝐵 ⊆ 𝐴 ) )
29	19 28	orim12d	⊢ ( ( Ord 𝐴 ∧ Ord 𝐵 ) → ( ( ¬ ( 𝐴 ∩ 𝐵 ) ∈ 𝐴 ∨ ¬ ( 𝐵 ∩ 𝐴 ) ∈ 𝐵 ) → ( 𝐴 ⊆ 𝐵 ∨ 𝐵 ⊆ 𝐴 ) ) )
30	11 29	mpd	⊢ ( ( Ord 𝐴 ∧ Ord 𝐵 ) → ( 𝐴 ⊆ 𝐵 ∨ 𝐵 ⊆ 𝐴 ) )
31		sspsstri	⊢ ( ( 𝐴 ⊆ 𝐵 ∨ 𝐵 ⊆ 𝐴 ) ↔ ( 𝐴 ⊊ 𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵 ⊊ 𝐴 ) )
32	30 31	sylib	⊢ ( ( Ord 𝐴 ∧ Ord 𝐵 ) → ( 𝐴 ⊊ 𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵 ⊊ 𝐴 ) )
33		ordelpss	⊢ ( ( Ord 𝐴 ∧ Ord 𝐵 ) → ( 𝐴 ∈ 𝐵 ↔ 𝐴 ⊊ 𝐵 ) )
34		biidd	⊢ ( ( Ord 𝐴 ∧ Ord 𝐵 ) → ( 𝐴 = 𝐵 ↔ 𝐴 = 𝐵 ) )
35		ordelpss	⊢ ( ( Ord 𝐵 ∧ Ord 𝐴 ) → ( 𝐵 ∈ 𝐴 ↔ 𝐵 ⊊ 𝐴 ) )
36	35	ancoms	⊢ ( ( Ord 𝐴 ∧ Ord 𝐵 ) → ( 𝐵 ∈ 𝐴 ↔ 𝐵 ⊊ 𝐴 ) )
37	33 34 36	3orbi123d	⊢ ( ( Ord 𝐴 ∧ Ord 𝐵 ) → ( ( 𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴 ) ↔ ( 𝐴 ⊊ 𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵 ⊊ 𝐴 ) ) )
38	32 37	mpbird	⊢ ( ( Ord 𝐴 ∧ Ord 𝐵 ) → ( 𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴 ) )