Theorem xpexg 7126

Description: The Cartesian product of two sets is a set. Proposition 6.2 of [TakeutiZaring] p. 23. See also xpexgALT 7327. (Contributed by NM, 14-Aug-1994.)

Assertion

Ref	Expression
xpexg	⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 × 𝐵) ∈ V)

Proof of Theorem xpexg

Step	Hyp	Ref	Expression
1		xpsspw 5389	. 2 ⊢ (𝐴 × 𝐵) ⊆ 𝒫 𝒫 (𝐴 ∪ 𝐵)
2		unexg 7125	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∪ 𝐵) ∈ V)
3		pwexg 4999	. . 3 ⊢ ((𝐴 ∪ 𝐵) ∈ V → 𝒫 (𝐴 ∪ 𝐵) ∈ V)
4		pwexg 4999	. . 3 ⊢ (𝒫 (𝐴 ∪ 𝐵) ∈ V → 𝒫 𝒫 (𝐴 ∪ 𝐵) ∈ V)
5	2, 3, 4	3syl 18	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝒫 𝒫 (𝐴 ∪ 𝐵) ∈ V)
6		ssexg 4956	. 2 ⊢ (((𝐴 × 𝐵) ⊆ 𝒫 𝒫 (𝐴 ∪ 𝐵) ∧ 𝒫 𝒫 (𝐴 ∪ 𝐵) ∈ V) → (𝐴 × 𝐵) ∈ V)
7	1, 5, 6	sylancr 698	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 × 𝐵) ∈ V)

Syntax hints:   → wi 4   ∧ wa 383   ∈ wcel 2139  Vcvv 3340   ∪ cun 3713   ⊆ wss 3715  𝒫 cpw 4302   × cxp 5264

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-8 2141  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-sep 4933  ax-nul 4941  ax-pow 4992  ax-pr 5055  ax-un 7115

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ral 3055  df-rex 3056  df-rab 3059  df-v 3342  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-nul 4059  df-if 4231  df-pw 4304  df-sn 4322  df-pr 4324  df-op 4328  df-uni 4589  df-opab 4865  df-xp 5272  df-rel 5273

This theorem is referenced by:  3xpexg  7127  xpex  7128  sqxpexg  7129  cnvexg  7278  coexg  7283  fex2  7287  fabexg  7288  resfunexgALT  7295  cofunexg  7296  fnexALT  7298  opabex3d  7311  opabex3  7312  oprabexd  7321  ofmresex  7331  opabex2  7395  mpt2exxg  7413  offval22  7422  fnwelem  7461  tposexg  7536  pmex  8030  mapex  8031  pmvalg  8036  elpmg  8041  fvdiagfn  8070  ixpexg  8100  map1  8203  xpdom2  8222  xpdom3  8225  omxpen  8229  fodomr  8278  disjenex  8285  domssex2  8287  domssex  8288  mapxpen  8293  xpfi  8398  fczfsuppd  8460  marypha1  8507  brwdom2  8645  wdom2d  8652  xpwdomg  8657  unxpwdom2  8660  ixpiunwdom  8663  djuex  8946  djuexALT  8958  fseqen  9060  cdaval  9204  cdaassen  9216  mapcdaen  9218  cdadom1  9220  cdainf  9226  hsmexlem2  9461  axdc2lem  9482  fnct  9571  iundom2g  9574  fpwwe2lem2  9666  fpwwe2lem5  9668  fpwwe2lem12  9675  fpwwe2lem13  9676  fpwwelem  9679  canthwe  9685  pwxpndom  9700  gchhar  9713  wrdexg  13521  trclexlem  13954  pwsbas  16369  pwsle  16374  pwssca  16378  isacs1i  16539  rescval2  16709  reschom  16711  rescabs  16714  setccofval  16953  isga  17944  sylow2a  18254  lsmhash  18338  efgtf  18355  frgpcpbl  18392  frgp0  18393  frgpeccl  18394  frgpadd  18396  frgpmhm  18398  vrgpf  18401  vrgpinv  18402  frgpupf  18406  frgpup1  18408  frgpup2  18409  frgpup3lem  18410  frgpnabllem1  18496  frgpnabllem2  18497  gsum2d2  18593  gsumcom2  18594  gsumxp  18595  dprd2da  18661  pwssplit3  19283  opsrval  19696  opsrtoslem2  19707  evlslem4  19730  mpt2frlmd  20338  frlmip  20339  matbas2d  20451  mattposvs  20483  mat1dimelbas  20499  mdetrlin  20630  lmfval  21258  txbasex  21591  txopn  21627  txcn  21651  txrest  21656  txindislem  21658  xkoinjcn  21712  tsmsxp  22179  ustssel  22230  ustfilxp  22237  trust  22254  restutop  22262  trcfilu  22319  cfiluweak  22320  imasdsf1olem  22399  blfvalps  22409  metustfbas  22583  restmetu  22596  bcthlem1  23341  bcthlem5  23345  rrxip  23398  perpln1  25825  perpln2  25826  isperp  25827  isleag  25953  isvcOLD  27764  resf1o  29835  locfinref  30238  metidval  30263  esum2dlem  30484  esum2d  30485  esumiun  30486  elsx  30587  madeval  32262  filnetlem3  32702  filnetlem4  32703  bj-xpexg2  33271  isrngod  34028  isgrpda  34085  iscringd  34128  inxpex  34449  xrninxpex  34493  wdom2d2  38122  unxpwdom3  38185  trclubgNEW  38445  relexpxpnnidm  38515  relexpxpmin  38529  enrelmap  38811  rfovd  38815  rfovcnvf1od  38818  fsovrfovd  38823  xpexd  39802  dvsinax  40648  sge0xp  41167  mpt2exxg2  42644