Theorem dfimak2 4298

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 2620	. . . 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 2862	. . . . . . 7 |- x e. _V
4		elp6 4263	. . . . . . 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 3220	. . . . . . . 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 4113	. . . . . . . . . . 11 |- <<z, {x}>> e. _V
8	7	elcompl 3225	. . . . . . . . . 10 |- (<<z, {x}>> e. ∼ (1c X.k _V) <-> -. <<z, {x}>> e. (1c X.k _V))
9		snex 4111	. . . . . . . . . . 11 |- {x} e. _V
10		vex 2862	. . . . . . . . . . . 12 |- z e. _V
11	10, 9	opkelxpk 4248	. . . . . . . . . . 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 4139	. . . . . . . . . . . 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 4111	. . . . . . . . . . 11 |- {y} e. _V
28		opkeq1 4059	. . . . . . . . . . . . . 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 2862	. . . . . . . . . . . . . . 15 |- y e. _V
31	30, 3	opksnelsik 4265	. . . . . . . . . . . . . 14 |- (<<{y}, {x}>> e. SIk ∼ (A i^i (B X.k _V)) <-> <<y, x>> e. ∼ (A i^i (B X.k _V)))
32		opkex 4113	. . . . . . . . . . . . . . 15 |- <<y, x>> e. _V
33	32	elcompl 3225	. . . . . . . . . . . . . 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 2894	. . . . . . . . . 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 3219	. . . . . . . . . . 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 4248	. . . . . . . . . . . . 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 4259	. . 3 |- (x e. (A"kB) <-> E.y e. B <<y, x>> e. A)
52	3	elcompl 3225	. . 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 2615  _Vcvv 2859   ∼ ccompl 3205   u. cun 3207   i^i cin 3208  {csn 3737  <<copk 4057  1_cc1c 4134   X._k cxpk 4174   P6 cp6 4178  "_kcimak 4179   SI_k csik 4181

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 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-ral 2619  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-1c 4136  df-xpk 4185  df-imak 4189  df-p6 4191  df-sik 4192

This theorem is referenced by:  imakexg  4299