Theorem xpexg 7600

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

Assertion

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

Proof of Theorem xpexg

Step	Hyp	Ref	Expression
1		xpsspw 5719	. 2 ⊢ (𝐴 × 𝐵) ⊆ 𝒫 𝒫 (𝐴 ∪ 𝐵)
2		unexg 7599	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∪ 𝐵) ∈ V)
3		pwexg 5301	. . 3 ⊢ ((𝐴 ∪ 𝐵) ∈ V → 𝒫 (𝐴 ∪ 𝐵) ∈ V)
4		pwexg 5301	. . 3 ⊢ (𝒫 (𝐴 ∪ 𝐵) ∈ V → 𝒫 𝒫 (𝐴 ∪ 𝐵) ∈ V)
5	2, 3, 4	3syl 18	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝒫 𝒫 (𝐴 ∪ 𝐵) ∈ V)
6		ssexg 5247	. 2 ⊢ (((𝐴 × 𝐵) ⊆ 𝒫 𝒫 (𝐴 ∪ 𝐵) ∧ 𝒫 𝒫 (𝐴 ∪ 𝐵) ∈ V) → (𝐴 × 𝐵) ∈ V)
7	1, 5, 6	sylancr 587	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 × 𝐵) ∈ V)

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2106  Vcvv 3432   ∪ cun 3885   ⊆ wss 3887  𝒫 cpw 4533   × cxp 5587

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709  ax-sep 5223  ax-nul 5230  ax-pow 5288  ax-pr 5352  ax-un 7588

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-pw 4535  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-opab 5137  df-xp 5595  df-rel 5596

This theorem is referenced by:  xpexd  7601  3xpexg  7602  xpex  7603  sqxpexg  7605  coexg  7776  fex2  7780  fabexg  7781  resfunexgALT  7790  fnexALT  7793  funexw  7794  opabex3d  7808  opabex3rd  7809  opabex3  7810  mpoexxg  7916  fnwelem  7972  pmex  8620  mapex  8621  pmvalg  8626  elpmg  8631  fvdiagfn  8679  ixpexg  8710  snmapen  8828  xpdom2  8854  xpdom3  8857  omxpen  8861  fodomr  8915  disjenex  8922  domssex2  8924  domssex  8925  mapxpen  8930  xpfi  9085  fczfsuppd  9146  brwdom2  9332  xpwdomg  9344  unxpwdom2  9347  djuex  9666  djuexALT  9680  fseqen  9783  djuassen  9934  mapdjuen  9936  djudom1  9938  djuinf  9944  hsmexlem2  10183  axdc2lem  10204  iundom2g  10296  fpwwe2lem12  10398  pwsbas  17198  pwsle  17203  pwssca  17207  isga  18897  efgtf  19328  frgpcpbl  19365  frgp0  19366  frgpeccl  19367  frgpadd  19369  frgpmhm  19371  vrgpf  19374  vrgpinv  19375  frgpupf  19379  frgpup1  19381  frgpup2  19382  frgpup3lem  19383  frgpnabllem1  19474  frgpnabllem2  19475  gsum2d2  19575  gsumcom2  19576  dprd2da  19645  pwssplit3  20323  mpofrlmd  20984  frlmip  20985  mattposvs  21604  mat1dimelbas  21620  mdetrlin  21751  lmfval  22383  txbasex  22717  txopn  22753  txrest  22782  txindislem  22784  xkoinjcn  22838  blfvalps  23536  bcthlem1  24488  bcthlem5  24492  rrxip  24554  isvcOLD  28941  resf1o  31065  locfinref  31791  esum2dlem  32060  esum2d  32061  elsx  32162  satfv0  33320  satf00  33336  filnetlem3  34569  filnetlem4  34570  bj-xpexg2  35150  inxpex  36474  xrninxpex  36520  relexpxpnnidm  41311  enrelmap  41605  mpoexxg2  45673  eufsn2  46170