Theorem ordtri2or3

Description: A consequence of total ordering for ordinal classes. Similar to ordtri2or2 . (Contributed by David Moews, 1-May-2017)

	Ref	Expression
Assertion	ordtri2or3	⊢ ( ( Ord 𝐴 ∧ Ord 𝐵 ) → ( 𝐴 = ( 𝐴 ∩ 𝐵 ) ∨ 𝐵 = ( 𝐴 ∩ 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		ordtri2or2	⊢ ( ( Ord 𝐴 ∧ Ord 𝐵 ) → ( 𝐴 ⊆ 𝐵 ∨ 𝐵 ⊆ 𝐴 ) )
2		dfss	⊢ ( 𝐴 ⊆ 𝐵 ↔ 𝐴 = ( 𝐴 ∩ 𝐵 ) )
3		sseqin2	⊢ ( 𝐵 ⊆ 𝐴 ↔ ( 𝐴 ∩ 𝐵 ) = 𝐵 )
4		eqcom	⊢ ( ( 𝐴 ∩ 𝐵 ) = 𝐵 ↔ 𝐵 = ( 𝐴 ∩ 𝐵 ) )
5	3 4	bitri	⊢ ( 𝐵 ⊆ 𝐴 ↔ 𝐵 = ( 𝐴 ∩ 𝐵 ) )
6	2 5	orbi12i	⊢ ( ( 𝐴 ⊆ 𝐵 ∨ 𝐵 ⊆ 𝐴 ) ↔ ( 𝐴 = ( 𝐴 ∩ 𝐵 ) ∨ 𝐵 = ( 𝐴 ∩ 𝐵 ) ) )
7	1 6	sylib	⊢ ( ( Ord 𝐴 ∧ Ord 𝐵 ) → ( 𝐴 = ( 𝐴 ∩ 𝐵 ) ∨ 𝐵 = ( 𝐴 ∩ 𝐵 ) ) )