Theorem xpexg 7748

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

Assertion

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

Proof of Theorem xpexg

Step	Hyp	Ref	Expression
1		xpsspw 5806	. 2 ⊢ (𝐴 × 𝐵) ⊆ 𝒫 𝒫 (𝐴 ∪ 𝐵)
2		unexg 7747	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∪ 𝐵) ∈ V)
3		pwexg 5373	. . 3 ⊢ ((𝐴 ∪ 𝐵) ∈ V → 𝒫 (𝐴 ∪ 𝐵) ∈ V)
4		pwexg 5373	. . 3 ⊢ (𝒫 (𝐴 ∪ 𝐵) ∈ V → 𝒫 𝒫 (𝐴 ∪ 𝐵) ∈ V)
5	2, 3, 4	3syl 18	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝒫 𝒫 (𝐴 ∪ 𝐵) ∈ V)
6		ssexg 5319	. 2 ⊢ (((𝐴 × 𝐵) ⊆ 𝒫 𝒫 (𝐴 ∪ 𝐵) ∧ 𝒫 𝒫 (𝐴 ∪ 𝐵) ∈ V) → (𝐴 × 𝐵) ∈ V)
7	1, 5, 6	sylancr 585	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 × 𝐵) ∈ V)

Syntax hints:   → wi 4   ∧ wa 394   ∈ wcel 2099  Vcvv 3463   ∪ cun 3945   ⊆ wss 3947  𝒫 cpw 4598   × cxp 5671

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2697  ax-sep 5295  ax-nul 5302  ax-pow 5360  ax-pr 5424  ax-un 7736

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-sb 2061  df-clab 2704  df-cleq 2718  df-clel 2803  df-ral 3052  df-rex 3061  df-rab 3421  df-v 3465  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4324  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-op 4631  df-uni 4907  df-opab 5207  df-xp 5679  df-rel 5680

This theorem is referenced by:  xpexd  7749  3xpexg  7750  xpex  7751  sqxpexg  7753  coexg  7932  fex2  7937  fabexgOLD  7940  resfunexgALT  7951  fnexALT  7954  funexw  7955  opabex3d  7969  opabex3rd  7970  opabex3  7971  mpoexxg  8079  fnwelem  8135  naddunif  8713  pmex  8850  mapexOLD  8851  pmvalg  8856  elpmg  8862  fvdiagfn  8910  ixpexg  8941  snmapen  9064  xpdom2  9095  xpdom3  9098  omxpen  9102  fodomr  9156  disjenex  9163  domssex2  9165  domssex  9166  mapxpen  9171  xpfiOLD  9352  fczfsuppd  9420  brwdom2  9607  xpwdomg  9619  unxpwdom2  9622  djuex  9942  djuexALT  9956  fseqen  10061  djuassen  10212  mapdjuen  10214  djudom1  10216  djuinf  10222  hsmexlem2  10459  axdc2lem  10480  iundom2g  10572  fpwwe2lem12  10674  pwsbas  17495  pwsle  17500  pwssca  17504  isga  19279  efgtf  19714  frgpcpbl  19751  frgp0  19752  frgpeccl  19753  frgpadd  19755  frgpmhm  19757  vrgpf  19760  vrgpinv  19761  frgpupf  19765  frgpup1  19767  frgpup2  19768  frgpup3lem  19769  frgpnabllem1  19865  frgpnabllem2  19866  gsum2d2  19966  gsumcom2  19967  dprd2da  20036  pwssplit3  21033  mpofrlmd  21769  frlmip  21770  mattposvs  22443  mat1dimelbas  22459  mdetrlin  22590  lmfval  23222  txbasex  23556  txopn  23592  txrest  23621  txindislem  23623  xkoinjcn  23677  blfvalps  24375  bcthlem1  25338  bcthlem5  25342  rrxip  25404  isvcOLD  30507  resf1o  32642  locfinref  33667  esum2dlem  33936  esum2d  33937  elsx  34038  satfv0  35197  satf00  35213  filnetlem3  36103  filnetlem4  36104  bj-xpexg2  36678  inxpex  38048  xrninxpex  38103  aks6d1c2  41840  relexpxpnnidm  43405  enrelmap  43699  mpoexxg2  47750  eufsn2  48244