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

Theorem xpexg 4513
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 4511 . 2 (𝐴 × 𝐵) ⊆ 𝒫 𝒫 (𝐴𝐵)
2 unexg 4235 . . 3 ((𝐴𝑉𝐵𝑊) → (𝐴𝐵) ∈ V)
3 pwexg 3983 . . 3 ((𝐴𝐵) ∈ V → 𝒫 (𝐴𝐵) ∈ V)
4 pwexg 3983 . . 3 (𝒫 (𝐴𝐵) ∈ V → 𝒫 𝒫 (𝐴𝐵) ∈ V)
52, 3, 43syl 17 . 2 ((𝐴𝑉𝐵𝑊) → 𝒫 𝒫 (𝐴𝐵) ∈ V)
6 ssexg 3946 . 2 (((𝐴 × 𝐵) ⊆ 𝒫 𝒫 (𝐴𝐵) ∧ 𝒫 𝒫 (𝐴𝐵) ∈ V) → (𝐴 × 𝐵) ∈ V)
71, 5, 6sylancr 405 1 ((𝐴𝑉𝐵𝑊) → (𝐴 × 𝐵) ∈ V)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102  wcel 1436  Vcvv 2614  cun 2984  wss 2986  𝒫 cpw 3409   × cxp 4402
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 663  ax-5 1379  ax-7 1380  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-8 1438  ax-10 1439  ax-11 1440  ax-i12 1441  ax-bndl 1442  ax-4 1443  ax-13 1447  ax-14 1448  ax-17 1462  ax-i9 1466  ax-ial 1470  ax-i5r 1471  ax-ext 2067  ax-sep 3925  ax-pow 3977  ax-pr 4003  ax-un 4227
This theorem depends on definitions:  df-bi 115  df-3an 924  df-tru 1290  df-nf 1393  df-sb 1690  df-clab 2072  df-cleq 2078  df-clel 2081  df-nfc 2214  df-rex 2361  df-v 2616  df-un 2990  df-in 2992  df-ss 2999  df-pw 3411  df-sn 3431  df-pr 3432  df-op 3434  df-uni 3631  df-opab 3869  df-xp 4410
This theorem is referenced by:  xpex  4514  resiexg  4717  cnvexg  4925  coexg  4932  fex2  5131  fabexg  5149  resfunexgALT  5819  cofunexg  5820  fnexALT  5822  opabex3d  5830  opabex3  5831  oprabexd  5836  ofmresex  5846  mpt2exxg  5915  tposexg  5958  erex  6249  pmex  6343  mapex  6344  pmvalg  6349  elpmg  6354  fvdiagfn  6383  map1  6462  xpdom2  6480  xpdom3m  6483  xpen  6494  mapxpen  6497  xpfi  6568  djuex  6657  shftfvalg  10094  climconst2  10518
  Copyright terms: Public domain W3C validator