Theorem xpexg 7791

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

Assertion

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

Proof of Theorem xpexg

Step	Hyp	Ref	Expression
1		xpsspw 5793	. 2 ⊢ (𝐴 × 𝐵) ⊆ 𝒫 𝒫 (𝐴 ∪ 𝐵)
2		unexg 7787	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∪ 𝐵) ∈ V)
3		pwexg 5345	. . 3 ⊢ ((𝐴 ∪ 𝐵) ∈ V → 𝒫 (𝐴 ∪ 𝐵) ∈ V)
4		pwexg 5345	. . 3 ⊢ (𝒫 (𝐴 ∪ 𝐵) ∈ V → 𝒫 𝒫 (𝐴 ∪ 𝐵) ∈ V)
5	2, 3, 4	3syl 19	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝒫 𝒫 (𝐴 ∪ 𝐵) ∈ V)
6		ssexg 5286	. 2 ⊢ (((𝐴 × 𝐵) ⊆ 𝒫 𝒫 (𝐴 ∪ 𝐵) ∧ 𝒫 𝒫 (𝐴 ∪ 𝐵) ∈ V) → (𝐴 × 𝐵) ∈ V)
7	1, 5, 6	sylancr 599	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 × 𝐵) ∈ V)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2147  Vcvv 3454   ⊆ wss 3900   ∪ cun 4152  𝒫 cpw 4560   × cxp 5654

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-sep 5253  ax-pow 5332  ax-pr 5396  ax-un 7778

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-opab 5172  df-xp 5662  df-rel 5663

This theorem is used by:  xpexd  7792  3xpexg  7793  xpex  7794  sqxpexg  7796  coexg  7968  fex2  7975  resfunexgALT  7987  fnexALT  7990  funexw  7991  opabex3d  8004  opabex3rd  8005  opabex3  8006  mpoexxg  8116  fnwelem  8173  naddunif  8734  pmex  8883  pmvalg  8888  elpmg  8894  fvdiagfn  8950  ixpexg  8981  snmapen  9097  xpdom2  9122  xpdom3  9125  omxpen  9129  fodomr  9178  disjenex  9185  domssex2  9187  domssex  9188  mapxpen  9193  fczfsuppd  9408  brwdom2  9597  xpwdomg  9609  unxpwdom2  9612  djuex  10019  djuexALT  10033  fseqen  10136  djuassen  10287  mapdjuen  10289  djudom1  10291  djuinf  10297  hsmexlem2  10535  axdc2lem  10556  iundom2g  10654  fpwwe2lem12  10757  pwsbas  17690  pwsle  17696  pwssca  17700  isga  19538  efgtf  19969  frgpcpbl  20006  frgp0  20007  frgpeccl  20008  frgpadd  20010  frgpmhm  20012  vrgpf  20015  vrgpinv  20016  frgpupf  20020  frgpup1  20022  frgpup2  20023  frgpup3lem  20024  frgpnabllem1  20120  frgpnabllem2  20121  gsum2d2  20221  gsumcom2  20222  dprd2da  20291  pwssplit3  21369  mpofrlmd  22116  frlmip  22117  mattposvs  22803  mat1dimelbas  22819  mdetrlin  22950  lmfval  23583  txbasex  23918  txopn  23954  txrest  23983  txindislem  23985  xkoinjcn  24039  blfvalps  24735  bcthlem1  25678  bcthlem5  25682  rrxip  25744  isvcOLD  31214  resf1o  33395  locfinref  34556  esum2dlem  34807  esum2d  34808  elsx  34910  satfv0  36303  satf00  36319  filnetlem3  37359  filnetlem4  37360  bj-xpexg2  38064  inxpex  39474  xrninxpex  39552  aks6d1c2  43383  relexpxpnnidm  44906  enrelmap  45200  mpoexxg2  49665  eufsn2  50169