| 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 8006. (Contributed by NM, 14-Aug-1994.) |
| Ref | Expression |
|---|---|
| xpexg | ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 × 𝐵) ∈ V) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | xpsspw 5819 | . 2 ⊢ (𝐴 × 𝐵) ⊆ 𝒫 𝒫 (𝐴 ∪ 𝐵) | |
| 2 | unexg 7763 | . . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∪ 𝐵) ∈ V) | |
| 3 | pwexg 5378 | . . 3 ⊢ ((𝐴 ∪ 𝐵) ∈ V → 𝒫 (𝐴 ∪ 𝐵) ∈ V) | |
| 4 | pwexg 5378 | . . 3 ⊢ (𝒫 (𝐴 ∪ 𝐵) ∈ V → 𝒫 𝒫 (𝐴 ∪ 𝐵) ∈ V) | |
| 5 | 2, 3, 4 | 3syl 18 | . 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝒫 𝒫 (𝐴 ∪ 𝐵) ∈ V) |
| 6 | ssexg 5323 | . 2 ⊢ (((𝐴 × 𝐵) ⊆ 𝒫 𝒫 (𝐴 ∪ 𝐵) ∧ 𝒫 𝒫 (𝐴 ∪ 𝐵) ∈ V) → (𝐴 × 𝐵) ∈ V) | |
| 7 | 1, 5, 6 | sylancr 587 | 1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 × 𝐵) ∈ V) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 395 ∈ wcel 2108 Vcvv 3480 ∪ cun 3949 ⊆ wss 3951 𝒫 cpw 4600 × cxp 5683 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 ax-sep 5296 ax-nul 5306 ax-pow 5365 ax-pr 5432 ax-un 7755 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3an 1089 df-tru 1543 df-fal 1553 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-ral 3062 df-rex 3071 df-rab 3437 df-v 3482 df-dif 3954 df-un 3956 df-in 3958 df-ss 3968 df-nul 4334 df-if 4526 df-pw 4602 df-sn 4627 df-pr 4629 df-op 4633 df-uni 4908 df-opab 5206 df-xp 5691 df-rel 5692 |
| This theorem is referenced by: xpexd 7771 3xpexg 7772 xpex 7773 sqxpexg 7775 coexg 7951 fex2 7958 fabexgOLD 7961 resfunexgALT 7972 fnexALT 7975 funexw 7976 opabex3d 7990 opabex3rd 7991 opabex3 7992 mpoexxg 8100 fnwelem 8156 naddunif 8731 pmex 8871 mapexOLD 8872 pmvalg 8877 elpmg 8883 fvdiagfn 8931 ixpexg 8962 snmapen 9078 xpdom2 9107 xpdom3 9110 omxpen 9114 fodomr 9168 disjenex 9175 domssex2 9177 domssex 9178 mapxpen 9183 xpfiOLD 9359 fczfsuppd 9426 brwdom2 9613 xpwdomg 9625 unxpwdom2 9628 djuex 9948 djuexALT 9962 fseqen 10067 djuassen 10219 mapdjuen 10221 djudom1 10223 djuinf 10229 hsmexlem2 10467 axdc2lem 10488 iundom2g 10580 fpwwe2lem12 10682 pwsbas 17532 pwsle 17537 pwssca 17541 isga 19309 efgtf 19740 frgpcpbl 19777 frgp0 19778 frgpeccl 19779 frgpadd 19781 frgpmhm 19783 vrgpf 19786 vrgpinv 19787 frgpupf 19791 frgpup1 19793 frgpup2 19794 frgpup3lem 19795 frgpnabllem1 19891 frgpnabllem2 19892 gsum2d2 19992 gsumcom2 19993 dprd2da 20062 pwssplit3 21060 mpofrlmd 21797 frlmip 21798 mattposvs 22461 mat1dimelbas 22477 mdetrlin 22608 lmfval 23240 txbasex 23574 txopn 23610 txrest 23639 txindislem 23641 xkoinjcn 23695 blfvalps 24393 bcthlem1 25358 bcthlem5 25362 rrxip 25424 isvcOLD 30598 resf1o 32741 locfinref 33840 esum2dlem 34093 esum2d 34094 elsx 34195 satfv0 35363 satf00 35379 filnetlem3 36381 filnetlem4 36382 bj-xpexg2 36961 inxpex 38340 xrninxpex 38395 aks6d1c2 42131 relexpxpnnidm 43716 enrelmap 44010 mpoexxg2 48254 eufsn2 48752 |
| Copyright terms: Public domain | W3C validator |