![]() |
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 7327. (Contributed by NM, 14-Aug-1994.) |
Ref | Expression |
---|---|
xpexg | ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 × 𝐵) ∈ V) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | xpsspw 5389 | . 2 ⊢ (𝐴 × 𝐵) ⊆ 𝒫 𝒫 (𝐴 ∪ 𝐵) | |
2 | unexg 7125 | . . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∪ 𝐵) ∈ V) | |
3 | pwexg 4999 | . . 3 ⊢ ((𝐴 ∪ 𝐵) ∈ V → 𝒫 (𝐴 ∪ 𝐵) ∈ V) | |
4 | pwexg 4999 | . . 3 ⊢ (𝒫 (𝐴 ∪ 𝐵) ∈ V → 𝒫 𝒫 (𝐴 ∪ 𝐵) ∈ V) | |
5 | 2, 3, 4 | 3syl 18 | . 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝒫 𝒫 (𝐴 ∪ 𝐵) ∈ V) |
6 | ssexg 4956 | . 2 ⊢ (((𝐴 × 𝐵) ⊆ 𝒫 𝒫 (𝐴 ∪ 𝐵) ∧ 𝒫 𝒫 (𝐴 ∪ 𝐵) ∈ V) → (𝐴 × 𝐵) ∈ V) | |
7 | 1, 5, 6 | sylancr 698 | 1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 × 𝐵) ∈ V) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 ∈ wcel 2139 Vcvv 3340 ∪ cun 3713 ⊆ wss 3715 𝒫 cpw 4302 × cxp 5264 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1871 ax-4 1886 ax-5 1988 ax-6 2054 ax-7 2090 ax-8 2141 ax-9 2148 ax-10 2168 ax-11 2183 ax-12 2196 ax-13 2391 ax-ext 2740 ax-sep 4933 ax-nul 4941 ax-pow 4992 ax-pr 5055 ax-un 7115 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3an 1074 df-tru 1635 df-ex 1854 df-nf 1859 df-sb 2047 df-clab 2747 df-cleq 2753 df-clel 2756 df-nfc 2891 df-ral 3055 df-rex 3056 df-rab 3059 df-v 3342 df-dif 3718 df-un 3720 df-in 3722 df-ss 3729 df-nul 4059 df-if 4231 df-pw 4304 df-sn 4322 df-pr 4324 df-op 4328 df-uni 4589 df-opab 4865 df-xp 5272 df-rel 5273 |
This theorem is referenced by: 3xpexg 7127 xpex 7128 sqxpexg 7129 cnvexg 7278 coexg 7283 fex2 7287 fabexg 7288 resfunexgALT 7295 cofunexg 7296 fnexALT 7298 opabex3d 7311 opabex3 7312 oprabexd 7321 ofmresex 7331 opabex2 7395 mpt2exxg 7413 offval22 7422 fnwelem 7461 tposexg 7536 pmex 8030 mapex 8031 pmvalg 8036 elpmg 8041 fvdiagfn 8070 ixpexg 8100 map1 8203 xpdom2 8222 xpdom3 8225 omxpen 8229 fodomr 8278 disjenex 8285 domssex2 8287 domssex 8288 mapxpen 8293 xpfi 8398 fczfsuppd 8460 marypha1 8507 brwdom2 8645 wdom2d 8652 xpwdomg 8657 unxpwdom2 8660 ixpiunwdom 8663 djuex 8946 djuexALT 8958 fseqen 9060 cdaval 9204 cdaassen 9216 mapcdaen 9218 cdadom1 9220 cdainf 9226 hsmexlem2 9461 axdc2lem 9482 fnct 9571 iundom2g 9574 fpwwe2lem2 9666 fpwwe2lem5 9668 fpwwe2lem12 9675 fpwwe2lem13 9676 fpwwelem 9679 canthwe 9685 pwxpndom 9700 gchhar 9713 wrdexg 13521 trclexlem 13954 pwsbas 16369 pwsle 16374 pwssca 16378 isacs1i 16539 rescval2 16709 reschom 16711 rescabs 16714 setccofval 16953 isga 17944 sylow2a 18254 lsmhash 18338 efgtf 18355 frgpcpbl 18392 frgp0 18393 frgpeccl 18394 frgpadd 18396 frgpmhm 18398 vrgpf 18401 vrgpinv 18402 frgpupf 18406 frgpup1 18408 frgpup2 18409 frgpup3lem 18410 frgpnabllem1 18496 frgpnabllem2 18497 gsum2d2 18593 gsumcom2 18594 gsumxp 18595 dprd2da 18661 pwssplit3 19283 opsrval 19696 opsrtoslem2 19707 evlslem4 19730 mpt2frlmd 20338 frlmip 20339 matbas2d 20451 mattposvs 20483 mat1dimelbas 20499 mdetrlin 20630 lmfval 21258 txbasex 21591 txopn 21627 txcn 21651 txrest 21656 txindislem 21658 xkoinjcn 21712 tsmsxp 22179 ustssel 22230 ustfilxp 22237 trust 22254 restutop 22262 trcfilu 22319 cfiluweak 22320 imasdsf1olem 22399 blfvalps 22409 metustfbas 22583 restmetu 22596 bcthlem1 23341 bcthlem5 23345 rrxip 23398 perpln1 25825 perpln2 25826 isperp 25827 isleag 25953 isvcOLD 27764 resf1o 29835 locfinref 30238 metidval 30263 esum2dlem 30484 esum2d 30485 esumiun 30486 elsx 30587 madeval 32262 filnetlem3 32702 filnetlem4 32703 bj-xpexg2 33271 isrngod 34028 isgrpda 34085 iscringd 34128 inxpex 34449 xrninxpex 34493 wdom2d2 38122 unxpwdom3 38185 trclubgNEW 38445 relexpxpnnidm 38515 relexpxpmin 38529 enrelmap 38811 rfovd 38815 rfovcnvf1od 38818 fsovrfovd 38823 xpexd 39802 dvsinax 40648 sge0xp 41167 mpt2exxg2 42644 |
Copyright terms: Public domain | W3C validator |