![]() |
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 7679. (Contributed by NM, 14-Aug-1994.) |
Ref | Expression |
---|---|
xpexg | ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 × 𝐵) ∈ V) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | xpsspw 5644 | . 2 ⊢ (𝐴 × 𝐵) ⊆ 𝒫 𝒫 (𝐴 ∪ 𝐵) | |
2 | unexg 7463 | . . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∪ 𝐵) ∈ V) | |
3 | pwexg 5240 | . . 3 ⊢ ((𝐴 ∪ 𝐵) ∈ V → 𝒫 (𝐴 ∪ 𝐵) ∈ V) | |
4 | pwexg 5240 | . . 3 ⊢ (𝒫 (𝐴 ∪ 𝐵) ∈ V → 𝒫 𝒫 (𝐴 ∪ 𝐵) ∈ V) | |
5 | 2, 3, 4 | 3syl 18 | . 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝒫 𝒫 (𝐴 ∪ 𝐵) ∈ V) |
6 | ssexg 5186 | . 2 ⊢ (((𝐴 × 𝐵) ⊆ 𝒫 𝒫 (𝐴 ∪ 𝐵) ∧ 𝒫 𝒫 (𝐴 ∪ 𝐵) ∈ V) → (𝐴 × 𝐵) ∈ V) | |
7 | 1, 5, 6 | sylancr 591 | 1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 × 𝐵) ∈ V) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 400 ∈ wcel 2112 Vcvv 3407 ∪ cun 3852 ⊆ wss 3854 𝒫 cpw 4487 × cxp 5515 |
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 1912 ax-6 1971 ax-7 2016 ax-8 2114 ax-9 2122 ax-10 2143 ax-11 2159 ax-12 2176 ax-ext 2730 ax-sep 5162 ax-nul 5169 ax-pow 5227 ax-pr 5291 ax-un 7452 |
This theorem depends on definitions: df-bi 210 df-an 401 df-or 846 df-3an 1087 df-tru 1542 df-ex 1783 df-nf 1787 df-sb 2071 df-clab 2737 df-cleq 2751 df-clel 2831 df-ral 3073 df-rex 3074 df-rab 3077 df-v 3409 df-dif 3857 df-un 3859 df-in 3861 df-ss 3871 df-nul 4222 df-if 4414 df-pw 4489 df-sn 4516 df-pr 4518 df-op 4522 df-uni 4792 df-opab 5088 df-xp 5523 df-rel 5524 |
This theorem is referenced by: xpexd 7465 3xpexg 7466 xpex 7467 sqxpexg 7469 coexg 7632 fex2 7636 fabexg 7637 resfunexgALT 7646 fnexALT 7649 funexw 7650 opabex3d 7663 opabex3rd 7664 opabex3 7665 mpoexxg 7771 fnwelem 7823 pmex 8414 mapex 8415 pmvalg 8420 elpmg 8425 fvdiagfn 8466 ixpexg 8497 snmapen 8602 xpdom2 8625 xpdom3 8628 omxpen 8632 fodomr 8682 disjenex 8689 domssex2 8691 domssex 8692 mapxpen 8697 xpfi 8807 fczfsuppd 8869 brwdom2 9055 xpwdomg 9067 unxpwdom2 9070 djuex 9355 djuexALT 9369 fseqen 9472 djuassen 9623 mapdjuen 9625 djudom1 9627 djuinf 9633 hsmexlem2 9872 axdc2lem 9893 iundom2g 9985 fpwwe2lem12 10087 pwsbas 16803 pwsle 16808 pwssca 16812 isga 18473 efgtf 18900 frgpcpbl 18937 frgp0 18938 frgpeccl 18939 frgpadd 18941 frgpmhm 18943 vrgpf 18946 vrgpinv 18947 frgpupf 18951 frgpup1 18953 frgpup2 18954 frgpup3lem 18955 frgpnabllem1 19046 frgpnabllem2 19047 gsum2d2 19147 gsumcom2 19148 dprd2da 19217 pwssplit3 19886 mpofrlmd 20527 frlmip 20528 mattposvs 21140 mat1dimelbas 21156 mdetrlin 21287 lmfval 21917 txbasex 22251 txopn 22287 txcn 22311 txrest 22316 txindislem 22318 xkoinjcn 22372 blfvalps 23070 bcthlem1 24009 bcthlem5 24013 rrxip 24075 isvcOLD 28446 resf1o 30574 locfinref 31297 esum2dlem 31564 esum2d 31565 elsx 31666 satfv0 32821 satf00 32837 filnetlem3 34103 filnetlem4 34104 bj-xpexg2 34662 inxpex 36021 xrninxpex 36067 relexpxpnnidm 40762 enrelmap 41056 mpoexxg2 45091 |
Copyright terms: Public domain | W3C validator |