New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > xpkexg | GIF version |
Description: The Kuratowski cross product of two sets is a set. (Contributed by SF, 13-Jan-2015.) |
Ref | Expression |
---|---|
xpkexg | ⊢ ((A ∈ V ∧ B ∈ W) → (A ×k B) ∈ V) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cnvkxpk 4276 | . . 3 ⊢ ◡k(V ×k A) = (A ×k V) | |
2 | xpkvexg 4285 | . . . 4 ⊢ (A ∈ V → (V ×k A) ∈ V) | |
3 | cnvkexg 4286 | . . . 4 ⊢ ((V ×k A) ∈ V → ◡k(V ×k A) ∈ V) | |
4 | 2, 3 | syl 15 | . . 3 ⊢ (A ∈ V → ◡k(V ×k A) ∈ V) |
5 | 1, 4 | syl5eqelr 2438 | . 2 ⊢ (A ∈ V → (A ×k V) ∈ V) |
6 | xpkvexg 4285 | . 2 ⊢ (B ∈ W → (V ×k B) ∈ V) | |
7 | inxpk 4277 | . . . 4 ⊢ ((A ×k V) ∩ (V ×k B)) = ((A ∩ V) ×k (V ∩ B)) | |
8 | inv1 3577 | . . . . 5 ⊢ (A ∩ V) = A | |
9 | incom 3448 | . . . . . 6 ⊢ (V ∩ B) = (B ∩ V) | |
10 | inv1 3577 | . . . . . 6 ⊢ (B ∩ V) = B | |
11 | 9, 10 | eqtri 2373 | . . . . 5 ⊢ (V ∩ B) = B |
12 | 8, 11 | xpkeq12i 4203 | . . . 4 ⊢ ((A ∩ V) ×k (V ∩ B)) = (A ×k B) |
13 | 7, 12 | eqtri 2373 | . . 3 ⊢ ((A ×k V) ∩ (V ×k B)) = (A ×k B) |
14 | inexg 4100 | . . 3 ⊢ (((A ×k V) ∈ V ∧ (V ×k B) ∈ V) → ((A ×k V) ∩ (V ×k B)) ∈ V) | |
15 | 13, 14 | syl5eqelr 2438 | . 2 ⊢ (((A ×k V) ∈ V ∧ (V ×k B) ∈ V) → (A ×k B) ∈ V) |
16 | 5, 6, 15 | syl2an 463 | 1 ⊢ ((A ∈ V ∧ B ∈ W) → (A ×k B) ∈ V) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 358 ∈ wcel 1710 Vcvv 2859 ∩ cin 3208 ×k cxpk 4174 ◡kccnvk 4175 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1546 ax-5 1557 ax-17 1616 ax-9 1654 ax-8 1675 ax-6 1729 ax-7 1734 ax-11 1746 ax-12 1925 ax-ext 2334 ax-nin 4078 ax-xp 4079 ax-cnv 4080 ax-sn 4087 |
This theorem depends on definitions: df-bi 177 df-or 359 df-an 360 df-3an 936 df-nan 1288 df-tru 1319 df-ex 1542 df-nf 1545 df-sb 1649 df-clab 2340 df-cleq 2346 df-clel 2349 df-nfc 2478 df-ne 2518 df-ral 2619 df-rex 2620 df-v 2861 df-nin 3211 df-compl 3212 df-in 3213 df-un 3214 df-dif 3215 df-ss 3259 df-nul 3551 df-sn 3741 df-pr 3742 df-opk 4058 df-xpk 4185 df-cnvk 4186 |
This theorem is referenced by: xpkex 4289 uni1exg 4292 imakexg 4299 pw1exg 4302 pwexg 4328 |
Copyright terms: Public domain | W3C validator |