Theorem ordtri2or

Description: A trichotomy law for ordinal classes. (Contributed by NM, 13-Sep-2003) (Proof shortened by Andrew Salmon, 12-Aug-2011)

	Ref	Expression
Assertion	ordtri2or	⊢ ( ( Ord 𝐴 ∧ Ord 𝐵 ) → ( 𝐴 ∈ 𝐵 ∨ 𝐵 ⊆ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		ordtri1	⊢ ( ( Ord 𝐵 ∧ Ord 𝐴 ) → ( 𝐵 ⊆ 𝐴 ↔ ¬ 𝐴 ∈ 𝐵 ) )
2	1	ancoms	⊢ ( ( Ord 𝐴 ∧ Ord 𝐵 ) → ( 𝐵 ⊆ 𝐴 ↔ ¬ 𝐴 ∈ 𝐵 ) )
3	2	biimprd	⊢ ( ( Ord 𝐴 ∧ Ord 𝐵 ) → ( ¬ 𝐴 ∈ 𝐵 → 𝐵 ⊆ 𝐴 ) )
4	3	orrd	⊢ ( ( Ord 𝐴 ∧ Ord 𝐵 ) → ( 𝐴 ∈ 𝐵 ∨ 𝐵 ⊆ 𝐴 ) )