| 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 7966. (Contributed by NM, 14-Aug-1994.) |
| Ref | Expression |
|---|---|
| xpexg | ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 × 𝐵) ∈ V) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | xpsspw 5786 | . 2 ⊢ (𝐴 × 𝐵) ⊆ 𝒫 𝒫 (𝐴 ∪ 𝐵) | |
| 2 | unexg 7730 | . . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∪ 𝐵) ∈ V) | |
| 3 | pwexg 5339 | . . 3 ⊢ ((𝐴 ∪ 𝐵) ∈ V → 𝒫 (𝐴 ∪ 𝐵) ∈ V) | |
| 4 | pwexg 5339 | . . 3 ⊢ (𝒫 (𝐴 ∪ 𝐵) ∈ V → 𝒫 𝒫 (𝐴 ∪ 𝐵) ∈ V) | |
| 5 | 2, 3, 4 | 3syl 19 | . 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝒫 𝒫 (𝐴 ∪ 𝐵) ∈ V) |
| 6 | ssexg 5283 | . 2 ⊢ (((𝐴 × 𝐵) ⊆ 𝒫 𝒫 (𝐴 ∪ 𝐵) ∧ 𝒫 𝒫 (𝐴 ∪ 𝐵) ∈ V) → (𝐴 × 𝐵) ∈ V) | |
| 7 | 1, 5, 6 | sylancr 598 | 1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 × 𝐵) ∈ V) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 400 ∈ wcel 2145 Vcvv 3457 ∪ cun 3905 ⊆ wss 3907 𝒫 cpw 4558 × cxp 5649 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1818 ax-4 1832 ax-5 1933 ax-6 1990 ax-7 2031 ax-8 2147 ax-9 2155 ax-ext 2737 ax-sep 5250 ax-pow 5326 ax-pr 5394 ax-un 7722 |
| This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3an 1103 df-tru 1566 df-fal 1576 df-ex 1803 df-sb 2094 df-clab 2744 df-cleq 2757 df-clel 2840 df-ral 3080 df-rex 3090 df-rab 3418 df-v 3459 df-dif 3910 df-un 3912 df-in 3914 df-ss 3924 df-nul 4289 df-if 4484 df-pw 4560 df-sn 4586 df-pr 4588 df-op 4592 df-uni 4868 df-opab 5167 df-xp 5657 df-rel 5658 |
| This theorem is referenced by: xpexd 7738 3xpexg 7739 xpex 7740 sqxpexg 7742 coexg 7914 fex2 7921 resfunexgALT 7933 fnexALT 7936 funexw 7937 opabex3d 7950 opabex3rd 7951 opabex3 7952 mpoexxg 8060 fnwelem 8115 naddunif 8668 pmex 8817 pmvalg 8822 elpmg 8828 fvdiagfn 8877 ixpexg 8908 snmapen 9023 xpdom2 9048 xpdom3 9051 omxpen 9055 fodomr 9104 disjenex 9111 domssex2 9113 domssex 9114 mapxpen 9119 fczfsuppd 9334 brwdom2 9523 xpwdomg 9535 unxpwdom2 9538 djuex 9882 djuexALT 9896 fseqen 9999 djuassen 10150 mapdjuen 10152 djudom1 10154 djuinf 10160 hsmexlem2 10399 axdc2lem 10420 iundom2g 10512 fpwwe2lem12 10615 pwsbas 17528 pwsle 17534 pwssca 17538 isga 19349 efgtf 19780 frgpcpbl 19817 frgp0 19818 frgpeccl 19819 frgpadd 19821 frgpmhm 19823 vrgpf 19826 vrgpinv 19827 frgpupf 19831 frgpup1 19833 frgpup2 19834 frgpup3lem 19835 frgpnabllem1 19931 frgpnabllem2 19932 gsum2d2 20032 gsumcom2 20033 dprd2da 20102 pwssplit3 21148 mpofrlmd 21884 frlmip 21885 mattposvs 22569 mat1dimelbas 22585 mdetrlin 22716 lmfval 23346 txbasex 23680 txopn 23716 txrest 23745 txindislem 23747 xkoinjcn 23801 blfvalps 24497 bcthlem1 25440 bcthlem5 25444 rrxip 25506 isvcOLD 30836 resf1o 32983 locfinref 34143 esum2dlem 34394 esum2d 34395 elsx 34496 satfv0 35716 satf00 35732 filnetlem3 36748 filnetlem4 36749 bj-xpexg2 37452 inxpex 38845 xrninxpex 38923 aks6d1c2 42754 relexpxpnnidm 44286 enrelmap 44580 mpoexxg2 48970 eufsn2 49473 |
| Copyright terms: Public domain | W3C validator |