![]() |
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 7664. (Contributed by NM, 14-Aug-1994.) |
Ref | Expression |
---|---|
xpexg | ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 × 𝐵) ∈ V) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | xpsspw 5646 | . 2 ⊢ (𝐴 × 𝐵) ⊆ 𝒫 𝒫 (𝐴 ∪ 𝐵) | |
2 | unexg 7452 | . . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∪ 𝐵) ∈ V) | |
3 | pwexg 5244 | . . 3 ⊢ ((𝐴 ∪ 𝐵) ∈ V → 𝒫 (𝐴 ∪ 𝐵) ∈ V) | |
4 | pwexg 5244 | . . 3 ⊢ (𝒫 (𝐴 ∪ 𝐵) ∈ V → 𝒫 𝒫 (𝐴 ∪ 𝐵) ∈ V) | |
5 | 2, 3, 4 | 3syl 18 | . 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝒫 𝒫 (𝐴 ∪ 𝐵) ∈ V) |
6 | ssexg 5191 | . 2 ⊢ (((𝐴 × 𝐵) ⊆ 𝒫 𝒫 (𝐴 ∪ 𝐵) ∧ 𝒫 𝒫 (𝐴 ∪ 𝐵) ∈ V) → (𝐴 × 𝐵) ∈ V) | |
7 | 1, 5, 6 | sylancr 590 | 1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 × 𝐵) ∈ V) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 399 ∈ wcel 2111 Vcvv 3441 ∪ cun 3879 ⊆ wss 3881 𝒫 cpw 4497 × cxp 5517 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-10 2142 ax-11 2158 ax-12 2175 ax-ext 2770 ax-sep 5167 ax-nul 5174 ax-pow 5231 ax-pr 5295 ax-un 7441 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-3an 1086 df-tru 1541 df-ex 1782 df-nf 1786 df-sb 2070 df-clab 2777 df-cleq 2791 df-clel 2870 df-nfc 2938 df-ral 3111 df-rex 3112 df-rab 3115 df-v 3443 df-dif 3884 df-un 3886 df-in 3888 df-ss 3898 df-nul 4244 df-if 4426 df-pw 4499 df-sn 4526 df-pr 4528 df-op 4532 df-uni 4801 df-opab 5093 df-xp 5525 df-rel 5526 |
This theorem is referenced by: xpexd 7454 3xpexg 7455 xpex 7456 sqxpexg 7457 coexg 7616 fex2 7620 fabexg 7621 resfunexgALT 7631 fnexALT 7634 funexw 7635 opabex3d 7648 opabex3rd 7649 opabex3 7650 mpoexxg 7756 fnwelem 7808 pmex 8394 mapex 8395 pmvalg 8400 elpmg 8405 fvdiagfn 8438 ixpexg 8469 snmapen 8573 xpdom2 8595 xpdom3 8598 omxpen 8602 fodomr 8652 disjenex 8659 domssex2 8661 domssex 8662 mapxpen 8667 xpfi 8773 fczfsuppd 8835 brwdom2 9021 xpwdomg 9033 unxpwdom2 9036 djuex 9321 djuexALT 9335 fseqen 9438 djuassen 9589 mapdjuen 9591 djudom1 9593 djuinf 9599 hsmexlem2 9838 axdc2lem 9859 iundom2g 9951 fpwwe2lem13 10053 pwsbas 16752 pwsle 16757 pwssca 16761 isga 18413 efgtf 18840 frgpcpbl 18877 frgp0 18878 frgpeccl 18879 frgpadd 18881 frgpmhm 18883 vrgpf 18886 vrgpinv 18887 frgpupf 18891 frgpup1 18893 frgpup2 18894 frgpup3lem 18895 frgpnabllem1 18986 frgpnabllem2 18987 gsum2d2 19087 gsumcom2 19088 dprd2da 19157 pwssplit3 19826 mpofrlmd 20466 frlmip 20467 mattposvs 21060 mat1dimelbas 21076 mdetrlin 21207 lmfval 21837 txbasex 22171 txopn 22207 txcn 22231 txrest 22236 txindislem 22238 xkoinjcn 22292 blfvalps 22990 bcthlem1 23928 bcthlem5 23932 rrxip 23994 isvcOLD 28362 resf1o 30492 locfinref 31194 esum2dlem 31461 esum2d 31462 elsx 31563 satfv0 32718 satf00 32734 filnetlem3 33841 filnetlem4 33842 bj-xpexg2 34396 inxpex 35756 xrninxpex 35802 relexpxpnnidm 40404 enrelmap 40698 mpoexxg2 44739 |
Copyright terms: Public domain | W3C validator |