ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  xpexg GIF version

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
StepHypRef Expression
1 xpsspw 4756 . 2 (𝐴 × 𝐵) ⊆ 𝒫 𝒫 (𝐴𝐵)
2 unexg 4461 . . 3 ((𝐴𝑉𝐵𝑊) → (𝐴𝐵) ∈ V)
3 pwexg 4198 . . 3 ((𝐴𝐵) ∈ V → 𝒫 (𝐴𝐵) ∈ V)
4 pwexg 4198 . . 3 (𝒫 (𝐴𝐵) ∈ V → 𝒫 𝒫 (𝐴𝐵) ∈ V)
52, 3, 43syl 17 . 2 ((𝐴𝑉𝐵𝑊) → 𝒫 𝒫 (𝐴𝐵) ∈ V)
6 ssexg 4157 . 2 (((𝐴 × 𝐵) ⊆ 𝒫 𝒫 (𝐴𝐵) ∧ 𝒫 𝒫 (𝐴𝐵) ∈ V) → (𝐴 × 𝐵) ∈ V)
71, 5, 6sylancr 414 1 ((𝐴𝑉𝐵𝑊) → (𝐴 × 𝐵) ∈ V)
Colors of variables: wff set class
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
  Copyright terms: Public domain W3C validator