Theorem opkelimagekg 4272

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

Assertion

Ref	Expression
opkelimagekg	⊢ ((A ∈ V ∧ B ∈ W) → (⟪A, B⟫ ∈ ImagekC ↔ B = (C “k A)))

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 176   ∧ wa 358  ∀wal 1540  ∃wex 1541   = wceq 1642   ∈ wcel 1710  ∃wrex 2616  Vcvv 2860   ∖ cdif 3207   ⊕ csymdif 3210  {csn 3738  ⟪copk 4058  1_cc1c 4135  ℘₁cpw1 4136   ×_k cxpk 4175  ^◡_kccnvk 4176   Ins2_k cins2k 4177   Ins3_k cins3k 4178   “_k cimak 4180   ∘_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