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	$$⊢\left(\mathrm{Ord}A\wedge \mathrm{Ord}B\right)\to \left(A=A\cap B\vee B=A\cap B\right)$$

Proof

Step	Hyp	Ref	Expression
1		ordtri2or2	$$⊢\left(\mathrm{Ord}A\wedge \mathrm{Ord}B\right)\to \left(A\subseteq B\vee B\subseteq A\right)$$
2		dfss	$$⊢A\subseteq B\leftrightarrow A=A\cap B$$
3		sseqin2	$$⊢B\subseteq A\leftrightarrow A\cap B=B$$
4		eqcom	$$⊢A\cap B=B\leftrightarrow B=A\cap B$$
5	3 4	bitri	$$⊢B\subseteq A\leftrightarrow B=A\cap B$$
6	2 5	orbi12i	$$⊢\left(A\subseteq B\vee B\subseteq A\right)\leftrightarrow \left(A=A\cap B\vee B=A\cap B\right)$$
7	1 6	sylib	$$⊢\left(\mathrm{Ord}A\wedge \mathrm{Ord}B\right)\to \left(A=A\cap B\vee B=A\cap B\right)$$