Theorem xpexg 7729

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

Assertion

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

Proof of Theorem xpexg

Step	Hyp	Ref	Expression
1		xpsspw 5780	. 2 ⊢ (𝐴 × 𝐵) ⊆ 𝒫 𝒫 (𝐴 ∪ 𝐵)
2		unexg 7722	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∪ 𝐵) ∈ V)
3		pwexg 5334	. . 3 ⊢ ((𝐴 ∪ 𝐵) ∈ V → 𝒫 (𝐴 ∪ 𝐵) ∈ V)
4		pwexg 5334	. . 3 ⊢ (𝒫 (𝐴 ∪ 𝐵) ∈ V → 𝒫 𝒫 (𝐴 ∪ 𝐵) ∈ V)
5	2, 3, 4	3syl 18	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝒫 𝒫 (𝐴 ∪ 𝐵) ∈ V)
6		ssexg 5278	. 2 ⊢ (((𝐴 × 𝐵) ⊆ 𝒫 𝒫 (𝐴 ∪ 𝐵) ∧ 𝒫 𝒫 (𝐴 ∪ 𝐵) ∈ V) → (𝐴 × 𝐵) ∈ V)
7	1, 5, 6	sylancr 596	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 × 𝐵) ∈ V)

Syntax hints:   → wi 4   ∧ wa 399   ∈ wcel 2141  Vcvv 3453   ∪ cun 3902   ⊆ wss 3904  𝒫 cpw 4554   × cxp 5643

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733  ax-sep 5245  ax-pow 5321  ax-pr 5389  ax-un 7714

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-ral 3076  df-rex 3086  df-rab 3414  df-v 3455  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-opab 5162  df-xp 5651  df-rel 5652

This theorem is referenced by:  xpexd  7730  3xpexg  7731  xpex  7732  sqxpexg  7734  coexg  7906  fex2  7913  resfunexgALT  7925  fnexALT  7928  funexw  7929  opabex3d  7942  opabex3rd  7943  opabex3  7944  mpoexxg  8052  fnwelem  8106  naddunif  8659  pmex  8808  mapexOLD  8809  pmvalg  8814  elpmg  8820  fvdiagfn  8869  ixpexg  8900  snmapen  9015  xpdom2  9040  xpdom3  9043  omxpen  9047  fodomr  9096  disjenex  9103  domssex2  9105  domssex  9106  mapxpen  9111  fczfsuppd  9329  brwdom2  9518  xpwdomg  9530  unxpwdom2  9533  djuex  9863  djuexALT  9877  fseqen  9980  djuassen  10132  mapdjuen  10134  djudom1  10136  djuinf  10142  hsmexlem2  10381  axdc2lem  10402  iundom2g  10494  fpwwe2lem12  10597  pwsbas  17499  pwsle  17505  pwssca  17509  isga  19314  efgtf  19745  frgpcpbl  19782  frgp0  19783  frgpeccl  19784  frgpadd  19786  frgpmhm  19788  vrgpf  19791  vrgpinv  19792  frgpupf  19796  frgpup1  19798  frgpup2  19799  frgpup3lem  19800  frgpnabllem1  19896  frgpnabllem2  19897  gsum2d2  19997  gsumcom2  19998  dprd2da  20067  pwssplit3  21108  mpofrlmd  21809  frlmip  21810  mattposvs  22495  mat1dimelbas  22511  mdetrlin  22642  lmfval  23272  txbasex  23606  txopn  23642  txrest  23671  txindislem  23673  xkoinjcn  23727  blfvalps  24423  bcthlem1  25366  bcthlem5  25370  rrxip  25432  isvcOLD  30728  resf1o  32882  locfinref  34099  esum2dlem  34350  esum2d  34351  elsx  34452  satfv0  35672  satf00  35688  filnetlem3  36704  filnetlem4  36705  bj-xpexg2  37409  inxpex  38802  xrninxpex  38880  aks6d1c2  42711  relexpxpnnidm  44243  enrelmap  44537  mpoexxg2  48924  eufsn2  49428