imakexg - New Foundations Explorer

	New Foundations Explorer		< Previous Next > Nearby theorems
Mirrors > Home > NFE Home > Th. List > imakexg		GIF version

Theorem imakexg 4299

Description: The image of a set under a set is a set. (Contributed by SF, 14-Jan-2015.)

**Assertion**
Ref	Expression
imakexg	⊢ ((A ∈ V ∧ B ∈ W) → (A “_k B) ∈ V)

**Proof of Theorem imakexg**
Step	Hyp	Ref	Expression
1		dfimak2 4298	. 2 ⊢ (A “_k B) = ∼ P6 ( ∼ (1_c ×_k V) ∪ SI_k ∼ (A ∩ (B ×_k V)))
2		1cex 4142	. . . . . 6 ⊢ 1_c ∈ V
3		vvex 4109	. . . . . 6 ⊢ V ∈ V
4	2, 3	xpkex 4289	. . . . 5 ⊢ (1_c ×_k V) ∈ V
5	4	complex 4104	. . . 4 ⊢ ∼ (1_c ×_k V) ∈ V
6		xpkexg 4288	. . . . . . 7 ⊢ ((B ∈ W ∧ V ∈ V) → (B ×_k V) ∈ V)
7	3, 6	mpan2 652	. . . . . 6 ⊢ (B ∈ W → (B ×_k V) ∈ V)
8		inexg 4100	. . . . . 6 ⊢ ((A ∈ V ∧ (B ×_k V) ∈ V) → (A ∩ (B ×_k V)) ∈ V)
9	7, 8	sylan2 460	. . . . 5 ⊢ ((A ∈ V ∧ B ∈ W) → (A ∩ (B ×_k V)) ∈ V)
10		complexg 4099	. . . . 5 ⊢ ((A ∩ (B ×_k V)) ∈ V → ∼ (A ∩ (B ×_k V)) ∈ V)
11		sikexg 4296	. . . . 5 ⊢ ( ∼ (A ∩ (B ×_k V)) ∈ V → SI_k ∼ (A ∩ (B ×_k V)) ∈ V)
12	9, 10, 11	3syl 18	. . . 4 ⊢ ((A ∈ V ∧ B ∈ W) → SI_k ∼ (A ∩ (B ×_k V)) ∈ V)
13		unexg 4101	. . . 4 ⊢ (( ∼ (1_c ×_k V) ∈ V ∧ SI_k ∼ (A ∩ (B ×_k V)) ∈ V) → ( ∼ (1_c ×_k V) ∪ SI_k ∼ (A ∩ (B ×_k V))) ∈ V)
14	5, 12, 13	sylancr 644	. . 3 ⊢ ((A ∈ V ∧ B ∈ W) → ( ∼ (1_c ×_k V) ∪ SI_k ∼ (A ∩ (B ×_k V))) ∈ V)
15		p6exg 4290	. . 3 ⊢ (( ∼ (1_c ×_k V) ∪ SI_k ∼ (A ∩ (B ×_k V))) ∈ V → P6 ( ∼ (1_c ×_k V) ∪ SI_k ∼ (A ∩ (B ×_k V))) ∈ V)
16		complexg 4099	. . 3 ⊢ ( P6 ( ∼ (1_c ×_k V) ∪ SI_k ∼ (A ∩ (B ×_k V))) ∈ V → ∼ P6 ( ∼ (1_c ×_k V) ∪ SI_k ∼ (A ∩ (B ×_k V))) ∈ V)
17	14, 15, 16	3syl 18	. 2 ⊢ ((A ∈ V ∧ B ∈ W) → ∼ P6 ( ∼ (1_c ×_k V) ∪ SI_k ∼ (A ∩ (B ×_k V))) ∈ V)
18	1, 17	syl5eqel 2437	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 ∼ ccompl 3205 ∪ cun 3207 ∩ cin 3208 1_cc1c 4134 ×_k cxpk 4174 P6 cp6 4178 “_k cimak 4179 SI_k csik 4181

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-1c 4081 ax-si 4083 ax-typlower 4086 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-1c 4136 df-xpk 4185 df-cnvk 4186 df-imak 4189 df-p6 4191 df-sik 4192

This theorem is referenced by: imakex 4300 pw1exg 4302 cokexg 4309 imagekexg 4311 uniexg 4316 intexg 4319 pwexg 4328 addcexg 4393 phiexg 4571 opexg 4587 proj1exg 4591 proj2exg 4592 imaexg 4746 coexg 4749 siexg 4752

W3C validator