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

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

Proof of Theorem xpexg
StepHypRef Expression
1 xpsspw 5156 . 2 (𝐴 × 𝐵) ⊆ 𝒫 𝒫 (𝐴𝐵)
2 unexg 6857 . . 3 ((𝐴𝑉𝐵𝑊) → (𝐴𝐵) ∈ V)
3 pwexg 4776 . . 3 ((𝐴𝐵) ∈ V → 𝒫 (𝐴𝐵) ∈ V)
4 pwexg 4776 . . 3 (𝒫 (𝐴𝐵) ∈ V → 𝒫 𝒫 (𝐴𝐵) ∈ V)
52, 3, 43syl 18 . 2 ((𝐴𝑉𝐵𝑊) → 𝒫 𝒫 (𝐴𝐵) ∈ V)
6 ssexg 4732 . 2 (((𝐴 × 𝐵) ⊆ 𝒫 𝒫 (𝐴𝐵) ∧ 𝒫 𝒫 (𝐴𝐵) ∈ V) → (𝐴 × 𝐵) ∈ V)
71, 5, 6sylancr 694 1 ((𝐴𝑉𝐵𝑊) → (𝐴 × 𝐵) ∈ V)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  wcel 1977  Vcvv 3173  cun 3538  wss 3540  𝒫 cpw 4108   × cxp 5036
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-opab 4644  df-xp 5044  df-rel 5045
This theorem is referenced by:  3xpexg  6859  xpex  6860  sqxpexg  6861  opabex2  6997  cnvexg  7005  coexg  7010  fex2  7014  fabexg  7015  resfunexgALT  7022  cofunexg  7023  fnexALT  7025  opabex3d  7037  opabex3  7038  oprabexd  7046  ofmresex  7056  mpt2exxg  7133  offval22  7140  fnwelem  7179  tposexg  7253  pmex  7749  mapex  7750  pmvalg  7755  elpmg  7759  fvdiagfn  7788  ixpexg  7818  map1  7921  xpdom2  7940  xpdom3  7943  omxpen  7947  fodomr  7996  disjenex  8003  domssex2  8005  domssex  8006  mapxpen  8011  xpfi  8116  fczfsuppd  8176  marypha1  8223  brwdom2  8361  wdom2d  8368  xpwdomg  8373  unxpwdom2  8376  ixpiunwdom  8379  fseqen  8733  cdaval  8875  cdaassen  8887  mapcdaen  8889  cdadom1  8891  cdainf  8897  hsmexlem2  9132  axdc2lem  9153  iundom2g  9241  fpwwe2lem2  9333  fpwwe2lem5  9335  fpwwe2lem12  9342  fpwwe2lem13  9343  fpwwelem  9346  canthwe  9352  pwxpndom  9367  gchhar  9380  wrdexg  13170  trclexlem  13581  pwsbas  15970  pwsle  15975  pwssca  15979  isacs1i  16141  rescval2  16311  reschom  16313  rescabs  16316  setccofval  16555  isga  17547  sylow2a  17857  lsmhash  17941  efgtf  17958  frgpcpbl  17995  frgp0  17996  frgpeccl  17997  frgpadd  17999  frgpmhm  18001  vrgpf  18004  vrgpinv  18005  frgpupf  18009  frgpup1  18011  frgpup2  18012  frgpup3lem  18013  frgpnabllem1  18099  frgpnabllem2  18100  gsum2d2  18196  gsumcom2  18197  gsumxp  18198  dprd2da  18264  pwssplit3  18882  opsrval  19295  opsrtoslem2  19306  evlslem4  19329  mpt2frlmd  19935  frlmip  19936  matbas2d  20048  mattposvs  20080  mat1dimelbas  20096  mdetrlin  20227  lmfval  20846  txbasex  21179  txopn  21215  txcn  21239  txrest  21244  txindislem  21246  xkoinjcn  21300  tsmsxp  21768  ustssel  21819  ustfilxp  21826  trust  21843  restutop  21851  trcfilu  21908  cfiluweak  21909  imasdsf1olem  21988  blfvalps  21998  metustfbas  22172  restmetu  22185  bcthlem1  22929  bcthlem5  22933  rrxip  22986  perpln1  25405  perpln2  25406  isperp  25407  isleag  25533  isvcOLD  26818  fnct  28876  resf1o  28893  locfinref  29236  metidval  29261  esum2dlem  29481  esum2d  29482  esumiun  29483  elsx  29584  filnetlem3  31545  filnetlem4  31546  bj-xpexg2  32140  isrngod  32867  isgrpda  32924  iscringd  32967  wdom2d2  36620  unxpwdom3  36683  trclubgNEW  36944  relexpxpnnidm  37014  relexpxpmin  37028  enrelmap  37311  rfovd  37315  rfovcnvf1od  37318  fsovrfovd  37323  xpexd  38314  dvsinax  38801  sge0xp  39322  mpt2exxg2  41909
  Copyright terms: Public domain W3C validator