This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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	$⊢ (A \times A) Er A$

Proof

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