Theorem xpexg 4758

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

Assertion

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

Proof of Theorem xpexg

Step	Hyp	Ref	Expression
1		xpsspw 4756	. 2 ⊢ (𝐴 × 𝐵) ⊆ 𝒫 𝒫 (𝐴 ∪ 𝐵)
2		unexg 4461	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∪ 𝐵) ∈ V)
3		pwexg 4198	. . 3 ⊢ ((𝐴 ∪ 𝐵) ∈ V → 𝒫 (𝐴 ∪ 𝐵) ∈ V)
4		pwexg 4198	. . 3 ⊢ (𝒫 (𝐴 ∪ 𝐵) ∈ V → 𝒫 𝒫 (𝐴 ∪ 𝐵) ∈ V)
5	2, 3, 4	3syl 17	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝒫 𝒫 (𝐴 ∪ 𝐵) ∈ V)
6		ssexg 4157	. 2 ⊢ (((𝐴 × 𝐵) ⊆ 𝒫 𝒫 (𝐴 ∪ 𝐵) ∧ 𝒫 𝒫 (𝐴 ∪ 𝐵) ∈ V) → (𝐴 × 𝐵) ∈ V)
7	1, 5, 6	sylancr 414	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 × 𝐵) ∈ V)

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2160  Vcvv 2752   ∪ cun 3142   ⊆ wss 3144  𝒫 cpw 3590   × cxp 4642

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-13 2162  ax-14 2163  ax-ext 2171  ax-sep 4136  ax-pow 4192  ax-pr 4227  ax-un 4451

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2176  df-cleq 2182  df-clel 2185  df-nfc 2321  df-rex 2474  df-v 2754  df-un 3148  df-in 3150  df-ss 3157  df-pw 3592  df-sn 3613  df-pr 3614  df-op 3616  df-uni 3825  df-opab 4080  df-xp 4650

This theorem is referenced by:  xpex  4759  sqxpexg  4760  resiexg  4970  cnvexg  5184  coexg  5191  fex2  5403  fabexg  5422  resfunexgALT  6134  cofunexg  6135  fnexALT  6137  funexw  6138  opabex3d  6147  opabex3  6148  oprabexd  6153  ofmresex  6163  mpoexxg  6236  tposexg  6284  erex  6584  pmex  6680  mapex  6681  pmvalg  6686  elpmg  6691  fvdiagfn  6720  ixpexgg  6749  ixpsnf1o  6763  map1  6839  xpdom2  6858  xpdom3m  6861  xpen  6874  mapxpen  6877  xpfi  6959  djuex  7073  djuassen  7247  cc2lem  7296  shftfvalg  10862  climconst2  11334  mulgnngsum  13084  releqgg  13176  eqgex  13177  eqgfval  13178  reldvdsrsrg  13459  dvdsrvald  13460  dvdsrex  13465  aprval  13615  aprap  13619  psrval  13961  psrbasg  13968  psrplusgg  13971  lmfval  14169  txbasex  14234  txopn  14242  txcn  14252  txrest  14253  blfvalps  14362  xmetxp  14484  limccnp2lem  14622  limccnp2cntop  14623  dvfvalap  14627