Theorem xpider

Description: A Cartesian square is an equivalence relation (in general, it is not a poset). (Contributed by FL, 31-Jul-2009) (Revised by Mario Carneiro, 12-Aug-2015)

	Ref	Expression
Assertion	xpider	$$⊢\left(A\times A\right)\mathrm{Er}A$$

Proof

Step	Hyp	Ref	Expression
1		relxp	$$⊢\mathrm{Rel}\left(A\times A\right)$$
2		dmxpid	$$⊢\mathrm{dom}\left(A\times A\right)=A$$
3		cnvxp	$$⊢{\left(A\times A\right)}^{-1}=A\times A$$
4		xpidtr	$$⊢\left(A\times A\right)\circ \left(A\times A\right)\subseteq A\times A$$
5		uneq1	$$⊢{\left(A\times A\right)}^{-1}=A\times A\to {\left(A\times A\right)}^{-1}\cup \left(A\times A\right)=\left(A\times A\right)\cup \left(A\times A\right)$$
6		unss2	$$⊢\left(A\times A\right)\circ \left(A\times A\right)\subseteq A\times A\to {\left(A\times A\right)}^{-1}\cup \left(\left(A\times A\right)\circ \left(A\times A\right)\right)\subseteq {\left(A\times A\right)}^{-1}\cup \left(A\times A\right)$$
7		unidm	$$⊢\left(A\times A\right)\cup \left(A\times A\right)=A\times A$$
8		eqtr	$$⊢\left({\left(A\times A\right)}^{-1}\cup \left(A\times A\right)=\left(A\times A\right)\cup \left(A\times A\right)\wedge \left(A\times A\right)\cup \left(A\times A\right)=A\times A\right)\to {\left(A\times A\right)}^{-1}\cup \left(A\times A\right)=A\times A$$
9		sseq2	$$⊢{\left(A\times A\right)}^{-1}\cup \left(A\times A\right)=A\times A\to \left({\left(A\times A\right)}^{-1}\cup \left(\left(A\times A\right)\circ \left(A\times A\right)\right)\subseteq {\left(A\times A\right)}^{-1}\cup \left(A\times A\right)\leftrightarrow {\left(A\times A\right)}^{-1}\cup \left(\left(A\times A\right)\circ \left(A\times A\right)\right)\subseteq A\times A\right)$$
10	9	biimpd	$$⊢{\left(A\times A\right)}^{-1}\cup \left(A\times A\right)=A\times A\to \left({\left(A\times A\right)}^{-1}\cup \left(\left(A\times A\right)\circ \left(A\times A\right)\right)\subseteq {\left(A\times A\right)}^{-1}\cup \left(A\times A\right)\to {\left(A\times A\right)}^{-1}\cup \left(\left(A\times A\right)\circ \left(A\times A\right)\right)\subseteq A\times A\right)$$
11	8 10	syl	$$⊢\left({\left(A\times A\right)}^{-1}\cup \left(A\times A\right)=\left(A\times A\right)\cup \left(A\times A\right)\wedge \left(A\times A\right)\cup \left(A\times A\right)=A\times A\right)\to \left({\left(A\times A\right)}^{-1}\cup \left(\left(A\times A\right)\circ \left(A\times A\right)\right)\subseteq {\left(A\times A\right)}^{-1}\cup \left(A\times A\right)\to {\left(A\times A\right)}^{-1}\cup \left(\left(A\times A\right)\circ \left(A\times A\right)\right)\subseteq A\times A\right)$$
12	7 11	mpan2	$$⊢{\left(A\times A\right)}^{-1}\cup \left(A\times A\right)=\left(A\times A\right)\cup \left(A\times A\right)\to \left({\left(A\times A\right)}^{-1}\cup \left(\left(A\times A\right)\circ \left(A\times A\right)\right)\subseteq {\left(A\times A\right)}^{-1}\cup \left(A\times A\right)\to {\left(A\times A\right)}^{-1}\cup \left(\left(A\times A\right)\circ \left(A\times A\right)\right)\subseteq A\times A\right)$$
13	5 6 12	syl2im	$$⊢{\left(A\times A\right)}^{-1}=A\times A\to \left(\left(A\times A\right)\circ \left(A\times A\right)\subseteq A\times A\to {\left(A\times A\right)}^{-1}\cup \left(\left(A\times A\right)\circ \left(A\times A\right)\right)\subseteq A\times A\right)$$
14	3 4 13	mp2	$$⊢{\left(A\times A\right)}^{-1}\cup \left(\left(A\times A\right)\circ \left(A\times A\right)\right)\subseteq A\times A$$
15		df-er	$$⊢\left(A\times A\right)\mathrm{Er}A\leftrightarrow \left(\mathrm{Rel}\left(A\times A\right)\wedge \mathrm{dom}\left(A\times A\right)=A\wedge {\left(A\times A\right)}^{-1}\cup \left(\left(A\times A\right)\circ \left(A\times A\right)\right)\subseteq A\times A\right)$$
16	1 2 14 15	mpbir3an	$$⊢\left(A\times A\right)\mathrm{Er}A$$