Theorem xpexg 7464

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

Assertion

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

Proof of Theorem xpexg

Step	Hyp	Ref	Expression
1		xpsspw 5644	. 2 ⊢ (𝐴 × 𝐵) ⊆ 𝒫 𝒫 (𝐴 ∪ 𝐵)
2		unexg 7463	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∪ 𝐵) ∈ V)
3		pwexg 5240	. . 3 ⊢ ((𝐴 ∪ 𝐵) ∈ V → 𝒫 (𝐴 ∪ 𝐵) ∈ V)
4		pwexg 5240	. . 3 ⊢ (𝒫 (𝐴 ∪ 𝐵) ∈ V → 𝒫 𝒫 (𝐴 ∪ 𝐵) ∈ V)
5	2, 3, 4	3syl 18	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝒫 𝒫 (𝐴 ∪ 𝐵) ∈ V)
6		ssexg 5186	. 2 ⊢ (((𝐴 × 𝐵) ⊆ 𝒫 𝒫 (𝐴 ∪ 𝐵) ∧ 𝒫 𝒫 (𝐴 ∪ 𝐵) ∈ V) → (𝐴 × 𝐵) ∈ V)
7	1, 5, 6	sylancr 591	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 × 𝐵) ∈ V)

Syntax hints:   → wi 4   ∧ wa 400   ∈ wcel 2112  Vcvv 3407   ∪ cun 3852   ⊆ wss 3854  𝒫 cpw 4487   × cxp 5515

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2730  ax-sep 5162  ax-nul 5169  ax-pow 5227  ax-pr 5291  ax-un 7452

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 846  df-3an 1087  df-tru 1542  df-ex 1783  df-nf 1787  df-sb 2071  df-clab 2737  df-cleq 2751  df-clel 2831  df-ral 3073  df-rex 3074  df-rab 3077  df-v 3409  df-dif 3857  df-un 3859  df-in 3861  df-ss 3871  df-nul 4222  df-if 4414  df-pw 4489  df-sn 4516  df-pr 4518  df-op 4522  df-uni 4792  df-opab 5088  df-xp 5523  df-rel 5524

This theorem is referenced by:  xpexd  7465  3xpexg  7466  xpex  7467  sqxpexg  7469  coexg  7632  fex2  7636  fabexg  7637  resfunexgALT  7646  fnexALT  7649  funexw  7650  opabex3d  7663  opabex3rd  7664  opabex3  7665  mpoexxg  7771  fnwelem  7823  pmex  8414  mapex  8415  pmvalg  8420  elpmg  8425  fvdiagfn  8466  ixpexg  8497  snmapen  8602  xpdom2  8625  xpdom3  8628  omxpen  8632  fodomr  8682  disjenex  8689  domssex2  8691  domssex  8692  mapxpen  8697  xpfi  8807  fczfsuppd  8869  brwdom2  9055  xpwdomg  9067  unxpwdom2  9070  djuex  9355  djuexALT  9369  fseqen  9472  djuassen  9623  mapdjuen  9625  djudom1  9627  djuinf  9633  hsmexlem2  9872  axdc2lem  9893  iundom2g  9985  fpwwe2lem12  10087  pwsbas  16803  pwsle  16808  pwssca  16812  isga  18473  efgtf  18900  frgpcpbl  18937  frgp0  18938  frgpeccl  18939  frgpadd  18941  frgpmhm  18943  vrgpf  18946  vrgpinv  18947  frgpupf  18951  frgpup1  18953  frgpup2  18954  frgpup3lem  18955  frgpnabllem1  19046  frgpnabllem2  19047  gsum2d2  19147  gsumcom2  19148  dprd2da  19217  pwssplit3  19886  mpofrlmd  20527  frlmip  20528  mattposvs  21140  mat1dimelbas  21156  mdetrlin  21287  lmfval  21917  txbasex  22251  txopn  22287  txcn  22311  txrest  22316  txindislem  22318  xkoinjcn  22372  blfvalps  23070  bcthlem1  24009  bcthlem5  24013  rrxip  24075  isvcOLD  28446  resf1o  30574  locfinref  31297  esum2dlem  31564  esum2d  31565  elsx  31666  satfv0  32821  satf00  32837  filnetlem3  34103  filnetlem4  34104  bj-xpexg2  34662  inxpex  36021  xrninxpex  36067  relexpxpnnidm  40762  enrelmap  41056  mpoexxg2  45091