Metamath Proof Explorer


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 ( ( 𝐴 × 𝐴 ) ∘ ( 𝐴 × 𝐴 ) ) = ( 𝐴 × 𝐴 )