Theorem opkelimagekg 4272

Description: Membership in the Kuratowski image functor. (Contributed by SF, 13-Jan-2015.)

Assertion

Ref	Expression
opkelimagekg	|- ((A e. V /\ B e. W) -> (<<A, B>> e. ImagekC <-> B = (C"kA)))

Proof of Theorem opkelimagekg

Dummy variables x y z are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		elex 2868	. 2 |- (A e. V -> A e. _V)
2		elex 2868	. 2 |- (B e. W -> B e. _V)
3		opkelxpkg 4248	. . . . . 6 |- ((A e. _V /\ B e. _V) -> (<<A, B>> e. (_V X.k _V) <-> (A e. _V /\ B e. _V)))
4	3	ibir 233	. . . . 5 |- ((A e. _V /\ B e. _V) -> <<A, B>> e. (_V X.k _V))
5	4	biantrurd 494	. . . 4 |- ((A e. _V /\ B e. _V) -> (-. <<A, B>> e. (( Ins2k Sk (+) Ins3k ( Sk o.k `'k SIk C))"k~P1 ~P1 1c) <-> (<<A, B>> e. (_V X.k _V) /\ -. <<A, B>> e. (( Ins2k Sk (+) Ins3k ( Sk o.k `'k SIk C))"k~P1 ~P1 1c))))
6		exnal 1574	. . . . . 6 |- (E.x -. (x e. B <-> x e. (C"kA)) <-> -. A.x(x e. B <-> x e. (C"kA)))
7		opkex 4114	. . . . . . . . 9 |- <<A, B>> e. _V
8	7	elimak 4260	. . . . . . . 8 |- (<<A, B>> e. (( Ins2k Sk (+) Ins3k ( Sk o.k `'k SIk C))"k~P1 ~P1 1c) <-> E.y e. ~P1 ~P1 1c<<y, <<A, B>>>> e. ( Ins2k Sk (+) Ins3k ( Sk o.k `'k SIk C)))
9		df-rex 2621	. . . . . . . 8 |- (E.y e. ~P1 ~P1 1c<<y, <<A, B>>>> e. ( Ins2k Sk (+) Ins3k ( Sk o.k `'k SIk C)) <-> E.y(y e. ~P1 ~P1 1c /\ <<y, <<A, B>>>> e. ( Ins2k Sk (+) Ins3k ( Sk o.k `'k SIk C))))
10		elpw121c 4149	. . . . . . . . . . . 12 |- (y e. ~P1 ~P1 1c <-> E.x y = {{{x}}})
11	10	anbi1i 676	. . . . . . . . . . 11 |- ((y e. ~P1 ~P1 1c /\ <<y, <<A, B>>>> e. ( Ins2k Sk (+) Ins3k ( Sk o.k `'k SIk C))) <-> (E.x y = {{{x}}} /\ <<y, <<A, B>>>> e. ( Ins2k Sk (+) Ins3k ( Sk o.k `'k SIk C))))
12		19.41v 1901	. . . . . . . . . . 11 |- (E.x(y = {{{x}}} /\ <<y, <<A, B>>>> e. ( Ins2k Sk (+) Ins3k ( Sk o.k `'k SIk C))) <-> (E.x y = {{{x}}} /\ <<y, <<A, B>>>> e. ( Ins2k Sk (+) Ins3k ( Sk o.k `'k SIk C))))
13	11, 12	bitr4i 243	. . . . . . . . . 10 |- ((y e. ~P1 ~P1 1c /\ <<y, <<A, B>>>> e. ( Ins2k Sk (+) Ins3k ( Sk o.k `'k SIk C))) <-> E.x(y = {{{x}}} /\ <<y, <<A, B>>>> e. ( Ins2k Sk (+) Ins3k ( Sk o.k `'k SIk C))))
14	13	exbii 1582	. . . . . . . . 9 |- (E.y(y e. ~P1 ~P1 1c /\ <<y, <<A, B>>>> e. ( Ins2k Sk (+) Ins3k ( Sk o.k `'k SIk C))) <-> E.yE.x(y = {{{x}}} /\ <<y, <<A, B>>>> e. ( Ins2k Sk (+) Ins3k ( Sk o.k `'k SIk C))))
15		excom 1741	. . . . . . . . 9 |- (E.yE.x(y = {{{x}}} /\ <<y, <<A, B>>>> e. ( Ins2k Sk (+) Ins3k ( Sk o.k `'k SIk C))) <-> E.xE.y(y = {{{x}}} /\ <<y, <<A, B>>>> e. ( Ins2k Sk (+) Ins3k ( Sk o.k `'k SIk C))))
16		snex 4112	. . . . . . . . . . 11 |- {{{x}}} e. _V
17		opkeq1 4060	. . . . . . . . . . . 12 |- (y = {{{x}}} -> <<y, <<A, B>>>> = <<{{{x}}}, <<A, B>>>>)
18	17	eleq1d 2419	. . . . . . . . . . 11 |- (y = {{{x}}} -> (<<y, <<A, B>>>> e. ( Ins2k Sk (+) Ins3k ( Sk o.k `'k SIk C)) <-> <<{{{x}}}, <<A, B>>>> e. ( Ins2k Sk (+) Ins3k ( Sk o.k `'k SIk C))))
19	16, 18	ceqsexv 2895	. . . . . . . . . 10 |- (E.y(y = {{{x}}} /\ <<y, <<A, B>>>> e. ( Ins2k Sk (+) Ins3k ( Sk o.k `'k SIk C))) <-> <<{{{x}}}, <<A, B>>>> e. ( Ins2k Sk (+) Ins3k ( Sk o.k `'k SIk C)))
20	19	exbii 1582	. . . . . . . . 9 |- (E.xE.y(y = {{{x}}} /\ <<y, <<A, B>>>> e. ( Ins2k Sk (+) Ins3k ( Sk o.k `'k SIk C))) <-> E.x<<{{{x}}}, <<A, B>>>> e. ( Ins2k Sk (+) Ins3k ( Sk o.k `'k SIk C)))
21	14, 15, 20	3bitri 262	. . . . . . . 8 |- (E.y(y e. ~P1 ~P1 1c /\ <<y, <<A, B>>>> e. ( Ins2k Sk (+) Ins3k ( Sk o.k `'k SIk C))) <-> E.x<<{{{x}}}, <<A, B>>>> e. ( Ins2k Sk (+) Ins3k ( Sk o.k `'k SIk C)))
22	8, 9, 21	3bitri 262	. . . . . . 7 |- (<<A, B>> e. (( Ins2k Sk (+) Ins3k ( Sk o.k `'k SIk C))"k~P1 ~P1 1c) <-> E.x<<{{{x}}}, <<A, B>>>> e. ( Ins2k Sk (+) Ins3k ( Sk o.k `'k SIk C)))
23		elsymdif 3224	. . . . . . . . 9 |- (<<{{{x}}}, <<A, B>>>> e. ( Ins2k Sk (+) Ins3k ( Sk o.k `'k SIk C)) <-> -. (<<{{{x}}}, <<A, B>>>> e. Ins2k Sk <-> <<{{{x}}}, <<A, B>>>> e. Ins3k ( Sk o.k `'k SIk C)))
24		snex 4112	. . . . . . . . . . . . 13 |- {x} e. _V
25		otkelins2kg 4254	. . . . . . . . . . . . 13 |- (({x} e. _V /\ A e. _V /\ B e. _V) -> (<<{{{x}}}, <<A, B>>>> e. Ins2k Sk <-> <<{x}, B>> e. Sk ))
26	24, 25	mp3an1 1264	. . . . . . . . . . . 12 |- ((A e. _V /\ B e. _V) -> (<<{{{x}}}, <<A, B>>>> e. Ins2k Sk <-> <<{x}, B>> e. Sk ))
27		vex 2863	. . . . . . . . . . . . . 14 |- x e. _V
28		elssetkg 4270	. . . . . . . . . . . . . 14 |- ((x e. _V /\ B e. _V) -> (<<{x}, B>> e. Sk <-> x e. B))
29	27, 28	mpan 651	. . . . . . . . . . . . 13 |- (B e. _V -> (<<{x}, B>> e. Sk <-> x e. B))
30	29	adantl 452	. . . . . . . . . . . 12 |- ((A e. _V /\ B e. _V) -> (<<{x}, B>> e. Sk <-> x e. B))
31	26, 30	bitrd 244	. . . . . . . . . . 11 |- ((A e. _V /\ B e. _V) -> (<<{{{x}}}, <<A, B>>>> e. Ins2k Sk <-> x e. B))
32		otkelins3kg 4255	. . . . . . . . . . . . 13 |- (({x} e. _V /\ A e. _V /\ B e. _V) -> (<<{{{x}}}, <<A, B>>>> e. Ins3k ( Sk o.k `'k SIk C) <-> <<{x}, A>> e. ( Sk o.k `'k SIk C)))
33	24, 32	mp3an1 1264	. . . . . . . . . . . 12 |- ((A e. _V /\ B e. _V) -> (<<{{{x}}}, <<A, B>>>> e. Ins3k ( Sk o.k `'k SIk C) <-> <<{x}, A>> e. ( Sk o.k `'k SIk C)))
34		opkelcokg 4262	. . . . . . . . . . . . . . . 16 |- (({x} e. _V /\ A e. _V) -> (<<{x}, A>> e. ( Sk o.k `'k SIk C) <-> E.z(<<{x}, z>> e. `'k SIk C /\ <<z, A>> e. Sk )))
35	24, 34	mpan 651	. . . . . . . . . . . . . . 15 |- (A e. _V -> (<<{x}, A>> e. ( Sk o.k `'k SIk C) <-> E.z(<<{x}, z>> e. `'k SIk C /\ <<z, A>> e. Sk )))
36		vex 2863	. . . . . . . . . . . . . . . . . . 19 |- y e. _V
37		elssetkg 4270	. . . . . . . . . . . . . . . . . . 19 |- ((y e. _V /\ A e. _V) -> (<<{y}, A>> e. Sk <-> y e. A))
38	36, 37	mpan 651	. . . . . . . . . . . . . . . . . 18 |- (A e. _V -> (<<{y}, A>> e. Sk <-> y e. A))
39	38	anbi1d 685	. . . . . . . . . . . . . . . . 17 |- (A e. _V -> ((<<{y}, A>> e. Sk /\ <<y, x>> e. C) <-> (y e. A /\ <<y, x>> e. C)))
40	39	exbidv 1626	. . . . . . . . . . . . . . . 16 |- (A e. _V -> (E.y(<<{y}, A>> e. Sk /\ <<y, x>> e. C) <-> E.y(y e. A /\ <<y, x>> e. C)))
41		vex 2863	. . . . . . . . . . . . . . . . . . . . . 22 |- z e. _V
42	24, 41	opkelcnvk 4251	. . . . . . . . . . . . . . . . . . . . 21 |- (<<{x}, z>> e. `'k SIk C <-> <<z, {x}>> e. SIk C)
43		sikss1c1c 4268	. . . . . . . . . . . . . . . . . . . . . . . 24 |- SIk C C_ (1c X.k 1c)
44	43	sseli 3270	. . . . . . . . . . . . . . . . . . . . . . 23 |- (<<z, {x}>> e. SIk C -> <<z, {x}>> e. (1c X.k 1c))
45	41, 24	opkelxpk 4249	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (<<z, {x}>> e. (1c X.k 1c) <-> (z e. 1c /\ {x} e. 1c))
46		el1c 4140	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (z e. 1c <-> E.y z = {y})
47	46	biimpi 186	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (z e. 1c -> E.y z = {y})
48	47	adantr 451	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((z e. 1c /\ {x} e. 1c) -> E.y z = {y})
49	45, 48	sylbi 187	. . . . . . . . . . . . . . . . . . . . . . 23 |- (<<z, {x}>> e. (1c X.k 1c) -> E.y z = {y})
50	44, 49	syl 15	. . . . . . . . . . . . . . . . . . . . . 22 |- (<<z, {x}>> e. SIk C -> E.y z = {y})
51	50	pm4.71ri 614	. . . . . . . . . . . . . . . . . . . . 21 |- (<<z, {x}>> e. SIk C <-> (E.y z = {y} /\ <<z, {x}>> e. SIk C))
52	42, 51	bitri 240	. . . . . . . . . . . . . . . . . . . 20 |- (<<{x}, z>> e. `'k SIk C <-> (E.y z = {y} /\ <<z, {x}>> e. SIk C))
53	52	anbi1i 676	. . . . . . . . . . . . . . . . . . 19 |- ((<<{x}, z>> e. `'k SIk C /\ <<z, A>> e. Sk ) <-> ((E.y z = {y} /\ <<z, {x}>> e. SIk C) /\ <<z, A>> e. Sk ))
54		anass 630	. . . . . . . . . . . . . . . . . . . 20 |- (((E.y z = {y} /\ <<z, {x}>> e. SIk C) /\ <<z, A>> e. Sk ) <-> (E.y z = {y} /\ (<<z, {x}>> e. SIk C /\ <<z, A>> e. Sk )))
55		19.41v 1901	. . . . . . . . . . . . . . . . . . . 20 |- (E.y(z = {y} /\ (<<z, {x}>> e. SIk C /\ <<z, A>> e. Sk )) <-> (E.y z = {y} /\ (<<z, {x}>> e. SIk C /\ <<z, A>> e. Sk )))
56	54, 55	bitr4i 243	. . . . . . . . . . . . . . . . . . 19 |- (((E.y z = {y} /\ <<z, {x}>> e. SIk C) /\ <<z, A>> e. Sk ) <-> E.y(z = {y} /\ (<<z, {x}>> e. SIk C /\ <<z, A>> e. Sk )))
57	53, 56	bitri 240	. . . . . . . . . . . . . . . . . 18 |- ((<<{x}, z>> e. `'k SIk C /\ <<z, A>> e. Sk ) <-> E.y(z = {y} /\ (<<z, {x}>> e. SIk C /\ <<z, A>> e. Sk )))
58	57	exbii 1582	. . . . . . . . . . . . . . . . 17 |- (E.z(<<{x}, z>> e. `'k SIk C /\ <<z, A>> e. Sk ) <-> E.zE.y(z = {y} /\ (<<z, {x}>> e. SIk C /\ <<z, A>> e. Sk )))
59		excom 1741	. . . . . . . . . . . . . . . . 17 |- (E.zE.y(z = {y} /\ (<<z, {x}>> e. SIk C /\ <<z, A>> e. Sk )) <-> E.yE.z(z = {y} /\ (<<z, {x}>> e. SIk C /\ <<z, A>> e. Sk )))
60		snex 4112	. . . . . . . . . . . . . . . . . . 19 |- {y} e. _V
61		opkeq1 4060	. . . . . . . . . . . . . . . . . . . . . 22 |- (z = {y} -> <<z, {x}>> = <<{y}, {x}>>)
62	61	eleq1d 2419	. . . . . . . . . . . . . . . . . . . . 21 |- (z = {y} -> (<<z, {x}>> e. SIk C <-> <<{y}, {x}>> e. SIk C))
63		opkeq1 4060	. . . . . . . . . . . . . . . . . . . . . 22 |- (z = {y} -> <<z, A>> = <<{y}, A>>)
64	63	eleq1d 2419	. . . . . . . . . . . . . . . . . . . . 21 |- (z = {y} -> (<<z, A>> e. Sk <-> <<{y}, A>> e. Sk ))
65	62, 64	anbi12d 691	. . . . . . . . . . . . . . . . . . . 20 |- (z = {y} -> ((<<z, {x}>> e. SIk C /\ <<z, A>> e. Sk ) <-> (<<{y}, {x}>> e. SIk C /\ <<{y}, A>> e. Sk )))
66		ancom 437	. . . . . . . . . . . . . . . . . . . . 21 |- ((<<{y}, {x}>> e. SIk C /\ <<{y}, A>> e. Sk ) <-> (<<{y}, A>> e. Sk /\ <<{y}, {x}>> e. SIk C))
67	36, 27	opksnelsik 4266	. . . . . . . . . . . . . . . . . . . . . 22 |- (<<{y}, {x}>> e. SIk C <-> <<y, x>> e. C)
68	67	anbi2i 675	. . . . . . . . . . . . . . . . . . . . 21 |- ((<<{y}, A>> e. Sk /\ <<{y}, {x}>> e. SIk C) <-> (<<{y}, A>> e. Sk /\ <<y, x>> e. C))
69	66, 68	bitri 240	. . . . . . . . . . . . . . . . . . . 20 |- ((<<{y}, {x}>> e. SIk C /\ <<{y}, A>> e. Sk ) <-> (<<{y}, A>> e. Sk /\ <<y, x>> e. C))
70	65, 69	syl6bb 252	. . . . . . . . . . . . . . . . . . 19 |- (z = {y} -> ((<<z, {x}>> e. SIk C /\ <<z, A>> e. Sk ) <-> (<<{y}, A>> e. Sk /\ <<y, x>> e. C)))
71	60, 70	ceqsexv 2895	. . . . . . . . . . . . . . . . . 18 |- (E.z(z = {y} /\ (<<z, {x}>> e. SIk C /\ <<z, A>> e. Sk )) <-> (<<{y}, A>> e. Sk /\ <<y, x>> e. C))
72	71	exbii 1582	. . . . . . . . . . . . . . . . 17 |- (E.yE.z(z = {y} /\ (<<z, {x}>> e. SIk C /\ <<z, A>> e. Sk )) <-> E.y(<<{y}, A>> e. Sk /\ <<y, x>> e. C))
73	58, 59, 72	3bitri 262	. . . . . . . . . . . . . . . 16 |- (E.z(<<{x}, z>> e. `'k SIk C /\ <<z, A>> e. Sk ) <-> E.y(<<{y}, A>> e. Sk /\ <<y, x>> e. C))
74		df-rex 2621	. . . . . . . . . . . . . . . 16 |- (E.y e. A <<y, x>> e. C <-> E.y(y e. A /\ <<y, x>> e. C))
75	40, 73, 74	3bitr4g 279	. . . . . . . . . . . . . . 15 |- (A e. _V -> (E.z(<<{x}, z>> e. `'k SIk C /\ <<z, A>> e. Sk ) <-> E.y e. A <<y, x>> e. C))
76	35, 75	bitrd 244	. . . . . . . . . . . . . 14 |- (A e. _V -> (<<{x}, A>> e. ( Sk o.k `'k SIk C) <-> E.y e. A <<y, x>> e. C))
77	27	elimak 4260	. . . . . . . . . . . . . 14 |- (x e. (C"kA) <-> E.y e. A <<y, x>> e. C)
78	76, 77	syl6bbr 254	. . . . . . . . . . . . 13 |- (A e. _V -> (<<{x}, A>> e. ( Sk o.k `'k SIk C) <-> x e. (C"kA)))
79	78	adantr 451	. . . . . . . . . . . 12 |- ((A e. _V /\ B e. _V) -> (<<{x}, A>> e. ( Sk o.k `'k SIk C) <-> x e. (C"kA)))
80	33, 79	bitrd 244	. . . . . . . . . . 11 |- ((A e. _V /\ B e. _V) -> (<<{{{x}}}, <<A, B>>>> e. Ins3k ( Sk o.k `'k SIk C) <-> x e. (C"kA)))
81	31, 80	bibi12d 312	. . . . . . . . . 10 |- ((A e. _V /\ B e. _V) -> ((<<{{{x}}}, <<A, B>>>> e. Ins2k Sk <-> <<{{{x}}}, <<A, B>>>> e. Ins3k ( Sk o.k `'k SIk C)) <-> (x e. B <-> x e. (C"kA))))
82	81	notbid 285	. . . . . . . . 9 |- ((A e. _V /\ B e. _V) -> (-. (<<{{{x}}}, <<A, B>>>> e. Ins2k Sk <-> <<{{{x}}}, <<A, B>>>> e. Ins3k ( Sk o.k `'k SIk C)) <-> -. (x e. B <-> x e. (C"kA))))
83	23, 82	syl5bb 248	. . . . . . . 8 |- ((A e. _V /\ B e. _V) -> (<<{{{x}}}, <<A, B>>>> e. ( Ins2k Sk (+) Ins3k ( Sk o.k `'k SIk C)) <-> -. (x e. B <-> x e. (C"kA))))
84	83	exbidv 1626	. . . . . . 7 |- ((A e. _V /\ B e. _V) -> (E.x<<{{{x}}}, <<A, B>>>> e. ( Ins2k Sk (+) Ins3k ( Sk o.k `'k SIk C)) <-> E.x -. (x e. B <-> x e. (C"kA))))
85	22, 84	syl5rbb 249	. . . . . 6 |- ((A e. _V /\ B e. _V) -> (E.x -. (x e. B <-> x e. (C"kA)) <-> <<A, B>> e. (( Ins2k Sk (+) Ins3k ( Sk o.k `'k SIk C))"k~P1 ~P1 1c)))
86	6, 85	syl5bbr 250	. . . . 5 |- ((A e. _V /\ B e. _V) -> (-. A.x(x e. B <-> x e. (C"kA)) <-> <<A, B>> e. (( Ins2k Sk (+) Ins3k ( Sk o.k `'k SIk C))"k~P1 ~P1 1c)))
87	86	con1bid 320	. . . 4 |- ((A e. _V /\ B e. _V) -> (-. <<A, B>> e. (( Ins2k Sk (+) Ins3k ( Sk o.k `'k SIk C))"k~P1 ~P1 1c) <-> A.x(x e. B <-> x e. (C"kA))))
88	5, 87	bitr3d 246	. . 3 |- ((A e. _V /\ B e. _V) -> ((<<A, B>> e. (_V X.k _V) /\ -. <<A, B>> e. (( Ins2k Sk (+) Ins3k ( Sk o.k `'k SIk C))"k~P1 ~P1 1c)) <-> A.x(x e. B <-> x e. (C"kA))))
89		df-imagek 4195	. . . . 5 |- ImagekC = ((_V X.k _V) \ (( Ins2k Sk (+) Ins3k ( Sk o.k `'k SIk C))"k~P1 ~P1 1c))
90	89	eleq2i 2417	. . . 4 |- (<<A, B>> e. ImagekC <-> <<A, B>> e. ((_V X.k _V) \ (( Ins2k Sk (+) Ins3k ( Sk o.k `'k SIk C))"k~P1 ~P1 1c)))
91		eldif 3222	. . . 4 |- (<<A, B>> e. ((_V X.k _V) \ (( Ins2k Sk (+) Ins3k ( Sk o.k `'k SIk C))"k~P1 ~P1 1c)) <-> (<<A, B>> e. (_V X.k _V) /\ -. <<A, B>> e. (( Ins2k Sk (+) Ins3k ( Sk o.k `'k SIk C))"k~P1 ~P1 1c)))
92	90, 91	bitri 240	. . 3 |- (<<A, B>> e. ImagekC <-> (<<A, B>> e. (_V X.k _V) /\ -. <<A, B>> e. (( Ins2k Sk (+) Ins3k ( Sk o.k `'k SIk C))"k~P1 ~P1 1c)))
93		dfcleq 2347	. . 3 |- (B = (C"kA) <-> A.x(x e. B <-> x e. (C"kA)))
94	88, 92, 93	3bitr4g 279	. 2 |- ((A e. _V /\ B e. _V) -> (<<A, B>> e. ImagekC <-> B = (C"kA)))
95	1, 2, 94	syl2an 463	1 |- ((A e. V /\ B e. W) -> (<<A, B>> e. ImagekC <-> B = (C"kA)))

Syntax hints:  -. wn 3   -> wi 4   <-> wb 176   /\ wa 358  A.wal 1540  E.wex 1541   = wceq 1642   e. wcel 1710  E.wrex 2616  _Vcvv 2860   \ cdif 3207   (+) csymdif 3210  {csn 3738  <<copk 4058  1_cc1c 4135  ~P₁ cpw1 4136   X._k cxpk 4175  `'_kccnvk 4176   Ins2_k cins2k 4177   Ins3_k cins3k 4178  "_kcimak 4180   o._k ccomk 4181   SI_k csik 4182  Image_kcimagek 4183   S_k cssetk 4184

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-ext 2334  ax-nin 4079  ax-sn 4088

This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-nan 1288  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2340  df-cleq 2346  df-clel 2349  df-nfc 2479  df-ne 2519  df-ral 2620  df-rex 2621  df-v 2862  df-nin 3212  df-compl 3213  df-in 3214  df-un 3215  df-dif 3216  df-symdif 3217  df-ss 3260  df-nul 3552  df-pw 3725  df-sn 3742  df-pr 3743  df-opk 4059  df-1c 4137  df-pw1 4138  df-xpk 4186  df-cnvk 4187  df-ins2k 4188  df-ins3k 4189  df-imak 4190  df-cok 4191  df-sik 4193  df-ssetk 4194  df-imagek 4195

This theorem is referenced by:  opkelimagek  4273  dfnnc2  4396  nnc0suc  4413  nncaddccl  4420  nnsucelrlem1  4425