MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  xp11 Structured version   Visualization version   GIF version

Theorem xp11 6194
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.)
Assertion
Ref Expression
xp11 ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) → ((𝐴 × 𝐵) = (𝐶 × 𝐷) ↔ (𝐴 = 𝐶𝐵 = 𝐷)))

Proof of Theorem xp11
StepHypRef Expression
1 xpnz 6178 . . 3 ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ↔ (𝐴 × 𝐵) ≠ ∅)
2 anidm 564 . . . . . 6 (((𝐴 × 𝐵) ≠ ∅ ∧ (𝐴 × 𝐵) ≠ ∅) ↔ (𝐴 × 𝐵) ≠ ∅)
3 neeq1 3002 . . . . . . 7 ((𝐴 × 𝐵) = (𝐶 × 𝐷) → ((𝐴 × 𝐵) ≠ ∅ ↔ (𝐶 × 𝐷) ≠ ∅))
43anbi2d 630 . . . . . 6 ((𝐴 × 𝐵) = (𝐶 × 𝐷) → (((𝐴 × 𝐵) ≠ ∅ ∧ (𝐴 × 𝐵) ≠ ∅) ↔ ((𝐴 × 𝐵) ≠ ∅ ∧ (𝐶 × 𝐷) ≠ ∅)))
52, 4bitr3id 285 . . . . 5 ((𝐴 × 𝐵) = (𝐶 × 𝐷) → ((𝐴 × 𝐵) ≠ ∅ ↔ ((𝐴 × 𝐵) ≠ ∅ ∧ (𝐶 × 𝐷) ≠ ∅)))
6 eqimss 4041 . . . . . . . 8 ((𝐴 × 𝐵) = (𝐶 × 𝐷) → (𝐴 × 𝐵) ⊆ (𝐶 × 𝐷))
7 ssxpb 6193 . . . . . . . 8 ((𝐴 × 𝐵) ≠ ∅ → ((𝐴 × 𝐵) ⊆ (𝐶 × 𝐷) ↔ (𝐴𝐶𝐵𝐷)))
86, 7syl5ibcom 245 . . . . . . 7 ((𝐴 × 𝐵) = (𝐶 × 𝐷) → ((𝐴 × 𝐵) ≠ ∅ → (𝐴𝐶𝐵𝐷)))
9 eqimss2 4042 . . . . . . . 8 ((𝐴 × 𝐵) = (𝐶 × 𝐷) → (𝐶 × 𝐷) ⊆ (𝐴 × 𝐵))
10 ssxpb 6193 . . . . . . . 8 ((𝐶 × 𝐷) ≠ ∅ → ((𝐶 × 𝐷) ⊆ (𝐴 × 𝐵) ↔ (𝐶𝐴𝐷𝐵)))
119, 10syl5ibcom 245 . . . . . . 7 ((𝐴 × 𝐵) = (𝐶 × 𝐷) → ((𝐶 × 𝐷) ≠ ∅ → (𝐶𝐴𝐷𝐵)))
128, 11anim12d 609 . . . . . 6 ((𝐴 × 𝐵) = (𝐶 × 𝐷) → (((𝐴 × 𝐵) ≠ ∅ ∧ (𝐶 × 𝐷) ≠ ∅) → ((𝐴𝐶𝐵𝐷) ∧ (𝐶𝐴𝐷𝐵))))
13 an4 656 . . . . . . 7 (((𝐴𝐶𝐵𝐷) ∧ (𝐶𝐴𝐷𝐵)) ↔ ((𝐴𝐶𝐶𝐴) ∧ (𝐵𝐷𝐷𝐵)))
14 eqss 3998 . . . . . . . 8 (𝐴 = 𝐶 ↔ (𝐴𝐶𝐶𝐴))
15 eqss 3998 . . . . . . . 8 (𝐵 = 𝐷 ↔ (𝐵𝐷𝐷𝐵))
1614, 15anbi12i 628 . . . . . . 7 ((𝐴 = 𝐶𝐵 = 𝐷) ↔ ((𝐴𝐶𝐶𝐴) ∧ (𝐵𝐷𝐷𝐵)))
1713, 16bitr4i 278 . . . . . 6 (((𝐴𝐶𝐵𝐷) ∧ (𝐶𝐴𝐷𝐵)) ↔ (𝐴 = 𝐶𝐵 = 𝐷))
1812, 17imbitrdi 251 . . . . 5 ((𝐴 × 𝐵) = (𝐶 × 𝐷) → (((𝐴 × 𝐵) ≠ ∅ ∧ (𝐶 × 𝐷) ≠ ∅) → (𝐴 = 𝐶𝐵 = 𝐷)))
195, 18sylbid 240 . . . 4 ((𝐴 × 𝐵) = (𝐶 × 𝐷) → ((𝐴 × 𝐵) ≠ ∅ → (𝐴 = 𝐶𝐵 = 𝐷)))
2019com12 32 . . 3 ((𝐴 × 𝐵) ≠ ∅ → ((𝐴 × 𝐵) = (𝐶 × 𝐷) → (𝐴 = 𝐶𝐵 = 𝐷)))
211, 20sylbi 217 . 2 ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) → ((𝐴 × 𝐵) = (𝐶 × 𝐷) → (𝐴 = 𝐶𝐵 = 𝐷)))
22 xpeq12 5709 . 2 ((𝐴 = 𝐶𝐵 = 𝐷) → (𝐴 × 𝐵) = (𝐶 × 𝐷))
2321, 22impbid1 225 1 ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) → ((𝐴 × 𝐵) = (𝐶 × 𝐷) ↔ (𝐴 = 𝐶𝐵 = 𝐷)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395   = wceq 1539  wne 2939  wss 3950  c0 4332   × cxp 5682
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-11 2156  ax-12 2176  ax-ext 2707  ax-sep 5295  ax-nul 5305  ax-pr 5431
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-ne 2940  df-ral 3061  df-rex 3070  df-rab 3436  df-v 3481  df-dif 3953  df-un 3955  df-ss 3967  df-nul 4333  df-if 4525  df-sn 4626  df-pr 4628  df-op 4632  df-br 5143  df-opab 5205  df-xp 5690  df-rel 5691  df-cnv 5692  df-dm 5694  df-rn 5695
This theorem is referenced by:  xpcan  6195  xpcan2  6196  fseqdom  10067  axcc2lem  10477  lmodfopnelem1  20897  xppss12  42269
  Copyright terms: Public domain W3C validator