![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > xpexg | GIF version |
Description: The cross product of two sets is a set. Proposition 6.2 of [TakeutiZaring] p. 23. (Contributed by NM, 14-Aug-1994.) |
Ref | Expression |
---|---|
xpexg | ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 × 𝐵) ∈ V) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | xpsspw 4739 | . 2 ⊢ (𝐴 × 𝐵) ⊆ 𝒫 𝒫 (𝐴 ∪ 𝐵) | |
2 | unexg 4444 | . . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∪ 𝐵) ∈ V) | |
3 | pwexg 4181 | . . 3 ⊢ ((𝐴 ∪ 𝐵) ∈ V → 𝒫 (𝐴 ∪ 𝐵) ∈ V) | |
4 | pwexg 4181 | . . 3 ⊢ (𝒫 (𝐴 ∪ 𝐵) ∈ V → 𝒫 𝒫 (𝐴 ∪ 𝐵) ∈ V) | |
5 | 2, 3, 4 | 3syl 17 | . 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝒫 𝒫 (𝐴 ∪ 𝐵) ∈ V) |
6 | ssexg 4143 | . 2 ⊢ (((𝐴 × 𝐵) ⊆ 𝒫 𝒫 (𝐴 ∪ 𝐵) ∧ 𝒫 𝒫 (𝐴 ∪ 𝐵) ∈ V) → (𝐴 × 𝐵) ∈ V) | |
7 | 1, 5, 6 | sylancr 414 | 1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 × 𝐵) ∈ V) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 104 ∈ wcel 2148 Vcvv 2738 ∪ cun 3128 ⊆ wss 3130 𝒫 cpw 3576 × cxp 4625 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-io 709 ax-5 1447 ax-7 1448 ax-gen 1449 ax-ie1 1493 ax-ie2 1494 ax-8 1504 ax-10 1505 ax-11 1506 ax-i12 1507 ax-bndl 1509 ax-4 1510 ax-17 1526 ax-i9 1530 ax-ial 1534 ax-i5r 1535 ax-13 2150 ax-14 2151 ax-ext 2159 ax-sep 4122 ax-pow 4175 ax-pr 4210 ax-un 4434 |
This theorem depends on definitions: df-bi 117 df-3an 980 df-tru 1356 df-nf 1461 df-sb 1763 df-clab 2164 df-cleq 2170 df-clel 2173 df-nfc 2308 df-rex 2461 df-v 2740 df-un 3134 df-in 3136 df-ss 3143 df-pw 3578 df-sn 3599 df-pr 3600 df-op 3602 df-uni 3811 df-opab 4066 df-xp 4633 |
This theorem is referenced by: xpex 4742 sqxpexg 4743 resiexg 4953 cnvexg 5167 coexg 5174 fex2 5385 fabexg 5404 resfunexgALT 6109 cofunexg 6110 fnexALT 6112 funexw 6113 opabex3d 6122 opabex3 6123 oprabexd 6128 ofmresex 6138 mpoexxg 6211 tposexg 6259 erex 6559 pmex 6653 mapex 6654 pmvalg 6659 elpmg 6664 fvdiagfn 6693 ixpexgg 6722 ixpsnf1o 6736 map1 6812 xpdom2 6831 xpdom3m 6834 xpen 6845 mapxpen 6848 xpfi 6929 djuex 7042 djuassen 7216 cc2lem 7265 shftfvalg 10827 climconst2 11299 releqgg 13080 eqgfval 13081 reldvdsrsrg 13261 dvdsrvald 13262 dvdsrex 13267 aprval 13372 aprap 13376 lmfval 13695 txbasex 13760 txopn 13768 txcn 13778 txrest 13779 blfvalps 13888 xmetxp 14010 limccnp2lem 14148 limccnp2cntop 14149 dvfvalap 14153 |
Copyright terms: Public domain | W3C validator |