![]() |
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 7968. (Contributed by NM, 14-Aug-1994.) |
Ref | Expression |
---|---|
xpexg | ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 × 𝐵) ∈ V) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | xpsspw 5810 | . 2 ⊢ (𝐴 × 𝐵) ⊆ 𝒫 𝒫 (𝐴 ∪ 𝐵) | |
2 | unexg 7736 | . . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∪ 𝐵) ∈ V) | |
3 | pwexg 5377 | . . 3 ⊢ ((𝐴 ∪ 𝐵) ∈ V → 𝒫 (𝐴 ∪ 𝐵) ∈ V) | |
4 | pwexg 5377 | . . 3 ⊢ (𝒫 (𝐴 ∪ 𝐵) ∈ V → 𝒫 𝒫 (𝐴 ∪ 𝐵) ∈ V) | |
5 | 2, 3, 4 | 3syl 18 | . 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝒫 𝒫 (𝐴 ∪ 𝐵) ∈ V) |
6 | ssexg 5324 | . 2 ⊢ (((𝐴 × 𝐵) ⊆ 𝒫 𝒫 (𝐴 ∪ 𝐵) ∧ 𝒫 𝒫 (𝐴 ∪ 𝐵) ∈ V) → (𝐴 × 𝐵) ∈ V) | |
7 | 1, 5, 6 | sylancr 588 | 1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 × 𝐵) ∈ V) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 397 ∈ wcel 2107 Vcvv 3475 ∪ cun 3947 ⊆ wss 3949 𝒫 cpw 4603 × cxp 5675 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2704 ax-sep 5300 ax-nul 5307 ax-pow 5364 ax-pr 5428 ax-un 7725 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-ral 3063 df-rex 3072 df-rab 3434 df-v 3477 df-dif 3952 df-un 3954 df-in 3956 df-ss 3966 df-nul 4324 df-if 4530 df-pw 4605 df-sn 4630 df-pr 4632 df-op 4636 df-uni 4910 df-opab 5212 df-xp 5683 df-rel 5684 |
This theorem is referenced by: xpexd 7738 3xpexg 7739 xpex 7740 sqxpexg 7742 coexg 7920 fex2 7924 fabexg 7925 resfunexgALT 7934 fnexALT 7937 funexw 7938 opabex3d 7952 opabex3rd 7953 opabex3 7954 mpoexxg 8062 fnwelem 8117 naddunif 8692 pmex 8825 mapex 8826 pmvalg 8831 elpmg 8837 fvdiagfn 8885 ixpexg 8916 snmapen 9038 xpdom2 9067 xpdom3 9070 omxpen 9074 fodomr 9128 disjenex 9135 domssex2 9137 domssex 9138 mapxpen 9143 xpfiOLD 9318 fczfsuppd 9381 brwdom2 9568 xpwdomg 9580 unxpwdom2 9583 djuex 9903 djuexALT 9917 fseqen 10022 djuassen 10173 mapdjuen 10175 djudom1 10177 djuinf 10183 hsmexlem2 10422 axdc2lem 10443 iundom2g 10535 fpwwe2lem12 10637 pwsbas 17433 pwsle 17438 pwssca 17442 isga 19155 efgtf 19590 frgpcpbl 19627 frgp0 19628 frgpeccl 19629 frgpadd 19631 frgpmhm 19633 vrgpf 19636 vrgpinv 19637 frgpupf 19641 frgpup1 19643 frgpup2 19644 frgpup3lem 19645 frgpnabllem1 19741 frgpnabllem2 19742 gsum2d2 19842 gsumcom2 19843 dprd2da 19912 pwssplit3 20672 mpofrlmd 21332 frlmip 21333 mattposvs 21957 mat1dimelbas 21973 mdetrlin 22104 lmfval 22736 txbasex 23070 txopn 23106 txrest 23135 txindislem 23137 xkoinjcn 23191 blfvalps 23889 bcthlem1 24841 bcthlem5 24845 rrxip 24907 isvcOLD 29832 resf1o 31955 locfinref 32821 esum2dlem 33090 esum2d 33091 elsx 33192 satfv0 34349 satf00 34365 filnetlem3 35265 filnetlem4 35266 bj-xpexg2 35841 inxpex 37208 xrninxpex 37264 relexpxpnnidm 42454 enrelmap 42748 mpoexxg2 47013 eufsn2 47509 |
Copyright terms: Public domain | W3C validator |