dfimak2 - New Foundations Explorer

	New Foundations Explorer		< Previous Next > Nearby theorems
Mirrors > Home > NFE Home > Th. List > dfimak2		GIF version

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 “_k B) = ∼ P6 ( ∼ (1_c ×_k V) ∪ SI_k ∼ (A ∩ (B ×_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 ⊢ (∃y ∈ B ⟪y, x⟫ ∈ A ↔ ∃y(y ∈ B ∧ ⟪y, x⟫ ∈ A))
2		exancom 1586	. . . 4 ⊢ (∃y(y ∈ B ∧ ⟪y, x⟫ ∈ A) ↔ ∃y(⟪y, x⟫ ∈ A ∧ y ∈ B))
3		vex 2863	. . . . . . 7 ⊢ x ∈ V
4		elp6 4264	. . . . . . 7 ⊢ (x ∈ V → (x ∈ P6 ( ∼ (1_c ×_k V) ∪ SI_k ∼ (A ∩ (B ×_k V))) ↔ ∀z⟪z, {x}⟫ ∈ ( ∼ (1_c ×_k V) ∪ SI_k ∼ (A ∩ (B ×_k V)))))
5	3, 4	ax-mp 5	. . . . . 6 ⊢ (x ∈ P6 ( ∼ (1_c ×_k V) ∪ SI_k ∼ (A ∩ (B ×_k V))) ↔ ∀z⟪z, {x}⟫ ∈ ( ∼ (1_c ×_k V) ∪ SI_k ∼ (A ∩ (B ×_k V))))
6		elun 3221	. . . . . . . 8 ⊢ (⟪z, {x}⟫ ∈ ( ∼ (1_c ×_k V) ∪ SI_k ∼ (A ∩ (B ×_k V))) ↔ (⟪z, {x}⟫ ∈ ∼ (1_c ×_k V) ∨ ⟪z, {x}⟫ ∈ SI_k ∼ (A ∩ (B ×_k V))))
7		opkex 4114	. . . . . . . . . . 11 ⊢ ⟪z, {x}⟫ ∈ V
8	7	elcompl 3226	. . . . . . . . . 10 ⊢ (⟪z, {x}⟫ ∈ ∼ (1_c ×_k V) ↔ ¬ ⟪z, {x}⟫ ∈ (1_c ×_k V))
9		snex 4112	. . . . . . . . . . 11 ⊢ {x} ∈ V
10		vex 2863	. . . . . . . . . . . 12 ⊢ z ∈ V
11	10, 9	opkelxpk 4249	. . . . . . . . . . 11 ⊢ (⟪z, {x}⟫ ∈ (1_c ×_k V) ↔ (z ∈ 1_c ∧ {x} ∈ V))
12	9, 11	mpbiran2 885	. . . . . . . . . 10 ⊢ (⟪z, {x}⟫ ∈ (1_c ×_k V) ↔ z ∈ 1_c)
13	8, 12	xchbinx 301	. . . . . . . . 9 ⊢ (⟪z, {x}⟫ ∈ ∼ (1_c ×_k V) ↔ ¬ z ∈ 1_c)
14	13	orbi1i 506	. . . . . . . 8 ⊢ ((⟪z, {x}⟫ ∈ ∼ (1_c ×_k V) ∨ ⟪z, {x}⟫ ∈ SI_k ∼ (A ∩ (B ×_k V))) ↔ (¬ z ∈ 1_c ∨ ⟪z, {x}⟫ ∈ SI_k ∼ (A ∩ (B ×_k V))))
15		iman 413	. . . . . . . . 9 ⊢ ((z ∈ 1_c → ⟪z, {x}⟫ ∈ SI_k ∼ (A ∩ (B ×_k V))) ↔ ¬ (z ∈ 1_c ∧ ¬ ⟪z, {x}⟫ ∈ SI_k ∼ (A ∩ (B ×_k V))))
16		imor 401	. . . . . . . . 9 ⊢ ((z ∈ 1_c → ⟪z, {x}⟫ ∈ SI_k ∼ (A ∩ (B ×_k V))) ↔ (¬ z ∈ 1_c ∨ ⟪z, {x}⟫ ∈ SI_k ∼ (A ∩ (B ×_k V))))
17		el1c 4140	. . . . . . . . . . . 12 ⊢ (z ∈ 1_c ↔ ∃y z = {y})
18	17	anbi1i 676	. . . . . . . . . . 11 ⊢ ((z ∈ 1_c ∧ ¬ ⟪z, {x}⟫ ∈ SI_k ∼ (A ∩ (B ×_k V))) ↔ (∃y z = {y} ∧ ¬ ⟪z, {x}⟫ ∈ SI_k ∼ (A ∩ (B ×_k V))))
19		19.41v 1901	. . . . . . . . . . 11 ⊢ (∃y(z = {y} ∧ ¬ ⟪z, {x}⟫ ∈ SI_k ∼ (A ∩ (B ×_k V))) ↔ (∃y z = {y} ∧ ¬ ⟪z, {x}⟫ ∈ SI_k ∼ (A ∩ (B ×_k V))))
20	18, 19	bitr4i 243	. . . . . . . . . 10 ⊢ ((z ∈ 1_c ∧ ¬ ⟪z, {x}⟫ ∈ SI_k ∼ (A ∩ (B ×_k V))) ↔ ∃y(z = {y} ∧ ¬ ⟪z, {x}⟫ ∈ SI_k ∼ (A ∩ (B ×_k V))))
21	20	notbii 287	. . . . . . . . 9 ⊢ (¬ (z ∈ 1_c ∧ ¬ ⟪z, {x}⟫ ∈ SI_k ∼ (A ∩ (B ×_k V))) ↔ ¬ ∃y(z = {y} ∧ ¬ ⟪z, {x}⟫ ∈ SI_k ∼ (A ∩ (B ×_k V))))
22	15, 16, 21	3bitr3i 266	. . . . . . . 8 ⊢ ((¬ z ∈ 1_c ∨ ⟪z, {x}⟫ ∈ SI_k ∼ (A ∩ (B ×_k V))) ↔ ¬ ∃y(z = {y} ∧ ¬ ⟪z, {x}⟫ ∈ SI_k ∼ (A ∩ (B ×_k V))))
23	6, 14, 22	3bitri 262	. . . . . . 7 ⊢ (⟪z, {x}⟫ ∈ ( ∼ (1_c ×_k V) ∪ SI_k ∼ (A ∩ (B ×_k V))) ↔ ¬ ∃y(z = {y} ∧ ¬ ⟪z, {x}⟫ ∈ SI_k ∼ (A ∩ (B ×_k V))))
24	23	albii 1566	. . . . . 6 ⊢ (∀z⟪z, {x}⟫ ∈ ( ∼ (1_c ×_k V) ∪ SI_k ∼ (A ∩ (B ×_k V))) ↔ ∀z ¬ ∃y(z = {y} ∧ ¬ ⟪z, {x}⟫ ∈ SI_k ∼ (A ∩ (B ×_k V))))
25		alnex 1543	. . . . . . 7 ⊢ (∀z ¬ ∃y(z = {y} ∧ ¬ ⟪z, {x}⟫ ∈ SI_k ∼ (A ∩ (B ×_k V))) ↔ ¬ ∃z∃y(z = {y} ∧ ¬ ⟪z, {x}⟫ ∈ SI_k ∼ (A ∩ (B ×_k V))))
26		excom 1741	. . . . . . . 8 ⊢ (∃z∃y(z = {y} ∧ ¬ ⟪z, {x}⟫ ∈ SI_k ∼ (A ∩ (B ×_k V))) ↔ ∃y∃z(z = {y} ∧ ¬ ⟪z, {x}⟫ ∈ SI_k ∼ (A ∩ (B ×_k V))))
27		snex 4112	. . . . . . . . . . 11 ⊢ {y} ∈ V
28		opkeq1 4060	. . . . . . . . . . . . . 14 ⊢ (z = {y} → ⟪z, {x}⟫ = ⟪{y}, {x}⟫)
29	28	eleq1d 2419	. . . . . . . . . . . . 13 ⊢ (z = {y} → (⟪z, {x}⟫ ∈ SI_k ∼ (A ∩ (B ×_k V)) ↔ ⟪{y}, {x}⟫ ∈ SI_k ∼ (A ∩ (B ×_k V))))
30		vex 2863	. . . . . . . . . . . . . . 15 ⊢ y ∈ V
31	30, 3	opksnelsik 4266	. . . . . . . . . . . . . 14 ⊢ (⟪{y}, {x}⟫ ∈ SI_k ∼ (A ∩ (B ×_k V)) ↔ ⟪y, x⟫ ∈ ∼ (A ∩ (B ×_k V)))
32		opkex 4114	. . . . . . . . . . . . . . 15 ⊢ ⟪y, x⟫ ∈ V
33	32	elcompl 3226	. . . . . . . . . . . . . 14 ⊢ (⟪y, x⟫ ∈ ∼ (A ∩ (B ×_k V)) ↔ ¬ ⟪y, x⟫ ∈ (A ∩ (B ×_k V)))
34	31, 33	bitri 240	. . . . . . . . . . . . 13 ⊢ (⟪{y}, {x}⟫ ∈ SI_k ∼ (A ∩ (B ×_k V)) ↔ ¬ ⟪y, x⟫ ∈ (A ∩ (B ×_k V)))
35	29, 34	syl6bb 252	. . . . . . . . . . . 12 ⊢ (z = {y} → (⟪z, {x}⟫ ∈ SI_k ∼ (A ∩ (B ×_k V)) ↔ ¬ ⟪y, x⟫ ∈ (A ∩ (B ×_k V))))
36	35	notbid 285	. . . . . . . . . . 11 ⊢ (z = {y} → (¬ ⟪z, {x}⟫ ∈ SI_k ∼ (A ∩ (B ×_k V)) ↔ ¬ ¬ ⟪y, x⟫ ∈ (A ∩ (B ×_k V))))
37	27, 36	ceqsexv 2895	. . . . . . . . . 10 ⊢ (∃z(z = {y} ∧ ¬ ⟪z, {x}⟫ ∈ SI_k ∼ (A ∩ (B ×_k V))) ↔ ¬ ¬ ⟪y, x⟫ ∈ (A ∩ (B ×_k V)))
38		elin 3220	. . . . . . . . . . 11 ⊢ (⟪y, x⟫ ∈ (A ∩ (B ×_k V)) ↔ (⟪y, x⟫ ∈ A ∧ ⟪y, x⟫ ∈ (B ×_k V)))
39		notnot 282	. . . . . . . . . . 11 ⊢ (⟪y, x⟫ ∈ (A ∩ (B ×_k V)) ↔ ¬ ¬ ⟪y, x⟫ ∈ (A ∩ (B ×_k V)))
40	30, 3	opkelxpk 4249	. . . . . . . . . . . . 13 ⊢ (⟪y, x⟫ ∈ (B ×_k V) ↔ (y ∈ B ∧ x ∈ V))
41	3, 40	mpbiran2 885	. . . . . . . . . . . 12 ⊢ (⟪y, x⟫ ∈ (B ×_k V) ↔ y ∈ B)
42	41	anbi2i 675	. . . . . . . . . . 11 ⊢ ((⟪y, x⟫ ∈ A ∧ ⟪y, x⟫ ∈ (B ×_k V)) ↔ (⟪y, x⟫ ∈ A ∧ y ∈ B))
43	38, 39, 42	3bitr3i 266	. . . . . . . . . 10 ⊢ (¬ ¬ ⟪y, x⟫ ∈ (A ∩ (B ×_k V)) ↔ (⟪y, x⟫ ∈ A ∧ y ∈ B))
44	37, 43	bitri 240	. . . . . . . . 9 ⊢ (∃z(z = {y} ∧ ¬ ⟪z, {x}⟫ ∈ SI_k ∼ (A ∩ (B ×_k V))) ↔ (⟪y, x⟫ ∈ A ∧ y ∈ B))
45	44	exbii 1582	. . . . . . . 8 ⊢ (∃y∃z(z = {y} ∧ ¬ ⟪z, {x}⟫ ∈ SI_k ∼ (A ∩ (B ×_k V))) ↔ ∃y(⟪y, x⟫ ∈ A ∧ y ∈ B))
46	26, 45	bitri 240	. . . . . . 7 ⊢ (∃z∃y(z = {y} ∧ ¬ ⟪z, {x}⟫ ∈ SI_k ∼ (A ∩ (B ×_k V))) ↔ ∃y(⟪y, x⟫ ∈ A ∧ y ∈ B))
47	25, 46	xchbinx 301	. . . . . 6 ⊢ (∀z ¬ ∃y(z = {y} ∧ ¬ ⟪z, {x}⟫ ∈ SI_k ∼ (A ∩ (B ×_k V))) ↔ ¬ ∃y(⟪y, x⟫ ∈ A ∧ y ∈ B))
48	5, 24, 47	3bitri 262	. . . . 5 ⊢ (x ∈ P6 ( ∼ (1_c ×_k V) ∪ SI_k ∼ (A ∩ (B ×_k V))) ↔ ¬ ∃y(⟪y, x⟫ ∈ A ∧ y ∈ B))
49	48	con2bii 322	. . . 4 ⊢ (∃y(⟪y, x⟫ ∈ A ∧ y ∈ B) ↔ ¬ x ∈ P6 ( ∼ (1_c ×_k V) ∪ SI_k ∼ (A ∩ (B ×_k V))))
50	1, 2, 49	3bitri 262	. . 3 ⊢ (∃y ∈ B ⟪y, x⟫ ∈ A ↔ ¬ x ∈ P6 ( ∼ (1_c ×_k V) ∪ SI_k ∼ (A ∩ (B ×_k V))))
51	3	elimak 4260	. . 3 ⊢ (x ∈ (A “_k B) ↔ ∃y ∈ B ⟪y, x⟫ ∈ A)
52	3	elcompl 3226	. . 3 ⊢ (x ∈ ∼ P6 ( ∼ (1_c ×_k V) ∪ SI_k ∼ (A ∩ (B ×_k V))) ↔ ¬ x ∈ P6 ( ∼ (1_c ×_k V) ∪ SI_k ∼ (A ∩ (B ×_k V))))
53	50, 51, 52	3bitr4i 268	. 2 ⊢ (x ∈ (A “_k B) ↔ x ∈ ∼ P6 ( ∼ (1_c ×_k V) ∪ SI_k ∼ (A ∩ (B ×_k V))))
54	53	eqriv 2350	1 ⊢ (A “_k B) = ∼ P6 ( ∼ (1_c ×_k V) ∪ SI_k ∼ (A ∩ (B ×_k V)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 176 ∨ wo 357 ∧ wa 358 ∀wal 1540 ∃wex 1541 = wceq 1642 ∈ wcel 1710 ∃wrex 2616 Vcvv 2860 ∼ ccompl 3206 ∪ cun 3208 ∩ cin 3209 {csn 3738 ⟪copk 4058 1_cc1c 4135 ×_k cxpk 4175 P6 cp6 4179 “_k cimak 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

W3C validator