ins2kss - New Foundations Explorer

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

Theorem ins2kss 4280

Description: Subset law for Ins2_k A. (Contributed by SF, 14-Jan-2015.)

**Assertion**
Ref	Expression
ins2kss	⊢ Ins2_k A ⊆ (℘₁1_c ×_k (V ×_k V))

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

Step	Hyp	Ref	Expression
1		vex 2863	. . . . 5 ⊢ y ∈ V
2		vex 2863	. . . . 5 ⊢ z ∈ V
3		opkelins2kg 4252	. . . . 5 ⊢ ((y ∈ V ∧ z ∈ V) → (⟪y, z⟫ ∈ Ins2_k A ↔ ∃w∃t∃u(y = {{w}} ∧ z = ⟪t, u⟫ ∧ ⟪w, u⟫ ∈ A)))
4	1, 2, 3	mp2an 653	. . . 4 ⊢ (⟪y, z⟫ ∈ Ins2_k A ↔ ∃w∃t∃u(y = {{w}} ∧ z = ⟪t, u⟫ ∧ ⟪w, u⟫ ∈ A))
5		opkeq12 4062	. . . . . . . 8 ⊢ ((y = {{w}} ∧ z = ⟪t, u⟫) → ⟪y, z⟫ = ⟪{{w}}, ⟪t, u⟫⟫)
6		vex 2863	. . . . . . . . . . 11 ⊢ w ∈ V
7	6	snel1c 4141	. . . . . . . . . 10 ⊢ {w} ∈ 1_c
8		snelpw1 4147	. . . . . . . . . 10 ⊢ ({{w}} ∈ ℘₁1_c ↔ {w} ∈ 1_c)
9	7, 8	mpbir 200	. . . . . . . . 9 ⊢ {{w}} ∈ ℘₁1_c
10		vex 2863	. . . . . . . . . 10 ⊢ t ∈ V
11		vex 2863	. . . . . . . . . 10 ⊢ u ∈ V
12	10, 11	opkelxpk 4249	. . . . . . . . . 10 ⊢ (⟪t, u⟫ ∈ (V ×_k V) ↔ (t ∈ V ∧ u ∈ V))
13	10, 11, 12	mpbir2an 886	. . . . . . . . 9 ⊢ ⟪t, u⟫ ∈ (V ×_k V)
14		snex 4112	. . . . . . . . . 10 ⊢ {{w}} ∈ V
15		opkex 4114	. . . . . . . . . 10 ⊢ ⟪t, u⟫ ∈ V
16	14, 15	opkelxpk 4249	. . . . . . . . 9 ⊢ (⟪{{w}}, ⟪t, u⟫⟫ ∈ (℘₁1_c ×_k (V ×_k V)) ↔ ({{w}} ∈ ℘₁1_c ∧ ⟪t, u⟫ ∈ (V ×_k V)))
17	9, 13, 16	mpbir2an 886	. . . . . . . 8 ⊢ ⟪{{w}}, ⟪t, u⟫⟫ ∈ (℘₁1_c ×_k (V ×_k V))
18	5, 17	syl6eqel 2441	. . . . . . 7 ⊢ ((y = {{w}} ∧ z = ⟪t, u⟫) → ⟪y, z⟫ ∈ (℘₁1_c ×_k (V ×_k V)))
19	18	3adant3 975	. . . . . 6 ⊢ ((y = {{w}} ∧ z = ⟪t, u⟫ ∧ ⟪w, u⟫ ∈ A) → ⟪y, z⟫ ∈ (℘₁1_c ×_k (V ×_k V)))
20	19	exlimiv 1634	. . . . 5 ⊢ (∃u(y = {{w}} ∧ z = ⟪t, u⟫ ∧ ⟪w, u⟫ ∈ A) → ⟪y, z⟫ ∈ (℘₁1_c ×_k (V ×_k V)))
21	20	exlimivv 1635	. . . 4 ⊢ (∃w∃t∃u(y = {{w}} ∧ z = ⟪t, u⟫ ∧ ⟪w, u⟫ ∈ A) → ⟪y, z⟫ ∈ (℘₁1_c ×_k (V ×_k V)))
22	4, 21	sylbi 187	. . 3 ⊢ (⟪y, z⟫ ∈ Ins2_k A → ⟪y, z⟫ ∈ (℘₁1_c ×_k (V ×_k V)))
23	22	gen2 1547	. 2 ⊢ ∀y∀z(⟪y, z⟫ ∈ Ins2_k A → ⟪y, z⟫ ∈ (℘₁1_c ×_k (V ×_k V)))
24		df-ins2k 4188	. . . 4 ⊢ Ins2_k A = {x ∣ ∃y∃z(x = ⟪y, z⟫ ∧ ∃t∃u∃w(y = {{t}} ∧ z = ⟪u, w⟫ ∧ ⟪t, w⟫ ∈ A))}
25	24	opkabssvvki 4210	. . 3 ⊢ Ins2_k A ⊆ (V ×_k V)
26		ssrelk 4212	. . 3 ⊢ ( Ins2_k A ⊆ (V ×_k V) → ( Ins2_k A ⊆ (℘₁1_c ×_k (V ×_k V)) ↔ ∀y∀z(⟪y, z⟫ ∈ Ins2_k A → ⟪y, z⟫ ∈ (℘₁1_c ×_k (V ×_k V)))))
27	25, 26	ax-mp 5	. 2 ⊢ ( Ins2_k A ⊆ (℘₁1_c ×_k (V ×_k V)) ↔ ∀y∀z(⟪y, z⟫ ∈ Ins2_k A → ⟪y, z⟫ ∈ (℘₁1_c ×_k (V ×_k V))))
28	23, 27	mpbir 200	1 ⊢ Ins2_k A ⊆ (℘₁1_c ×_k (V ×_k V))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 176 ∧ wa 358 ∧ w3a 934 ∀wal 1540 ∃wex 1541 = wceq 1642 ∈ wcel 1710 Vcvv 2860 ⊆ wss 3258 {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-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-ins2k 4188

This theorem is used by: ins2kexg 4306

W3C validator