Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > xpexg | Structured version Visualization version GIF version |
Description: The Cartesian product of two sets is a set. Proposition 6.2 of [TakeutiZaring] p. 23. See also xpexgALT 7161. (Contributed by NM, 14-Aug-1994.) |
Ref | Expression |
---|---|
xpexg | ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 × 𝐵) ∈ V) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | xpsspw 5233 | . 2 ⊢ (𝐴 × 𝐵) ⊆ 𝒫 𝒫 (𝐴 ∪ 𝐵) | |
2 | unexg 6959 | . . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∪ 𝐵) ∈ V) | |
3 | pwexg 4850 | . . 3 ⊢ ((𝐴 ∪ 𝐵) ∈ V → 𝒫 (𝐴 ∪ 𝐵) ∈ V) | |
4 | pwexg 4850 | . . 3 ⊢ (𝒫 (𝐴 ∪ 𝐵) ∈ V → 𝒫 𝒫 (𝐴 ∪ 𝐵) ∈ V) | |
5 | 2, 3, 4 | 3syl 18 | . 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝒫 𝒫 (𝐴 ∪ 𝐵) ∈ V) |
6 | ssexg 4804 | . 2 ⊢ (((𝐴 × 𝐵) ⊆ 𝒫 𝒫 (𝐴 ∪ 𝐵) ∧ 𝒫 𝒫 (𝐴 ∪ 𝐵) ∈ V) → (𝐴 × 𝐵) ∈ V) | |
7 | 1, 5, 6 | sylancr 695 | 1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 × 𝐵) ∈ V) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 384 ∈ wcel 1990 Vcvv 3200 ∪ cun 3572 ⊆ wss 3574 𝒫 cpw 4158 × cxp 5112 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-8 1992 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-sep 4781 ax-nul 4789 ax-pow 4843 ax-pr 4906 ax-un 6949 |
This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3an 1039 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ral 2917 df-rex 2918 df-rab 2921 df-v 3202 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-nul 3916 df-if 4087 df-pw 4160 df-sn 4178 df-pr 4180 df-op 4184 df-uni 4437 df-opab 4713 df-xp 5120 df-rel 5121 |
This theorem is referenced by: 3xpexg 6961 xpex 6962 sqxpexg 6963 cnvexg 7112 coexg 7117 fex2 7121 fabexg 7122 resfunexgALT 7129 cofunexg 7130 fnexALT 7132 opabex3d 7145 opabex3 7146 oprabexd 7155 ofmresex 7165 opabex2 7227 mpt2exxg 7244 offval22 7253 fnwelem 7292 tposexg 7366 pmex 7862 mapex 7863 pmvalg 7868 elpmg 7873 fvdiagfn 7902 ixpexg 7932 map1 8036 xpdom2 8055 xpdom3 8058 omxpen 8062 fodomr 8111 disjenex 8118 domssex2 8120 domssex 8121 mapxpen 8126 xpfi 8231 fczfsuppd 8293 marypha1 8340 brwdom2 8478 wdom2d 8485 xpwdomg 8490 unxpwdom2 8493 ixpiunwdom 8496 fseqen 8850 cdaval 8992 cdaassen 9004 mapcdaen 9006 cdadom1 9008 cdainf 9014 hsmexlem2 9249 axdc2lem 9270 fnct 9359 iundom2g 9362 fpwwe2lem2 9454 fpwwe2lem5 9456 fpwwe2lem12 9463 fpwwe2lem13 9464 fpwwelem 9467 canthwe 9473 pwxpndom 9488 gchhar 9501 wrdexg 13315 trclexlem 13733 pwsbas 16147 pwsle 16152 pwssca 16156 isacs1i 16318 rescval2 16488 reschom 16490 rescabs 16493 setccofval 16732 isga 17724 sylow2a 18034 lsmhash 18118 efgtf 18135 frgpcpbl 18172 frgp0 18173 frgpeccl 18174 frgpadd 18176 frgpmhm 18178 vrgpf 18181 vrgpinv 18182 frgpupf 18186 frgpup1 18188 frgpup2 18189 frgpup3lem 18190 frgpnabllem1 18276 frgpnabllem2 18277 gsum2d2 18373 gsumcom2 18374 gsumxp 18375 dprd2da 18441 pwssplit3 19061 opsrval 19474 opsrtoslem2 19485 evlslem4 19508 mpt2frlmd 20116 frlmip 20117 matbas2d 20229 mattposvs 20261 mat1dimelbas 20277 mdetrlin 20408 lmfval 21036 txbasex 21369 txopn 21405 txcn 21429 txrest 21434 txindislem 21436 xkoinjcn 21490 tsmsxp 21958 ustssel 22009 ustfilxp 22016 trust 22033 restutop 22041 trcfilu 22098 cfiluweak 22099 imasdsf1olem 22178 blfvalps 22188 metustfbas 22362 restmetu 22375 bcthlem1 23121 bcthlem5 23125 rrxip 23178 perpln1 25605 perpln2 25606 isperp 25607 isleag 25733 isvcOLD 27434 resf1o 29505 locfinref 29908 metidval 29933 esum2dlem 30154 esum2d 30155 esumiun 30156 elsx 30257 madeval 31935 filnetlem3 32375 filnetlem4 32376 bj-xpexg2 32947 isrngod 33697 isgrpda 33754 iscringd 33797 inxpex 34107 wdom2d2 37602 unxpwdom3 37665 trclubgNEW 37925 relexpxpnnidm 37995 relexpxpmin 38009 enrelmap 38291 rfovd 38295 rfovcnvf1od 38298 fsovrfovd 38303 xpexd 39285 dvsinax 40127 sge0xp 40646 mpt2exxg2 42116 |
Copyright terms: Public domain | W3C validator |