Theorem dfimak2 4299

Description: Alternate definition of Kuratowski image. This is the first of a series of definitions throughout the file designed to prove existence of various operations. (Contributed by SF, 14-Jan-2015.)

Assertion

Ref	Expression
dfimak2	|- (A"kB) = ∼ P6 ( ∼ (1c X.k _V) u. SIk ∼ (A i^i (B X.k _V)))

Proof of Theorem dfimak2

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

Step	Hyp	Ref	Expression
1		df-rex 2621	. . . 4 |- (E.y e. B <<y, x>> e. A <-> E.y(y e. B /\ <<y, x>> e. A))
2		exancom 1586	. . . 4 |- (E.y(y e. B /\ <<y, x>> e. A) <-> E.y(<<y, x>> e. A /\ y e. B))
3		vex 2863	. . . . . . 7 |- x e. _V
4		elp6 4264	. . . . . . 7 |- (x e. _V -> (x e. P6 ( ∼ (1c X.k _V) u. SIk ∼ (A i^i (B X.k _V))) <-> A.z<<z, {x}>> e. ( ∼ (1c X.k _V) u. SIk ∼ (A i^i (B X.k _V)))))
5	3, 4	ax-mp 5	. . . . . 6 |- (x e. P6 ( ∼ (1c X.k _V) u. SIk ∼ (A i^i (B X.k _V))) <-> A.z<<z, {x}>> e. ( ∼ (1c X.k _V) u. SIk ∼ (A i^i (B X.k _V))))
6		elun 3221	. . . . . . . 8 |- (<<z, {x}>> e. ( ∼ (1c X.k _V) u. SIk ∼ (A i^i (B X.k _V))) <-> (<<z, {x}>> e. ∼ (1c X.k _V) \/ <<z, {x}>> e. SIk ∼ (A i^i (B X.k _V))))
7		opkex 4114	. . . . . . . . . . 11 |- <<z, {x}>> e. _V
8	7	elcompl 3226	. . . . . . . . . 10 |- (<<z, {x}>> e. ∼ (1c X.k _V) <-> -. <<z, {x}>> e. (1c X.k _V))
9		snex 4112	. . . . . . . . . . 11 |- {x} e. _V
10		vex 2863	. . . . . . . . . . . 12 |- z e. _V
11	10, 9	opkelxpk 4249	. . . . . . . . . . 11 |- (<<z, {x}>> e. (1c X.k _V) <-> (z e. 1c /\ {x} e. _V))
12	9, 11	mpbiran2 885	. . . . . . . . . 10 |- (<<z, {x}>> e. (1c X.k _V) <-> z e. 1c)
13	8, 12	xchbinx 301	. . . . . . . . 9 |- (<<z, {x}>> e. ∼ (1c X.k _V) <-> -. z e. 1c)
14	13	orbi1i 506	. . . . . . . 8 |- ((<<z, {x}>> e. ∼ (1c X.k _V) \/ <<z, {x}>> e. SIk ∼ (A i^i (B X.k _V))) <-> (-. z e. 1c \/ <<z, {x}>> e. SIk ∼ (A i^i (B X.k _V))))
15		iman 413	. . . . . . . . 9 |- ((z e. 1c -> <<z, {x}>> e. SIk ∼ (A i^i (B X.k _V))) <-> -. (z e. 1c /\ -. <<z, {x}>> e. SIk ∼ (A i^i (B X.k _V))))
16		imor 401	. . . . . . . . 9 |- ((z e. 1c -> <<z, {x}>> e. SIk ∼ (A i^i (B X.k _V))) <-> (-. z e. 1c \/ <<z, {x}>> e. SIk ∼ (A i^i (B X.k _V))))
17		el1c 4140	. . . . . . . . . . . 12 |- (z e. 1c <-> E.y z = {y})
18	17	anbi1i 676	. . . . . . . . . . 11 |- ((z e. 1c /\ -. <<z, {x}>> e. SIk ∼ (A i^i (B X.k _V))) <-> (E.y z = {y} /\ -. <<z, {x}>> e. SIk ∼ (A i^i (B X.k _V))))
19		19.41v 1901	. . . . . . . . . . 11 |- (E.y(z = {y} /\ -. <<z, {x}>> e. SIk ∼ (A i^i (B X.k _V))) <-> (E.y z = {y} /\ -. <<z, {x}>> e. SIk ∼ (A i^i (B X.k _V))))
20	18, 19	bitr4i 243	. . . . . . . . . 10 |- ((z e. 1c /\ -. <<z, {x}>> e. SIk ∼ (A i^i (B X.k _V))) <-> E.y(z = {y} /\ -. <<z, {x}>> e. SIk ∼ (A i^i (B X.k _V))))
21	20	notbii 287	. . . . . . . . 9 |- (-. (z e. 1c /\ -. <<z, {x}>> e. SIk ∼ (A i^i (B X.k _V))) <-> -. E.y(z = {y} /\ -. <<z, {x}>> e. SIk ∼ (A i^i (B X.k _V))))
22	15, 16, 21	3bitr3i 266	. . . . . . . 8 |- ((-. z e. 1c \/ <<z, {x}>> e. SIk ∼ (A i^i (B X.k _V))) <-> -. E.y(z = {y} /\ -. <<z, {x}>> e. SIk ∼ (A i^i (B X.k _V))))
23	6, 14, 22	3bitri 262	. . . . . . 7 |- (<<z, {x}>> e. ( ∼ (1c X.k _V) u. SIk ∼ (A i^i (B X.k _V))) <-> -. E.y(z = {y} /\ -. <<z, {x}>> e. SIk ∼ (A i^i (B X.k _V))))
24	23	albii 1566	. . . . . 6 |- (A.z<<z, {x}>> e. ( ∼ (1c X.k _V) u. SIk ∼ (A i^i (B X.k _V))) <-> A.z -. E.y(z = {y} /\ -. <<z, {x}>> e. SIk ∼ (A i^i (B X.k _V))))
25		alnex 1543	. . . . . . 7 |- (A.z -. E.y(z = {y} /\ -. <<z, {x}>> e. SIk ∼ (A i^i (B X.k _V))) <-> -. E.zE.y(z = {y} /\ -. <<z, {x}>> e. SIk ∼ (A i^i (B X.k _V))))
26		excom 1741	. . . . . . . 8 |- (E.zE.y(z = {y} /\ -. <<z, {x}>> e. SIk ∼ (A i^i (B X.k _V))) <-> E.yE.z(z = {y} /\ -. <<z, {x}>> e. SIk ∼ (A i^i (B X.k _V))))
27		snex 4112	. . . . . . . . . . 11 |- {y} e. _V
28		opkeq1 4060	. . . . . . . . . . . . . 14 |- (z = {y} -> <<z, {x}>> = <<{y}, {x}>>)
29	28	eleq1d 2419	. . . . . . . . . . . . 13 |- (z = {y} -> (<<z, {x}>> e. SIk ∼ (A i^i (B X.k _V)) <-> <<{y}, {x}>> e. SIk ∼ (A i^i (B X.k _V))))
30		vex 2863	. . . . . . . . . . . . . . 15 |- y e. _V
31	30, 3	opksnelsik 4266	. . . . . . . . . . . . . 14 |- (<<{y}, {x}>> e. SIk ∼ (A i^i (B X.k _V)) <-> <<y, x>> e. ∼ (A i^i (B X.k _V)))
32		opkex 4114	. . . . . . . . . . . . . . 15 |- <<y, x>> e. _V
33	32	elcompl 3226	. . . . . . . . . . . . . 14 |- (<<y, x>> e. ∼ (A i^i (B X.k _V)) <-> -. <<y, x>> e. (A i^i (B X.k _V)))
34	31, 33	bitri 240	. . . . . . . . . . . . 13 |- (<<{y}, {x}>> e. SIk ∼ (A i^i (B X.k _V)) <-> -. <<y, x>> e. (A i^i (B X.k _V)))
35	29, 34	syl6bb 252	. . . . . . . . . . . 12 |- (z = {y} -> (<<z, {x}>> e. SIk ∼ (A i^i (B X.k _V)) <-> -. <<y, x>> e. (A i^i (B X.k _V))))
36	35	notbid 285	. . . . . . . . . . 11 |- (z = {y} -> (-. <<z, {x}>> e. SIk ∼ (A i^i (B X.k _V)) <-> -. -. <<y, x>> e. (A i^i (B X.k _V))))
37	27, 36	ceqsexv 2895	. . . . . . . . . 10 |- (E.z(z = {y} /\ -. <<z, {x}>> e. SIk ∼ (A i^i (B X.k _V))) <-> -. -. <<y, x>> e. (A i^i (B X.k _V)))
38		elin 3220	. . . . . . . . . . 11 |- (<<y, x>> e. (A i^i (B X.k _V)) <-> (<<y, x>> e. A /\ <<y, x>> e. (B X.k _V)))
39		notnot 282	. . . . . . . . . . 11 |- (<<y, x>> e. (A i^i (B X.k _V)) <-> -. -. <<y, x>> e. (A i^i (B X.k _V)))
40	30, 3	opkelxpk 4249	. . . . . . . . . . . . 13 |- (<<y, x>> e. (B X.k _V) <-> (y e. B /\ x e. _V))
41	3, 40	mpbiran2 885	. . . . . . . . . . . 12 |- (<<y, x>> e. (B X.k _V) <-> y e. B)
42	41	anbi2i 675	. . . . . . . . . . 11 |- ((<<y, x>> e. A /\ <<y, x>> e. (B X.k _V)) <-> (<<y, x>> e. A /\ y e. B))
43	38, 39, 42	3bitr3i 266	. . . . . . . . . 10 |- (-. -. <<y, x>> e. (A i^i (B X.k _V)) <-> (<<y, x>> e. A /\ y e. B))
44	37, 43	bitri 240	. . . . . . . . 9 |- (E.z(z = {y} /\ -. <<z, {x}>> e. SIk ∼ (A i^i (B X.k _V))) <-> (<<y, x>> e. A /\ y e. B))
45	44	exbii 1582	. . . . . . . 8 |- (E.yE.z(z = {y} /\ -. <<z, {x}>> e. SIk ∼ (A i^i (B X.k _V))) <-> E.y(<<y, x>> e. A /\ y e. B))
46	26, 45	bitri 240	. . . . . . 7 |- (E.zE.y(z = {y} /\ -. <<z, {x}>> e. SIk ∼ (A i^i (B X.k _V))) <-> E.y(<<y, x>> e. A /\ y e. B))
47	25, 46	xchbinx 301	. . . . . 6 |- (A.z -. E.y(z = {y} /\ -. <<z, {x}>> e. SIk ∼ (A i^i (B X.k _V))) <-> -. E.y(<<y, x>> e. A /\ y e. B))
48	5, 24, 47	3bitri 262	. . . . 5 |- (x e. P6 ( ∼ (1c X.k _V) u. SIk ∼ (A i^i (B X.k _V))) <-> -. E.y(<<y, x>> e. A /\ y e. B))
49	48	con2bii 322	. . . 4 |- (E.y(<<y, x>> e. A /\ y e. B) <-> -. x e. P6 ( ∼ (1c X.k _V) u. SIk ∼ (A i^i (B X.k _V))))
50	1, 2, 49	3bitri 262	. . 3 |- (E.y e. B <<y, x>> e. A <-> -. x e. P6 ( ∼ (1c X.k _V) u. SIk ∼ (A i^i (B X.k _V))))
51	3	elimak 4260	. . 3 |- (x e. (A"kB) <-> E.y e. B <<y, x>> e. A)
52	3	elcompl 3226	. . 3 |- (x e. ∼ P6 ( ∼ (1c X.k _V) u. SIk ∼ (A i^i (B X.k _V))) <-> -. x e. P6 ( ∼ (1c X.k _V) u. SIk ∼ (A i^i (B X.k _V))))
53	50, 51, 52	3bitr4i 268	. 2 |- (x e. (A"kB) <-> x e. ∼ P6 ( ∼ (1c X.k _V) u. SIk ∼ (A i^i (B X.k _V))))
54	53	eqriv 2350	1 |- (A"kB) = ∼ P6 ( ∼ (1c X.k _V) u. SIk ∼ (A i^i (B X.k _V)))

Syntax hints:  -. wn 3   -> wi 4   <-> wb 176   \/ wo 357   /\ wa 358  A.wal 1540  E.wex 1541   = wceq 1642   e. wcel 1710  E.wrex 2616  _Vcvv 2860   ∼ ccompl 3206   u. cun 3208   i^i cin 3209  {csn 3738  <<copk 4058  1_cc1c 4135   X._k cxpk 4175   P6 cp6 4179  "_kcimak 4180   SI_k csik 4182

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-ss 3260  df-nul 3552  df-sn 3742  df-pr 3743  df-opk 4059  df-1c 4137  df-xpk 4186  df-imak 4190  df-p6 4192  df-sik 4193

This theorem is referenced by:  imakexg  4300