![]() |
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 7985. (Contributed by NM, 14-Aug-1994.) |
Ref | Expression |
---|---|
xpexg | ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 × 𝐵) ∈ V) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | xpsspw 5806 | . 2 ⊢ (𝐴 × 𝐵) ⊆ 𝒫 𝒫 (𝐴 ∪ 𝐵) | |
2 | unexg 7747 | . . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∪ 𝐵) ∈ V) | |
3 | pwexg 5373 | . . 3 ⊢ ((𝐴 ∪ 𝐵) ∈ V → 𝒫 (𝐴 ∪ 𝐵) ∈ V) | |
4 | pwexg 5373 | . . 3 ⊢ (𝒫 (𝐴 ∪ 𝐵) ∈ V → 𝒫 𝒫 (𝐴 ∪ 𝐵) ∈ V) | |
5 | 2, 3, 4 | 3syl 18 | . 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝒫 𝒫 (𝐴 ∪ 𝐵) ∈ V) |
6 | ssexg 5319 | . 2 ⊢ (((𝐴 × 𝐵) ⊆ 𝒫 𝒫 (𝐴 ∪ 𝐵) ∧ 𝒫 𝒫 (𝐴 ∪ 𝐵) ∈ V) → (𝐴 × 𝐵) ∈ V) | |
7 | 1, 5, 6 | sylancr 585 | 1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 × 𝐵) ∈ V) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 394 ∈ wcel 2099 Vcvv 3463 ∪ cun 3945 ⊆ wss 3947 𝒫 cpw 4598 × cxp 5671 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-ext 2697 ax-sep 5295 ax-nul 5302 ax-pow 5360 ax-pr 5424 ax-un 7736 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3an 1086 df-tru 1537 df-fal 1547 df-ex 1775 df-sb 2061 df-clab 2704 df-cleq 2718 df-clel 2803 df-ral 3052 df-rex 3061 df-rab 3421 df-v 3465 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-nul 4324 df-if 4525 df-pw 4600 df-sn 4625 df-pr 4627 df-op 4631 df-uni 4907 df-opab 5207 df-xp 5679 df-rel 5680 |
This theorem is referenced by: xpexd 7749 3xpexg 7750 xpex 7751 sqxpexg 7753 coexg 7932 fex2 7937 fabexgOLD 7940 resfunexgALT 7951 fnexALT 7954 funexw 7955 opabex3d 7969 opabex3rd 7970 opabex3 7971 mpoexxg 8079 fnwelem 8135 naddunif 8713 pmex 8850 mapexOLD 8851 pmvalg 8856 elpmg 8862 fvdiagfn 8910 ixpexg 8941 snmapen 9064 xpdom2 9095 xpdom3 9098 omxpen 9102 fodomr 9156 disjenex 9163 domssex2 9165 domssex 9166 mapxpen 9171 xpfiOLD 9352 fczfsuppd 9420 brwdom2 9607 xpwdomg 9619 unxpwdom2 9622 djuex 9942 djuexALT 9956 fseqen 10061 djuassen 10212 mapdjuen 10214 djudom1 10216 djuinf 10222 hsmexlem2 10459 axdc2lem 10480 iundom2g 10572 fpwwe2lem12 10674 pwsbas 17495 pwsle 17500 pwssca 17504 isga 19279 efgtf 19714 frgpcpbl 19751 frgp0 19752 frgpeccl 19753 frgpadd 19755 frgpmhm 19757 vrgpf 19760 vrgpinv 19761 frgpupf 19765 frgpup1 19767 frgpup2 19768 frgpup3lem 19769 frgpnabllem1 19865 frgpnabllem2 19866 gsum2d2 19966 gsumcom2 19967 dprd2da 20036 pwssplit3 21033 mpofrlmd 21769 frlmip 21770 mattposvs 22443 mat1dimelbas 22459 mdetrlin 22590 lmfval 23222 txbasex 23556 txopn 23592 txrest 23621 txindislem 23623 xkoinjcn 23677 blfvalps 24375 bcthlem1 25338 bcthlem5 25342 rrxip 25404 isvcOLD 30507 resf1o 32642 locfinref 33667 esum2dlem 33936 esum2d 33937 elsx 34038 satfv0 35197 satf00 35213 filnetlem3 36103 filnetlem4 36104 bj-xpexg2 36678 inxpex 38048 xrninxpex 38103 aks6d1c2 41840 relexpxpnnidm 43405 enrelmap 43699 mpoexxg2 47750 eufsn2 48244 |
Copyright terms: Public domain | W3C validator |