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

Metamath Proof Explorer

Theorem ordtri3or

Description: A trichotomy law for ordinals. Proposition 7.10 of TakeutiZaring p. 38. Theorem 1.9(iii) of Schloeder p. 1. (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 dfss2 ⊢ ( 𝐴 ⊆ 𝐵 ↔ ( 𝐴 ∩ 𝐵 ) = 𝐴 )
19 17 18 imbitrrdi ⊢ ( ( 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 dfss2 ⊢ ( 𝐵 ⊆ 𝐴 ↔ ( 𝐵 ∩ 𝐴 ) = 𝐵 )
28 26 27 imbitrrdi ⊢ ( ( 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 𝐵 ) → ( 𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴 ) )