Theorem xpidtr

Description: A Cartesian square is a transitive relation. (Contributed by FL, 31-Jul-2009)

	Ref	Expression
Assertion	xpidtr	$$⊢\left(A\times A\right)\circ \left(A\times A\right)\subseteq A\times A$$

Proof

Step	Hyp	Ref	Expression
1		brxp	$$⊢x\left(A\times A\right)y\leftrightarrow \left(x\in A\wedge y\in A\right)$$
2		brxp	$$⊢y\left(A\times A\right)z\leftrightarrow \left(y\in A\wedge z\in A\right)$$
3		brxp	$$⊢x\left(A\times A\right)z\leftrightarrow \left(x\in A\wedge z\in A\right)$$
4	3	simplbi2com	$$⊢z\in A\to \left(x\in A\to x\left(A\times A\right)z\right)$$
5	2 4	simplbiim	$$⊢y\left(A\times A\right)z\to \left(x\in A\to x\left(A\times A\right)z\right)$$
6	5	com12	$$⊢x\in A\to \left(y\left(A\times A\right)z\to x\left(A\times A\right)z\right)$$
7	6	adantr	$$⊢\left(x\in A\wedge y\in A\right)\to \left(y\left(A\times A\right)z\to x\left(A\times A\right)z\right)$$
8	1 7	sylbi	$$⊢x\left(A\times A\right)y\to \left(y\left(A\times A\right)z\to x\left(A\times A\right)z\right)$$
9	8	imp	$$⊢\left(x\left(A\times A\right)y\wedge y\left(A\times A\right)z\right)\to x\left(A\times A\right)z$$
10	9	ax-gen	$$⊢\forall z\left(\left(x\left(A\times A\right)y\wedge y\left(A\times A\right)z\right)\to x\left(A\times A\right)z\right)$$
11	10	gen2	$$⊢\forall x\forall y\forall z\left(\left(x\left(A\times A\right)y\wedge y\left(A\times A\right)z\right)\to x\left(A\times A\right)z\right)$$
12		cotr	$$⊢\left(A\times A\right)\circ \left(A\times A\right)\subseteq A\times A\leftrightarrow \forall x\forall y\forall z\left(\left(x\left(A\times A\right)y\wedge y\left(A\times A\right)z\right)\to x\left(A\times A\right)z\right)$$
13	11 12	mpbir	$$⊢\left(A\times A\right)\circ \left(A\times A\right)\subseteq A\times A$$