Theorem xpexg 7736

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

Assertion

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

Proof of Theorem xpexg

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

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2106  Vcvv 3474   ∪ cun 3946   ⊆ wss 3948  𝒫 cpw 4602   × cxp 5674

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7724

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-opab 5211  df-xp 5682  df-rel 5683

This theorem is referenced by:  xpexd  7737  3xpexg  7738  xpex  7739  sqxpexg  7741  coexg  7919  fex2  7923  fabexg  7924  resfunexgALT  7933  fnexALT  7936  funexw  7937  opabex3d  7951  opabex3rd  7952  opabex3  7953  mpoexxg  8061  fnwelem  8116  naddunif  8691  pmex  8824  mapex  8825  pmvalg  8830  elpmg  8836  fvdiagfn  8884  ixpexg  8915  snmapen  9037  xpdom2  9066  xpdom3  9069  omxpen  9073  fodomr  9127  disjenex  9134  domssex2  9136  domssex  9137  mapxpen  9142  xpfiOLD  9317  fczfsuppd  9380  brwdom2  9567  xpwdomg  9579  unxpwdom2  9582  djuex  9902  djuexALT  9916  fseqen  10021  djuassen  10172  mapdjuen  10174  djudom1  10176  djuinf  10182  hsmexlem2  10421  axdc2lem  10442  iundom2g  10534  fpwwe2lem12  10636  pwsbas  17432  pwsle  17437  pwssca  17441  isga  19154  efgtf  19589  frgpcpbl  19626  frgp0  19627  frgpeccl  19628  frgpadd  19630  frgpmhm  19632  vrgpf  19635  vrgpinv  19636  frgpupf  19640  frgpup1  19642  frgpup2  19643  frgpup3lem  19644  frgpnabllem1  19740  frgpnabllem2  19741  gsum2d2  19841  gsumcom2  19842  dprd2da  19911  pwssplit3  20671  mpofrlmd  21331  frlmip  21332  mattposvs  21956  mat1dimelbas  21972  mdetrlin  22103  lmfval  22735  txbasex  23069  txopn  23105  txrest  23134  txindislem  23136  xkoinjcn  23190  blfvalps  23888  bcthlem1  24840  bcthlem5  24844  rrxip  24906  isvcOLD  29827  resf1o  31950  locfinref  32816  esum2dlem  33085  esum2d  33086  elsx  33187  satfv0  34344  satf00  34360  filnetlem3  35260  filnetlem4  35261  bj-xpexg2  35836  inxpex  37203  xrninxpex  37259  relexpxpnnidm  42444  enrelmap  42738  mpoexxg2  47003  eufsn2  47499