Definition df-imagek 4195

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

Assertion

Ref	Expression
df-imagek	|- ImagekA = ((_V X.k _V) \ (( Ins2k Sk (+) Ins3k ( Sk o.k `'k SIk A))"k~P1 ~P1 1c))

Detailed syntax breakdown of Definition df-imagek

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2	1	cimagek 4183	. 2 class ImagekA
3		cvv 2860	. . . 4 class _V
4	3, 3	cxpk 4175	. . 3 class (_V X.k _V)
5		cssetk 4184	. . . . . 6 class Sk
6	5	cins2k 4177	. . . . 5 class Ins2k Sk
7	1	csik 4182	. . . . . . . 8 class SIk A
8	7	ccnvk 4176	. . . . . . 7 class `'k SIk A
9	5, 8	ccomk 4181	. . . . . 6 class ( Sk o.k `'k SIk A)
10	9	cins3k 4178	. . . . 5 class Ins3k ( Sk o.k `'k SIk A)
11	6, 10	csymdif 3210	. . . 4 class ( Ins2k Sk (+) Ins3k ( Sk o.k `'k SIk A))
12		c1c 4135	. . . . . 6 class 1c
13	12	cpw1 4136	. . . . 5 class ~P1 1c
14	13	cpw1 4136	. . . 4 class ~P1 ~P1 1c
15	11, 14	cimak 4180	. . 3 class (( Ins2k Sk (+) Ins3k ( Sk o.k `'k SIk A))"k~P1 ~P1 1c)
16	4, 15	cdif 3207	. 2 class ((_V X.k _V) \ (( Ins2k Sk (+) Ins3k ( Sk o.k `'k SIk A))"k~P1 ~P1 1c))
17	2, 16	wceq 1642	1 wff ImagekA = ((_V X.k _V) \ (( Ins2k Sk (+) Ins3k ( Sk o.k `'k SIk A))"k~P1 ~P1 1c))

This definition is referenced by:  imagekeq  4245  opkelimagekg  4272  imagekrelk  4274  imagekexg  4312