Theorem xpexg 4871

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2205  Vcvv 2815   ∪ cun 3212   ⊆ wss 3214  𝒫 cpw 3675   × cxp 4754

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-14 2208  ax-ext 2216  ax-sep 4234  ax-pow 4293  ax-pr 4328  ax-un 4560

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-rex 2528  df-v 2817  df-un 3218  df-in 3220  df-ss 3227  df-pw 3677  df-sn 3701  df-pr 3702  df-op 3704  df-uni 3921  df-opab 4178  df-xp 4762

This theorem is referenced by:  xpexd  4872  xpex  4873  sqxpexg  4875  resiexg  5090  cnvexg  5307  coexg  5314  fex2  5538  fabexg  5561  resfunexgALT  6312  cofunexg  6313  fnexALT  6315  funexw  6316  opabex3d  6325  opabex3  6326  oprabexd  6335  ofmresex  6345  mpoexxg  6421  tposexg  6504  erex  6806  pmex  6902  mapex  6903  pmvalg  6908  elpmg  6913  fvdiagfn  6943  ixpexgg  6972  ixpsnf1o  6986  map1  7069  xpdom2  7097  xpdom3m  7100  xpen  7113  mapxpen  7116  xpfi  7207  djuex  7349  djuassen  7539  cc2lem  7598  shftfvalg  11533  climconst2  12007  mulgnngsum  13886  releqgg  13979  eqgex  13980  eqgfval  13981  prdsval  14121  prdsbaslemss  14122  pwsval  14152  pwsbas  14153  dvdsrvald  14344  dvdsrex  14349  aprval  14535  aprap  14542  psrval  14946  psrbasg  14961  psrplusgg  14965  lmfval  15190  txbasex  15254  txopn  15262  txcn  15272  txrest  15273  blfvalps  15382  xmetxp  15504  limccnp2lem  15673  limccnp2cntop  15674  dvfvalap  15678