Definition df-cok 4190

Description: Define the Kuratowski composition operator. (Contributed by SF, 12-Jan-2015.)

Assertion

Ref	Expression
df-cok	|- (A o.k B) = (( Ins2k A i^i Ins3k `'kB)"k_V)

Detailed syntax breakdown of Definition df-cok

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2		cB	. . 3 class B
3	1, 2	ccomk 4180	. 2 class (A o.k B)
4	1	cins2k 4176	. . . 4 class Ins2k A
5	2	ccnvk 4175	. . . . 5 class `'kB
6	5	cins3k 4177	. . . 4 class Ins3k `'kB
7	4, 6	cin 3208	. . 3 class ( Ins2k A i^i Ins3k `'kB)
8		cvv 2859	. . 3 class _V
9	7, 8	cimak 4179	. 2 class (( Ins2k A i^i Ins3k `'kB)"k_V)
10	3, 9	wceq 1642	1 wff (A o.k B) = (( Ins2k A i^i Ins3k `'kB)"k_V)

This definition is referenced by:  cokeq1  4230  cokeq2  4231  opkelcokg  4261  cokrelk  4284  cokexg  4309