New Foundations Explorer		< Previous   Next > Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  df-imagek		Unicode version

---

Definition df-imagek 4194

Description: Define the Kuratowski image function. See opkelimagek 4272 for membership. (Contributed by SF, 12-Jan-2015.)

Assertion

Ref	Expression
df-imagek	Imagek k Ins2k Sk Ins3k Sk k k SIk k1 1 1c

---

Detailed syntax breakdown of Definition df-imagek

Step	Hyp	Ref	Expression
1		cA	. . 3
2	1	cimagek 4182	. 2 Imagek
3		cvv 2859	. . . 4
4	3, 3	cxpk 4174	. . 3 k
5		cssetk 4183	. . . . . 6 Sk
6	5	cins2k 4176	. . . . 5 Ins2k Sk
7	1	csik 4181	. . . . . . . 8 SIk
8	7	ccnvk 4175	. . . . . . 7 k SIk
9	5, 8	ccomk 4180	. . . . . 6 Sk k k SIk
10	9	cins3k 4177	. . . . 5 Ins3k Sk k k SIk
11	6, 10	csymdif 3209	. . . 4 Ins2k Sk Ins3k Sk k k SIk
12		c1c 4134	. . . . . 6 1c
13	12	cpw1 4135	. . . . 5 1 1c
14	13	cpw1 4135	. . . 4 1 1 1c
15	11, 14	cimak 4179	. . 3 Ins2k Sk Ins3k Sk k k SIk k1 1 1c
16	4, 15	cdif 3206	. 2 k Ins2k Sk Ins3k Sk k k SIk k1 1 1c
17	2, 16	wceq 1642	1 Imagek k Ins2k Sk Ins3k Sk k k SIk k1 1 1c

Colors of variables: wff setvar class

This definition is referenced by:  imagekeq  4244  opkelimagekg  4271  imagekrelk  4273  imagekexg  4311

Copyright terms: Public domain

W3C validator