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

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

Proof of Theorem xpexg
StepHypRef Expression
1 xpsspw 5266 . 2 (𝐴 × 𝐵) ⊆ 𝒫 𝒫 (𝐴𝐵)
2 unexg 7001 . . 3 ((𝐴𝑉𝐵𝑊) → (𝐴𝐵) ∈ V)
3 pwexg 4880 . . 3 ((𝐴𝐵) ∈ V → 𝒫 (𝐴𝐵) ∈ V)
4 pwexg 4880 . . 3 (𝒫 (𝐴𝐵) ∈ V → 𝒫 𝒫 (𝐴𝐵) ∈ V)
52, 3, 43syl 18 . 2 ((𝐴𝑉𝐵𝑊) → 𝒫 𝒫 (𝐴𝐵) ∈ V)
6 ssexg 4837 . 2 (((𝐴 × 𝐵) ⊆ 𝒫 𝒫 (𝐴𝐵) ∧ 𝒫 𝒫 (𝐴𝐵) ∈ V) → (𝐴 × 𝐵) ∈ V)
71, 5, 6sylancr 696 1 ((𝐴𝑉𝐵𝑊) → (𝐴 × 𝐵) ∈ V)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  wcel 2030  Vcvv 3231  cun 3605  wss 3607  𝒫 cpw 4191   × cxp 5141
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ral 2946  df-rex 2947  df-rab 2950  df-v 3233  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-op 4217  df-uni 4469  df-opab 4746  df-xp 5149  df-rel 5150
This theorem is referenced by:  3xpexg  7003  xpex  7004  sqxpexg  7005  cnvexg  7154  coexg  7159  fex2  7163  fabexg  7164  resfunexgALT  7171  cofunexg  7172  fnexALT  7174  opabex3d  7187  opabex3  7188  oprabexd  7197  ofmresex  7207  opabex2  7271  mpt2exxg  7289  offval22  7298  fnwelem  7337  tposexg  7411  pmex  7904  mapex  7905  pmvalg  7910  elpmg  7915  fvdiagfn  7944  ixpexg  7974  map1  8077  xpdom2  8096  xpdom3  8099  omxpen  8103  fodomr  8152  disjenex  8159  domssex2  8161  domssex  8162  mapxpen  8167  xpfi  8272  fczfsuppd  8334  marypha1  8381  brwdom2  8519  wdom2d  8526  xpwdomg  8531  unxpwdom2  8534  ixpiunwdom  8537  fseqen  8888  cdaval  9030  cdaassen  9042  mapcdaen  9044  cdadom1  9046  cdainf  9052  hsmexlem2  9287  axdc2lem  9308  fnct  9397  iundom2g  9400  fpwwe2lem2  9492  fpwwe2lem5  9494  fpwwe2lem12  9501  fpwwe2lem13  9502  fpwwelem  9505  canthwe  9511  pwxpndom  9526  gchhar  9539  wrdexg  13347  trclexlem  13779  pwsbas  16194  pwsle  16199  pwssca  16203  isacs1i  16365  rescval2  16535  reschom  16537  rescabs  16540  setccofval  16779  isga  17770  sylow2a  18080  lsmhash  18164  efgtf  18181  frgpcpbl  18218  frgp0  18219  frgpeccl  18220  frgpadd  18222  frgpmhm  18224  vrgpf  18227  vrgpinv  18228  frgpupf  18232  frgpup1  18234  frgpup2  18235  frgpup3lem  18236  frgpnabllem1  18322  frgpnabllem2  18323  gsum2d2  18419  gsumcom2  18420  gsumxp  18421  dprd2da  18487  pwssplit3  19109  opsrval  19522  opsrtoslem2  19533  evlslem4  19556  mpt2frlmd  20164  frlmip  20165  matbas2d  20277  mattposvs  20309  mat1dimelbas  20325  mdetrlin  20456  lmfval  21084  txbasex  21417  txopn  21453  txcn  21477  txrest  21482  txindislem  21484  xkoinjcn  21538  tsmsxp  22005  ustssel  22056  ustfilxp  22063  trust  22080  restutop  22088  trcfilu  22145  cfiluweak  22146  imasdsf1olem  22225  blfvalps  22235  metustfbas  22409  restmetu  22422  bcthlem1  23167  bcthlem5  23171  rrxip  23224  perpln1  25650  perpln2  25651  isperp  25652  isleag  25778  isvcOLD  27562  resf1o  29633  locfinref  30036  metidval  30061  esum2dlem  30282  esum2d  30283  esumiun  30284  elsx  30385  madeval  32060  filnetlem3  32500  filnetlem4  32501  bj-xpexg2  33072  isrngod  33827  isgrpda  33884  iscringd  33927  inxpex  34248  xrninxpex  34292  wdom2d2  37919  unxpwdom3  37982  trclubgNEW  38242  relexpxpnnidm  38312  relexpxpmin  38326  enrelmap  38608  rfovd  38612  rfovcnvf1od  38615  fsovrfovd  38620  xpexd  39599  dvsinax  40445  sge0xp  40964  mpt2exxg2  42441
  Copyright terms: Public domain W3C validator