Theorem insklem 4305

Description: Lemma for ins2kexg 4306 and ins3kexg 4307. Equality for subsets of (℘₁1_c ×_k (V ×_k V)). (Contributed by SF, 14-Jan-2015.)

Hypotheses

Ref	Expression
insklem.1	⊢ A ⊆ (℘11c ×k (V ×k V))
insklem.2	⊢ B ⊆ (℘11c ×k (V ×k V))

Assertion

Ref	Expression
insklem	⊢ (A = B ↔ ∀x∀y∀z(⟪{{x}}, ⟪y, z⟫⟫ ∈ A ↔ ⟪{{x}}, ⟪y, z⟫⟫ ∈ B))

Distinct variable groups:   x,A,y,z   x,B,y,z

Proof of Theorem insklem

Dummy variables w t u are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		insklem.1	. . 3 ⊢ A ⊆ (℘11c ×k (V ×k V))
2		insklem.2	. . 3 ⊢ B ⊆ (℘11c ×k (V ×k V))
3		ssofeq 4078	. . 3 ⊢ ((A ⊆ (℘11c ×k (V ×k V)) ∧ B ⊆ (℘11c ×k (V ×k V))) → (A = B ↔ ∀w ∈ (℘11c ×k (V ×k V))(w ∈ A ↔ w ∈ B)))
4	1, 2, 3	mp2an 653	. 2 ⊢ (A = B ↔ ∀w ∈ (℘11c ×k (V ×k V))(w ∈ A ↔ w ∈ B))
5		19.23v 1891	. . . . 5 ⊢ (∀x(∃y∃z w = ⟪{{x}}, ⟪y, z⟫⟫ → (w ∈ A ↔ w ∈ B)) ↔ (∃x∃y∃z w = ⟪{{x}}, ⟪y, z⟫⟫ → (w ∈ A ↔ w ∈ B)))
6		19.23vv 1892	. . . . . 6 ⊢ (∀y∀z(w = ⟪{{x}}, ⟪y, z⟫⟫ → (w ∈ A ↔ w ∈ B)) ↔ (∃y∃z w = ⟪{{x}}, ⟪y, z⟫⟫ → (w ∈ A ↔ w ∈ B)))
7	6	albii 1566	. . . . 5 ⊢ (∀x∀y∀z(w = ⟪{{x}}, ⟪y, z⟫⟫ → (w ∈ A ↔ w ∈ B)) ↔ ∀x(∃y∃z w = ⟪{{x}}, ⟪y, z⟫⟫ → (w ∈ A ↔ w ∈ B)))
8		19.42vv 1907	. . . . . . . . . 10 ⊢ (∃y∃z(t ∈ ℘11c ∧ u = ⟪y, z⟫) ↔ (t ∈ ℘11c ∧ ∃y∃z u = ⟪y, z⟫))
9	8	anbi2i 675	. . . . . . . . 9 ⊢ ((w = ⟪t, u⟫ ∧ ∃y∃z(t ∈ ℘11c ∧ u = ⟪y, z⟫)) ↔ (w = ⟪t, u⟫ ∧ (t ∈ ℘11c ∧ ∃y∃z u = ⟪y, z⟫)))
10		19.42vv 1907	. . . . . . . . 9 ⊢ (∃y∃z(w = ⟪t, u⟫ ∧ (t ∈ ℘11c ∧ u = ⟪y, z⟫)) ↔ (w = ⟪t, u⟫ ∧ ∃y∃z(t ∈ ℘11c ∧ u = ⟪y, z⟫)))
11		elvvk 4208	. . . . . . . . . . 11 ⊢ (u ∈ (V ×k V) ↔ ∃y∃z u = ⟪y, z⟫)
12	11	anbi2i 675	. . . . . . . . . 10 ⊢ ((t ∈ ℘11c ∧ u ∈ (V ×k V)) ↔ (t ∈ ℘11c ∧ ∃y∃z u = ⟪y, z⟫))
13	12	anbi2i 675	. . . . . . . . 9 ⊢ ((w = ⟪t, u⟫ ∧ (t ∈ ℘11c ∧ u ∈ (V ×k V))) ↔ (w = ⟪t, u⟫ ∧ (t ∈ ℘11c ∧ ∃y∃z u = ⟪y, z⟫)))
14	9, 10, 13	3bitr4ri 269	. . . . . . . 8 ⊢ ((w = ⟪t, u⟫ ∧ (t ∈ ℘11c ∧ u ∈ (V ×k V))) ↔ ∃y∃z(w = ⟪t, u⟫ ∧ (t ∈ ℘11c ∧ u = ⟪y, z⟫)))
15	14	2exbii 1583	. . . . . . 7 ⊢ (∃t∃u(w = ⟪t, u⟫ ∧ (t ∈ ℘11c ∧ u ∈ (V ×k V))) ↔ ∃t∃u∃y∃z(w = ⟪t, u⟫ ∧ (t ∈ ℘11c ∧ u = ⟪y, z⟫)))
16		elxpk 4197	. . . . . . 7 ⊢ (w ∈ (℘11c ×k (V ×k V)) ↔ ∃t∃u(w = ⟪t, u⟫ ∧ (t ∈ ℘11c ∧ u ∈ (V ×k V))))
17		exrot3 1744	. . . . . . . 8 ⊢ (∃x∃y∃z w = ⟪{{x}}, ⟪y, z⟫⟫ ↔ ∃y∃z∃x w = ⟪{{x}}, ⟪y, z⟫⟫)
18		exancom 1586	. . . . . . . . . . . 12 ⊢ (∃t(w = ⟪t, ⟪y, z⟫⟫ ∧ t ∈ ℘11c) ↔ ∃t(t ∈ ℘11c ∧ w = ⟪t, ⟪y, z⟫⟫))
19		elpw11c 4148	. . . . . . . . . . . . . . 15 ⊢ (t ∈ ℘11c ↔ ∃x t = {{x}})
20	19	anbi1i 676	. . . . . . . . . . . . . 14 ⊢ ((t ∈ ℘11c ∧ w = ⟪t, ⟪y, z⟫⟫) ↔ (∃x t = {{x}} ∧ w = ⟪t, ⟪y, z⟫⟫))
21		19.41v 1901	. . . . . . . . . . . . . 14 ⊢ (∃x(t = {{x}} ∧ w = ⟪t, ⟪y, z⟫⟫) ↔ (∃x t = {{x}} ∧ w = ⟪t, ⟪y, z⟫⟫))
22	20, 21	bitr4i 243	. . . . . . . . . . . . 13 ⊢ ((t ∈ ℘11c ∧ w = ⟪t, ⟪y, z⟫⟫) ↔ ∃x(t = {{x}} ∧ w = ⟪t, ⟪y, z⟫⟫))
23	22	exbii 1582	. . . . . . . . . . . 12 ⊢ (∃t(t ∈ ℘11c ∧ w = ⟪t, ⟪y, z⟫⟫) ↔ ∃t∃x(t = {{x}} ∧ w = ⟪t, ⟪y, z⟫⟫))
24	18, 23	bitri 240	. . . . . . . . . . 11 ⊢ (∃t(w = ⟪t, ⟪y, z⟫⟫ ∧ t ∈ ℘11c) ↔ ∃t∃x(t = {{x}} ∧ w = ⟪t, ⟪y, z⟫⟫))
25		ancom 437	. . . . . . . . . . . . . . 15 ⊢ ((t ∈ ℘11c ∧ u = ⟪y, z⟫) ↔ (u = ⟪y, z⟫ ∧ t ∈ ℘11c))
26	25	anbi2i 675	. . . . . . . . . . . . . 14 ⊢ ((w = ⟪t, u⟫ ∧ (t ∈ ℘11c ∧ u = ⟪y, z⟫)) ↔ (w = ⟪t, u⟫ ∧ (u = ⟪y, z⟫ ∧ t ∈ ℘11c)))
27		an12 772	. . . . . . . . . . . . . 14 ⊢ ((w = ⟪t, u⟫ ∧ (u = ⟪y, z⟫ ∧ t ∈ ℘11c)) ↔ (u = ⟪y, z⟫ ∧ (w = ⟪t, u⟫ ∧ t ∈ ℘11c)))
28	26, 27	bitri 240	. . . . . . . . . . . . 13 ⊢ ((w = ⟪t, u⟫ ∧ (t ∈ ℘11c ∧ u = ⟪y, z⟫)) ↔ (u = ⟪y, z⟫ ∧ (w = ⟪t, u⟫ ∧ t ∈ ℘11c)))
29	28	2exbii 1583	. . . . . . . . . . . 12 ⊢ (∃t∃u(w = ⟪t, u⟫ ∧ (t ∈ ℘11c ∧ u = ⟪y, z⟫)) ↔ ∃t∃u(u = ⟪y, z⟫ ∧ (w = ⟪t, u⟫ ∧ t ∈ ℘11c)))
30		opkex 4114	. . . . . . . . . . . . . 14 ⊢ ⟪y, z⟫ ∈ V
31		opkeq2 4061	. . . . . . . . . . . . . . . 16 ⊢ (u = ⟪y, z⟫ → ⟪t, u⟫ = ⟪t, ⟪y, z⟫⟫)
32	31	eqeq2d 2364	. . . . . . . . . . . . . . 15 ⊢ (u = ⟪y, z⟫ → (w = ⟪t, u⟫ ↔ w = ⟪t, ⟪y, z⟫⟫))
33	32	anbi1d 685	. . . . . . . . . . . . . 14 ⊢ (u = ⟪y, z⟫ → ((w = ⟪t, u⟫ ∧ t ∈ ℘11c) ↔ (w = ⟪t, ⟪y, z⟫⟫ ∧ t ∈ ℘11c)))
34	30, 33	ceqsexv 2895	. . . . . . . . . . . . 13 ⊢ (∃u(u = ⟪y, z⟫ ∧ (w = ⟪t, u⟫ ∧ t ∈ ℘11c)) ↔ (w = ⟪t, ⟪y, z⟫⟫ ∧ t ∈ ℘11c))
35	34	exbii 1582	. . . . . . . . . . . 12 ⊢ (∃t∃u(u = ⟪y, z⟫ ∧ (w = ⟪t, u⟫ ∧ t ∈ ℘11c)) ↔ ∃t(w = ⟪t, ⟪y, z⟫⟫ ∧ t ∈ ℘11c))
36	29, 35	bitri 240	. . . . . . . . . . 11 ⊢ (∃t∃u(w = ⟪t, u⟫ ∧ (t ∈ ℘11c ∧ u = ⟪y, z⟫)) ↔ ∃t(w = ⟪t, ⟪y, z⟫⟫ ∧ t ∈ ℘11c))
37		snex 4112	. . . . . . . . . . . . . 14 ⊢ {{x}} ∈ V
38		opkeq1 4060	. . . . . . . . . . . . . . 15 ⊢ (t = {{x}} → ⟪t, ⟪y, z⟫⟫ = ⟪{{x}}, ⟪y, z⟫⟫)
39	38	eqeq2d 2364	. . . . . . . . . . . . . 14 ⊢ (t = {{x}} → (w = ⟪t, ⟪y, z⟫⟫ ↔ w = ⟪{{x}}, ⟪y, z⟫⟫))
40	37, 39	ceqsexv 2895	. . . . . . . . . . . . 13 ⊢ (∃t(t = {{x}} ∧ w = ⟪t, ⟪y, z⟫⟫) ↔ w = ⟪{{x}}, ⟪y, z⟫⟫)
41	40	exbii 1582	. . . . . . . . . . . 12 ⊢ (∃x∃t(t = {{x}} ∧ w = ⟪t, ⟪y, z⟫⟫) ↔ ∃x w = ⟪{{x}}, ⟪y, z⟫⟫)
42		excom 1741	. . . . . . . . . . . 12 ⊢ (∃x∃t(t = {{x}} ∧ w = ⟪t, ⟪y, z⟫⟫) ↔ ∃t∃x(t = {{x}} ∧ w = ⟪t, ⟪y, z⟫⟫))
43	41, 42	bitr3i 242	. . . . . . . . . . 11 ⊢ (∃x w = ⟪{{x}}, ⟪y, z⟫⟫ ↔ ∃t∃x(t = {{x}} ∧ w = ⟪t, ⟪y, z⟫⟫))
44	24, 36, 43	3bitr4ri 269	. . . . . . . . . 10 ⊢ (∃x w = ⟪{{x}}, ⟪y, z⟫⟫ ↔ ∃t∃u(w = ⟪t, u⟫ ∧ (t ∈ ℘11c ∧ u = ⟪y, z⟫)))
45	44	2exbii 1583	. . . . . . . . 9 ⊢ (∃y∃z∃x w = ⟪{{x}}, ⟪y, z⟫⟫ ↔ ∃y∃z∃t∃u(w = ⟪t, u⟫ ∧ (t ∈ ℘11c ∧ u = ⟪y, z⟫)))
46		exrot4 1745	. . . . . . . . 9 ⊢ (∃y∃z∃t∃u(w = ⟪t, u⟫ ∧ (t ∈ ℘11c ∧ u = ⟪y, z⟫)) ↔ ∃t∃u∃y∃z(w = ⟪t, u⟫ ∧ (t ∈ ℘11c ∧ u = ⟪y, z⟫)))
47	45, 46	bitri 240	. . . . . . . 8 ⊢ (∃y∃z∃x w = ⟪{{x}}, ⟪y, z⟫⟫ ↔ ∃t∃u∃y∃z(w = ⟪t, u⟫ ∧ (t ∈ ℘11c ∧ u = ⟪y, z⟫)))
48	17, 47	bitri 240	. . . . . . 7 ⊢ (∃x∃y∃z w = ⟪{{x}}, ⟪y, z⟫⟫ ↔ ∃t∃u∃y∃z(w = ⟪t, u⟫ ∧ (t ∈ ℘11c ∧ u = ⟪y, z⟫)))
49	15, 16, 48	3bitr4i 268	. . . . . 6 ⊢ (w ∈ (℘11c ×k (V ×k V)) ↔ ∃x∃y∃z w = ⟪{{x}}, ⟪y, z⟫⟫)
50	49	imbi1i 315	. . . . 5 ⊢ ((w ∈ (℘11c ×k (V ×k V)) → (w ∈ A ↔ w ∈ B)) ↔ (∃x∃y∃z w = ⟪{{x}}, ⟪y, z⟫⟫ → (w ∈ A ↔ w ∈ B)))
51	5, 7, 50	3bitr4ri 269	. . . 4 ⊢ ((w ∈ (℘11c ×k (V ×k V)) → (w ∈ A ↔ w ∈ B)) ↔ ∀x∀y∀z(w = ⟪{{x}}, ⟪y, z⟫⟫ → (w ∈ A ↔ w ∈ B)))
52	51	albii 1566	. . 3 ⊢ (∀w(w ∈ (℘11c ×k (V ×k V)) → (w ∈ A ↔ w ∈ B)) ↔ ∀w∀x∀y∀z(w = ⟪{{x}}, ⟪y, z⟫⟫ → (w ∈ A ↔ w ∈ B)))
53		df-ral 2620	. . 3 ⊢ (∀w ∈ (℘11c ×k (V ×k V))(w ∈ A ↔ w ∈ B) ↔ ∀w(w ∈ (℘11c ×k (V ×k V)) → (w ∈ A ↔ w ∈ B)))
54		alcom 1737	. . . 4 ⊢ (∀w∀x∀y∀z(w = ⟪{{x}}, ⟪y, z⟫⟫ → (w ∈ A ↔ w ∈ B)) ↔ ∀x∀w∀y∀z(w = ⟪{{x}}, ⟪y, z⟫⟫ → (w ∈ A ↔ w ∈ B)))
55		alrot3 1738	. . . . 5 ⊢ (∀w∀y∀z(w = ⟪{{x}}, ⟪y, z⟫⟫ → (w ∈ A ↔ w ∈ B)) ↔ ∀y∀z∀w(w = ⟪{{x}}, ⟪y, z⟫⟫ → (w ∈ A ↔ w ∈ B)))
56	55	albii 1566	. . . 4 ⊢ (∀x∀w∀y∀z(w = ⟪{{x}}, ⟪y, z⟫⟫ → (w ∈ A ↔ w ∈ B)) ↔ ∀x∀y∀z∀w(w = ⟪{{x}}, ⟪y, z⟫⟫ → (w ∈ A ↔ w ∈ B)))
57		opkex 4114	. . . . . . 7 ⊢ ⟪{{x}}, ⟪y, z⟫⟫ ∈ V
58		eleq1 2413	. . . . . . . 8 ⊢ (w = ⟪{{x}}, ⟪y, z⟫⟫ → (w ∈ A ↔ ⟪{{x}}, ⟪y, z⟫⟫ ∈ A))
59		eleq1 2413	. . . . . . . 8 ⊢ (w = ⟪{{x}}, ⟪y, z⟫⟫ → (w ∈ B ↔ ⟪{{x}}, ⟪y, z⟫⟫ ∈ B))
60	58, 59	bibi12d 312	. . . . . . 7 ⊢ (w = ⟪{{x}}, ⟪y, z⟫⟫ → ((w ∈ A ↔ w ∈ B) ↔ (⟪{{x}}, ⟪y, z⟫⟫ ∈ A ↔ ⟪{{x}}, ⟪y, z⟫⟫ ∈ B)))
61	57, 60	ceqsalv 2886	. . . . . 6 ⊢ (∀w(w = ⟪{{x}}, ⟪y, z⟫⟫ → (w ∈ A ↔ w ∈ B)) ↔ (⟪{{x}}, ⟪y, z⟫⟫ ∈ A ↔ ⟪{{x}}, ⟪y, z⟫⟫ ∈ B))
62	61	albii 1566	. . . . 5 ⊢ (∀z∀w(w = ⟪{{x}}, ⟪y, z⟫⟫ → (w ∈ A ↔ w ∈ B)) ↔ ∀z(⟪{{x}}, ⟪y, z⟫⟫ ∈ A ↔ ⟪{{x}}, ⟪y, z⟫⟫ ∈ B))
63	62	2albii 1567	. . . 4 ⊢ (∀x∀y∀z∀w(w = ⟪{{x}}, ⟪y, z⟫⟫ → (w ∈ A ↔ w ∈ B)) ↔ ∀x∀y∀z(⟪{{x}}, ⟪y, z⟫⟫ ∈ A ↔ ⟪{{x}}, ⟪y, z⟫⟫ ∈ B))
64	54, 56, 63	3bitrri 263	. . 3 ⊢ (∀x∀y∀z(⟪{{x}}, ⟪y, z⟫⟫ ∈ A ↔ ⟪{{x}}, ⟪y, z⟫⟫ ∈ B) ↔ ∀w∀x∀y∀z(w = ⟪{{x}}, ⟪y, z⟫⟫ → (w ∈ A ↔ w ∈ B)))
65	52, 53, 64	3bitr4i 268	. 2 ⊢ (∀w ∈ (℘11c ×k (V ×k V))(w ∈ A ↔ w ∈ B) ↔ ∀x∀y∀z(⟪{{x}}, ⟪y, z⟫⟫ ∈ A ↔ ⟪{{x}}, ⟪y, z⟫⟫ ∈ B))
66	4, 65	bitri 240	1 ⊢ (A = B ↔ ∀x∀y∀z(⟪{{x}}, ⟪y, z⟫⟫ ∈ A ↔ ⟪{{x}}, ⟪y, z⟫⟫ ∈ B))

Syntax hints:   → wi 4   ↔ wb 176   ∧ wa 358  ∀wal 1540  ∃wex 1541   = wceq 1642   ∈ wcel 1710  ∀wral 2615  Vcvv 2860   ⊆ wss 3258  {csn 3738  ⟪copk 4058  1_cc1c 4135  ℘₁cpw1 4136   ×_k cxpk 4175

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-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

This theorem is referenced by:  ins2kexg  4306  ins3kexg  4307