nnadjoinlem1 - New Foundations Explorer

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

Theorem nnadjoinlem1 4520

Description: Lemma for nnadjoin 4521. Establish stratification. (Contributed by SF, 29-Jan-2015.)

**Assertion**
Ref	Expression
nnadjoinlem1	⊢ {n ∣ ∀l ∈ n (y ∈ ∼ ∪l → {x ∣ ∃b ∈ l x = (b ∪ {y})} ∈ n)} ∈ V

Distinct variable group: n,l,y,x,b

Proof of Theorem nnadjoinlem1 Dummy variables t z are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		snex 4112	. . . . . . . . 9 ⊢ {l} ∈ V
2		opkeq1 4060	. . . . . . . . . 10 ⊢ (t = {l} → ⟪t, n⟫ = ⟪{l}, n⟫)
3	2	eleq1d 2419	. . . . . . . . 9 ⊢ (t = {l} → (⟪t, n⟫ ∈ ( S_k ∩ (( ∼ ℘₁(((℘₁{z ∣ y ∈ z} ×_k V) ∩ S_k ) “_k 1_c) ×_k V) ∖ (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k (( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c))) ↔ ⟪{l}, n⟫ ∈ ( S_k ∩ (( ∼ ℘₁(((℘₁{z ∣ y ∈ z} ×_k V) ∩ S_k ) “_k 1_c) ×_k V) ∖ (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k (( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c)))))
4	1, 3	ceqsexv 2895	. . . . . . . 8 ⊢ (∃t(t = {l} ∧ ⟪t, n⟫ ∈ ( S_k ∩ (( ∼ ℘₁(((℘₁{z ∣ y ∈ z} ×_k V) ∩ S_k ) “_k 1_c) ×_k V) ∖ (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k (( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c)))) ↔ ⟪{l}, n⟫ ∈ ( S_k ∩ (( ∼ ℘₁(((℘₁{z ∣ y ∈ z} ×_k V) ∩ S_k ) “_k 1_c) ×_k V) ∖ (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k (( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c))))
5		elin 3220	. . . . . . . 8 ⊢ (⟪{l}, n⟫ ∈ ( S_k ∩ (( ∼ ℘₁(((℘₁{z ∣ y ∈ z} ×_k V) ∩ S_k ) “_k 1_c) ×_k V) ∖ (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k (( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c))) ↔ (⟪{l}, n⟫ ∈ S_k ∧ ⟪{l}, n⟫ ∈ (( ∼ ℘₁(((℘₁{z ∣ y ∈ z} ×_k V) ∩ S_k ) “_k 1_c) ×_k V) ∖ (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k (( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c))))
6		vex 2863	. . . . . . . . . 10 ⊢ l ∈ V
7		vex 2863	. . . . . . . . . 10 ⊢ n ∈ V
8	6, 7	elssetk 4271	. . . . . . . . 9 ⊢ (⟪{l}, n⟫ ∈ S_k ↔ l ∈ n)
9		eldif 3222	. . . . . . . . . 10 ⊢ (⟪{l}, n⟫ ∈ (( ∼ ℘₁(((℘₁{z ∣ y ∈ z} ×_k V) ∩ S_k ) “_k 1_c) ×_k V) ∖ (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k (( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c)) ↔ (⟪{l}, n⟫ ∈ ( ∼ ℘₁(((℘₁{z ∣ y ∈ z} ×_k V) ∩ S_k ) “_k 1_c) ×_k V) ∧ ¬ ⟪{l}, n⟫ ∈ (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k (( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c)))
10	1	elcompl 3226	. . . . . . . . . . . . 13 ⊢ ({l} ∈ ∼ ℘₁(((℘₁{z ∣ y ∈ z} ×_k V) ∩ S_k ) “_k 1_c) ↔ ¬ {l} ∈ ℘₁(((℘₁{z ∣ y ∈ z} ×_k V) ∩ S_k ) “_k 1_c))
11	6	elimak 4260	. . . . . . . . . . . . . . 15 ⊢ (l ∈ (((℘₁{z ∣ y ∈ z} ×_k V) ∩ S_k ) “_k 1_c) ↔ ∃t ∈ 1_c ⟪t, l⟫ ∈ ((℘₁{z ∣ y ∈ z} ×_k V) ∩ S_k ))
12		el1c 4140	. . . . . . . . . . . . . . . . . . 19 ⊢ (t ∈ 1_c ↔ ∃x t = {x})
13	12	anbi1i 676	. . . . . . . . . . . . . . . . . 18 ⊢ ((t ∈ 1_c ∧ ⟪t, l⟫ ∈ ((℘₁{z ∣ y ∈ z} ×_k V) ∩ S_k )) ↔ (∃x t = {x} ∧ ⟪t, l⟫ ∈ ((℘₁{z ∣ y ∈ z} ×_k V) ∩ S_k )))
14		19.41v 1901	. . . . . . . . . . . . . . . . . 18 ⊢ (∃x(t = {x} ∧ ⟪t, l⟫ ∈ ((℘₁{z ∣ y ∈ z} ×_k V) ∩ S_k )) ↔ (∃x t = {x} ∧ ⟪t, l⟫ ∈ ((℘₁{z ∣ y ∈ z} ×_k V) ∩ S_k )))
15	13, 14	bitr4i 243	. . . . . . . . . . . . . . . . 17 ⊢ ((t ∈ 1_c ∧ ⟪t, l⟫ ∈ ((℘₁{z ∣ y ∈ z} ×_k V) ∩ S_k )) ↔ ∃x(t = {x} ∧ ⟪t, l⟫ ∈ ((℘₁{z ∣ y ∈ z} ×_k V) ∩ S_k )))
16	15	exbii 1582	. . . . . . . . . . . . . . . 16 ⊢ (∃t(t ∈ 1_c ∧ ⟪t, l⟫ ∈ ((℘₁{z ∣ y ∈ z} ×_k V) ∩ S_k )) ↔ ∃t∃x(t = {x} ∧ ⟪t, l⟫ ∈ ((℘₁{z ∣ y ∈ z} ×_k V) ∩ S_k )))
17		df-rex 2621	. . . . . . . . . . . . . . . 16 ⊢ (∃t ∈ 1_c ⟪t, l⟫ ∈ ((℘₁{z ∣ y ∈ z} ×_k V) ∩ S_k ) ↔ ∃t(t ∈ 1_c ∧ ⟪t, l⟫ ∈ ((℘₁{z ∣ y ∈ z} ×_k V) ∩ S_k )))
18		excom 1741	. . . . . . . . . . . . . . . 16 ⊢ (∃x∃t(t = {x} ∧ ⟪t, l⟫ ∈ ((℘₁{z ∣ y ∈ z} ×_k V) ∩ S_k )) ↔ ∃t∃x(t = {x} ∧ ⟪t, l⟫ ∈ ((℘₁{z ∣ y ∈ z} ×_k V) ∩ S_k )))
19	16, 17, 18	3bitr4i 268	. . . . . . . . . . . . . . 15 ⊢ (∃t ∈ 1_c ⟪t, l⟫ ∈ ((℘₁{z ∣ y ∈ z} ×_k V) ∩ S_k ) ↔ ∃x∃t(t = {x} ∧ ⟪t, l⟫ ∈ ((℘₁{z ∣ y ∈ z} ×_k V) ∩ S_k )))
20		snex 4112	. . . . . . . . . . . . . . . . . 18 ⊢ {x} ∈ V
21		opkeq1 4060	. . . . . . . . . . . . . . . . . . 19 ⊢ (t = {x} → ⟪t, l⟫ = ⟪{x}, l⟫)
22	21	eleq1d 2419	. . . . . . . . . . . . . . . . . 18 ⊢ (t = {x} → (⟪t, l⟫ ∈ ((℘₁{z ∣ y ∈ z} ×_k V) ∩ S_k ) ↔ ⟪{x}, l⟫ ∈ ((℘₁{z ∣ y ∈ z} ×_k V) ∩ S_k )))
23	20, 22	ceqsexv 2895	. . . . . . . . . . . . . . . . 17 ⊢ (∃t(t = {x} ∧ ⟪t, l⟫ ∈ ((℘₁{z ∣ y ∈ z} ×_k V) ∩ S_k )) ↔ ⟪{x}, l⟫ ∈ ((℘₁{z ∣ y ∈ z} ×_k V) ∩ S_k ))
24		elin 3220	. . . . . . . . . . . . . . . . 17 ⊢ (⟪{x}, l⟫ ∈ ((℘₁{z ∣ y ∈ z} ×_k V) ∩ S_k ) ↔ (⟪{x}, l⟫ ∈ (℘₁{z ∣ y ∈ z} ×_k V) ∧ ⟪{x}, l⟫ ∈ S_k ))
25	20, 6	opkelxpk 4249	. . . . . . . . . . . . . . . . . . . 20 ⊢ (⟪{x}, l⟫ ∈ (℘₁{z ∣ y ∈ z} ×_k V) ↔ ({x} ∈ ℘₁{z ∣ y ∈ z} ∧ l ∈ V))
26	6, 25	mpbiran2 885	. . . . . . . . . . . . . . . . . . 19 ⊢ (⟪{x}, l⟫ ∈ (℘₁{z ∣ y ∈ z} ×_k V) ↔ {x} ∈ ℘₁{z ∣ y ∈ z})
27		snelpw1 4147	. . . . . . . . . . . . . . . . . . 19 ⊢ ({x} ∈ ℘₁{z ∣ y ∈ z} ↔ x ∈ {z ∣ y ∈ z})
28		vex 2863	. . . . . . . . . . . . . . . . . . . 20 ⊢ x ∈ V
29		elequ2 1715	. . . . . . . . . . . . . . . . . . . 20 ⊢ (z = x → (y ∈ z ↔ y ∈ x))
30	28, 29	elab 2986	. . . . . . . . . . . . . . . . . . 19 ⊢ (x ∈ {z ∣ y ∈ z} ↔ y ∈ x)
31	26, 27, 30	3bitri 262	. . . . . . . . . . . . . . . . . 18 ⊢ (⟪{x}, l⟫ ∈ (℘₁{z ∣ y ∈ z} ×_k V) ↔ y ∈ x)
32	28, 6	elssetk 4271	. . . . . . . . . . . . . . . . . 18 ⊢ (⟪{x}, l⟫ ∈ S_k ↔ x ∈ l)
33	31, 32	anbi12i 678	. . . . . . . . . . . . . . . . 17 ⊢ ((⟪{x}, l⟫ ∈ (℘₁{z ∣ y ∈ z} ×_k V) ∧ ⟪{x}, l⟫ ∈ S_k ) ↔ (y ∈ x ∧ x ∈ l))
34	23, 24, 33	3bitri 262	. . . . . . . . . . . . . . . 16 ⊢ (∃t(t = {x} ∧ ⟪t, l⟫ ∈ ((℘₁{z ∣ y ∈ z} ×_k V) ∩ S_k )) ↔ (y ∈ x ∧ x ∈ l))
35	34	exbii 1582	. . . . . . . . . . . . . . 15 ⊢ (∃x∃t(t = {x} ∧ ⟪t, l⟫ ∈ ((℘₁{z ∣ y ∈ z} ×_k V) ∩ S_k )) ↔ ∃x(y ∈ x ∧ x ∈ l))
36	11, 19, 35	3bitri 262	. . . . . . . . . . . . . 14 ⊢ (l ∈ (((℘₁{z ∣ y ∈ z} ×_k V) ∩ S_k ) “_k 1_c) ↔ ∃x(y ∈ x ∧ x ∈ l))
37		snelpw1 4147	. . . . . . . . . . . . . 14 ⊢ ({l} ∈ ℘₁(((℘₁{z ∣ y ∈ z} ×_k V) ∩ S_k ) “_k 1_c) ↔ l ∈ (((℘₁{z ∣ y ∈ z} ×_k V) ∩ S_k ) “_k 1_c))
38		eluni 3895	. . . . . . . . . . . . . 14 ⊢ (y ∈ ∪l ↔ ∃x(y ∈ x ∧ x ∈ l))
39	36, 37, 38	3bitr4i 268	. . . . . . . . . . . . 13 ⊢ ({l} ∈ ℘₁(((℘₁{z ∣ y ∈ z} ×_k V) ∩ S_k ) “_k 1_c) ↔ y ∈ ∪l)
40	10, 39	xchbinx 301	. . . . . . . . . . . 12 ⊢ ({l} ∈ ∼ ℘₁(((℘₁{z ∣ y ∈ z} ×_k V) ∩ S_k ) “_k 1_c) ↔ ¬ y ∈ ∪l)
41	1, 7	opkelxpk 4249	. . . . . . . . . . . . 13 ⊢ (⟪{l}, n⟫ ∈ ( ∼ ℘₁(((℘₁{z ∣ y ∈ z} ×_k V) ∩ S_k ) “_k 1_c) ×_k V) ↔ ({l} ∈ ∼ ℘₁(((℘₁{z ∣ y ∈ z} ×_k V) ∩ S_k ) “_k 1_c) ∧ n ∈ V))
42	7, 41	mpbiran2 885	. . . . . . . . . . . 12 ⊢ (⟪{l}, n⟫ ∈ ( ∼ ℘₁(((℘₁{z ∣ y ∈ z} ×_k V) ∩ S_k ) “_k 1_c) ×_k V) ↔ {l} ∈ ∼ ℘₁(((℘₁{z ∣ y ∈ z} ×_k V) ∩ S_k ) “_k 1_c))
43		vex 2863	. . . . . . . . . . . . 13 ⊢ y ∈ V
44	43	elcompl 3226	. . . . . . . . . . . 12 ⊢ (y ∈ ∼ ∪l ↔ ¬ y ∈ ∪l)
45	40, 42, 44	3bitr4i 268	. . . . . . . . . . 11 ⊢ (⟪{l}, n⟫ ∈ ( ∼ ℘₁(((℘₁{z ∣ y ∈ z} ×_k V) ∩ S_k ) “_k 1_c) ×_k V) ↔ y ∈ ∼ ∪l)
46		eqabb 2459	. . . . . . . . . . . . . . 15 ⊢ (z = {x ∣ ∃b ∈ l x = (b ∪ {y})} ↔ ∀x(x ∈ z ↔ ∃b ∈ l x = (b ∪ {y})))
47	46	anbi1i 676	. . . . . . . . . . . . . 14 ⊢ ((z = {x ∣ ∃b ∈ l x = (b ∪ {y})} ∧ z ∈ n) ↔ (∀x(x ∈ z ↔ ∃b ∈ l x = (b ∪ {y})) ∧ z ∈ n))
48	47	exbii 1582	. . . . . . . . . . . . 13 ⊢ (∃z(z = {x ∣ ∃b ∈ l x = (b ∪ {y})} ∧ z ∈ n) ↔ ∃z(∀x(x ∈ z ↔ ∃b ∈ l x = (b ∪ {y})) ∧ z ∈ n))
49		df-clel 2349	. . . . . . . . . . . . 13 ⊢ ({x ∣ ∃b ∈ l x = (b ∪ {y})} ∈ n ↔ ∃z(z = {x ∣ ∃b ∈ l x = (b ∪ {y})} ∧ z ∈ n))
50		opkex 4114	. . . . . . . . . . . . . . 15 ⊢ ⟪{l}, n⟫ ∈ V
51	50	elimak 4260	. . . . . . . . . . . . . 14 ⊢ (⟪{l}, n⟫ ∈ (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k (( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ↔ ∃t ∈ ℘₁ ℘₁1_c⟪t, ⟪{l}, n⟫⟫ ∈ ( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k (( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ))
52		elpw121c 4149	. . . . . . . . . . . . . . . . . 18 ⊢ (t ∈ ℘₁℘₁1_c ↔ ∃z t = {{{z}}})
53	52	anbi1i 676	. . . . . . . . . . . . . . . . 17 ⊢ ((t ∈ ℘₁℘₁1_c ∧ ⟪t, ⟪{l}, n⟫⟫ ∈ ( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k (( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k )) ↔ (∃z t = {{{z}}} ∧ ⟪t, ⟪{l}, n⟫⟫ ∈ ( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k (( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k )))
54		19.41v 1901	. . . . . . . . . . . . . . . . 17 ⊢ (∃z(t = {{{z}}} ∧ ⟪t, ⟪{l}, n⟫⟫ ∈ ( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k (( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k )) ↔ (∃z t = {{{z}}} ∧ ⟪t, ⟪{l}, n⟫⟫ ∈ ( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k (( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k )))
55	53, 54	bitr4i 243	. . . . . . . . . . . . . . . 16 ⊢ ((t ∈ ℘₁℘₁1_c ∧ ⟪t, ⟪{l}, n⟫⟫ ∈ ( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k (( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k )) ↔ ∃z(t = {{{z}}} ∧ ⟪t, ⟪{l}, n⟫⟫ ∈ ( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k (( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k )))
56	55	exbii 1582	. . . . . . . . . . . . . . 15 ⊢ (∃t(t ∈ ℘₁℘₁1_c ∧ ⟪t, ⟪{l}, n⟫⟫ ∈ ( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k (( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k )) ↔ ∃t∃z(t = {{{z}}} ∧ ⟪t, ⟪{l}, n⟫⟫ ∈ ( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k (( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k )))
57		df-rex 2621	. . . . . . . . . . . . . . 15 ⊢ (∃t ∈ ℘₁ ℘₁1_c⟪t, ⟪{l}, n⟫⟫ ∈ ( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k (( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) ↔ ∃t(t ∈ ℘₁℘₁1_c ∧ ⟪t, ⟪{l}, n⟫⟫ ∈ ( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k (( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k )))
58		excom 1741	. . . . . . . . . . . . . . 15 ⊢ (∃z∃t(t = {{{z}}} ∧ ⟪t, ⟪{l}, n⟫⟫ ∈ ( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k (( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k )) ↔ ∃t∃z(t = {{{z}}} ∧ ⟪t, ⟪{l}, n⟫⟫ ∈ ( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k (( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k )))
59	56, 57, 58	3bitr4i 268	. . . . . . . . . . . . . 14 ⊢ (∃t ∈ ℘₁ ℘₁1_c⟪t, ⟪{l}, n⟫⟫ ∈ ( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k (( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) ↔ ∃z∃t(t = {{{z}}} ∧ ⟪t, ⟪{l}, n⟫⟫ ∈ ( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k (( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k )))
60		snex 4112	. . . . . . . . . . . . . . . . 17 ⊢ {{{z}}} ∈ V
61		opkeq1 4060	. . . . . . . . . . . . . . . . . 18 ⊢ (t = {{{z}}} → ⟪t, ⟪{l}, n⟫⟫ = ⟪{{{z}}}, ⟪{l}, n⟫⟫)
62	61	eleq1d 2419	. . . . . . . . . . . . . . . . 17 ⊢ (t = {{{z}}} → (⟪t, ⟪{l}, n⟫⟫ ∈ ( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k (( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) ↔ ⟪{{{z}}}, ⟪{l}, n⟫⟫ ∈ ( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k (( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k )))
63	60, 62	ceqsexv 2895	. . . . . . . . . . . . . . . 16 ⊢ (∃t(t = {{{z}}} ∧ ⟪t, ⟪{l}, n⟫⟫ ∈ ( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k (( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k )) ↔ ⟪{{{z}}}, ⟪{l}, n⟫⟫ ∈ ( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k (( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ))
64		elin 3220	. . . . . . . . . . . . . . . 16 ⊢ (⟪{{{z}}}, ⟪{l}, n⟫⟫ ∈ ( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k (( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) ↔ (⟪{{{z}}}, ⟪{l}, n⟫⟫ ∈ Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k (( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∧ ⟪{{{z}}}, ⟪{l}, n⟫⟫ ∈ Ins2_k S_k ))
65		snex 4112	. . . . . . . . . . . . . . . . . . 19 ⊢ {z} ∈ V
66	65, 1, 7	otkelins3k 4257	. . . . . . . . . . . . . . . . . 18 ⊢ (⟪{{{z}}}, ⟪{l}, n⟫⟫ ∈ Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k (( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ↔ ⟪{z}, {l}⟫ ∈ SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k (( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c))
67		vex 2863	. . . . . . . . . . . . . . . . . . 19 ⊢ z ∈ V
68	67, 6	opksnelsik 4266	. . . . . . . . . . . . . . . . . 18 ⊢ (⟪{z}, {l}⟫ ∈ SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k (( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ↔ ⟪z, l⟫ ∈ ∼ (( Ins3_k S_k ⊕ Ins2_k (( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c))
69		opkex 4114	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ⟪z, l⟫ ∈ V
70	69	elimak 4260	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (⟪z, l⟫ ∈ (( Ins3_k S_k ⊕ Ins2_k (( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ↔ ∃t ∈ ℘₁ ℘₁1_c⟪t, ⟪z, l⟫⟫ ∈ ( Ins3_k S_k ⊕ Ins2_k (( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c)))
71		elpw121c 4149	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (t ∈ ℘₁℘₁1_c ↔ ∃x t = {{{x}}})
72	71	anbi1i 676	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((t ∈ ℘₁℘₁1_c ∧ ⟪t, ⟪z, l⟫⟫ ∈ ( Ins3_k S_k ⊕ Ins2_k (( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c))) ↔ (∃x t = {{{x}}} ∧ ⟪t, ⟪z, l⟫⟫ ∈ ( Ins3_k S_k ⊕ Ins2_k (( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c))))
73		19.41v 1901	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (∃x(t = {{{x}}} ∧ ⟪t, ⟪z, l⟫⟫ ∈ ( Ins3_k S_k ⊕ Ins2_k (( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c))) ↔ (∃x t = {{{x}}} ∧ ⟪t, ⟪z, l⟫⟫ ∈ ( Ins3_k S_k ⊕ Ins2_k (( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c))))
74	72, 73	bitr4i 243	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((t ∈ ℘₁℘₁1_c ∧ ⟪t, ⟪z, l⟫⟫ ∈ ( Ins3_k S_k ⊕ Ins2_k (( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c))) ↔ ∃x(t = {{{x}}} ∧ ⟪t, ⟪z, l⟫⟫ ∈ ( Ins3_k S_k ⊕ Ins2_k (( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c))))
75	74	exbii 1582	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∃t(t ∈ ℘₁℘₁1_c ∧ ⟪t, ⟪z, l⟫⟫ ∈ ( Ins3_k S_k ⊕ Ins2_k (( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c))) ↔ ∃t∃x(t = {{{x}}} ∧ ⟪t, ⟪z, l⟫⟫ ∈ ( Ins3_k S_k ⊕ Ins2_k (( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c))))
76		df-rex 2621	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∃t ∈ ℘₁ ℘₁1_c⟪t, ⟪z, l⟫⟫ ∈ ( Ins3_k S_k ⊕ Ins2_k (( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c)) ↔ ∃t(t ∈ ℘₁℘₁1_c ∧ ⟪t, ⟪z, l⟫⟫ ∈ ( Ins3_k S_k ⊕ Ins2_k (( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c))))
77		excom 1741	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∃x∃t(t = {{{x}}} ∧ ⟪t, ⟪z, l⟫⟫ ∈ ( Ins3_k S_k ⊕ Ins2_k (( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c))) ↔ ∃t∃x(t = {{{x}}} ∧ ⟪t, ⟪z, l⟫⟫ ∈ ( Ins3_k S_k ⊕ Ins2_k (( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c))))
78	75, 76, 77	3bitr4i 268	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∃t ∈ ℘₁ ℘₁1_c⟪t, ⟪z, l⟫⟫ ∈ ( Ins3_k S_k ⊕ Ins2_k (( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c)) ↔ ∃x∃t(t = {{{x}}} ∧ ⟪t, ⟪z, l⟫⟫ ∈ ( Ins3_k S_k ⊕ Ins2_k (( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c))))
79		snex 4112	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ {{{x}}} ∈ V
80		opkeq1 4060	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (t = {{{x}}} → ⟪t, ⟪z, l⟫⟫ = ⟪{{{x}}}, ⟪z, l⟫⟫)
81	80	eleq1d 2419	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (t = {{{x}}} → (⟪t, ⟪z, l⟫⟫ ∈ ( Ins3_k S_k ⊕ Ins2_k (( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c)) ↔ ⟪{{{x}}}, ⟪z, l⟫⟫ ∈ ( Ins3_k S_k ⊕ Ins2_k (( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c))))
82	79, 81	ceqsexv 2895	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (∃t(t = {{{x}}} ∧ ⟪t, ⟪z, l⟫⟫ ∈ ( Ins3_k S_k ⊕ Ins2_k (( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c))) ↔ ⟪{{{x}}}, ⟪z, l⟫⟫ ∈ ( Ins3_k S_k ⊕ Ins2_k (( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c)))
83		elsymdif 3224	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (⟪{{{x}}}, ⟪z, l⟫⟫ ∈ ( Ins3_k S_k ⊕ Ins2_k (( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c)) ↔ ¬ (⟪{{{x}}}, ⟪z, l⟫⟫ ∈ Ins3_k S_k ↔ ⟪{{{x}}}, ⟪z, l⟫⟫ ∈ Ins2_k (( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c)))
84	20, 67, 6	otkelins3k 4257	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (⟪{{{x}}}, ⟪z, l⟫⟫ ∈ Ins3_k S_k ↔ ⟪{x}, z⟫ ∈ S_k )
85	28, 67	elssetk 4271	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (⟪{x}, z⟫ ∈ S_k ↔ x ∈ z)
86	84, 85	bitri 240	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (⟪{{{x}}}, ⟪z, l⟫⟫ ∈ Ins3_k S_k ↔ x ∈ z)
87		opkex 4114	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ⟪{x}, l⟫ ∈ V
88	87	elimak 4260	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (⟪{x}, l⟫ ∈ (( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ↔ ∃t ∈ ℘₁ ℘₁1_c⟪t, ⟪{x}, l⟫⟫ ∈ ( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) “_k ℘₁℘₁1_c)))
89		elpw121c 4149	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (t ∈ ℘₁℘₁1_c ↔ ∃b t = {{{b}}})
90	89	anbi1i 676	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((t ∈ ℘₁℘₁1_c ∧ ⟪t, ⟪{x}, l⟫⟫ ∈ ( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) “_k ℘₁℘₁1_c))) ↔ (∃b t = {{{b}}} ∧ ⟪t, ⟪{x}, l⟫⟫ ∈ ( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) “_k ℘₁℘₁1_c))))
91		19.41v 1901	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (∃b(t = {{{b}}} ∧ ⟪t, ⟪{x}, l⟫⟫ ∈ ( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) “_k ℘₁℘₁1_c))) ↔ (∃b t = {{{b}}} ∧ ⟪t, ⟪{x}, l⟫⟫ ∈ ( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) “_k ℘₁℘₁1_c))))
92	90, 91	bitr4i 243	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((t ∈ ℘₁℘₁1_c ∧ ⟪t, ⟪{x}, l⟫⟫ ∈ ( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) “_k ℘₁℘₁1_c))) ↔ ∃b(t = {{{b}}} ∧ ⟪t, ⟪{x}, l⟫⟫ ∈ ( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) “_k ℘₁℘₁1_c))))
93	92	exbii 1582	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (∃t(t ∈ ℘₁℘₁1_c ∧ ⟪t, ⟪{x}, l⟫⟫ ∈ ( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) “_k ℘₁℘₁1_c))) ↔ ∃t∃b(t = {{{b}}} ∧ ⟪t, ⟪{x}, l⟫⟫ ∈ ( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) “_k ℘₁℘₁1_c))))
94		df-rex 2621	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (∃t ∈ ℘₁ ℘₁1_c⟪t, ⟪{x}, l⟫⟫ ∈ ( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) “_k ℘₁℘₁1_c)) ↔ ∃t(t ∈ ℘₁℘₁1_c ∧ ⟪t, ⟪{x}, l⟫⟫ ∈ ( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) “_k ℘₁℘₁1_c))))
95		excom 1741	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (∃b∃t(t = {{{b}}} ∧ ⟪t, ⟪{x}, l⟫⟫ ∈ ( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) “_k ℘₁℘₁1_c))) ↔ ∃t∃b(t = {{{b}}} ∧ ⟪t, ⟪{x}, l⟫⟫ ∈ ( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) “_k ℘₁℘₁1_c))))
96	93, 94, 95	3bitr4i 268	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (∃t ∈ ℘₁ ℘₁1_c⟪t, ⟪{x}, l⟫⟫ ∈ ( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) “_k ℘₁℘₁1_c)) ↔ ∃b∃t(t = {{{b}}} ∧ ⟪t, ⟪{x}, l⟫⟫ ∈ ( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) “_k ℘₁℘₁1_c))))
97		snex 4112	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ {{{b}}} ∈ V
98		opkeq1 4060	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (t = {{{b}}} → ⟪t, ⟪{x}, l⟫⟫ = ⟪{{{b}}}, ⟪{x}, l⟫⟫)
99	98	eleq1d 2419	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (t = {{{b}}} → (⟪t, ⟪{x}, l⟫⟫ ∈ ( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) “_k ℘₁℘₁1_c)) ↔ ⟪{{{b}}}, ⟪{x}, l⟫⟫ ∈ ( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) “_k ℘₁℘₁1_c))))
100	97, 99	ceqsexv 2895	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (∃t(t = {{{b}}} ∧ ⟪t, ⟪{x}, l⟫⟫ ∈ ( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) “_k ℘₁℘₁1_c))) ↔ ⟪{{{b}}}, ⟪{x}, l⟫⟫ ∈ ( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) “_k ℘₁℘₁1_c)))
101		elin 3220	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (⟪{{{b}}}, ⟪{x}, l⟫⟫ ∈ ( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) “_k ℘₁℘₁1_c)) ↔ (⟪{{{b}}}, ⟪{x}, l⟫⟫ ∈ Ins2_k S_k ∧ ⟪{{{b}}}, ⟪{x}, l⟫⟫ ∈ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) “_k ℘₁℘₁1_c)))
102		snex 4112	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ {b} ∈ V
103	102, 20, 6	otkelins2k 4256	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (⟪{{{b}}}, ⟪{x}, l⟫⟫ ∈ Ins2_k S_k ↔ ⟪{b}, l⟫ ∈ S_k )
104		vex 2863	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ b ∈ V
105	104, 6	elssetk 4271	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (⟪{b}, l⟫ ∈ S_k ↔ b ∈ l)
106	103, 105	bitri 240	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (⟪{{{b}}}, ⟪{x}, l⟫⟫ ∈ Ins2_k S_k ↔ b ∈ l)
107	102, 20, 6	otkelins3k 4257	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (⟪{{{b}}}, ⟪{x}, l⟫⟫ ∈ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) “_k ℘₁℘₁1_c) ↔ ⟪{b}, {x}⟫ ∈ SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) “_k ℘₁℘₁1_c))
108	104, 28	opksnelsik 4266	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (⟪{b}, {x}⟫ ∈ SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) “_k ℘₁℘₁1_c) ↔ ⟪b, x⟫ ∈ ∼ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) “_k ℘₁℘₁1_c))
109		alex 1572	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (∀z(z ∈ x ↔ z ∈ (b ∪ {y})) ↔ ¬ ∃z ¬ (z ∈ x ↔ z ∈ (b ∪ {y})))
110		dfcleq 2347	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (x = (b ∪ {y}) ↔ ∀z(z ∈ x ↔ z ∈ (b ∪ {y})))
111		opkex 4114	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ⟪b, x⟫ ∈ V
112	111	elcompl 3226	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (⟪b, x⟫ ∈ ∼ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) “_k ℘₁℘₁1_c) ↔ ¬ ⟪b, x⟫ ∈ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) “_k ℘₁℘₁1_c))
113	111	elimak 4260	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (⟪b, x⟫ ∈ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) “_k ℘₁℘₁1_c) ↔ ∃t ∈ ℘₁ ℘₁1_c⟪t, ⟪b, x⟫⟫ ∈ ( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))))
114	52	anbi1i 676	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((t ∈ ℘₁℘₁1_c ∧ ⟪t, ⟪b, x⟫⟫ ∈ ( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V)))) ↔ (∃z t = {{{z}}} ∧ ⟪t, ⟪b, x⟫⟫ ∈ ( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V)))))
115		19.41v 1901	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (∃z(t = {{{z}}} ∧ ⟪t, ⟪b, x⟫⟫ ∈ ( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V)))) ↔ (∃z t = {{{z}}} ∧ ⟪t, ⟪b, x⟫⟫ ∈ ( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V)))))
116	114, 115	bitr4i 243	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((t ∈ ℘₁℘₁1_c ∧ ⟪t, ⟪b, x⟫⟫ ∈ ( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V)))) ↔ ∃z(t = {{{z}}} ∧ ⟪t, ⟪b, x⟫⟫ ∈ ( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V)))))
117	116	exbii 1582	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (∃t(t ∈ ℘₁℘₁1_c ∧ ⟪t, ⟪b, x⟫⟫ ∈ ( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V)))) ↔ ∃t∃z(t = {{{z}}} ∧ ⟪t, ⟪b, x⟫⟫ ∈ ( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V)))))
118		df-rex 2621	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (∃t ∈ ℘₁ ℘₁1_c⟪t, ⟪b, x⟫⟫ ∈ ( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) ↔ ∃t(t ∈ ℘₁℘₁1_c ∧ ⟪t, ⟪b, x⟫⟫ ∈ ( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V)))))
119		excom 1741	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (∃z∃t(t = {{{z}}} ∧ ⟪t, ⟪b, x⟫⟫ ∈ ( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V)))) ↔ ∃t∃z(t = {{{z}}} ∧ ⟪t, ⟪b, x⟫⟫ ∈ ( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V)))))
120	117, 118, 119	3bitr4i 268	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (∃t ∈ ℘₁ ℘₁1_c⟪t, ⟪b, x⟫⟫ ∈ ( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) ↔ ∃z∃t(t = {{{z}}} ∧ ⟪t, ⟪b, x⟫⟫ ∈ ( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V)))))
121		opkeq1 4060	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (t = {{{z}}} → ⟪t, ⟪b, x⟫⟫ = ⟪{{{z}}}, ⟪b, x⟫⟫)
122	121	eleq1d 2419	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (t = {{{z}}} → (⟪t, ⟪b, x⟫⟫ ∈ ( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) ↔ ⟪{{{z}}}, ⟪b, x⟫⟫ ∈ ( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V)))))
123	60, 122	ceqsexv 2895	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (∃t(t = {{{z}}} ∧ ⟪t, ⟪b, x⟫⟫ ∈ ( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V)))) ↔ ⟪{{{z}}}, ⟪b, x⟫⟫ ∈ ( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))))
124		elsymdif 3224	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (⟪{{{z}}}, ⟪b, x⟫⟫ ∈ ( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) ↔ ¬ (⟪{{{z}}}, ⟪b, x⟫⟫ ∈ Ins2_k S_k ↔ ⟪{{{z}}}, ⟪b, x⟫⟫ ∈ Ins3_k ( S_k ∪ ({{y}} ×_k V))))
125	65, 104, 28	otkelins2k 4256	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (⟪{{{z}}}, ⟪b, x⟫⟫ ∈ Ins2_k S_k ↔ ⟪{z}, x⟫ ∈ S_k )
126	67, 28	elssetk 4271	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (⟪{z}, x⟫ ∈ S_k ↔ z ∈ x)
127	125, 126	bitri 240	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (⟪{{{z}}}, ⟪b, x⟫⟫ ∈ Ins2_k S_k ↔ z ∈ x)
128	65, 104, 28	otkelins3k 4257	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (⟪{{{z}}}, ⟪b, x⟫⟫ ∈ Ins3_k ( S_k ∪ ({{y}} ×_k V)) ↔ ⟪{z}, b⟫ ∈ ( S_k ∪ ({{y}} ×_k V)))
129	67, 104	elssetk 4271	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (⟪{z}, b⟫ ∈ S_k ↔ z ∈ b)
130	65	elsnc 3757	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ ({z} ∈ {{y}} ↔ {z} = {y})
131	67	sneqb 3877	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ ({z} = {y} ↔ z = y)
132	130, 131	bitri 240	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ ({z} ∈ {{y}} ↔ z = y)
133	65, 104	opkelxpk 4249	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (⟪{z}, b⟫ ∈ ({{y}} ×_k V) ↔ ({z} ∈ {{y}} ∧ b ∈ V))
134	104, 133	mpbiran2 885	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (⟪{z}, b⟫ ∈ ({{y}} ×_k V) ↔ {z} ∈ {{y}})
135	67	elsnc 3757	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (z ∈ {y} ↔ z = y)
136	132, 134, 135	3bitr4i 268	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (⟪{z}, b⟫ ∈ ({{y}} ×_k V) ↔ z ∈ {y})
137	129, 136	orbi12i 507	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ ((⟪{z}, b⟫ ∈ S_k ∨ ⟪{z}, b⟫ ∈ ({{y}} ×_k V)) ↔ (z ∈ b ∨ z ∈ {y}))
138		elun 3221	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (⟪{z}, b⟫ ∈ ( S_k ∪ ({{y}} ×_k V)) ↔ (⟪{z}, b⟫ ∈ S_k ∨ ⟪{z}, b⟫ ∈ ({{y}} ×_k V)))
139		elun 3221	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (z ∈ (b ∪ {y}) ↔ (z ∈ b ∨ z ∈ {y}))
140	137, 138, 139	3bitr4i 268	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (⟪{z}, b⟫ ∈ ( S_k ∪ ({{y}} ×_k V)) ↔ z ∈ (b ∪ {y}))
141	128, 140	bitri 240	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (⟪{{{z}}}, ⟪b, x⟫⟫ ∈ Ins3_k ( S_k ∪ ({{y}} ×_k V)) ↔ z ∈ (b ∪ {y}))
142	127, 141	bibi12i 306	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((⟪{{{z}}}, ⟪b, x⟫⟫ ∈ Ins2_k S_k ↔ ⟪{{{z}}}, ⟪b, x⟫⟫ ∈ Ins3_k ( S_k ∪ ({{y}} ×_k V))) ↔ (z ∈ x ↔ z ∈ (b ∪ {y})))
143	124, 142	xchbinx 301	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (⟪{{{z}}}, ⟪b, x⟫⟫ ∈ ( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) ↔ ¬ (z ∈ x ↔ z ∈ (b ∪ {y})))
144	123, 143	bitri 240	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (∃t(t = {{{z}}} ∧ ⟪t, ⟪b, x⟫⟫ ∈ ( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V)))) ↔ ¬ (z ∈ x ↔ z ∈ (b ∪ {y})))
145	144	exbii 1582	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (∃z∃t(t = {{{z}}} ∧ ⟪t, ⟪b, x⟫⟫ ∈ ( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V)))) ↔ ∃z ¬ (z ∈ x ↔ z ∈ (b ∪ {y})))
146	113, 120, 145	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (⟪b, x⟫ ∈ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) “_k ℘₁℘₁1_c) ↔ ∃z ¬ (z ∈ x ↔ z ∈ (b ∪ {y})))
147	112, 146	xchbinx 301	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (⟪b, x⟫ ∈ ∼ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) “_k ℘₁℘₁1_c) ↔ ¬ ∃z ¬ (z ∈ x ↔ z ∈ (b ∪ {y})))
148	109, 110, 147	3bitr4ri 269	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (⟪b, x⟫ ∈ ∼ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) “_k ℘₁℘₁1_c) ↔ x = (b ∪ {y}))
149	107, 108, 148	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (⟪{{{b}}}, ⟪{x}, l⟫⟫ ∈ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) “_k ℘₁℘₁1_c) ↔ x = (b ∪ {y}))
150	106, 149	anbi12i 678	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((⟪{{{b}}}, ⟪{x}, l⟫⟫ ∈ Ins2_k S_k ∧ ⟪{{{b}}}, ⟪{x}, l⟫⟫ ∈ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) “_k ℘₁℘₁1_c)) ↔ (b ∈ l ∧ x = (b ∪ {y})))
151	100, 101, 150	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (∃t(t = {{{b}}} ∧ ⟪t, ⟪{x}, l⟫⟫ ∈ ( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) “_k ℘₁℘₁1_c))) ↔ (b ∈ l ∧ x = (b ∪ {y})))
152	151	exbii 1582	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (∃b∃t(t = {{{b}}} ∧ ⟪t, ⟪{x}, l⟫⟫ ∈ ( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) “_k ℘₁℘₁1_c))) ↔ ∃b(b ∈ l ∧ x = (b ∪ {y})))
153	88, 96, 152	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (⟪{x}, l⟫ ∈ (( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ↔ ∃b(b ∈ l ∧ x = (b ∪ {y})))
154	20, 67, 6	otkelins2k 4256	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (⟪{{{x}}}, ⟪z, l⟫⟫ ∈ Ins2_k (( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ↔ ⟪{x}, l⟫ ∈ (( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c))
155		df-rex 2621	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (∃b ∈ l x = (b ∪ {y}) ↔ ∃b(b ∈ l ∧ x = (b ∪ {y})))
156	153, 154, 155	3bitr4i 268	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (⟪{{{x}}}, ⟪z, l⟫⟫ ∈ Ins2_k (( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ↔ ∃b ∈ l x = (b ∪ {y}))
157	86, 156	bibi12i 306	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((⟪{{{x}}}, ⟪z, l⟫⟫ ∈ Ins3_k S_k ↔ ⟪{{{x}}}, ⟪z, l⟫⟫ ∈ Ins2_k (( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c)) ↔ (x ∈ z ↔ ∃b ∈ l x = (b ∪ {y})))
158	83, 157	xchbinx 301	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (⟪{{{x}}}, ⟪z, l⟫⟫ ∈ ( Ins3_k S_k ⊕ Ins2_k (( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c)) ↔ ¬ (x ∈ z ↔ ∃b ∈ l x = (b ∪ {y})))
159	82, 158	bitri 240	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∃t(t = {{{x}}} ∧ ⟪t, ⟪z, l⟫⟫ ∈ ( Ins3_k S_k ⊕ Ins2_k (( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c))) ↔ ¬ (x ∈ z ↔ ∃b ∈ l x = (b ∪ {y})))
160	159	exbii 1582	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∃x∃t(t = {{{x}}} ∧ ⟪t, ⟪z, l⟫⟫ ∈ ( Ins3_k S_k ⊕ Ins2_k (( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c))) ↔ ∃x ¬ (x ∈ z ↔ ∃b ∈ l x = (b ∪ {y})))
161	70, 78, 160	3bitri 262	. . . . . . . . . . . . . . . . . . . 20 ⊢ (⟪z, l⟫ ∈ (( Ins3_k S_k ⊕ Ins2_k (( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ↔ ∃x ¬ (x ∈ z ↔ ∃b ∈ l x = (b ∪ {y})))
162	161	notbii 287	. . . . . . . . . . . . . . . . . . 19 ⊢ (¬ ⟪z, l⟫ ∈ (( Ins3_k S_k ⊕ Ins2_k (( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ↔ ¬ ∃x ¬ (x ∈ z ↔ ∃b ∈ l x = (b ∪ {y})))
163	69	elcompl 3226	. . . . . . . . . . . . . . . . . . 19 ⊢ (⟪z, l⟫ ∈ ∼ (( Ins3_k S_k ⊕ Ins2_k (( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ↔ ¬ ⟪z, l⟫ ∈ (( Ins3_k S_k ⊕ Ins2_k (( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c))
164		alex 1572	. . . . . . . . . . . . . . . . . . 19 ⊢ (∀x(x ∈ z ↔ ∃b ∈ l x = (b ∪ {y})) ↔ ¬ ∃x ¬ (x ∈ z ↔ ∃b ∈ l x = (b ∪ {y})))
165	162, 163, 164	3bitr4i 268	. . . . . . . . . . . . . . . . . 18 ⊢ (⟪z, l⟫ ∈ ∼ (( Ins3_k S_k ⊕ Ins2_k (( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ↔ ∀x(x ∈ z ↔ ∃b ∈ l x = (b ∪ {y})))
166	66, 68, 165	3bitri 262	. . . . . . . . . . . . . . . . 17 ⊢ (⟪{{{z}}}, ⟪{l}, n⟫⟫ ∈ Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k (( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ↔ ∀x(x ∈ z ↔ ∃b ∈ l x = (b ∪ {y})))
167	65, 1, 7	otkelins2k 4256	. . . . . . . . . . . . . . . . . 18 ⊢ (⟪{{{z}}}, ⟪{l}, n⟫⟫ ∈ Ins2_k S_k ↔ ⟪{z}, n⟫ ∈ S_k )
168	67, 7	elssetk 4271	. . . . . . . . . . . . . . . . . 18 ⊢ (⟪{z}, n⟫ ∈ S_k ↔ z ∈ n)
169	167, 168	bitri 240	. . . . . . . . . . . . . . . . 17 ⊢ (⟪{{{z}}}, ⟪{l}, n⟫⟫ ∈ Ins2_k S_k ↔ z ∈ n)
170	166, 169	anbi12i 678	. . . . . . . . . . . . . . . 16 ⊢ ((⟪{{{z}}}, ⟪{l}, n⟫⟫ ∈ Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k (( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∧ ⟪{{{z}}}, ⟪{l}, n⟫⟫ ∈ Ins2_k S_k ) ↔ (∀x(x ∈ z ↔ ∃b ∈ l x = (b ∪ {y})) ∧ z ∈ n))
171	63, 64, 170	3bitri 262	. . . . . . . . . . . . . . 15 ⊢ (∃t(t = {{{z}}} ∧ ⟪t, ⟪{l}, n⟫⟫ ∈ ( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k (( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k )) ↔ (∀x(x ∈ z ↔ ∃b ∈ l x = (b ∪ {y})) ∧ z ∈ n))
172	171	exbii 1582	. . . . . . . . . . . . . 14 ⊢ (∃z∃t(t = {{{z}}} ∧ ⟪t, ⟪{l}, n⟫⟫ ∈ ( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k (( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k )) ↔ ∃z(∀x(x ∈ z ↔ ∃b ∈ l x = (b ∪ {y})) ∧ z ∈ n))
173	51, 59, 172	3bitri 262	. . . . . . . . . . . . 13 ⊢ (⟪{l}, n⟫ ∈ (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k (( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ↔ ∃z(∀x(x ∈ z ↔ ∃b ∈ l x = (b ∪ {y})) ∧ z ∈ n))
174	48, 49, 173	3bitr4ri 269	. . . . . . . . . . . 12 ⊢ (⟪{l}, n⟫ ∈ (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k (( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ↔ {x ∣ ∃b ∈ l x = (b ∪ {y})} ∈ n)
175	174	notbii 287	. . . . . . . . . . 11 ⊢ (¬ ⟪{l}, n⟫ ∈ (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k (( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ↔ ¬ {x ∣ ∃b ∈ l x = (b ∪ {y})} ∈ n)
176	45, 175	anbi12i 678	. . . . . . . . . 10 ⊢ ((⟪{l}, n⟫ ∈ ( ∼ ℘₁(((℘₁{z ∣ y ∈ z} ×_k V) ∩ S_k ) “_k 1_c) ×_k V) ∧ ¬ ⟪{l}, n⟫ ∈ (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k (( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c)) ↔ (y ∈ ∼ ∪l ∧ ¬ {x ∣ ∃b ∈ l x = (b ∪ {y})} ∈ n))
177		annim 414	. . . . . . . . . 10 ⊢ ((y ∈ ∼ ∪l ∧ ¬ {x ∣ ∃b ∈ l x = (b ∪ {y})} ∈ n) ↔ ¬ (y ∈ ∼ ∪l → {x ∣ ∃b ∈ l x = (b ∪ {y})} ∈ n))
178	9, 176, 177	3bitri 262	. . . . . . . . 9 ⊢ (⟪{l}, n⟫ ∈ (( ∼ ℘₁(((℘₁{z ∣ y ∈ z} ×_k V) ∩ S_k ) “_k 1_c) ×_k V) ∖ (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k (( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c)) ↔ ¬ (y ∈ ∼ ∪l → {x ∣ ∃b ∈ l x = (b ∪ {y})} ∈ n))
179	8, 178	anbi12i 678	. . . . . . . 8 ⊢ ((⟪{l}, n⟫ ∈ S_k ∧ ⟪{l}, n⟫ ∈ (( ∼ ℘₁(((℘₁{z ∣ y ∈ z} ×_k V) ∩ S_k ) “_k 1_c) ×_k V) ∖ (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k (( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c))) ↔ (l ∈ n ∧ ¬ (y ∈ ∼ ∪l → {x ∣ ∃b ∈ l x = (b ∪ {y})} ∈ n)))
180	4, 5, 179	3bitri 262	. . . . . . 7 ⊢ (∃t(t = {l} ∧ ⟪t, n⟫ ∈ ( S_k ∩ (( ∼ ℘₁(((℘₁{z ∣ y ∈ z} ×_k V) ∩ S_k ) “_k 1_c) ×_k V) ∖ (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k (( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c)))) ↔ (l ∈ n ∧ ¬ (y ∈ ∼ ∪l → {x ∣ ∃b ∈ l x = (b ∪ {y})} ∈ n)))
181	180	exbii 1582	. . . . . 6 ⊢ (∃l∃t(t = {l} ∧ ⟪t, n⟫ ∈ ( S_k ∩ (( ∼ ℘₁(((℘₁{z ∣ y ∈ z} ×_k V) ∩ S_k ) “_k 1_c) ×_k V) ∖ (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k (( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c)))) ↔ ∃l(l ∈ n ∧ ¬ (y ∈ ∼ ∪l → {x ∣ ∃b ∈ l x = (b ∪ {y})} ∈ n)))
182	7	elimak 4260	. . . . . . 7 ⊢ (n ∈ (( S_k ∩ (( ∼ ℘₁(((℘₁{z ∣ y ∈ z} ×_k V) ∩ S_k ) “_k 1_c) ×_k V) ∖ (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k (( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c))) “_k 1_c) ↔ ∃t ∈ 1_c ⟪t, n⟫ ∈ ( S_k ∩ (( ∼ ℘₁(((℘₁{z ∣ y ∈ z} ×_k V) ∩ S_k ) “_k 1_c) ×_k V) ∖ (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k (( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c))))
183		el1c 4140	. . . . . . . . . . 11 ⊢ (t ∈ 1_c ↔ ∃l t = {l})
184	183	anbi1i 676	. . . . . . . . . 10 ⊢ ((t ∈ 1_c ∧ ⟪t, n⟫ ∈ ( S_k ∩ (( ∼ ℘₁(((℘₁{z ∣ y ∈ z} ×_k V) ∩ S_k ) “_k 1_c) ×_k V) ∖ (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k (( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c)))) ↔ (∃l t = {l} ∧ ⟪t, n⟫ ∈ ( S_k ∩ (( ∼ ℘₁(((℘₁{z ∣ y ∈ z} ×_k V) ∩ S_k ) “_k 1_c) ×_k V) ∖ (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k (( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c)))))
185		19.41v 1901	. . . . . . . . . 10 ⊢ (∃l(t = {l} ∧ ⟪t, n⟫ ∈ ( S_k ∩ (( ∼ ℘₁(((℘₁{z ∣ y ∈ z} ×_k V) ∩ S_k ) “_k 1_c) ×_k V) ∖ (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k (( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c)))) ↔ (∃l t = {l} ∧ ⟪t, n⟫ ∈ ( S_k ∩ (( ∼ ℘₁(((℘₁{z ∣ y ∈ z} ×_k V) ∩ S_k ) “_k 1_c) ×_k V) ∖ (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k (( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c)))))
186	184, 185	bitr4i 243	. . . . . . . . 9 ⊢ ((t ∈ 1_c ∧ ⟪t, n⟫ ∈ ( S_k ∩ (( ∼ ℘₁(((℘₁{z ∣ y ∈ z} ×_k V) ∩ S_k ) “_k 1_c) ×_k V) ∖ (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k (( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c)))) ↔ ∃l(t = {l} ∧ ⟪t, n⟫ ∈ ( S_k ∩ (( ∼ ℘₁(((℘₁{z ∣ y ∈ z} ×_k V) ∩ S_k ) “_k 1_c) ×_k V) ∖ (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k (( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c)))))
187	186	exbii 1582	. . . . . . . 8 ⊢ (∃t(t ∈ 1_c ∧ ⟪t, n⟫ ∈ ( S_k ∩ (( ∼ ℘₁(((℘₁{z ∣ y ∈ z} ×_k V) ∩ S_k ) “_k 1_c) ×_k V) ∖ (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k (( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c)))) ↔ ∃t∃l(t = {l} ∧ ⟪t, n⟫ ∈ ( S_k ∩ (( ∼ ℘₁(((℘₁{z ∣ y ∈ z} ×_k V) ∩ S_k ) “_k 1_c) ×_k V) ∖ (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k (( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c)))))
188		df-rex 2621	. . . . . . . 8 ⊢ (∃t ∈ 1_c ⟪t, n⟫ ∈ ( S_k ∩ (( ∼ ℘₁(((℘₁{z ∣ y ∈ z} ×_k V) ∩ S_k ) “_k 1_c) ×_k V) ∖ (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k (( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c))) ↔ ∃t(t ∈ 1_c ∧ ⟪t, n⟫ ∈ ( S_k ∩ (( ∼ ℘₁(((℘₁{z ∣ y ∈ z} ×_k V) ∩ S_k ) “_k 1_c) ×_k V) ∖ (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k (( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c)))))
189		excom 1741	. . . . . . . 8 ⊢ (∃l∃t(t = {l} ∧ ⟪t, n⟫ ∈ ( S_k ∩ (( ∼ ℘₁(((℘₁{z ∣ y ∈ z} ×_k V) ∩ S_k ) “_k 1_c) ×_k V) ∖ (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k (( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c)))) ↔ ∃t∃l(t = {l} ∧ ⟪t, n⟫ ∈ ( S_k ∩ (( ∼ ℘₁(((℘₁{z ∣ y ∈ z} ×_k V) ∩ S_k ) “_k 1_c) ×_k V) ∖ (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k (( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c)))))
190	187, 188, 189	3bitr4i 268	. . . . . . 7 ⊢ (∃t ∈ 1_c ⟪t, n⟫ ∈ ( S_k ∩ (( ∼ ℘₁(((℘₁{z ∣ y ∈ z} ×_k V) ∩ S_k ) “_k 1_c) ×_k V) ∖ (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k (( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c))) ↔ ∃l∃t(t = {l} ∧ ⟪t, n⟫ ∈ ( S_k ∩ (( ∼ ℘₁(((℘₁{z ∣ y ∈ z} ×_k V) ∩ S_k ) “_k 1_c) ×_k V) ∖ (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k (( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c)))))
191	182, 190	bitri 240	. . . . . 6 ⊢ (n ∈ (( S_k ∩ (( ∼ ℘₁(((℘₁{z ∣ y ∈ z} ×_k V) ∩ S_k ) “_k 1_c) ×_k V) ∖ (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k (( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c))) “_k 1_c) ↔ ∃l∃t(t = {l} ∧ ⟪t, n⟫ ∈ ( S_k ∩ (( ∼ ℘₁(((℘₁{z ∣ y ∈ z} ×_k V) ∩ S_k ) “_k 1_c) ×_k V) ∖ (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k (( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c)))))
192		df-rex 2621	. . . . . 6 ⊢ (∃l ∈ n ¬ (y ∈ ∼ ∪l → {x ∣ ∃b ∈ l x = (b ∪ {y})} ∈ n) ↔ ∃l(l ∈ n ∧ ¬ (y ∈ ∼ ∪l → {x ∣ ∃b ∈ l x = (b ∪ {y})} ∈ n)))
193	181, 191, 192	3bitr4i 268	. . . . 5 ⊢ (n ∈ (( S_k ∩ (( ∼ ℘₁(((℘₁{z ∣ y ∈ z} ×_k V) ∩ S_k ) “_k 1_c) ×_k V) ∖ (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k (( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c))) “_k 1_c) ↔ ∃l ∈ n ¬ (y ∈ ∼ ∪l → {x ∣ ∃b ∈ l x = (b ∪ {y})} ∈ n))
194	193	notbii 287	. . . 4 ⊢ (¬ n ∈ (( S_k ∩ (( ∼ ℘₁(((℘₁{z ∣ y ∈ z} ×_k V) ∩ S_k ) “_k 1_c) ×_k V) ∖ (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k (( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c))) “_k 1_c) ↔ ¬ ∃l ∈ n ¬ (y ∈ ∼ ∪l → {x ∣ ∃b ∈ l x = (b ∪ {y})} ∈ n))
195	7	elcompl 3226	. . . 4 ⊢ (n ∈ ∼ (( S_k ∩ (( ∼ ℘₁(((℘₁{z ∣ y ∈ z} ×_k V) ∩ S_k ) “_k 1_c) ×_k V) ∖ (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k (( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c))) “_k 1_c) ↔ ¬ n ∈ (( S_k ∩ (( ∼ ℘₁(((℘₁{z ∣ y ∈ z} ×_k V) ∩ S_k ) “_k 1_c) ×_k V) ∖ (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k (( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c))) “_k 1_c))
196		dfral2 2627	. . . 4 ⊢ (∀l ∈ n (y ∈ ∼ ∪l → {x ∣ ∃b ∈ l x = (b ∪ {y})} ∈ n) ↔ ¬ ∃l ∈ n ¬ (y ∈ ∼ ∪l → {x ∣ ∃b ∈ l x = (b ∪ {y})} ∈ n))
197	194, 195, 196	3bitr4i 268	. . 3 ⊢ (n ∈ ∼ (( S_k ∩ (( ∼ ℘₁(((℘₁{z ∣ y ∈ z} ×_k V) ∩ S_k ) “_k 1_c) ×_k V) ∖ (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k (( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c))) “_k 1_c) ↔ ∀l ∈ n (y ∈ ∼ ∪l → {x ∣ ∃b ∈ l x = (b ∪ {y})} ∈ n))
198	197	eqabi 2465	. 2 ⊢ ∼ (( S_k ∩ (( ∼ ℘₁(((℘₁{z ∣ y ∈ z} ×_k V) ∩ S_k ) “_k 1_c) ×_k V) ∖ (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k (( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c))) “_k 1_c) = {n ∣ ∀l ∈ n (y ∈ ∼ ∪l → {x ∣ ∃b ∈ l x = (b ∪ {y})} ∈ n)}
199		ssetkex 4295	. . . . 5 ⊢ S_k ∈ V
200		setswithex 4323	. . . . . . . . . . . . 13 ⊢ {z ∣ y ∈ z} ∈ V
201	200	pw1ex 4304	. . . . . . . . . . . 12 ⊢ ℘₁{z ∣ y ∈ z} ∈ V
202		vvex 4110	. . . . . . . . . . . 12 ⊢ V ∈ V
203	201, 202	xpkex 4290	. . . . . . . . . . 11 ⊢ (℘₁{z ∣ y ∈ z} ×_k V) ∈ V
204	203, 199	inex 4106	. . . . . . . . . 10 ⊢ ((℘₁{z ∣ y ∈ z} ×_k V) ∩ S_k ) ∈ V
205		1cex 4143	. . . . . . . . . 10 ⊢ 1_c ∈ V
206	204, 205	imakex 4301	. . . . . . . . 9 ⊢ (((℘₁{z ∣ y ∈ z} ×_k V) ∩ S_k ) “_k 1_c) ∈ V
207	206	pw1ex 4304	. . . . . . . 8 ⊢ ℘₁(((℘₁{z ∣ y ∈ z} ×_k V) ∩ S_k ) “_k 1_c) ∈ V
208	207	complex 4105	. . . . . . 7 ⊢ ∼ ℘₁(((℘₁{z ∣ y ∈ z} ×_k V) ∩ S_k ) “_k 1_c) ∈ V
209	208, 202	xpkex 4290	. . . . . 6 ⊢ ( ∼ ℘₁(((℘₁{z ∣ y ∈ z} ×_k V) ∩ S_k ) “_k 1_c) ×_k V) ∈ V
210	199	ins3kex 4309	. . . . . . . . . . . . 13 ⊢ Ins3_k S_k ∈ V
211	199	ins2kex 4308	. . . . . . . . . . . . . . . 16 ⊢ Ins2_k S_k ∈ V
212		snex 4112	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ {{y}} ∈ V
213	212, 202	xpkex 4290	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ({{y}} ×_k V) ∈ V
214	199, 213	unex 4107	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ( S_k ∪ ({{y}} ×_k V)) ∈ V
215	214	ins3kex 4309	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ins3_k ( S_k ∪ ({{y}} ×_k V)) ∈ V
216	211, 215	symdifex 4109	. . . . . . . . . . . . . . . . . . . 20 ⊢ ( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) ∈ V
217	205	pw1ex 4304	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ℘₁1_c ∈ V
218	217	pw1ex 4304	. . . . . . . . . . . . . . . . . . . 20 ⊢ ℘₁℘₁1_c ∈ V
219	216, 218	imakex 4301	. . . . . . . . . . . . . . . . . . 19 ⊢ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) “_k ℘₁℘₁1_c) ∈ V
220	219	complex 4105	. . . . . . . . . . . . . . . . . 18 ⊢ ∼ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) “_k ℘₁℘₁1_c) ∈ V
221	220	sikex 4298	. . . . . . . . . . . . . . . . 17 ⊢ SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) “_k ℘₁℘₁1_c) ∈ V
222	221	ins3kex 4309	. . . . . . . . . . . . . . . 16 ⊢ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) “_k ℘₁℘₁1_c) ∈ V
223	211, 222	inex 4106	. . . . . . . . . . . . . . 15 ⊢ ( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) “_k ℘₁℘₁1_c)) ∈ V
224	223, 218	imakex 4301	. . . . . . . . . . . . . 14 ⊢ (( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∈ V
225	224	ins2kex 4308	. . . . . . . . . . . . 13 ⊢ Ins2_k (( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∈ V
226	210, 225	symdifex 4109	. . . . . . . . . . . 12 ⊢ ( Ins3_k S_k ⊕ Ins2_k (( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c)) ∈ V
227	226, 218	imakex 4301	. . . . . . . . . . 11 ⊢ (( Ins3_k S_k ⊕ Ins2_k (( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∈ V
228	227	complex 4105	. . . . . . . . . 10 ⊢ ∼ (( Ins3_k S_k ⊕ Ins2_k (( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∈ V
229	228	sikex 4298	. . . . . . . . 9 ⊢ SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k (( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∈ V
230	229	ins3kex 4309	. . . . . . . 8 ⊢ Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k (( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∈ V
231	230, 211	inex 4106	. . . . . . 7 ⊢ ( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k (( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) ∈ V
232	231, 218	imakex 4301	. . . . . 6 ⊢ (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k (( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∈ V
233	209, 232	difex 4108	. . . . 5 ⊢ (( ∼ ℘₁(((℘₁{z ∣ y ∈ z} ×_k V) ∩ S_k ) “_k 1_c) ×_k V) ∖ (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k (( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c)) ∈ V
234	199, 233	inex 4106	. . . 4 ⊢ ( S_k ∩ (( ∼ ℘₁(((℘₁{z ∣ y ∈ z} ×_k V) ∩ S_k ) “_k 1_c) ×_k V) ∖ (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k (( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c))) ∈ V
235	234, 205	imakex 4301	. . 3 ⊢ (( S_k ∩ (( ∼ ℘₁(((℘₁{z ∣ y ∈ z} ×_k V) ∩ S_k ) “_k 1_c) ×_k V) ∖ (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k (( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c))) “_k 1_c) ∈ V
236	235	complex 4105	. 2 ⊢ ∼ (( S_k ∩ (( ∼ ℘₁(((℘₁{z ∣ y ∈ z} ×_k V) ∩ S_k ) “_k 1_c) ×_k V) ∖ (( Ins3_k SI_k ∼ (( Ins3_k S_k ⊕ Ins2_k (( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∪ ({{y}} ×_k V))) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c))) “_k 1_c) ∈ V
237	198, 236	eqeltrri 2424	1 ⊢ {n ∣ ∀l ∈ n (y ∈ ∼ ∪l → {x ∣ ∃b ∈ l x = (b ∪ {y})} ∈ n)} ∈ V

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ↔ wb 176 ∨ wo 357 ∧ wa 358 ∀wal 1540 ∃wex 1541 = wceq 1642 ∈ wcel 1710 {cab 2339 ∀wral 2615 ∃wrex 2616 Vcvv 2860 ∼ ccompl 3206 ∖ cdif 3207 ∪ cun 3208 ∩ cin 3209 ⊕ csymdif 3210 {csn 3738 ∪cuni 3892 ⟪copk 4058 1_cc1c 4135 ℘₁cpw1 4136 ×_k cxpk 4175 Ins2_k cins2k 4177 Ins3_k cins3k 4178 “_k cimak 4180 SI_k csik 4182 S_k cssetk 4184

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-14 1714 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-sset 4083 ax-si 4084 ax-ins2 4085 ax-ins3 4086 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-sbc 3048 df-nin 3212 df-compl 3213 df-in 3214 df-un 3215 df-dif 3216 df-symdif 3217 df-ss 3260 df-nul 3552 df-if 3664 df-pw 3725 df-sn 3742 df-pr 3743 df-uni 3893 df-opk 4059 df-1c 4137 df-pw1 4138 df-xpk 4186 df-cnvk 4187 df-ins2k 4188 df-ins3k 4189 df-imak 4190 df-p6 4192 df-sik 4193 df-ssetk 4194

This theorem is used by: nnadjoin 4521

W3C validator