Metamath Proof Explorer

Theorem ordtri1

Description: A trichotomy law for ordinals. (Contributed by NM, 25-Mar-1995) (Proof shortened by Andrew Salmon, 25-Jul-2011)

Ref Expression
Assertion ordtri1 ( ( Ord 𝐴 ∧ Ord 𝐵 ) → ( 𝐴 ⊆ 𝐵 ↔ ¬ 𝐵 ∈ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 ordsseleq ⊢ ( ( Ord 𝐴 ∧ Ord 𝐵 ) → ( 𝐴 ⊆ 𝐵 ↔ ( 𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵 ) ) )
2 ordn2lp ⊢ ( Ord 𝐴 → ¬ ( 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐴 ) )
3 imnan ⊢ ( ( 𝐴 ∈ 𝐵 → ¬ 𝐵 ∈ 𝐴 ) ↔ ¬ ( 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐴 ) )
4 2 3 sylibr ⊢ ( Ord 𝐴 → ( 𝐴 ∈ 𝐵 → ¬ 𝐵 ∈ 𝐴 ) )
5 ordirr ⊢ ( Ord 𝐵 → ¬ 𝐵 ∈ 𝐵 )
6 eleq2 ⊢ ( 𝐴 = 𝐵 → ( 𝐵 ∈ 𝐴 ↔ 𝐵 ∈ 𝐵 ) )
7 6 notbid ⊢ ( 𝐴 = 𝐵 → ( ¬ 𝐵 ∈ 𝐴 ↔ ¬ 𝐵 ∈ 𝐵 ) )
8 5 7 syl5ibrcom ⊢ ( Ord 𝐵 → ( 𝐴 = 𝐵 → ¬ 𝐵 ∈ 𝐴 ) )
9 4 8 jaao ⊢ ( ( Ord 𝐴 ∧ Ord 𝐵 ) → ( ( 𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵 ) → ¬ 𝐵 ∈ 𝐴 ) )
10 ordtri3or ⊢ ( ( Ord 𝐴 ∧ Ord 𝐵 ) → ( 𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴 ) )
11 df-3or ⊢ ( ( 𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴 ) ↔ ( ( 𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵 ) ∨ 𝐵 ∈ 𝐴 ) )
12 10 11 sylib ⊢ ( ( Ord 𝐴 ∧ Ord 𝐵 ) → ( ( 𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵 ) ∨ 𝐵 ∈ 𝐴 ) )
13 12 orcomd ⊢ ( ( Ord 𝐴 ∧ Ord 𝐵 ) → ( 𝐵 ∈ 𝐴 ∨ ( 𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵 ) ) )
14 13 ord ⊢ ( ( Ord 𝐴 ∧ Ord 𝐵 ) → ( ¬ 𝐵 ∈ 𝐴 → ( 𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵 ) ) )
15 9 14 impbid ⊢ ( ( Ord 𝐴 ∧ Ord 𝐵 ) → ( ( 𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵 ) ↔ ¬ 𝐵 ∈ 𝐴 ) )
16 1 15 bitrd ⊢ ( ( Ord 𝐴 ∧ Ord 𝐵 ) → ( 𝐴 ⊆ 𝐵 ↔ ¬ 𝐵 ∈ 𝐴 ) )