xpcoid

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

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

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

Metamath Proof Explorer