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 ×k V) ∖ (( Ins2k Sk ⊕ Ins3k ( Sk ∘k ◡k SIk A)) “k ℘1℘11c))

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 ×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 ∘k ◡k SIk A)
10	9	cins3k 4178	. . . . 5 class Ins3k ( Sk ∘k ◡k SIk A)
11	6, 10	csymdif 3210	. . . 4 class ( Ins2k Sk ⊕ Ins3k ( Sk ∘k ◡k SIk A))
12		c1c 4135	. . . . . 6 class 1c
13	12	cpw1 4136	. . . . 5 class ℘11c
14	13	cpw1 4136	. . . 4 class ℘1℘11c
15	11, 14	cimak 4180	. . 3 class (( Ins2k Sk ⊕ Ins3k ( Sk ∘k ◡k SIk A)) “k ℘1℘11c)
16	4, 15	cdif 3207	. 2 class ((V ×k V) ∖ (( Ins2k Sk ⊕ Ins3k ( Sk ∘k ◡k SIk A)) “k ℘1℘11c))
17	2, 16	wceq 1642	1 wff ImagekA = ((V ×k V) ∖ (( Ins2k Sk ⊕ Ins3k ( Sk ∘k ◡k SIk A)) “k ℘1℘11c))

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