ins2kexg - New Foundations Explorer

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

Theorem ins2kexg 4306

Description: Ins2_k preserves sethood. (Contributed by SF, 14-Jan-2015.)

**Assertion**
Ref	Expression
ins2kexg	⊢ (A ∈ V → Ins2_k A ∈ V)

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

Step	Hyp	Ref	Expression
1		ins2keq 4219	. . 3 ⊢ (x = A → Ins2_k x = Ins2_k A)
2	1	eleq1d 2419	. 2 ⊢ (x = A → ( Ins2_k x ∈ V ↔ Ins2_k A ∈ V))
3		ax-ins2 4085	. . 3 ⊢ ∃y∀z∀w∀t(⟪{{z}}, ⟪w, t⟫⟫ ∈ y ↔ ⟪z, t⟫ ∈ x)
4		inss1 3476	. . . . . . . 8 ⊢ ((℘₁1_c ×_k (V ×_k V)) ∩ y) ⊆ (℘₁1_c ×_k (V ×_k V))
5		ins2kss 4280	. . . . . . . 8 ⊢ Ins2_k x ⊆ (℘₁1_c ×_k (V ×_k V))
6	4, 5	insklem 4305	. . . . . . 7 ⊢ (((℘₁1_c ×_k (V ×_k V)) ∩ y) = Ins2_k x ↔ ∀z∀w∀t(⟪{{z}}, ⟪w, t⟫⟫ ∈ ((℘₁1_c ×_k (V ×_k V)) ∩ y) ↔ ⟪{{z}}, ⟪w, t⟫⟫ ∈ Ins2_k x))
7		vex 2863	. . . . . . . . . . . . . 14 ⊢ z ∈ V
8	7	snel1c 4141	. . . . . . . . . . . . 13 ⊢ {z} ∈ 1_c
9		snelpw1 4147	. . . . . . . . . . . . 13 ⊢ ({{z}} ∈ ℘₁1_c ↔ {z} ∈ 1_c)
10	8, 9	mpbir 200	. . . . . . . . . . . 12 ⊢ {{z}} ∈ ℘₁1_c
11		vex 2863	. . . . . . . . . . . . 13 ⊢ w ∈ V
12		vex 2863	. . . . . . . . . . . . 13 ⊢ t ∈ V
13	11, 12	opkelxpk 4249	. . . . . . . . . . . . 13 ⊢ (⟪w, t⟫ ∈ (V ×_k V) ↔ (w ∈ V ∧ t ∈ V))
14	11, 12, 13	mpbir2an 886	. . . . . . . . . . . 12 ⊢ ⟪w, t⟫ ∈ (V ×_k V)
15		snex 4112	. . . . . . . . . . . . 13 ⊢ {{z}} ∈ V
16		opkex 4114	. . . . . . . . . . . . 13 ⊢ ⟪w, t⟫ ∈ V
17	15, 16	opkelxpk 4249	. . . . . . . . . . . 12 ⊢ (⟪{{z}}, ⟪w, t⟫⟫ ∈ (℘₁1_c ×_k (V ×_k V)) ↔ ({{z}} ∈ ℘₁1_c ∧ ⟪w, t⟫ ∈ (V ×_k V)))
18	10, 14, 17	mpbir2an 886	. . . . . . . . . . 11 ⊢ ⟪{{z}}, ⟪w, t⟫⟫ ∈ (℘₁1_c ×_k (V ×_k V))
19		elin 3220	. . . . . . . . . . 11 ⊢ (⟪{{z}}, ⟪w, t⟫⟫ ∈ ((℘₁1_c ×_k (V ×_k V)) ∩ y) ↔ (⟪{{z}}, ⟪w, t⟫⟫ ∈ (℘₁1_c ×_k (V ×_k V)) ∧ ⟪{{z}}, ⟪w, t⟫⟫ ∈ y))
20	18, 19	mpbiran 884	. . . . . . . . . 10 ⊢ (⟪{{z}}, ⟪w, t⟫⟫ ∈ ((℘₁1_c ×_k (V ×_k V)) ∩ y) ↔ ⟪{{z}}, ⟪w, t⟫⟫ ∈ y)
21	7, 11, 12	otkelins2k 4256	. . . . . . . . . 10 ⊢ (⟪{{z}}, ⟪w, t⟫⟫ ∈ Ins2_k x ↔ ⟪z, t⟫ ∈ x)
22	20, 21	bibi12i 306	. . . . . . . . 9 ⊢ ((⟪{{z}}, ⟪w, t⟫⟫ ∈ ((℘₁1_c ×_k (V ×_k V)) ∩ y) ↔ ⟪{{z}}, ⟪w, t⟫⟫ ∈ Ins2_k x) ↔ (⟪{{z}}, ⟪w, t⟫⟫ ∈ y ↔ ⟪z, t⟫ ∈ x))
23	22	albii 1566	. . . . . . . 8 ⊢ (∀t(⟪{{z}}, ⟪w, t⟫⟫ ∈ ((℘₁1_c ×_k (V ×_k V)) ∩ y) ↔ ⟪{{z}}, ⟪w, t⟫⟫ ∈ Ins2_k x) ↔ ∀t(⟪{{z}}, ⟪w, t⟫⟫ ∈ y ↔ ⟪z, t⟫ ∈ x))
24	23	2albii 1567	. . . . . . 7 ⊢ (∀z∀w∀t(⟪{{z}}, ⟪w, t⟫⟫ ∈ ((℘₁1_c ×_k (V ×_k V)) ∩ y) ↔ ⟪{{z}}, ⟪w, t⟫⟫ ∈ Ins2_k x) ↔ ∀z∀w∀t(⟪{{z}}, ⟪w, t⟫⟫ ∈ y ↔ ⟪z, t⟫ ∈ x))
25	6, 24	bitri 240	. . . . . 6 ⊢ (((℘₁1_c ×_k (V ×_k V)) ∩ y) = Ins2_k x ↔ ∀z∀w∀t(⟪{{z}}, ⟪w, t⟫⟫ ∈ y ↔ ⟪z, t⟫ ∈ x))
26	25	biimpri 197	. . . . 5 ⊢ (∀z∀w∀t(⟪{{z}}, ⟪w, t⟫⟫ ∈ y ↔ ⟪z, t⟫ ∈ x) → ((℘₁1_c ×_k (V ×_k V)) ∩ y) = Ins2_k x)
27		1cex 4143	. . . . . . . 8 ⊢ 1_c ∈ V
28	27	pw1ex 4304	. . . . . . 7 ⊢ ℘₁1_c ∈ V
29		vvex 4110	. . . . . . . 8 ⊢ V ∈ V
30	29, 29	xpkex 4290	. . . . . . 7 ⊢ (V ×_k V) ∈ V
31	28, 30	xpkex 4290	. . . . . 6 ⊢ (℘₁1_c ×_k (V ×_k V)) ∈ V
32		vex 2863	. . . . . 6 ⊢ y ∈ V
33	31, 32	inex 4106	. . . . 5 ⊢ ((℘₁1_c ×_k (V ×_k V)) ∩ y) ∈ V
34	26, 33	syl6eqelr 2442	. . . 4 ⊢ (∀z∀w∀t(⟪{{z}}, ⟪w, t⟫⟫ ∈ y ↔ ⟪z, t⟫ ∈ x) → Ins2_k x ∈ V)
35	34	exlimiv 1634	. . 3 ⊢ (∃y∀z∀w∀t(⟪{{z}}, ⟪w, t⟫⟫ ∈ y ↔ ⟪z, t⟫ ∈ x) → Ins2_k x ∈ V)
36	3, 35	ax-mp 5	. 2 ⊢ Ins2_k x ∈ V
37	2, 36	vtoclg 2915	1 ⊢ (A ∈ V → Ins2_k A ∈ V)

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 176 ∀wal 1540 ∃wex 1541 = wceq 1642 ∈ wcel 1710 Vcvv 2860 ∩ cin 3209 {csn 3738 ⟪copk 4058 1_cc1c 4135 ℘₁cpw1 4136 ×_k cxpk 4175 Ins2_k cins2k 4177

This proof depends on 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-1c 4082 ax-si 4084 ax-ins2 4085 ax-typlower 4087 ax-sn 4088

This proof 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-pw 3725 df-sn 3742 df-pr 3743 df-opk 4059 df-1c 4137 df-pw1 4138 df-xpk 4186 df-cnvk 4187 df-ins2k 4188 df-imak 4190 df-p6 4192 df-sik 4193

This theorem is used by: ins2kex 4308 cokexg 4310

W3C validator