Theorem xpexg 7590

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

Assertion

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

Proof of Theorem xpexg

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

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2106  Vcvv 3429   ∪ cun 3884   ⊆ wss 3886  𝒫 cpw 4533   × cxp 5582

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-12 2171  ax-ext 2709  ax-sep 5221  ax-nul 5228  ax-pow 5286  ax-pr 5350  ax-un 7578

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3431  df-dif 3889  df-un 3891  df-in 3893  df-ss 3903  df-nul 4257  df-if 4460  df-pw 4535  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-opab 5136  df-xp 5590  df-rel 5591

This theorem is referenced by:  xpexd  7591  3xpexg  7592  xpex  7593  sqxpexg  7595  coexg  7766  fex2  7770  fabexg  7771  resfunexgALT  7780  fnexALT  7783  funexw  7784  opabex3d  7797  opabex3rd  7798  opabex3  7799  mpoexxg  7905  fnwelem  7959  pmex  8607  mapex  8608  pmvalg  8613  elpmg  8618  fvdiagfn  8666  ixpexg  8697  snmapen  8815  xpdom2  8841  xpdom3  8844  omxpen  8848  fodomr  8902  disjenex  8909  domssex2  8911  domssex  8912  mapxpen  8917  xpfi  9072  fczfsuppd  9133  brwdom2  9319  xpwdomg  9331  unxpwdom2  9334  djuex  9676  djuexALT  9690  fseqen  9793  djuassen  9944  mapdjuen  9946  djudom1  9948  djuinf  9954  hsmexlem2  10193  axdc2lem  10214  iundom2g  10306  fpwwe2lem12  10408  pwsbas  17208  pwsle  17213  pwssca  17217  isga  18907  efgtf  19338  frgpcpbl  19375  frgp0  19376  frgpeccl  19377  frgpadd  19379  frgpmhm  19381  vrgpf  19384  vrgpinv  19385  frgpupf  19389  frgpup1  19391  frgpup2  19392  frgpup3lem  19393  frgpnabllem1  19484  frgpnabllem2  19485  gsum2d2  19585  gsumcom2  19586  dprd2da  19655  pwssplit3  20333  mpofrlmd  20994  frlmip  20995  mattposvs  21614  mat1dimelbas  21630  mdetrlin  21761  lmfval  22393  txbasex  22727  txopn  22763  txrest  22792  txindislem  22794  xkoinjcn  22848  blfvalps  23546  bcthlem1  24498  bcthlem5  24502  rrxip  24564  isvcOLD  28949  resf1o  31073  locfinref  31799  esum2dlem  32068  esum2d  32069  elsx  32170  satfv0  33328  satf00  33344  filnetlem3  34577  filnetlem4  34578  bj-xpexg2  35158  inxpex  36482  xrninxpex  36528  relexpxpnnidm  41292  enrelmap  41586  mpoexxg2  45651  eufsn2  46148