Theorem xpexg 4777

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 4775	. 2 ⊢ (𝐴 × 𝐵) ⊆ 𝒫 𝒫 (𝐴 ∪ 𝐵)
2		unexg 4478	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∪ 𝐵) ∈ V)
3		pwexg 4213	. . 3 ⊢ ((𝐴 ∪ 𝐵) ∈ V → 𝒫 (𝐴 ∪ 𝐵) ∈ V)
4		pwexg 4213	. . 3 ⊢ (𝒫 (𝐴 ∪ 𝐵) ∈ V → 𝒫 𝒫 (𝐴 ∪ 𝐵) ∈ V)
5	2, 3, 4	3syl 17	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝒫 𝒫 (𝐴 ∪ 𝐵) ∈ V)
6		ssexg 4172	. 2 ⊢ (((𝐴 × 𝐵) ⊆ 𝒫 𝒫 (𝐴 ∪ 𝐵) ∧ 𝒫 𝒫 (𝐴 ∪ 𝐵) ∈ V) → (𝐴 × 𝐵) ∈ V)
7	1, 5, 6	sylancr 414	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 × 𝐵) ∈ V)

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2167  Vcvv 2763   ∪ cun 3155   ⊆ wss 3157  𝒫 cpw 3605   × cxp 4661

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 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-13 2169  ax-14 2170  ax-ext 2178  ax-sep 4151  ax-pow 4207  ax-pr 4242  ax-un 4468

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-rex 2481  df-v 2765  df-un 3161  df-in 3163  df-ss 3170  df-pw 3607  df-sn 3628  df-pr 3629  df-op 3631  df-uni 3840  df-opab 4095  df-xp 4669

This theorem is referenced by:  xpex  4778  sqxpexg  4779  resiexg  4991  cnvexg  5207  coexg  5214  fex2  5426  fabexg  5445  resfunexgALT  6165  cofunexg  6166  fnexALT  6168  funexw  6169  opabex3d  6178  opabex3  6179  oprabexd  6184  ofmresex  6194  mpoexxg  6268  tposexg  6316  erex  6616  pmex  6712  mapex  6713  pmvalg  6718  elpmg  6723  fvdiagfn  6752  ixpexgg  6781  ixpsnf1o  6795  map1  6871  xpdom2  6890  xpdom3m  6893  xpen  6906  mapxpen  6909  xpfi  6993  djuex  7109  djuassen  7284  cc2lem  7333  shftfvalg  10983  climconst2  11456  mulgnngsum  13257  releqgg  13350  eqgex  13351  eqgfval  13352  reldvdsrsrg  13648  dvdsrvald  13649  dvdsrex  13654  aprval  13838  aprap  13842  psrval  14220  psrbasg  14227  psrplusgg  14230  lmfval  14428  txbasex  14493  txopn  14501  txcn  14511  txrest  14512  blfvalps  14621  xmetxp  14743  limccnp2lem  14912  limccnp2cntop  14913  dvfvalap  14917