NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  df-imagek GIF 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 ImagekA = ((V ×k V) (( Ins2k SkIns3k ( Sk k k SIk A)) “k 111c))

Detailed syntax breakdown of Definition df-imagek
StepHypRef Expression
1 cA . . 3 class A
21cimagek 4182 . 2 class ImagekA
3 cvv 2859 . . . 4 class V
43, 3cxpk 4174 . . 3 class (V ×k V)
5 cssetk 4183 . . . . . 6 class Sk
65cins2k 4176 . . . . 5 class Ins2k Sk
71csik 4181 . . . . . . . 8 class SIk A
87ccnvk 4175 . . . . . . 7 class k SIk A
95, 8ccomk 4180 . . . . . 6 class ( Sk k k SIk A)
109cins3k 4177 . . . . 5 class Ins3k ( Sk k k SIk A)
116, 10csymdif 3209 . . . 4 class ( Ins2k SkIns3k ( Sk k k SIk A))
12 c1c 4134 . . . . . 6 class 1c
1312cpw1 4135 . . . . 5 class 11c
1413cpw1 4135 . . . 4 class 111c
1511, 14cimak 4179 . . 3 class (( Ins2k SkIns3k ( Sk k k SIk A)) “k 111c)
164, 15cdif 3206 . 2 class ((V ×k V) (( Ins2k SkIns3k ( Sk k k SIk A)) “k 111c))
172, 16wceq 1642 1 wff ImagekA = ((V ×k V) (( Ins2k SkIns3k ( Sk k k SIk A)) “k 111c))
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