Theorem xpexg 7750

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

Assertion

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

Proof of Theorem xpexg

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

Syntax hints:   → wi 4   ∧ wa 400   ∈ wcel 2143  Vcvv 3455   ∪ cun 3904   ⊆ wss 3906  𝒫 cpw 4563   × cxp 5661

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-sep 5258  ax-pow 5338  ax-pr 5406  ax-un 7734

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4489  df-pw 4565  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4874  df-opab 5175  df-xp 5669  df-rel 5670

This theorem is referenced by:  xpexd  7751  3xpexg  7752  xpex  7753  sqxpexg  7755  coexg  7927  fex2  7934  resfunexgALT  7946  fnexALT  7949  funexw  7950  opabex3d  7963  opabex3rd  7964  opabex3  7965  mpoexxg  8073  fnwelem  8128  naddunif  8681  pmex  8830  pmvalg  8835  elpmg  8841  fvdiagfn  8890  ixpexg  8921  snmapen  9036  xpdom2  9061  xpdom3  9064  omxpen  9068  fodomr  9117  disjenex  9124  domssex2  9126  domssex  9127  mapxpen  9132  fczfsuppd  9347  brwdom2  9536  xpwdomg  9548  unxpwdom2  9551  djuex  9895  djuexALT  9909  fseqen  10012  djuassen  10163  mapdjuen  10165  djudom1  10167  djuinf  10173  hsmexlem2  10412  axdc2lem  10433  iundom2g  10525  fpwwe2lem12  10628  pwsbas  17541  pwsle  17547  pwssca  17551  isga  19362  efgtf  19793  frgpcpbl  19830  frgp0  19831  frgpeccl  19832  frgpadd  19834  frgpmhm  19836  vrgpf  19839  vrgpinv  19840  frgpupf  19844  frgpup1  19846  frgpup2  19847  frgpup3lem  19848  frgpnabllem1  19944  frgpnabllem2  19945  gsum2d2  20045  gsumcom2  20046  dprd2da  20115  pwssplit3  21163  mpofrlmd  21908  frlmip  21909  mattposvs  22593  mat1dimelbas  22609  mdetrlin  22740  lmfval  23370  txbasex  23704  txopn  23740  txrest  23769  txindislem  23771  xkoinjcn  23825  blfvalps  24521  bcthlem1  25464  bcthlem5  25468  rrxip  25530  isvcOLD  30912  resf1o  33056  locfinref  34212  esum2dlem  34463  esum2d  34464  elsx  34565  satfv0  35831  satf00  35847  filnetlem3  36872  filnetlem4  36873  bj-xpexg2  37577  inxpex  38969  xrninxpex  39047  aks6d1c2  42878  relexpxpnnidm  44412  enrelmap  44706  mpoexxg2  49101  eufsn2  49604