Theorem dfso2

Description: Quantifier-free definition of a strict order. (Contributed by Scott Fenton, 22-Feb-2013)

	Ref	Expression
Assertion	dfso2	$$⊢R\mathrm{Or}A\leftrightarrow \left(R\mathrm{Po}A\wedge A\times A\subseteq R\cup \left(\mathrm{I}\cup R^{-1}\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		df-so	$$⊢R\mathrm{Or}A\leftrightarrow \left(R\mathrm{Po}A\wedge \forall x\in A\forall y\in A\left(xRy\vee x=y\vee yRx\right)\right)$$
2		opelxp	$$⊢⟨x,y⟩\in \left(A\times A\right)\leftrightarrow \left(x\in A\wedge y\in A\right)$$
3		brun	$$⊢x\left(\mathrm{I}\cup R^{-1}\right)y\leftrightarrow \left(x\mathrm{I}y\vee x{R}^{-1}y\right)$$
4		vex	$$⊢y\in \mathrm{V}$$
5	4	ideq	$$⊢x\mathrm{I}y\leftrightarrow x=y$$
6		vex	$$⊢x\in \mathrm{V}$$
7	6 4	brcnv	$$⊢x{R}^{-1}y\leftrightarrow yRx$$
8	5 7	orbi12i	$$⊢\left(x\mathrm{I}y\vee x{R}^{-1}y\right)\leftrightarrow \left(x=y\vee yRx\right)$$
9	3 8	bitr2i	$$⊢\left(x=y\vee yRx\right)\leftrightarrow x\left(\mathrm{I}\cup R^{-1}\right)y$$
10	9	orbi2i	$$⊢\left(xRy\vee \left(x=y\vee yRx\right)\right)\leftrightarrow \left(xRy\vee x\left(\mathrm{I}\cup R^{-1}\right)y\right)$$
11		3orass	$$⊢\left(xRy\vee x=y\vee yRx\right)\leftrightarrow \left(xRy\vee \left(x=y\vee yRx\right)\right)$$
12		brun	$$⊢x\left(R\cup \left(\mathrm{I}\cup R^{-1}\right)\right)y\leftrightarrow \left(xRy\vee x\left(\mathrm{I}\cup R^{-1}\right)y\right)$$
13	10 11 12	3bitr4i	$$⊢\left(xRy\vee x=y\vee yRx\right)\leftrightarrow x\left(R\cup \left(\mathrm{I}\cup R^{-1}\right)\right)y$$
14		df-br	$$⊢x\left(R\cup \left(\mathrm{I}\cup R^{-1}\right)\right)y\leftrightarrow ⟨x,y⟩\in \left(R\cup \left(\mathrm{I}\cup R^{-1}\right)\right)$$
15	13 14	bitr2i	$$⊢⟨x,y⟩\in \left(R\cup \left(\mathrm{I}\cup R^{-1}\right)\right)\leftrightarrow \left(xRy\vee x=y\vee yRx\right)$$
16	2 15	imbi12i	$$⊢\left(⟨x,y⟩\in \left(A\times A\right)\to ⟨x,y⟩\in \left(R\cup \left(\mathrm{I}\cup R^{-1}\right)\right)\right)\leftrightarrow \left(\left(x\in A\wedge y\in A\right)\to \left(xRy\vee x=y\vee yRx\right)\right)$$
17	16	2albii	$$⊢\forall x\forall y\left(⟨x,y⟩\in \left(A\times A\right)\to ⟨x,y⟩\in \left(R\cup \left(\mathrm{I}\cup R^{-1}\right)\right)\right)\leftrightarrow \forall x\forall y\left(\left(x\in A\wedge y\in A\right)\to \left(xRy\vee x=y\vee yRx\right)\right)$$
18		relxp	$$⊢\mathrm{Rel}\left(A\times A\right)$$
19		ssrel	$$⊢\mathrm{Rel}\left(A\times A\right)\to \left(A\times A\subseteq R\cup \left(\mathrm{I}\cup R^{-1}\right)\leftrightarrow \forall x\forall y\left(⟨x,y⟩\in \left(A\times A\right)\to ⟨x,y⟩\in \left(R\cup \left(\mathrm{I}\cup R^{-1}\right)\right)\right)\right)$$
20	18 19	ax-mp	$$⊢A\times A\subseteq R\cup \left(\mathrm{I}\cup R^{-1}\right)\leftrightarrow \forall x\forall y\left(⟨x,y⟩\in \left(A\times A\right)\to ⟨x,y⟩\in \left(R\cup \left(\mathrm{I}\cup R^{-1}\right)\right)\right)$$
21		r2al	$$⊢\forall x\in A\forall y\in A\left(xRy\vee x=y\vee yRx\right)\leftrightarrow \forall x\forall y\left(\left(x\in A\wedge y\in A\right)\to \left(xRy\vee x=y\vee yRx\right)\right)$$
22	17 20 21	3bitr4i	$$⊢A\times A\subseteq R\cup \left(\mathrm{I}\cup R^{-1}\right)\leftrightarrow \forall x\in A\forall y\in A\left(xRy\vee x=y\vee yRx\right)$$
23	22	anbi2i	$$⊢\left(R\mathrm{Po}A\wedge A\times A\subseteq R\cup \left(\mathrm{I}\cup R^{-1}\right)\right)\leftrightarrow \left(R\mathrm{Po}A\wedge \forall x\in A\forall y\in A\left(xRy\vee x=y\vee yRx\right)\right)$$
24	1 23	bitr4i	$$⊢R\mathrm{Or}A\leftrightarrow \left(R\mathrm{Po}A\wedge A\times A\subseteq R\cup \left(\mathrm{I}\cup R^{-1}\right)\right)$$