Theorem poleloe

Description: Express "less than or equals" for general strict orders. (Contributed by Stefan O'Rear, 17-Jan-2015)

	Ref	Expression
Assertion	poleloe	$$⊢B\in V\to \left(A\left(R\cup \mathrm{I}\right)B\leftrightarrow \left(ARB\vee A=B\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		brun	$$⊢A\left(R\cup \mathrm{I}\right)B\leftrightarrow \left(ARB\vee A\mathrm{I}B\right)$$
2		ideqg	$$⊢B\in V\to \left(A\mathrm{I}B\leftrightarrow A=B\right)$$
3	2	orbi2d	$$⊢B\in V\to \left(\left(ARB\vee A\mathrm{I}B\right)\leftrightarrow \left(ARB\vee A=B\right)\right)$$
4	1 3	bitrid	$$⊢B\in V\to \left(A\left(R\cup \mathrm{I}\right)B\leftrightarrow \left(ARB\vee A=B\right)\right)$$