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

Theorem xpexg 7465
Description: The Cartesian product of two sets is a set. Proposition 6.2 of [TakeutiZaring] p. 23. See also xpexgALT 7674. (Contributed by NM, 14-Aug-1994.)
Assertion
Ref Expression
xpexg ((𝐴𝑉𝐵𝑊) → (𝐴 × 𝐵) ∈ V)

Proof of Theorem xpexg
StepHypRef Expression
1 xpsspw 5675 . 2 (𝐴 × 𝐵) ⊆ 𝒫 𝒫 (𝐴𝐵)
2 unexg 7464 . . 3 ((𝐴𝑉𝐵𝑊) → (𝐴𝐵) ∈ V)
3 pwexg 5270 . . 3 ((𝐴𝐵) ∈ V → 𝒫 (𝐴𝐵) ∈ V)
4 pwexg 5270 . . 3 (𝒫 (𝐴𝐵) ∈ V → 𝒫 𝒫 (𝐴𝐵) ∈ V)
52, 3, 43syl 18 . 2 ((𝐴𝑉𝐵𝑊) → 𝒫 𝒫 (𝐴𝐵) ∈ V)
6 ssexg 5218 . 2 (((𝐴 × 𝐵) ⊆ 𝒫 𝒫 (𝐴𝐵) ∧ 𝒫 𝒫 (𝐴𝐵) ∈ V) → (𝐴 × 𝐵) ∈ V)
71, 5, 6sylancr 589 1 ((𝐴𝑉𝐵𝑊) → (𝐴 × 𝐵) ∈ V)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 398  wcel 2107  Vcvv 3493  cun 3932  wss 3934  𝒫 cpw 4537   × cxp 5546
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2791  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7453
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-ral 3141  df-rex 3142  df-rab 3145  df-v 3495  df-dif 3937  df-un 3939  df-in 3941  df-ss 3950  df-nul 4290  df-if 4466  df-pw 4539  df-sn 4560  df-pr 4562  df-op 4566  df-uni 4831  df-opab 5120  df-xp 5554  df-rel 5555
This theorem is referenced by:  xpexd  7466  3xpexg  7467  xpex  7468  sqxpexg  7469  coexg  7626  fex2  7630  fabexg  7631  resfunexgALT  7641  fnexALT  7644  funexw  7645  opabex3d  7658  opabex3rd  7659  opabex3  7660  mpoexxg  7765  fnwelem  7817  pmex  8403  mapex  8404  pmvalg  8409  elpmg  8414  fvdiagfn  8447  ixpexg  8478  snmapen  8582  xpdom2  8604  xpdom3  8607  omxpen  8611  fodomr  8660  disjenex  8667  domssex2  8669  domssex  8670  mapxpen  8675  xpfi  8781  fczfsuppd  8843  brwdom2  9029  xpwdomg  9041  unxpwdom2  9044  djuex  9329  djuexALT  9343  fseqen  9445  djuassen  9596  mapdjuen  9598  djudom1  9600  djuinf  9606  hsmexlem2  9841  axdc2lem  9862  iundom2g  9954  fpwwe2lem13  10056  wrdexgOLD  13864  pwsbas  16752  pwsle  16757  pwssca  16761  isga  18413  efgtf  18840  frgpcpbl  18877  frgp0  18878  frgpeccl  18879  frgpadd  18881  frgpmhm  18883  vrgpf  18886  vrgpinv  18887  frgpupf  18891  frgpup1  18893  frgpup2  18894  frgpup3lem  18895  frgpnabllem1  18985  frgpnabllem2  18986  gsum2d2  19086  gsumcom2  19087  dprd2da  19156  pwssplit3  19825  mpofrlmd  20913  frlmip  20914  mattposvs  21056  mat1dimelbas  21072  mdetrlin  21203  lmfval  21832  txbasex  22166  txopn  22202  txcn  22226  txrest  22231  txindislem  22233  xkoinjcn  22287  blfvalps  22985  bcthlem1  23919  bcthlem5  23923  rrxip  23985  isvcOLD  28348  resf1o  30458  locfinref  31093  esum2dlem  31339  esum2d  31340  elsx  31441  satfv0  32593  satf00  32609  filnetlem3  33716  filnetlem4  33717  bj-xpexg2  34260  inxpex  35578  xrninxpex  35624  relexpxpnnidm  40028  enrelmap  40323  mpoexxg2  44366
  Copyright terms: Public domain W3C validator