This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem xpcoidgend

Description: If two classes are not disjoint, then the composition of their Cartesian product with itself is idempotent. (Contributed by RP, 24-Dec-2019)

		Ref	Expression
	Hypothesis	xpcoidgend.1	⊢ ( 𝜑 → ( 𝐴 ∩ 𝐵 ) ≠ ∅ )
	Assertion	xpcoidgend	⊢ ( 𝜑 → ( ( 𝐴 × 𝐵 ) ∘ ( 𝐴 × 𝐵 ) ) = ( 𝐴 × 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		xpcoidgend.1	⊢ ( 𝜑 → ( 𝐴 ∩ 𝐵 ) ≠ ∅ )
2		incom	⊢ ( 𝐴 ∩ 𝐵 ) = ( 𝐵 ∩ 𝐴 )
3	2 1	eqnetrrid	⊢ ( 𝜑 → ( 𝐵 ∩ 𝐴 ) ≠ ∅ )
4	3	xpcogend	⊢ ( 𝜑 → ( ( 𝐴 × 𝐵 ) ∘ ( 𝐴 × 𝐵 ) ) = ( 𝐴 × 𝐵 ) )