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 7052. (Contributed by NM, 14-Aug-1994.) |
Ref | Expression |
---|---|
xpexg | ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 × 𝐵) ∈ V) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | xpsspw 5156 | . 2 ⊢ (𝐴 × 𝐵) ⊆ 𝒫 𝒫 (𝐴 ∪ 𝐵) | |
2 | unexg 6857 | . . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∪ 𝐵) ∈ V) | |
3 | pwexg 4776 | . . 3 ⊢ ((𝐴 ∪ 𝐵) ∈ V → 𝒫 (𝐴 ∪ 𝐵) ∈ V) | |
4 | pwexg 4776 | . . 3 ⊢ (𝒫 (𝐴 ∪ 𝐵) ∈ V → 𝒫 𝒫 (𝐴 ∪ 𝐵) ∈ V) | |
5 | 2, 3, 4 | 3syl 18 | . 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝒫 𝒫 (𝐴 ∪ 𝐵) ∈ V) |
6 | ssexg 4732 | . 2 ⊢ (((𝐴 × 𝐵) ⊆ 𝒫 𝒫 (𝐴 ∪ 𝐵) ∧ 𝒫 𝒫 (𝐴 ∪ 𝐵) ∈ V) → (𝐴 × 𝐵) ∈ V) | |
7 | 1, 5, 6 | sylancr 694 | 1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 × 𝐵) ∈ V) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 ∈ wcel 1977 Vcvv 3173 ∪ cun 3538 ⊆ wss 3540 𝒫 cpw 4108 × cxp 5036 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-8 1979 ax-9 1986 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 ax-sep 4709 ax-nul 4717 ax-pow 4769 ax-pr 4833 ax-un 6847 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-3an 1033 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-ral 2901 df-rex 2902 df-rab 2905 df-v 3175 df-dif 3543 df-un 3545 df-in 3547 df-ss 3554 df-nul 3875 df-if 4037 df-pw 4110 df-sn 4126 df-pr 4128 df-op 4132 df-uni 4373 df-opab 4644 df-xp 5044 df-rel 5045 |
This theorem is referenced by: 3xpexg 6859 xpex 6860 sqxpexg 6861 opabex2 6997 cnvexg 7005 coexg 7010 fex2 7014 fabexg 7015 resfunexgALT 7022 cofunexg 7023 fnexALT 7025 opabex3d 7037 opabex3 7038 oprabexd 7046 ofmresex 7056 mpt2exxg 7133 offval22 7140 fnwelem 7179 tposexg 7253 pmex 7749 mapex 7750 pmvalg 7755 elpmg 7759 fvdiagfn 7788 ixpexg 7818 map1 7921 xpdom2 7940 xpdom3 7943 omxpen 7947 fodomr 7996 disjenex 8003 domssex2 8005 domssex 8006 mapxpen 8011 xpfi 8116 fczfsuppd 8176 marypha1 8223 brwdom2 8361 wdom2d 8368 xpwdomg 8373 unxpwdom2 8376 ixpiunwdom 8379 fseqen 8733 cdaval 8875 cdaassen 8887 mapcdaen 8889 cdadom1 8891 cdainf 8897 hsmexlem2 9132 axdc2lem 9153 iundom2g 9241 fpwwe2lem2 9333 fpwwe2lem5 9335 fpwwe2lem12 9342 fpwwe2lem13 9343 fpwwelem 9346 canthwe 9352 pwxpndom 9367 gchhar 9380 wrdexg 13170 trclexlem 13581 pwsbas 15970 pwsle 15975 pwssca 15979 isacs1i 16141 rescval2 16311 reschom 16313 rescabs 16316 setccofval 16555 isga 17547 sylow2a 17857 lsmhash 17941 efgtf 17958 frgpcpbl 17995 frgp0 17996 frgpeccl 17997 frgpadd 17999 frgpmhm 18001 vrgpf 18004 vrgpinv 18005 frgpupf 18009 frgpup1 18011 frgpup2 18012 frgpup3lem 18013 frgpnabllem1 18099 frgpnabllem2 18100 gsum2d2 18196 gsumcom2 18197 gsumxp 18198 dprd2da 18264 pwssplit3 18882 opsrval 19295 opsrtoslem2 19306 evlslem4 19329 mpt2frlmd 19935 frlmip 19936 matbas2d 20048 mattposvs 20080 mat1dimelbas 20096 mdetrlin 20227 lmfval 20846 txbasex 21179 txopn 21215 txcn 21239 txrest 21244 txindislem 21246 xkoinjcn 21300 tsmsxp 21768 ustssel 21819 ustfilxp 21826 trust 21843 restutop 21851 trcfilu 21908 cfiluweak 21909 imasdsf1olem 21988 blfvalps 21998 metustfbas 22172 restmetu 22185 bcthlem1 22929 bcthlem5 22933 rrxip 22986 perpln1 25405 perpln2 25406 isperp 25407 isleag 25533 isvcOLD 26818 fnct 28876 resf1o 28893 locfinref 29236 metidval 29261 esum2dlem 29481 esum2d 29482 esumiun 29483 elsx 29584 filnetlem3 31545 filnetlem4 31546 bj-xpexg2 32140 isrngod 32867 isgrpda 32924 iscringd 32967 wdom2d2 36620 unxpwdom3 36683 trclubgNEW 36944 relexpxpnnidm 37014 relexpxpmin 37028 enrelmap 37311 rfovd 37315 rfovcnvf1od 37318 fsovrfovd 37323 xpexd 38314 dvsinax 38801 sge0xp 39322 mpt2exxg2 41909 |
Copyright terms: Public domain | W3C validator |