Metamath Proof Explorer


Theorem xp11

Description: The Cartesian product of nonempty classes is a one-to-one "function" of its two "arguments". In other words, two Cartesian products, at least one with nonempty factors, are equal if and only if their respective factors are equal. (Contributed by NM, 31-May-2008)

Ref Expression
Assertion xp11 ( ( 𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅ ) → ( ( 𝐴 × 𝐵 ) = ( 𝐶 × 𝐷 ) ↔ ( 𝐴 = 𝐶𝐵 = 𝐷 ) ) )

Proof

Step Hyp Ref Expression
1 xpnz ( ( 𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅ ) ↔ ( 𝐴 × 𝐵 ) ≠ ∅ )
2 anidm ( ( ( 𝐴 × 𝐵 ) ≠ ∅ ∧ ( 𝐴 × 𝐵 ) ≠ ∅ ) ↔ ( 𝐴 × 𝐵 ) ≠ ∅ )
3 neeq1 ( ( 𝐴 × 𝐵 ) = ( 𝐶 × 𝐷 ) → ( ( 𝐴 × 𝐵 ) ≠ ∅ ↔ ( 𝐶 × 𝐷 ) ≠ ∅ ) )
4 3 anbi2d ( ( 𝐴 × 𝐵 ) = ( 𝐶 × 𝐷 ) → ( ( ( 𝐴 × 𝐵 ) ≠ ∅ ∧ ( 𝐴 × 𝐵 ) ≠ ∅ ) ↔ ( ( 𝐴 × 𝐵 ) ≠ ∅ ∧ ( 𝐶 × 𝐷 ) ≠ ∅ ) ) )
5 2 4 bitr3id ( ( 𝐴 × 𝐵 ) = ( 𝐶 × 𝐷 ) → ( ( 𝐴 × 𝐵 ) ≠ ∅ ↔ ( ( 𝐴 × 𝐵 ) ≠ ∅ ∧ ( 𝐶 × 𝐷 ) ≠ ∅ ) ) )
6 eqimss ( ( 𝐴 × 𝐵 ) = ( 𝐶 × 𝐷 ) → ( 𝐴 × 𝐵 ) ⊆ ( 𝐶 × 𝐷 ) )
7 ssxpb ( ( 𝐴 × 𝐵 ) ≠ ∅ → ( ( 𝐴 × 𝐵 ) ⊆ ( 𝐶 × 𝐷 ) ↔ ( 𝐴𝐶𝐵𝐷 ) ) )
8 6 7 syl5ibcom ( ( 𝐴 × 𝐵 ) = ( 𝐶 × 𝐷 ) → ( ( 𝐴 × 𝐵 ) ≠ ∅ → ( 𝐴𝐶𝐵𝐷 ) ) )
9 eqimss2 ( ( 𝐴 × 𝐵 ) = ( 𝐶 × 𝐷 ) → ( 𝐶 × 𝐷 ) ⊆ ( 𝐴 × 𝐵 ) )
10 ssxpb ( ( 𝐶 × 𝐷 ) ≠ ∅ → ( ( 𝐶 × 𝐷 ) ⊆ ( 𝐴 × 𝐵 ) ↔ ( 𝐶𝐴𝐷𝐵 ) ) )
11 9 10 syl5ibcom ( ( 𝐴 × 𝐵 ) = ( 𝐶 × 𝐷 ) → ( ( 𝐶 × 𝐷 ) ≠ ∅ → ( 𝐶𝐴𝐷𝐵 ) ) )
12 8 11 anim12d ( ( 𝐴 × 𝐵 ) = ( 𝐶 × 𝐷 ) → ( ( ( 𝐴 × 𝐵 ) ≠ ∅ ∧ ( 𝐶 × 𝐷 ) ≠ ∅ ) → ( ( 𝐴𝐶𝐵𝐷 ) ∧ ( 𝐶𝐴𝐷𝐵 ) ) ) )
13 an4 ( ( ( 𝐴𝐶𝐵𝐷 ) ∧ ( 𝐶𝐴𝐷𝐵 ) ) ↔ ( ( 𝐴𝐶𝐶𝐴 ) ∧ ( 𝐵𝐷𝐷𝐵 ) ) )
14 eqss ( 𝐴 = 𝐶 ↔ ( 𝐴𝐶𝐶𝐴 ) )
15 eqss ( 𝐵 = 𝐷 ↔ ( 𝐵𝐷𝐷𝐵 ) )
16 14 15 anbi12i ( ( 𝐴 = 𝐶𝐵 = 𝐷 ) ↔ ( ( 𝐴𝐶𝐶𝐴 ) ∧ ( 𝐵𝐷𝐷𝐵 ) ) )
17 13 16 bitr4i ( ( ( 𝐴𝐶𝐵𝐷 ) ∧ ( 𝐶𝐴𝐷𝐵 ) ) ↔ ( 𝐴 = 𝐶𝐵 = 𝐷 ) )
18 12 17 syl6ib ( ( 𝐴 × 𝐵 ) = ( 𝐶 × 𝐷 ) → ( ( ( 𝐴 × 𝐵 ) ≠ ∅ ∧ ( 𝐶 × 𝐷 ) ≠ ∅ ) → ( 𝐴 = 𝐶𝐵 = 𝐷 ) ) )
19 5 18 sylbid ( ( 𝐴 × 𝐵 ) = ( 𝐶 × 𝐷 ) → ( ( 𝐴 × 𝐵 ) ≠ ∅ → ( 𝐴 = 𝐶𝐵 = 𝐷 ) ) )
20 19 com12 ( ( 𝐴 × 𝐵 ) ≠ ∅ → ( ( 𝐴 × 𝐵 ) = ( 𝐶 × 𝐷 ) → ( 𝐴 = 𝐶𝐵 = 𝐷 ) ) )
21 1 20 sylbi ( ( 𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅ ) → ( ( 𝐴 × 𝐵 ) = ( 𝐶 × 𝐷 ) → ( 𝐴 = 𝐶𝐵 = 𝐷 ) ) )
22 xpeq12 ( ( 𝐴 = 𝐶𝐵 = 𝐷 ) → ( 𝐴 × 𝐵 ) = ( 𝐶 × 𝐷 ) )
23 21 22 impbid1 ( ( 𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅ ) → ( ( 𝐴 × 𝐵 ) = ( 𝐶 × 𝐷 ) ↔ ( 𝐴 = 𝐶𝐵 = 𝐷 ) ) )