Theorem ordtri2or2

Description: A trichotomy law for ordinal classes. (Contributed by NM, 2-Nov-2003)

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

Proof

Step	Hyp	Ref	Expression
1		ordtri2or	⊢ ( ( Ord 𝐴 ∧ Ord 𝐵 ) → ( 𝐴 ∈ 𝐵 ∨ 𝐵 ⊆ 𝐴 ) )
2		ordelss	⊢ ( ( Ord 𝐵 ∧ 𝐴 ∈ 𝐵 ) → 𝐴 ⊆ 𝐵 )
3	2	ex	⊢ ( Ord 𝐵 → ( 𝐴 ∈ 𝐵 → 𝐴 ⊆ 𝐵 ) )
4	3	orim1d	⊢ ( Ord 𝐵 → ( ( 𝐴 ∈ 𝐵 ∨ 𝐵 ⊆ 𝐴 ) → ( 𝐴 ⊆ 𝐵 ∨ 𝐵 ⊆ 𝐴 ) ) )
5	4	adantl	⊢ ( ( Ord 𝐴 ∧ Ord 𝐵 ) → ( ( 𝐴 ∈ 𝐵 ∨ 𝐵 ⊆ 𝐴 ) → ( 𝐴 ⊆ 𝐵 ∨ 𝐵 ⊆ 𝐴 ) ) )
6	1 5	mpd	⊢ ( ( Ord 𝐴 ∧ Ord 𝐵 ) → ( 𝐴 ⊆ 𝐵 ∨ 𝐵 ⊆ 𝐴 ) )