![]() |
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 7438. (Contributed by NM, 14-Aug-1994.) |
Ref | Expression |
---|---|
xpexg | ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 × 𝐵) ∈ V) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | xpsspw 5480 | . 2 ⊢ (𝐴 × 𝐵) ⊆ 𝒫 𝒫 (𝐴 ∪ 𝐵) | |
2 | unexg 7236 | . . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∪ 𝐵) ∈ V) | |
3 | pwexg 5090 | . . 3 ⊢ ((𝐴 ∪ 𝐵) ∈ V → 𝒫 (𝐴 ∪ 𝐵) ∈ V) | |
4 | pwexg 5090 | . . 3 ⊢ (𝒫 (𝐴 ∪ 𝐵) ∈ V → 𝒫 𝒫 (𝐴 ∪ 𝐵) ∈ V) | |
5 | 2, 3, 4 | 3syl 18 | . 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝒫 𝒫 (𝐴 ∪ 𝐵) ∈ V) |
6 | ssexg 5041 | . 2 ⊢ (((𝐴 × 𝐵) ⊆ 𝒫 𝒫 (𝐴 ∪ 𝐵) ∧ 𝒫 𝒫 (𝐴 ∪ 𝐵) ∈ V) → (𝐴 × 𝐵) ∈ V) | |
7 | 1, 5, 6 | sylancr 581 | 1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 × 𝐵) ∈ V) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 386 ∈ wcel 2106 Vcvv 3397 ∪ cun 3789 ⊆ wss 3791 𝒫 cpw 4378 × cxp 5353 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1839 ax-4 1853 ax-5 1953 ax-6 2021 ax-7 2054 ax-8 2108 ax-9 2115 ax-10 2134 ax-11 2149 ax-12 2162 ax-13 2333 ax-ext 2753 ax-sep 5017 ax-nul 5025 ax-pow 5077 ax-pr 5138 ax-un 7226 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 837 df-3an 1073 df-tru 1605 df-ex 1824 df-nf 1828 df-sb 2012 df-clab 2763 df-cleq 2769 df-clel 2773 df-nfc 2920 df-ral 3094 df-rex 3095 df-rab 3098 df-v 3399 df-dif 3794 df-un 3796 df-in 3798 df-ss 3805 df-nul 4141 df-if 4307 df-pw 4380 df-sn 4398 df-pr 4400 df-op 4404 df-uni 4672 df-opab 4949 df-xp 5361 df-rel 5362 |
This theorem is referenced by: xpexd 7238 3xpexg 7239 xpex 7240 sqxpexg 7241 coexg 7396 fex2 7400 fabexg 7401 resfunexgALT 7408 fnexALT 7411 opabex3d 7423 opabex3 7424 mpt2exxg 7524 fnwelem 7573 pmex 8145 mapex 8146 pmvalg 8151 elpmg 8156 fvdiagfn 8188 ixpexg 8218 snmapen 8322 xpdom2 8343 xpdom3 8346 omxpen 8350 fodomr 8399 disjenex 8406 domssex2 8408 domssex 8409 mapxpen 8414 xpfi 8519 fczfsuppd 8581 brwdom2 8767 xpwdomg 8779 unxpwdom2 8782 djuex 9068 djuexALT 9081 fseqen 9183 cdaval 9327 cdaassen 9339 mapcdaen 9341 cdadom1 9343 cdainf 9349 hsmexlem2 9584 axdc2lem 9605 iundom2g 9697 fpwwe2lem13 9799 wrdexgOLD 13610 pwsbas 16533 pwsle 16538 pwssca 16542 isga 18107 efgtf 18519 frgpcpbl 18558 frgp0 18559 frgpeccl 18560 frgpadd 18562 frgpmhm 18564 vrgpf 18567 vrgpinv 18568 frgpupf 18572 frgpup1 18574 frgpup2 18575 frgpup3lem 18576 frgpnabllem1 18662 frgpnabllem2 18663 gsum2d2 18759 gsumcom2 18760 dprd2da 18828 pwssplit3 19456 mpt2frlmd 20520 frlmip 20521 mattposvs 20666 mat1dimelbas 20682 mdetrlin 20813 lmfval 21444 txbasex 21778 txopn 21814 txcn 21838 txrest 21843 txindislem 21845 xkoinjcn 21899 blfvalps 22596 bcthlem1 23530 bcthlem5 23534 rrxip 23596 isleag 26196 isvcOLD 28006 resf1o 30071 locfinref 30506 esum2dlem 30752 esum2d 30753 elsx 30855 filnetlem3 32963 filnetlem4 32964 bj-xpexg2 33519 inxpex 34730 xrninxpex 34775 relexpxpnnidm 38945 enrelmap 39240 mpt2exxg2 43124 |
Copyright terms: Public domain | W3C validator |