Theorem xpcan

Description: Cancellation law for Cartesian product. (Contributed by NM, 30-Aug-2011)

	Ref	Expression
Assertion	xpcan	⊢ ( 𝐶 ≠ ∅ → ( ( 𝐶 × 𝐴 ) = ( 𝐶 × 𝐵 ) ↔ 𝐴 = 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		xp11	⊢ ( ( 𝐶 ≠ ∅ ∧ 𝐴 ≠ ∅ ) → ( ( 𝐶 × 𝐴 ) = ( 𝐶 × 𝐵 ) ↔ ( 𝐶 = 𝐶 ∧ 𝐴 = 𝐵 ) ) )
2		eqid	⊢ 𝐶 = 𝐶
3	2	biantrur	⊢ ( 𝐴 = 𝐵 ↔ ( 𝐶 = 𝐶 ∧ 𝐴 = 𝐵 ) )
4	1 3	bitr4di	⊢ ( ( 𝐶 ≠ ∅ ∧ 𝐴 ≠ ∅ ) → ( ( 𝐶 × 𝐴 ) = ( 𝐶 × 𝐵 ) ↔ 𝐴 = 𝐵 ) )
5		nne	⊢ ( ¬ 𝐴 ≠ ∅ ↔ 𝐴 = ∅ )
6		simpr	⊢ ( ( 𝐶 ≠ ∅ ∧ 𝐴 = ∅ ) → 𝐴 = ∅ )
7		xpeq2	⊢ ( 𝐴 = ∅ → ( 𝐶 × 𝐴 ) = ( 𝐶 × ∅ ) )
8		xp0	⊢ ( 𝐶 × ∅ ) = ∅
9	7 8	eqtrdi	⊢ ( 𝐴 = ∅ → ( 𝐶 × 𝐴 ) = ∅ )
10	9	eqeq1d	⊢ ( 𝐴 = ∅ → ( ( 𝐶 × 𝐴 ) = ( 𝐶 × 𝐵 ) ↔ ∅ = ( 𝐶 × 𝐵 ) ) )
11		eqcom	⊢ ( ∅ = ( 𝐶 × 𝐵 ) ↔ ( 𝐶 × 𝐵 ) = ∅ )
12	10 11	bitrdi	⊢ ( 𝐴 = ∅ → ( ( 𝐶 × 𝐴 ) = ( 𝐶 × 𝐵 ) ↔ ( 𝐶 × 𝐵 ) = ∅ ) )
13	12	adantl	⊢ ( ( 𝐶 ≠ ∅ ∧ 𝐴 = ∅ ) → ( ( 𝐶 × 𝐴 ) = ( 𝐶 × 𝐵 ) ↔ ( 𝐶 × 𝐵 ) = ∅ ) )
14		df-ne	⊢ ( 𝐶 ≠ ∅ ↔ ¬ 𝐶 = ∅ )
15		xpeq0	⊢ ( ( 𝐶 × 𝐵 ) = ∅ ↔ ( 𝐶 = ∅ ∨ 𝐵 = ∅ ) )
16		orel1	⊢ ( ¬ 𝐶 = ∅ → ( ( 𝐶 = ∅ ∨ 𝐵 = ∅ ) → 𝐵 = ∅ ) )
17	15 16	syl5bi	⊢ ( ¬ 𝐶 = ∅ → ( ( 𝐶 × 𝐵 ) = ∅ → 𝐵 = ∅ ) )
18	14 17	sylbi	⊢ ( 𝐶 ≠ ∅ → ( ( 𝐶 × 𝐵 ) = ∅ → 𝐵 = ∅ ) )
19	18	adantr	⊢ ( ( 𝐶 ≠ ∅ ∧ 𝐴 = ∅ ) → ( ( 𝐶 × 𝐵 ) = ∅ → 𝐵 = ∅ ) )
20	13 19	sylbid	⊢ ( ( 𝐶 ≠ ∅ ∧ 𝐴 = ∅ ) → ( ( 𝐶 × 𝐴 ) = ( 𝐶 × 𝐵 ) → 𝐵 = ∅ ) )
21		eqtr3	⊢ ( ( 𝐴 = ∅ ∧ 𝐵 = ∅ ) → 𝐴 = 𝐵 )
22	6 20 21	syl6an	⊢ ( ( 𝐶 ≠ ∅ ∧ 𝐴 = ∅ ) → ( ( 𝐶 × 𝐴 ) = ( 𝐶 × 𝐵 ) → 𝐴 = 𝐵 ) )
23	5 22	sylan2b	⊢ ( ( 𝐶 ≠ ∅ ∧ ¬ 𝐴 ≠ ∅ ) → ( ( 𝐶 × 𝐴 ) = ( 𝐶 × 𝐵 ) → 𝐴 = 𝐵 ) )
24		xpeq2	⊢ ( 𝐴 = 𝐵 → ( 𝐶 × 𝐴 ) = ( 𝐶 × 𝐵 ) )
25	23 24	impbid1	⊢ ( ( 𝐶 ≠ ∅ ∧ ¬ 𝐴 ≠ ∅ ) → ( ( 𝐶 × 𝐴 ) = ( 𝐶 × 𝐵 ) ↔ 𝐴 = 𝐵 ) )
26	4 25	pm2.61dan	⊢ ( 𝐶 ≠ ∅ → ( ( 𝐶 × 𝐴 ) = ( 𝐶 × 𝐵 ) ↔ 𝐴 = 𝐵 ) )