Theorem opkelcokg 4261

Description: Membership in a Kuratowski composition. (Contributed by SF, 13-Jan-2015.)

Assertion

Ref	Expression
opkelcokg	⊢ ((A ∈ V ∧ B ∈ W) → (⟪A, B⟫ ∈ (C ∘k D) ↔ ∃x(⟪A, x⟫ ∈ D ∧ ⟪x, B⟫ ∈ C)))

Distinct variable groups:   x,A   x,B   x,C   x,D

Allowed substitution hints:   V(x)   W(x)

Proof of Theorem opkelcokg

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

Step	Hyp	Ref	Expression
1		elex 2867	. 2 ⊢ (A ∈ V → A ∈ V)
2		elex 2867	. 2 ⊢ (B ∈ W → B ∈ V)
3		df-cok 4190	. . . . 5 ⊢ (C ∘k D) = (( Ins2k C ∩ Ins3k ◡kD) “k V)
4	3	eleq2i 2417	. . . 4 ⊢ (⟪A, B⟫ ∈ (C ∘k D) ↔ ⟪A, B⟫ ∈ (( Ins2k C ∩ Ins3k ◡kD) “k V))
5		opkex 4113	. . . . 5 ⊢ ⟪A, B⟫ ∈ V
6	5	elimakv 4260	. . . 4 ⊢ (⟪A, B⟫ ∈ (( Ins2k C ∩ Ins3k ◡kD) “k V) ↔ ∃y⟪y, ⟪A, B⟫⟫ ∈ ( Ins2k C ∩ Ins3k ◡kD))
7		vex 2862	. . . . . . . . . 10 ⊢ y ∈ V
8		opkelins2kg 4251	. . . . . . . . . 10 ⊢ ((y ∈ V ∧ ⟪A, B⟫ ∈ V) → (⟪y, ⟪A, B⟫⟫ ∈ Ins2k C ↔ ∃x∃z∃w(y = {{x}} ∧ ⟪A, B⟫ = ⟪z, w⟫ ∧ ⟪x, w⟫ ∈ C)))
9	7, 5, 8	mp2an 653	. . . . . . . . 9 ⊢ (⟪y, ⟪A, B⟫⟫ ∈ Ins2k C ↔ ∃x∃z∃w(y = {{x}} ∧ ⟪A, B⟫ = ⟪z, w⟫ ∧ ⟪x, w⟫ ∈ C))
10		3anass 938	. . . . . . . . . . . 12 ⊢ ((y = {{x}} ∧ ⟪A, B⟫ = ⟪z, w⟫ ∧ ⟪x, w⟫ ∈ C) ↔ (y = {{x}} ∧ (⟪A, B⟫ = ⟪z, w⟫ ∧ ⟪x, w⟫ ∈ C)))
11	10	2exbii 1583	. . . . . . . . . . 11 ⊢ (∃z∃w(y = {{x}} ∧ ⟪A, B⟫ = ⟪z, w⟫ ∧ ⟪x, w⟫ ∈ C) ↔ ∃z∃w(y = {{x}} ∧ (⟪A, B⟫ = ⟪z, w⟫ ∧ ⟪x, w⟫ ∈ C)))
12		19.42vv 1907	. . . . . . . . . . 11 ⊢ (∃z∃w(y = {{x}} ∧ (⟪A, B⟫ = ⟪z, w⟫ ∧ ⟪x, w⟫ ∈ C)) ↔ (y = {{x}} ∧ ∃z∃w(⟪A, B⟫ = ⟪z, w⟫ ∧ ⟪x, w⟫ ∈ C)))
13	11, 12	bitri 240	. . . . . . . . . 10 ⊢ (∃z∃w(y = {{x}} ∧ ⟪A, B⟫ = ⟪z, w⟫ ∧ ⟪x, w⟫ ∈ C) ↔ (y = {{x}} ∧ ∃z∃w(⟪A, B⟫ = ⟪z, w⟫ ∧ ⟪x, w⟫ ∈ C)))
14	13	exbii 1582	. . . . . . . . 9 ⊢ (∃x∃z∃w(y = {{x}} ∧ ⟪A, B⟫ = ⟪z, w⟫ ∧ ⟪x, w⟫ ∈ C) ↔ ∃x(y = {{x}} ∧ ∃z∃w(⟪A, B⟫ = ⟪z, w⟫ ∧ ⟪x, w⟫ ∈ C)))
15	9, 14	bitri 240	. . . . . . . 8 ⊢ (⟪y, ⟪A, B⟫⟫ ∈ Ins2k C ↔ ∃x(y = {{x}} ∧ ∃z∃w(⟪A, B⟫ = ⟪z, w⟫ ∧ ⟪x, w⟫ ∈ C)))
16	15	anbi1i 676	. . . . . . 7 ⊢ ((⟪y, ⟪A, B⟫⟫ ∈ Ins2k C ∧ ⟪y, ⟪A, B⟫⟫ ∈ Ins3k ◡kD) ↔ (∃x(y = {{x}} ∧ ∃z∃w(⟪A, B⟫ = ⟪z, w⟫ ∧ ⟪x, w⟫ ∈ C)) ∧ ⟪y, ⟪A, B⟫⟫ ∈ Ins3k ◡kD))
17		elin 3219	. . . . . . 7 ⊢ (⟪y, ⟪A, B⟫⟫ ∈ ( Ins2k C ∩ Ins3k ◡kD) ↔ (⟪y, ⟪A, B⟫⟫ ∈ Ins2k C ∧ ⟪y, ⟪A, B⟫⟫ ∈ Ins3k ◡kD))
18		19.41v 1901	. . . . . . 7 ⊢ (∃x((y = {{x}} ∧ ∃z∃w(⟪A, B⟫ = ⟪z, w⟫ ∧ ⟪x, w⟫ ∈ C)) ∧ ⟪y, ⟪A, B⟫⟫ ∈ Ins3k ◡kD) ↔ (∃x(y = {{x}} ∧ ∃z∃w(⟪A, B⟫ = ⟪z, w⟫ ∧ ⟪x, w⟫ ∈ C)) ∧ ⟪y, ⟪A, B⟫⟫ ∈ Ins3k ◡kD))
19	16, 17, 18	3bitr4i 268	. . . . . 6 ⊢ (⟪y, ⟪A, B⟫⟫ ∈ ( Ins2k C ∩ Ins3k ◡kD) ↔ ∃x((y = {{x}} ∧ ∃z∃w(⟪A, B⟫ = ⟪z, w⟫ ∧ ⟪x, w⟫ ∈ C)) ∧ ⟪y, ⟪A, B⟫⟫ ∈ Ins3k ◡kD))
20	19	exbii 1582	. . . . 5 ⊢ (∃y⟪y, ⟪A, B⟫⟫ ∈ ( Ins2k C ∩ Ins3k ◡kD) ↔ ∃y∃x((y = {{x}} ∧ ∃z∃w(⟪A, B⟫ = ⟪z, w⟫ ∧ ⟪x, w⟫ ∈ C)) ∧ ⟪y, ⟪A, B⟫⟫ ∈ Ins3k ◡kD))
21		excom 1741	. . . . 5 ⊢ (∃y∃x((y = {{x}} ∧ ∃z∃w(⟪A, B⟫ = ⟪z, w⟫ ∧ ⟪x, w⟫ ∈ C)) ∧ ⟪y, ⟪A, B⟫⟫ ∈ Ins3k ◡kD) ↔ ∃x∃y((y = {{x}} ∧ ∃z∃w(⟪A, B⟫ = ⟪z, w⟫ ∧ ⟪x, w⟫ ∈ C)) ∧ ⟪y, ⟪A, B⟫⟫ ∈ Ins3k ◡kD))
22		anass 630	. . . . . . . 8 ⊢ (((y = {{x}} ∧ ∃z∃w(⟪A, B⟫ = ⟪z, w⟫ ∧ ⟪x, w⟫ ∈ C)) ∧ ⟪y, ⟪A, B⟫⟫ ∈ Ins3k ◡kD) ↔ (y = {{x}} ∧ (∃z∃w(⟪A, B⟫ = ⟪z, w⟫ ∧ ⟪x, w⟫ ∈ C) ∧ ⟪y, ⟪A, B⟫⟫ ∈ Ins3k ◡kD)))
23	22	exbii 1582	. . . . . . 7 ⊢ (∃y((y = {{x}} ∧ ∃z∃w(⟪A, B⟫ = ⟪z, w⟫ ∧ ⟪x, w⟫ ∈ C)) ∧ ⟪y, ⟪A, B⟫⟫ ∈ Ins3k ◡kD) ↔ ∃y(y = {{x}} ∧ (∃z∃w(⟪A, B⟫ = ⟪z, w⟫ ∧ ⟪x, w⟫ ∈ C) ∧ ⟪y, ⟪A, B⟫⟫ ∈ Ins3k ◡kD)))
24		snex 4111	. . . . . . . 8 ⊢ {{x}} ∈ V
25		opkeq1 4059	. . . . . . . . . 10 ⊢ (y = {{x}} → ⟪y, ⟪A, B⟫⟫ = ⟪{{x}}, ⟪A, B⟫⟫)
26	25	eleq1d 2419	. . . . . . . . 9 ⊢ (y = {{x}} → (⟪y, ⟪A, B⟫⟫ ∈ Ins3k ◡kD ↔ ⟪{{x}}, ⟪A, B⟫⟫ ∈ Ins3k ◡kD))
27	26	anbi2d 684	. . . . . . . 8 ⊢ (y = {{x}} → ((∃z∃w(⟪A, B⟫ = ⟪z, w⟫ ∧ ⟪x, w⟫ ∈ C) ∧ ⟪y, ⟪A, B⟫⟫ ∈ Ins3k ◡kD) ↔ (∃z∃w(⟪A, B⟫ = ⟪z, w⟫ ∧ ⟪x, w⟫ ∈ C) ∧ ⟪{{x}}, ⟪A, B⟫⟫ ∈ Ins3k ◡kD)))
28	24, 27	ceqsexv 2894	. . . . . . 7 ⊢ (∃y(y = {{x}} ∧ (∃z∃w(⟪A, B⟫ = ⟪z, w⟫ ∧ ⟪x, w⟫ ∈ C) ∧ ⟪y, ⟪A, B⟫⟫ ∈ Ins3k ◡kD)) ↔ (∃z∃w(⟪A, B⟫ = ⟪z, w⟫ ∧ ⟪x, w⟫ ∈ C) ∧ ⟪{{x}}, ⟪A, B⟫⟫ ∈ Ins3k ◡kD))
29	23, 28	bitri 240	. . . . . 6 ⊢ (∃y((y = {{x}} ∧ ∃z∃w(⟪A, B⟫ = ⟪z, w⟫ ∧ ⟪x, w⟫ ∈ C)) ∧ ⟪y, ⟪A, B⟫⟫ ∈ Ins3k ◡kD) ↔ (∃z∃w(⟪A, B⟫ = ⟪z, w⟫ ∧ ⟪x, w⟫ ∈ C) ∧ ⟪{{x}}, ⟪A, B⟫⟫ ∈ Ins3k ◡kD))
30	29	exbii 1582	. . . . 5 ⊢ (∃x∃y((y = {{x}} ∧ ∃z∃w(⟪A, B⟫ = ⟪z, w⟫ ∧ ⟪x, w⟫ ∈ C)) ∧ ⟪y, ⟪A, B⟫⟫ ∈ Ins3k ◡kD) ↔ ∃x(∃z∃w(⟪A, B⟫ = ⟪z, w⟫ ∧ ⟪x, w⟫ ∈ C) ∧ ⟪{{x}}, ⟪A, B⟫⟫ ∈ Ins3k ◡kD))
31	20, 21, 30	3bitri 262	. . . 4 ⊢ (∃y⟪y, ⟪A, B⟫⟫ ∈ ( Ins2k C ∩ Ins3k ◡kD) ↔ ∃x(∃z∃w(⟪A, B⟫ = ⟪z, w⟫ ∧ ⟪x, w⟫ ∈ C) ∧ ⟪{{x}}, ⟪A, B⟫⟫ ∈ Ins3k ◡kD))
32	4, 6, 31	3bitri 262	. . 3 ⊢ (⟪A, B⟫ ∈ (C ∘k D) ↔ ∃x(∃z∃w(⟪A, B⟫ = ⟪z, w⟫ ∧ ⟪x, w⟫ ∈ C) ∧ ⟪{{x}}, ⟪A, B⟫⟫ ∈ Ins3k ◡kD))
33		ancom 437	. . . . 5 ⊢ ((∃z∃w(⟪A, B⟫ = ⟪z, w⟫ ∧ ⟪x, w⟫ ∈ C) ∧ ⟪{{x}}, ⟪A, B⟫⟫ ∈ Ins3k ◡kD) ↔ (⟪{{x}}, ⟪A, B⟫⟫ ∈ Ins3k ◡kD ∧ ∃z∃w(⟪A, B⟫ = ⟪z, w⟫ ∧ ⟪x, w⟫ ∈ C)))
34		vex 2862	. . . . . . . 8 ⊢ x ∈ V
35		otkelins3kg 4254	. . . . . . . 8 ⊢ ((x ∈ V ∧ A ∈ V ∧ B ∈ V) → (⟪{{x}}, ⟪A, B⟫⟫ ∈ Ins3k ◡kD ↔ ⟪x, A⟫ ∈ ◡kD))
36	34, 35	mp3an1 1264	. . . . . . 7 ⊢ ((A ∈ V ∧ B ∈ V) → (⟪{{x}}, ⟪A, B⟫⟫ ∈ Ins3k ◡kD ↔ ⟪x, A⟫ ∈ ◡kD))
37		opkelcnvkg 4249	. . . . . . . . 9 ⊢ ((x ∈ V ∧ A ∈ V) → (⟪x, A⟫ ∈ ◡kD ↔ ⟪A, x⟫ ∈ D))
38	34, 37	mpan 651	. . . . . . . 8 ⊢ (A ∈ V → (⟪x, A⟫ ∈ ◡kD ↔ ⟪A, x⟫ ∈ D))
39	38	adantr 451	. . . . . . 7 ⊢ ((A ∈ V ∧ B ∈ V) → (⟪x, A⟫ ∈ ◡kD ↔ ⟪A, x⟫ ∈ D))
40	36, 39	bitrd 244	. . . . . 6 ⊢ ((A ∈ V ∧ B ∈ V) → (⟪{{x}}, ⟪A, B⟫⟫ ∈ Ins3k ◡kD ↔ ⟪A, x⟫ ∈ D))
41		eqcom 2355	. . . . . . . . . 10 ⊢ (⟪A, B⟫ = ⟪z, w⟫ ↔ ⟪z, w⟫ = ⟪A, B⟫)
42	41	anbi1i 676	. . . . . . . . 9 ⊢ ((⟪A, B⟫ = ⟪z, w⟫ ∧ ⟪x, w⟫ ∈ C) ↔ (⟪z, w⟫ = ⟪A, B⟫ ∧ ⟪x, w⟫ ∈ C))
43	42	2exbii 1583	. . . . . . . 8 ⊢ (∃z∃w(⟪A, B⟫ = ⟪z, w⟫ ∧ ⟪x, w⟫ ∈ C) ↔ ∃z∃w(⟪z, w⟫ = ⟪A, B⟫ ∧ ⟪x, w⟫ ∈ C))
44		vex 2862	. . . . . . . . . . . . . 14 ⊢ z ∈ V
45		vex 2862	. . . . . . . . . . . . . 14 ⊢ w ∈ V
46		opkthg 4131	. . . . . . . . . . . . . 14 ⊢ ((z ∈ V ∧ w ∈ V ∧ B ∈ V) → (⟪z, w⟫ = ⟪A, B⟫ ↔ (z = A ∧ w = B)))
47	44, 45, 46	mp3an12 1267	. . . . . . . . . . . . 13 ⊢ (B ∈ V → (⟪z, w⟫ = ⟪A, B⟫ ↔ (z = A ∧ w = B)))
48	47	anbi1d 685	. . . . . . . . . . . 12 ⊢ (B ∈ V → ((⟪z, w⟫ = ⟪A, B⟫ ∧ ⟪x, w⟫ ∈ C) ↔ ((z = A ∧ w = B) ∧ ⟪x, w⟫ ∈ C)))
49		anass 630	. . . . . . . . . . . 12 ⊢ (((z = A ∧ w = B) ∧ ⟪x, w⟫ ∈ C) ↔ (z = A ∧ (w = B ∧ ⟪x, w⟫ ∈ C)))
50	48, 49	syl6bb 252	. . . . . . . . . . 11 ⊢ (B ∈ V → ((⟪z, w⟫ = ⟪A, B⟫ ∧ ⟪x, w⟫ ∈ C) ↔ (z = A ∧ (w = B ∧ ⟪x, w⟫ ∈ C))))
51	50	2exbidv 1628	. . . . . . . . . 10 ⊢ (B ∈ V → (∃z∃w(⟪z, w⟫ = ⟪A, B⟫ ∧ ⟪x, w⟫ ∈ C) ↔ ∃z∃w(z = A ∧ (w = B ∧ ⟪x, w⟫ ∈ C))))
52	51	adantl 452	. . . . . . . . 9 ⊢ ((A ∈ V ∧ B ∈ V) → (∃z∃w(⟪z, w⟫ = ⟪A, B⟫ ∧ ⟪x, w⟫ ∈ C) ↔ ∃z∃w(z = A ∧ (w = B ∧ ⟪x, w⟫ ∈ C))))
53		eeanv 1913	. . . . . . . . 9 ⊢ (∃z∃w(z = A ∧ (w = B ∧ ⟪x, w⟫ ∈ C)) ↔ (∃z z = A ∧ ∃w(w = B ∧ ⟪x, w⟫ ∈ C)))
54	52, 53	syl6bb 252	. . . . . . . 8 ⊢ ((A ∈ V ∧ B ∈ V) → (∃z∃w(⟪z, w⟫ = ⟪A, B⟫ ∧ ⟪x, w⟫ ∈ C) ↔ (∃z z = A ∧ ∃w(w = B ∧ ⟪x, w⟫ ∈ C))))
55	43, 54	syl5bb 248	. . . . . . 7 ⊢ ((A ∈ V ∧ B ∈ V) → (∃z∃w(⟪A, B⟫ = ⟪z, w⟫ ∧ ⟪x, w⟫ ∈ C) ↔ (∃z z = A ∧ ∃w(w = B ∧ ⟪x, w⟫ ∈ C))))
56		elisset 2869	. . . . . . . . . 10 ⊢ (A ∈ V → ∃z z = A)
57	56	biantrurd 494	. . . . . . . . 9 ⊢ (A ∈ V → (∃w(w = B ∧ ⟪x, w⟫ ∈ C) ↔ (∃z z = A ∧ ∃w(w = B ∧ ⟪x, w⟫ ∈ C))))
58	57	bicomd 192	. . . . . . . 8 ⊢ (A ∈ V → ((∃z z = A ∧ ∃w(w = B ∧ ⟪x, w⟫ ∈ C)) ↔ ∃w(w = B ∧ ⟪x, w⟫ ∈ C)))
59		opkeq2 4060	. . . . . . . . . 10 ⊢ (w = B → ⟪x, w⟫ = ⟪x, B⟫)
60	59	eleq1d 2419	. . . . . . . . 9 ⊢ (w = B → (⟪x, w⟫ ∈ C ↔ ⟪x, B⟫ ∈ C))
61	60	ceqsexgv 2971	. . . . . . . 8 ⊢ (B ∈ V → (∃w(w = B ∧ ⟪x, w⟫ ∈ C) ↔ ⟪x, B⟫ ∈ C))
62	58, 61	sylan9bb 680	. . . . . . 7 ⊢ ((A ∈ V ∧ B ∈ V) → ((∃z z = A ∧ ∃w(w = B ∧ ⟪x, w⟫ ∈ C)) ↔ ⟪x, B⟫ ∈ C))
63	55, 62	bitrd 244	. . . . . 6 ⊢ ((A ∈ V ∧ B ∈ V) → (∃z∃w(⟪A, B⟫ = ⟪z, w⟫ ∧ ⟪x, w⟫ ∈ C) ↔ ⟪x, B⟫ ∈ C))
64	40, 63	anbi12d 691	. . . . 5 ⊢ ((A ∈ V ∧ B ∈ V) → ((⟪{{x}}, ⟪A, B⟫⟫ ∈ Ins3k ◡kD ∧ ∃z∃w(⟪A, B⟫ = ⟪z, w⟫ ∧ ⟪x, w⟫ ∈ C)) ↔ (⟪A, x⟫ ∈ D ∧ ⟪x, B⟫ ∈ C)))
65	33, 64	syl5bb 248	. . . 4 ⊢ ((A ∈ V ∧ B ∈ V) → ((∃z∃w(⟪A, B⟫ = ⟪z, w⟫ ∧ ⟪x, w⟫ ∈ C) ∧ ⟪{{x}}, ⟪A, B⟫⟫ ∈ Ins3k ◡kD) ↔ (⟪A, x⟫ ∈ D ∧ ⟪x, B⟫ ∈ C)))
66	65	exbidv 1626	. . 3 ⊢ ((A ∈ V ∧ B ∈ V) → (∃x(∃z∃w(⟪A, B⟫ = ⟪z, w⟫ ∧ ⟪x, w⟫ ∈ C) ∧ ⟪{{x}}, ⟪A, B⟫⟫ ∈ Ins3k ◡kD) ↔ ∃x(⟪A, x⟫ ∈ D ∧ ⟪x, B⟫ ∈ C)))
67	32, 66	syl5bb 248	. 2 ⊢ ((A ∈ V ∧ B ∈ V) → (⟪A, B⟫ ∈ (C ∘k D) ↔ ∃x(⟪A, x⟫ ∈ D ∧ ⟪x, B⟫ ∈ C)))
68	1, 2, 67	syl2an 463	1 ⊢ ((A ∈ V ∧ B ∈ W) → (⟪A, B⟫ ∈ (C ∘k D) ↔ ∃x(⟪A, x⟫ ∈ D ∧ ⟪x, B⟫ ∈ C)))

Syntax hints:   → wi 4   ↔ wb 176   ∧ wa 358   ∧ w3a 934  ∃wex 1541   = wceq 1642   ∈ wcel 1710  Vcvv 2859   ∩ cin 3208  {csn 3737  ⟪copk 4057  ^◡_kccnvk 4175   Ins2_k cins2k 4176   Ins3_k cins3k 4177   “_k cimak 4179   ∘_k ccomk 4180

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 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 4078  ax-sn 4087

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 2478  df-ne 2518  df-rex 2620  df-v 2861  df-nin 3211  df-compl 3212  df-in 3213  df-un 3214  df-dif 3215  df-ss 3259  df-nul 3551  df-sn 3741  df-pr 3742  df-opk 4058  df-cnvk 4186  df-ins2k 4187  df-ins3k 4188  df-imak 4189  df-cok 4190

This theorem is referenced by:  opkelcok  4262  opkelimagekg  4271