cnvkexg - New Foundations Explorer

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

Theorem cnvkexg 4287

Description: The Kuratowski converse of a set is a set. (Contributed by SF, 13-Jan-2015.)

**Assertion**
Ref	Expression
cnvkexg	⊢ (A ∈ V → ^◡_kA ∈ V)

Proof of Theorem cnvkexg Dummy variables x y z w are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		cnvkeq 4216	. . 3 ⊢ (x = A → ^◡_kx = ^◡_kA)
2	1	eleq1d 2419	. 2 ⊢ (x = A → (^◡_kx ∈ V ↔ ^◡_kA ∈ V))
3		ax-cnv 4081	. . 3 ⊢ ∃y∀z∀w(⟪z, w⟫ ∈ y ↔ ⟪w, z⟫ ∈ x)
4		inss1 3476	. . . . . . . 8 ⊢ ((V ×_k V) ∩ y) ⊆ (V ×_k V)
5		cnvkssvvk 4276	. . . . . . . 8 ⊢ ^◡_kx ⊆ (V ×_k V)
6		eqrelk 4213	. . . . . . . 8 ⊢ ((((V ×_k V) ∩ y) ⊆ (V ×_k V) ∧ ^◡_kx ⊆ (V ×_k V)) → (((V ×_k V) ∩ y) = ^◡_kx ↔ ∀z∀w(⟪z, w⟫ ∈ ((V ×_k V) ∩ y) ↔ ⟪z, w⟫ ∈ ^◡_kx)))
7	4, 5, 6	mp2an 653	. . . . . . 7 ⊢ (((V ×_k V) ∩ y) = ^◡_kx ↔ ∀z∀w(⟪z, w⟫ ∈ ((V ×_k V) ∩ y) ↔ ⟪z, w⟫ ∈ ^◡_kx))
8		vex 2863	. . . . . . . . . . 11 ⊢ z ∈ V
9		vex 2863	. . . . . . . . . . 11 ⊢ w ∈ V
10	8, 9	opkelxpk 4249	. . . . . . . . . . 11 ⊢ (⟪z, w⟫ ∈ (V ×_k V) ↔ (z ∈ V ∧ w ∈ V))
11	8, 9, 10	mpbir2an 886	. . . . . . . . . 10 ⊢ ⟪z, w⟫ ∈ (V ×_k V)
12		elin 3220	. . . . . . . . . 10 ⊢ (⟪z, w⟫ ∈ ((V ×_k V) ∩ y) ↔ (⟪z, w⟫ ∈ (V ×_k V) ∧ ⟪z, w⟫ ∈ y))
13	11, 12	mpbiran 884	. . . . . . . . 9 ⊢ (⟪z, w⟫ ∈ ((V ×_k V) ∩ y) ↔ ⟪z, w⟫ ∈ y)
14	8, 9	opkelcnvk 4251	. . . . . . . . 9 ⊢ (⟪z, w⟫ ∈ ^◡_kx ↔ ⟪w, z⟫ ∈ x)
15	13, 14	bibi12i 306	. . . . . . . 8 ⊢ ((⟪z, w⟫ ∈ ((V ×_k V) ∩ y) ↔ ⟪z, w⟫ ∈ ^◡_kx) ↔ (⟪z, w⟫ ∈ y ↔ ⟪w, z⟫ ∈ x))
16	15	2albii 1567	. . . . . . 7 ⊢ (∀z∀w(⟪z, w⟫ ∈ ((V ×_k V) ∩ y) ↔ ⟪z, w⟫ ∈ ^◡_kx) ↔ ∀z∀w(⟪z, w⟫ ∈ y ↔ ⟪w, z⟫ ∈ x))
17	7, 16	bitri 240	. . . . . 6 ⊢ (((V ×_k V) ∩ y) = ^◡_kx ↔ ∀z∀w(⟪z, w⟫ ∈ y ↔ ⟪w, z⟫ ∈ x))
18	17	biimpri 197	. . . . 5 ⊢ (∀z∀w(⟪z, w⟫ ∈ y ↔ ⟪w, z⟫ ∈ x) → ((V ×_k V) ∩ y) = ^◡_kx)
19		vvex 4110	. . . . . . 7 ⊢ V ∈ V
20		xpkvexg 4286	. . . . . . 7 ⊢ (V ∈ V → (V ×_k V) ∈ V)
21	19, 20	ax-mp 5	. . . . . 6 ⊢ (V ×_k V) ∈ V
22		vex 2863	. . . . . 6 ⊢ y ∈ V
23	21, 22	inex 4106	. . . . 5 ⊢ ((V ×_k V) ∩ y) ∈ V
24	18, 23	syl6eqelr 2442	. . . 4 ⊢ (∀z∀w(⟪z, w⟫ ∈ y ↔ ⟪w, z⟫ ∈ x) → ^◡_kx ∈ V)
25	24	exlimiv 1634	. . 3 ⊢ (∃y∀z∀w(⟪z, w⟫ ∈ y ↔ ⟪w, z⟫ ∈ x) → ^◡_kx ∈ V)
26	3, 25	ax-mp 5	. 2 ⊢ ^◡_kx ∈ V
27	2, 26	vtoclg 2915	1 ⊢ (A ∈ V → ^◡_kA ∈ V)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 176 ∀wal 1540 ∃wex 1541 = wceq 1642 ∈ wcel 1710 Vcvv 2860 ∩ cin 3209 ⊆ wss 3258 ⟪copk 4058 ×_k cxpk 4175 ^◡_kccnvk 4176

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-xp 4080 ax-cnv 4081 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-xpk 4186 df-cnvk 4187

This theorem is referenced by: cnvkex 4288 xpkexg 4289 cokexg 4310 imagekexg 4312

W3C validator