Theorem xpcoid

Description: Composition of two Cartesian squares. (Contributed by Thierry Arnoux, 14-Jan-2018)

	Ref	Expression
Assertion	xpcoid	$$⊢\left(A\times A\right)\circ \left(A\times A\right)=A\times A$$

Proof

Step	Hyp	Ref	Expression
1		co01	$$⊢\varnothing \circ \varnothing =\varnothing$$
2		id	$$⊢A=\varnothing \to A=\varnothing$$
3	2	sqxpeqd	$$⊢A=\varnothing \to A\times A=\varnothing \times \varnothing$$
4		0xp	$$⊢\varnothing \times \varnothing =\varnothing$$
5	3 4	eqtrdi	$$⊢A=\varnothing \to A\times A=\varnothing$$
6	5 5	coeq12d	$$⊢A=\varnothing \to \left(A\times A\right)\circ \left(A\times A\right)=\varnothing \circ \varnothing$$
7	1 6 5	3eqtr4a	$$⊢A=\varnothing \to \left(A\times A\right)\circ \left(A\times A\right)=A\times A$$
8		xpco	$$⊢A\ne \varnothing \to \left(A\times A\right)\circ \left(A\times A\right)=A\times A$$
9	7 8	pm2.61ine	$$⊢\left(A\times A\right)\circ \left(A\times A\right)=A\times A$$