Theorem xpexg 7737

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

Assertion

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

Proof of Theorem xpexg

Step	Hyp	Ref	Expression
1		xpsspw 5787	. 2 ⊢ (𝐴 × 𝐵) ⊆ 𝒫 𝒫 (𝐴 ∪ 𝐵)
2		unexg 7730	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∪ 𝐵) ∈ V)
3		pwexg 5340	. . 3 ⊢ ((𝐴 ∪ 𝐵) ∈ V → 𝒫 (𝐴 ∪ 𝐵) ∈ V)
4		pwexg 5340	. . 3 ⊢ (𝒫 (𝐴 ∪ 𝐵) ∈ V → 𝒫 𝒫 (𝐴 ∪ 𝐵) ∈ V)
5	2, 3, 4	3syl 19	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝒫 𝒫 (𝐴 ∪ 𝐵) ∈ V)
6		ssexg 5284	. 2 ⊢ (((𝐴 × 𝐵) ⊆ 𝒫 𝒫 (𝐴 ∪ 𝐵) ∧ 𝒫 𝒫 (𝐴 ∪ 𝐵) ∈ V) → (𝐴 × 𝐵) ∈ V)
7	1, 5, 6	sylancr 598	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 × 𝐵) ∈ V)

Syntax hints:   → wi 4   ∧ wa 400   ∈ wcel 2145  Vcvv 3457   ∪ cun 3905   ⊆ wss 3907  𝒫 cpw 4558   × cxp 5650

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737  ax-sep 5251  ax-pow 5327  ax-pr 5395  ax-un 7722

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-ral 3080  df-rex 3090  df-rab 3418  df-v 3459  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-nul 4289  df-if 4484  df-pw 4560  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4869  df-opab 5168  df-xp 5658  df-rel 5659

This theorem is referenced by:  xpexd  7738  3xpexg  7739  xpex  7740  sqxpexg  7742  coexg  7914  fex2  7921  resfunexgALT  7933  fnexALT  7936  funexw  7937  opabex3d  7950  opabex3rd  7951  opabex3  7952  mpoexxg  8060  fnwelem  8115  naddunif  8668  pmex  8817  pmvalg  8822  elpmg  8828  fvdiagfn  8877  ixpexg  8908  snmapen  9023  xpdom2  9048  xpdom3  9051  omxpen  9055  fodomr  9104  disjenex  9111  domssex2  9113  domssex  9114  mapxpen  9119  fczfsuppd  9334  brwdom2  9523  xpwdomg  9535  unxpwdom2  9538  djuex  9882  djuexALT  9896  fseqen  9999  djuassen  10150  mapdjuen  10152  djudom1  10154  djuinf  10160  hsmexlem2  10399  axdc2lem  10420  iundom2g  10512  fpwwe2lem12  10615  pwsbas  17530  pwsle  17536  pwssca  17540  isga  19352  efgtf  19783  frgpcpbl  19820  frgp0  19821  frgpeccl  19822  frgpadd  19824  frgpmhm  19826  vrgpf  19829  vrgpinv  19830  frgpupf  19834  frgpup1  19836  frgpup2  19837  frgpup3lem  19838  frgpnabllem1  19934  frgpnabllem2  19935  gsum2d2  20035  gsumcom2  20036  dprd2da  20105  pwssplit3  21151  mpofrlmd  21887  frlmip  21888  mattposvs  22573  mat1dimelbas  22589  mdetrlin  22720  lmfval  23350  txbasex  23684  txopn  23720  txrest  23749  txindislem  23751  xkoinjcn  23805  blfvalps  24501  bcthlem1  25444  bcthlem5  25448  rrxip  25510  isvcOLD  30840  resf1o  32987  locfinref  34148  esum2dlem  34399  esum2d  34400  elsx  34501  satfv0  35721  satf00  35737  filnetlem3  36753  filnetlem4  36754  bj-xpexg2  37457  inxpex  38850  xrninxpex  38928  aks6d1c2  42759  relexpxpnnidm  44291  enrelmap  44585  mpoexxg2  48969  eufsn2  49472