Theorem xpexg 7695

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

Assertion

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

Proof of Theorem xpexg

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2113  Vcvv 3440   ∪ cun 3899   ⊆ wss 3901  𝒫 cpw 4554   × cxp 5622

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pow 5310  ax-pr 5377  ax-un 7680

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-opab 5161  df-xp 5630  df-rel 5631

This theorem is referenced by:  xpexd  7696  3xpexg  7697  xpex  7698  sqxpexg  7700  coexg  7871  fex2  7878  fabexgOLD  7881  resfunexgALT  7892  fnexALT  7895  funexw  7896  opabex3d  7909  opabex3rd  7910  opabex3  7911  mpoexxg  8019  fnwelem  8073  naddunif  8621  pmex  8768  mapexOLD  8769  pmvalg  8774  elpmg  8780  fvdiagfn  8829  ixpexg  8860  snmapen  8975  xpdom2  9000  xpdom3  9003  omxpen  9007  fodomr  9056  disjenex  9063  domssex2  9065  domssex  9066  mapxpen  9071  fczfsuppd  9289  brwdom2  9478  xpwdomg  9490  unxpwdom2  9493  djuex  9820  djuexALT  9834  fseqen  9937  djuassen  10089  mapdjuen  10091  djudom1  10093  djuinf  10099  hsmexlem2  10337  axdc2lem  10358  iundom2g  10450  fpwwe2lem12  10553  pwsbas  17407  pwsle  17413  pwssca  17417  isga  19220  efgtf  19651  frgpcpbl  19688  frgp0  19689  frgpeccl  19690  frgpadd  19692  frgpmhm  19694  vrgpf  19697  vrgpinv  19698  frgpupf  19702  frgpup1  19704  frgpup2  19705  frgpup3lem  19706  frgpnabllem1  19802  frgpnabllem2  19803  gsum2d2  19903  gsumcom2  19904  dprd2da  19973  pwssplit3  21013  mpofrlmd  21732  frlmip  21733  mattposvs  22399  mat1dimelbas  22415  mdetrlin  22546  lmfval  23176  txbasex  23510  txopn  23546  txrest  23575  txindislem  23577  xkoinjcn  23631  blfvalps  24327  bcthlem1  25280  bcthlem5  25284  rrxip  25346  isvcOLD  30654  resf1o  32809  locfinref  33998  esum2dlem  34249  esum2d  34250  elsx  34351  satfv0  35552  satf00  35568  filnetlem3  36574  filnetlem4  36575  bj-xpexg2  37161  inxpex  38528  xrninxpex  38598  aks6d1c2  42380  relexpxpnnidm  43940  enrelmap  44234  mpoexxg2  48580  eufsn2  49084