Definition df-cok 4191

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

Assertion

Ref	Expression
df-cok	⊢ (A ∘k B) = (( Ins2k A ∩ 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 4181	. 2 class (A ∘k B)
4	1	cins2k 4177	. . . 4 class Ins2k A
5	2	ccnvk 4176	. . . . 5 class ◡kB
6	5	cins3k 4178	. . . 4 class Ins3k ◡kB
7	4, 6	cin 3209	. . 3 class ( Ins2k A ∩ Ins3k ◡kB)
8		cvv 2860	. . 3 class V
9	7, 8	cimak 4180	. 2 class (( Ins2k A ∩ Ins3k ◡kB) “k V)
10	3, 9	wceq 1642	1 wff (A ∘k B) = (( Ins2k A ∩ Ins3k ◡kB) “k V)

This definition is referenced by:  cokeq1  4231  cokeq2  4232  opkelcokg  4262  cokrelk  4285  cokexg  4310