Theorem xpcoid

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

	Ref	Expression
Assertion	xpcoid	⊢ ( ( 𝐴 × 𝐴 ) ∘ ( 𝐴 × 𝐴 ) ) = ( 𝐴 × 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		co01	⊢ ( ∅ ∘ ∅ ) = ∅
2		id	⊢ ( 𝐴 = ∅ → 𝐴 = ∅ )
3	2	sqxpeqd	⊢ ( 𝐴 = ∅ → ( 𝐴 × 𝐴 ) = ( ∅ × ∅ ) )
4		0xp	⊢ ( ∅ × ∅ ) = ∅
5	3 4	eqtrdi	⊢ ( 𝐴 = ∅ → ( 𝐴 × 𝐴 ) = ∅ )
6	5 5	coeq12d	⊢ ( 𝐴 = ∅ → ( ( 𝐴 × 𝐴 ) ∘ ( 𝐴 × 𝐴 ) ) = ( ∅ ∘ ∅ ) )
7	1 6 5	3eqtr4a	⊢ ( 𝐴 = ∅ → ( ( 𝐴 × 𝐴 ) ∘ ( 𝐴 × 𝐴 ) ) = ( 𝐴 × 𝐴 ) )
8		xpco	⊢ ( 𝐴 ≠ ∅ → ( ( 𝐴 × 𝐴 ) ∘ ( 𝐴 × 𝐴 ) ) = ( 𝐴 × 𝐴 ) )
9	7 8	pm2.61ine	⊢ ( ( 𝐴 × 𝐴 ) ∘ ( 𝐴 × 𝐴 ) ) = ( 𝐴 × 𝐴 )