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

 Description: Lemma for nnadjoin 4520. 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

Dummy variables t z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 snex 4111 . . . . . . . . 9 {l} V
2 opkeq1 4059 . . . . . . . . . 10 (t = {l} → ⟪t, n⟫ = ⟪{l}, n⟫)
32eleq1d 2419 . . . . . . . . 9 (t = {l} → (⟪t, n ( Sk ∩ (( ∼ 1(((1{z y z} ×k V) ∩ Sk ) “k 1c) ×k V) (( Ins3k SIk ∼ (( Ins3k SkIns2k (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) “k 111c)) “k 111c)) “k 111c) ∩ Ins2k Sk ) “k 111c))) ↔ ⟪{l}, n ( Sk ∩ (( ∼ 1(((1{z y z} ×k V) ∩ Sk ) “k 1c) ×k V) (( Ins3k SIk ∼ (( Ins3k SkIns2k (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) “k 111c)) “k 111c)) “k 111c) ∩ Ins2k Sk ) “k 111c)))))
41, 3ceqsexv 2894 . . . . . . . 8 (t(t = {l} t, n ( Sk ∩ (( ∼ 1(((1{z y z} ×k V) ∩ Sk ) “k 1c) ×k V) (( Ins3k SIk ∼ (( Ins3k SkIns2k (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) “k 111c)) “k 111c)) “k 111c) ∩ Ins2k Sk ) “k 111c)))) ↔ ⟪{l}, n ( Sk ∩ (( ∼ 1(((1{z y z} ×k V) ∩ Sk ) “k 1c) ×k V) (( Ins3k SIk ∼ (( Ins3k SkIns2k (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) “k 111c)) “k 111c)) “k 111c) ∩ Ins2k Sk ) “k 111c))))
5 elin 3219 . . . . . . . 8 (⟪{l}, n ( Sk ∩ (( ∼ 1(((1{z y z} ×k V) ∩ Sk ) “k 1c) ×k V) (( Ins3k SIk ∼ (( Ins3k SkIns2k (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) “k 111c)) “k 111c)) “k 111c) ∩ Ins2k Sk ) “k 111c))) ↔ (⟪{l}, n Sk ⟪{l}, n (( ∼ 1(((1{z y z} ×k V) ∩ Sk ) “k 1c) ×k V) (( Ins3k SIk ∼ (( Ins3k SkIns2k (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) “k 111c)) “k 111c)) “k 111c) ∩ Ins2k Sk ) “k 111c))))
6 vex 2862 . . . . . . . . . 10 l V
7 vex 2862 . . . . . . . . . 10 n V
86, 7elssetk 4270 . . . . . . . . 9 (⟪{l}, n Skl n)
9 eldif 3221 . . . . . . . . . 10 (⟪{l}, n (( ∼ 1(((1{z y z} ×k V) ∩ Sk ) “k 1c) ×k V) (( Ins3k SIk ∼ (( Ins3k SkIns2k (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) “k 111c)) “k 111c)) “k 111c) ∩ Ins2k Sk ) “k 111c)) ↔ (⟪{l}, n ( ∼ 1(((1{z y z} ×k V) ∩ Sk ) “k 1c) ×k V) ¬ ⟪{l}, n (( Ins3k SIk ∼ (( Ins3k SkIns2k (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) “k 111c)) “k 111c)) “k 111c) ∩ Ins2k Sk ) “k 111c)))
101elcompl 3225 . . . . . . . . . . . . 13 ({l} 1(((1{z y z} ×k V) ∩ Sk ) “k 1c) ↔ ¬ {l} 1(((1{z y z} ×k V) ∩ Sk ) “k 1c))
116elimak 4259 . . . . . . . . . . . . . . 15 (l (((1{z y z} ×k V) ∩ Sk ) “k 1c) ↔ t 1ct, l ((1{z y z} ×k V) ∩ Sk ))
12 el1c 4139 . . . . . . . . . . . . . . . . . . 19 (t 1cx t = {x})
1312anbi1i 676 . . . . . . . . . . . . . . . . . 18 ((t 1c t, l ((1{z y z} ×k V) ∩ Sk )) ↔ (x t = {x} t, l ((1{z y z} ×k V) ∩ Sk )))
14 19.41v 1901 . . . . . . . . . . . . . . . . . 18 (x(t = {x} t, l ((1{z y z} ×k V) ∩ Sk )) ↔ (x t = {x} t, l ((1{z y z} ×k V) ∩ Sk )))
1513, 14bitr4i 243 . . . . . . . . . . . . . . . . 17 ((t 1c t, l ((1{z y z} ×k V) ∩ Sk )) ↔ x(t = {x} t, l ((1{z y z} ×k V) ∩ Sk )))
1615exbii 1582 . . . . . . . . . . . . . . . 16 (t(t 1c t, l ((1{z y z} ×k V) ∩ Sk )) ↔ tx(t = {x} t, l ((1{z y z} ×k V) ∩ Sk )))
17 df-rex 2620 . . . . . . . . . . . . . . . 16 (t 1ct, l ((1{z y z} ×k V) ∩ Sk ) ↔ t(t 1c t, l ((1{z y z} ×k V) ∩ Sk )))
18 excom 1741 . . . . . . . . . . . . . . . 16 (xt(t = {x} t, l ((1{z y z} ×k V) ∩ Sk )) ↔ tx(t = {x} t, l ((1{z y z} ×k V) ∩ Sk )))
1916, 17, 183bitr4i 268 . . . . . . . . . . . . . . 15 (t 1ct, l ((1{z y z} ×k V) ∩ Sk ) ↔ xt(t = {x} t, l ((1{z y z} ×k V) ∩ Sk )))
20 snex 4111 . . . . . . . . . . . . . . . . . 18 {x} V
21 opkeq1 4059 . . . . . . . . . . . . . . . . . . 19 (t = {x} → ⟪t, l⟫ = ⟪{x}, l⟫)
2221eleq1d 2419 . . . . . . . . . . . . . . . . . 18 (t = {x} → (⟪t, l ((1{z y z} ×k V) ∩ Sk ) ↔ ⟪{x}, l ((1{z y z} ×k V) ∩ Sk )))
2320, 22ceqsexv 2894 . . . . . . . . . . . . . . . . 17 (t(t = {x} t, l ((1{z y z} ×k V) ∩ Sk )) ↔ ⟪{x}, l ((1{z y z} ×k V) ∩ Sk ))
24 elin 3219 . . . . . . . . . . . . . . . . 17 (⟪{x}, l ((1{z y z} ×k V) ∩ Sk ) ↔ (⟪{x}, l (1{z y z} ×k V) ⟪{x}, l Sk ))
2520, 6opkelxpk 4248 . . . . . . . . . . . . . . . . . . . 20 (⟪{x}, l (1{z y z} ×k V) ↔ ({x} 1{z y z} l V))
266, 25mpbiran2 885 . . . . . . . . . . . . . . . . . . 19 (⟪{x}, l (1{z y z} ×k V) ↔ {x} 1{z y z})
27 snelpw1 4146 . . . . . . . . . . . . . . . . . . 19 ({x} 1{z y z} ↔ x {z y z})
28 vex 2862 . . . . . . . . . . . . . . . . . . . 20 x V
29 elequ2 1715 . . . . . . . . . . . . . . . . . . . 20 (z = x → (y zy x))
3028, 29elab 2985 . . . . . . . . . . . . . . . . . . 19 (x {z y z} ↔ y x)
3126, 27, 303bitri 262 . . . . . . . . . . . . . . . . . 18 (⟪{x}, l (1{z y z} ×k V) ↔ y x)
3228, 6elssetk 4270 . . . . . . . . . . . . . . . . . 18 (⟪{x}, l Skx l)
3331, 32anbi12i 678 . . . . . . . . . . . . . . . . 17 ((⟪{x}, l (1{z y z} ×k V) ⟪{x}, l Sk ) ↔ (y x x l))
3423, 24, 333bitri 262 . . . . . . . . . . . . . . . 16 (t(t = {x} t, l ((1{z y z} ×k V) ∩ Sk )) ↔ (y x x l))
3534exbii 1582 . . . . . . . . . . . . . . 15 (xt(t = {x} t, l ((1{z y z} ×k V) ∩ Sk )) ↔ x(y x x l))
3611, 19, 353bitri 262 . . . . . . . . . . . . . 14 (l (((1{z y z} ×k V) ∩ Sk ) “k 1c) ↔ x(y x x l))
37 snelpw1 4146 . . . . . . . . . . . . . 14 ({l} 1(((1{z y z} ×k V) ∩ Sk ) “k 1c) ↔ l (((1{z y z} ×k V) ∩ Sk ) “k 1c))
38 eluni 3894 . . . . . . . . . . . . . 14 (y lx(y x x l))
3936, 37, 383bitr4i 268 . . . . . . . . . . . . 13 ({l} 1(((1{z y z} ×k V) ∩ Sk ) “k 1c) ↔ y l)
4010, 39xchbinx 301 . . . . . . . . . . . 12 ({l} 1(((1{z y z} ×k V) ∩ Sk ) “k 1c) ↔ ¬ y l)
411, 7opkelxpk 4248 . . . . . . . . . . . . 13 (⟪{l}, n ( ∼ 1(((1{z y z} ×k V) ∩ Sk ) “k 1c) ×k V) ↔ ({l} 1(((1{z y z} ×k V) ∩ Sk ) “k 1c) n V))
427, 41mpbiran2 885 . . . . . . . . . . . 12 (⟪{l}, n ( ∼ 1(((1{z y z} ×k V) ∩ Sk ) “k 1c) ×k V) ↔ {l} 1(((1{z y z} ×k V) ∩ Sk ) “k 1c))
43 vex 2862 . . . . . . . . . . . . 13 y V
4443elcompl 3225 . . . . . . . . . . . 12 (y l ↔ ¬ y l)
4540, 42, 443bitr4i 268 . . . . . . . . . . 11 (⟪{l}, n ( ∼ 1(((1{z y z} ×k V) ∩ Sk ) “k 1c) ×k V) ↔ y l)
46 abeq2 2458 . . . . . . . . . . . . . . 15 (z = {x b l x = (b ∪ {y})} ↔ x(x zb l x = (b ∪ {y})))
4746anbi1i 676 . . . . . . . . . . . . . 14 ((z = {x b l x = (b ∪ {y})} z n) ↔ (x(x zb l x = (b ∪ {y})) z n))
4847exbii 1582 . . . . . . . . . . . . 13 (z(z = {x b l x = (b ∪ {y})} z n) ↔ z(x(x zb l x = (b ∪ {y})) z n))
49 df-clel 2349 . . . . . . . . . . . . 13 ({x b l x = (b ∪ {y})} nz(z = {x b l x = (b ∪ {y})} z n))
50 opkex 4113 . . . . . . . . . . . . . . 15 ⟪{l}, n V
5150elimak 4259 . . . . . . . . . . . . . 14 (⟪{l}, n (( Ins3k SIk ∼ (( Ins3k SkIns2k (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) “k 111c)) “k 111c)) “k 111c) ∩ Ins2k Sk ) “k 111c) ↔ t 1 11ct, ⟪{l}, n⟫⟫ ( Ins3k SIk ∼ (( Ins3k SkIns2k (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) “k 111c)) “k 111c)) “k 111c) ∩ Ins2k Sk ))
52 elpw121c 4148 . . . . . . . . . . . . . . . . . 18 (t 111cz t = {{{z}}})
5352anbi1i 676 . . . . . . . . . . . . . . . . 17 ((t 111c t, ⟪{l}, n⟫⟫ ( Ins3k SIk ∼ (( Ins3k SkIns2k (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) “k 111c)) “k 111c)) “k 111c) ∩ Ins2k Sk )) ↔ (z t = {{{z}}} t, ⟪{l}, n⟫⟫ ( Ins3k SIk ∼ (( Ins3k SkIns2k (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) “k 111c)) “k 111c)) “k 111c) ∩ Ins2k Sk )))
54 19.41v 1901 . . . . . . . . . . . . . . . . 17 (z(t = {{{z}}} t, ⟪{l}, n⟫⟫ ( Ins3k SIk ∼ (( Ins3k SkIns2k (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) “k 111c)) “k 111c)) “k 111c) ∩ Ins2k Sk )) ↔ (z t = {{{z}}} t, ⟪{l}, n⟫⟫ ( Ins3k SIk ∼ (( Ins3k SkIns2k (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) “k 111c)) “k 111c)) “k 111c) ∩ Ins2k Sk )))
5553, 54bitr4i 243 . . . . . . . . . . . . . . . 16 ((t 111c t, ⟪{l}, n⟫⟫ ( Ins3k SIk ∼ (( Ins3k SkIns2k (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) “k 111c)) “k 111c)) “k 111c) ∩ Ins2k Sk )) ↔ z(t = {{{z}}} t, ⟪{l}, n⟫⟫ ( Ins3k SIk ∼ (( Ins3k SkIns2k (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) “k 111c)) “k 111c)) “k 111c) ∩ Ins2k Sk )))
5655exbii 1582 . . . . . . . . . . . . . . 15 (t(t 111c t, ⟪{l}, n⟫⟫ ( Ins3k SIk ∼ (( Ins3k SkIns2k (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) “k 111c)) “k 111c)) “k 111c) ∩ Ins2k Sk )) ↔ tz(t = {{{z}}} t, ⟪{l}, n⟫⟫ ( Ins3k SIk ∼ (( Ins3k SkIns2k (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) “k 111c)) “k 111c)) “k 111c) ∩ Ins2k Sk )))
57 df-rex 2620 . . . . . . . . . . . . . . 15 (t 1 11ct, ⟪{l}, n⟫⟫ ( Ins3k SIk ∼ (( Ins3k SkIns2k (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) “k 111c)) “k 111c)) “k 111c) ∩ Ins2k Sk ) ↔ t(t 111c t, ⟪{l}, n⟫⟫ ( Ins3k SIk ∼ (( Ins3k SkIns2k (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) “k 111c)) “k 111c)) “k 111c) ∩ Ins2k Sk )))
58 excom 1741 . . . . . . . . . . . . . . 15 (zt(t = {{{z}}} t, ⟪{l}, n⟫⟫ ( Ins3k SIk ∼ (( Ins3k SkIns2k (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) “k 111c)) “k 111c)) “k 111c) ∩ Ins2k Sk )) ↔ tz(t = {{{z}}} t, ⟪{l}, n⟫⟫ ( Ins3k SIk ∼ (( Ins3k SkIns2k (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) “k 111c)) “k 111c)) “k 111c) ∩ Ins2k Sk )))
5956, 57, 583bitr4i 268 . . . . . . . . . . . . . 14 (t 1 11ct, ⟪{l}, n⟫⟫ ( Ins3k SIk ∼ (( Ins3k SkIns2k (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) “k 111c)) “k 111c)) “k 111c) ∩ Ins2k Sk ) ↔ zt(t = {{{z}}} t, ⟪{l}, n⟫⟫ ( Ins3k SIk ∼ (( Ins3k SkIns2k (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) “k 111c)) “k 111c)) “k 111c) ∩ Ins2k Sk )))
60 snex 4111 . . . . . . . . . . . . . . . . 17 {{{z}}} V
61 opkeq1 4059 . . . . . . . . . . . . . . . . . 18 (t = {{{z}}} → ⟪t, ⟪{l}, n⟫⟫ = ⟪{{{z}}}, ⟪{l}, n⟫⟫)
6261eleq1d 2419 . . . . . . . . . . . . . . . . 17 (t = {{{z}}} → (⟪t, ⟪{l}, n⟫⟫ ( Ins3k SIk ∼ (( Ins3k SkIns2k (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) “k 111c)) “k 111c)) “k 111c) ∩ Ins2k Sk ) ↔ ⟪{{{z}}}, ⟪{l}, n⟫⟫ ( Ins3k SIk ∼ (( Ins3k SkIns2k (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) “k 111c)) “k 111c)) “k 111c) ∩ Ins2k Sk )))
6360, 62ceqsexv 2894 . . . . . . . . . . . . . . . 16 (t(t = {{{z}}} t, ⟪{l}, n⟫⟫ ( Ins3k SIk ∼ (( Ins3k SkIns2k (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) “k 111c)) “k 111c)) “k 111c) ∩ Ins2k Sk )) ↔ ⟪{{{z}}}, ⟪{l}, n⟫⟫ ( Ins3k SIk ∼ (( Ins3k SkIns2k (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) “k 111c)) “k 111c)) “k 111c) ∩ Ins2k Sk ))
64 elin 3219 . . . . . . . . . . . . . . . 16 (⟪{{{z}}}, ⟪{l}, n⟫⟫ ( Ins3k SIk ∼ (( Ins3k SkIns2k (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) “k 111c)) “k 111c)) “k 111c) ∩ Ins2k Sk ) ↔ (⟪{{{z}}}, ⟪{l}, n⟫⟫ Ins3k SIk ∼ (( Ins3k SkIns2k (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) “k 111c)) “k 111c)) “k 111c) ⟪{{{z}}}, ⟪{l}, n⟫⟫ Ins2k Sk ))
65 snex 4111 . . . . . . . . . . . . . . . . . . 19 {z} V
6665, 1, 7otkelins3k 4256 . . . . . . . . . . . . . . . . . 18 (⟪{{{z}}}, ⟪{l}, n⟫⟫ Ins3k SIk ∼ (( Ins3k SkIns2k (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) “k 111c)) “k 111c)) “k 111c) ↔ ⟪{z}, {l}⟫ SIk ∼ (( Ins3k SkIns2k (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) “k 111c)) “k 111c)) “k 111c))
67 vex 2862 . . . . . . . . . . . . . . . . . . 19 z V
6867, 6opksnelsik 4265 . . . . . . . . . . . . . . . . . 18 (⟪{z}, {l}⟫ SIk ∼ (( Ins3k SkIns2k (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) “k 111c)) “k 111c)) “k 111c) ↔ ⟪z, l ∼ (( Ins3k SkIns2k (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) “k 111c)) “k 111c)) “k 111c))
69 opkex 4113 . . . . . . . . . . . . . . . . . . . . . 22 z, l V
7069elimak 4259 . . . . . . . . . . . . . . . . . . . . 21 (⟪z, l (( Ins3k SkIns2k (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) “k 111c)) “k 111c)) “k 111c) ↔ t 1 11ct, ⟪z, l⟫⟫ ( Ins3k SkIns2k (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) “k 111c)) “k 111c)))
71 elpw121c 4148 . . . . . . . . . . . . . . . . . . . . . . . . 25 (t 111cx t = {{{x}}})
7271anbi1i 676 . . . . . . . . . . . . . . . . . . . . . . . 24 ((t 111c t, ⟪z, l⟫⟫ ( Ins3k SkIns2k (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) “k 111c)) “k 111c))) ↔ (x t = {{{x}}} t, ⟪z, l⟫⟫ ( Ins3k SkIns2k (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) “k 111c)) “k 111c))))
73 19.41v 1901 . . . . . . . . . . . . . . . . . . . . . . . 24 (x(t = {{{x}}} t, ⟪z, l⟫⟫ ( Ins3k SkIns2k (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) “k 111c)) “k 111c))) ↔ (x t = {{{x}}} t, ⟪z, l⟫⟫ ( Ins3k SkIns2k (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) “k 111c)) “k 111c))))
7472, 73bitr4i 243 . . . . . . . . . . . . . . . . . . . . . . 23 ((t 111c t, ⟪z, l⟫⟫ ( Ins3k SkIns2k (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) “k 111c)) “k 111c))) ↔ x(t = {{{x}}} t, ⟪z, l⟫⟫ ( Ins3k SkIns2k (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) “k 111c)) “k 111c))))
7574exbii 1582 . . . . . . . . . . . . . . . . . . . . . 22 (t(t 111c t, ⟪z, l⟫⟫ ( Ins3k SkIns2k (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) “k 111c)) “k 111c))) ↔ tx(t = {{{x}}} t, ⟪z, l⟫⟫ ( Ins3k SkIns2k (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) “k 111c)) “k 111c))))
76 df-rex 2620 . . . . . . . . . . . . . . . . . . . . . 22 (t 1 11ct, ⟪z, l⟫⟫ ( Ins3k SkIns2k (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) “k 111c)) “k 111c)) ↔ t(t 111c t, ⟪z, l⟫⟫ ( Ins3k SkIns2k (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) “k 111c)) “k 111c))))
77 excom 1741 . . . . . . . . . . . . . . . . . . . . . 22 (xt(t = {{{x}}} t, ⟪z, l⟫⟫ ( Ins3k SkIns2k (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) “k 111c)) “k 111c))) ↔ tx(t = {{{x}}} t, ⟪z, l⟫⟫ ( Ins3k SkIns2k (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) “k 111c)) “k 111c))))
7875, 76, 773bitr4i 268 . . . . . . . . . . . . . . . . . . . . 21 (t 1 11ct, ⟪z, l⟫⟫ ( Ins3k SkIns2k (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) “k 111c)) “k 111c)) ↔ xt(t = {{{x}}} t, ⟪z, l⟫⟫ ( Ins3k SkIns2k (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) “k 111c)) “k 111c))))
79 snex 4111 . . . . . . . . . . . . . . . . . . . . . . . 24 {{{x}}} V
80 opkeq1 4059 . . . . . . . . . . . . . . . . . . . . . . . . 25 (t = {{{x}}} → ⟪t, ⟪z, l⟫⟫ = ⟪{{{x}}}, ⟪z, l⟫⟫)
8180eleq1d 2419 . . . . . . . . . . . . . . . . . . . . . . . 24 (t = {{{x}}} → (⟪t, ⟪z, l⟫⟫ ( Ins3k SkIns2k (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) “k 111c)) “k 111c)) ↔ ⟪{{{x}}}, ⟪z, l⟫⟫ ( Ins3k SkIns2k (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) “k 111c)) “k 111c))))
8279, 81ceqsexv 2894 . . . . . . . . . . . . . . . . . . . . . . 23 (t(t = {{{x}}} t, ⟪z, l⟫⟫ ( Ins3k SkIns2k (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) “k 111c)) “k 111c))) ↔ ⟪{{{x}}}, ⟪z, l⟫⟫ ( Ins3k SkIns2k (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) “k 111c)) “k 111c)))
83 elsymdif 3223 . . . . . . . . . . . . . . . . . . . . . . . 24 (⟪{{{x}}}, ⟪z, l⟫⟫ ( Ins3k SkIns2k (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) “k 111c)) “k 111c)) ↔ ¬ (⟪{{{x}}}, ⟪z, l⟫⟫ Ins3k Sk ↔ ⟪{{{x}}}, ⟪z, l⟫⟫ Ins2k (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) “k 111c)) “k 111c)))
8420, 67, 6otkelins3k 4256 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (⟪{{{x}}}, ⟪z, l⟫⟫ Ins3k Sk ↔ ⟪{x}, z Sk )
8528, 67elssetk 4270 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (⟪{x}, z Skx z)
8684, 85bitri 240 . . . . . . . . . . . . . . . . . . . . . . . . 25 (⟪{{{x}}}, ⟪z, l⟫⟫ Ins3k Skx z)
87 opkex 4113 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⟪{x}, l V
8887elimak 4259 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (⟪{x}, l (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) “k 111c)) “k 111c) ↔ t 1 11ct, ⟪{x}, l⟫⟫ ( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) “k 111c)))
89 elpw121c 4148 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (t 111cb t = {{{b}}})
9089anbi1i 676 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((t 111c t, ⟪{x}, l⟫⟫ ( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) “k 111c))) ↔ (b t = {{{b}}} t, ⟪{x}, l⟫⟫ ( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) “k 111c))))
91 19.41v 1901 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (b(t = {{{b}}} t, ⟪{x}, l⟫⟫ ( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) “k 111c))) ↔ (b t = {{{b}}} t, ⟪{x}, l⟫⟫ ( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) “k 111c))))
9290, 91bitr4i 243 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((t 111c t, ⟪{x}, l⟫⟫ ( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) “k 111c))) ↔ b(t = {{{b}}} t, ⟪{x}, l⟫⟫ ( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) “k 111c))))
9392exbii 1582 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (t(t 111c t, ⟪{x}, l⟫⟫ ( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) “k 111c))) ↔ tb(t = {{{b}}} t, ⟪{x}, l⟫⟫ ( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) “k 111c))))
94 df-rex 2620 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (t 1 11ct, ⟪{x}, l⟫⟫ ( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) “k 111c)) ↔ t(t 111c t, ⟪{x}, l⟫⟫ ( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) “k 111c))))
95 excom 1741 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (bt(t = {{{b}}} t, ⟪{x}, l⟫⟫ ( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) “k 111c))) ↔ tb(t = {{{b}}} t, ⟪{x}, l⟫⟫ ( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) “k 111c))))
9693, 94, 953bitr4i 268 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (t 1 11ct, ⟪{x}, l⟫⟫ ( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) “k 111c)) ↔ bt(t = {{{b}}} t, ⟪{x}, l⟫⟫ ( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) “k 111c))))
97 snex 4111 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 {{{b}}} V
98 opkeq1 4059 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (t = {{{b}}} → ⟪t, ⟪{x}, l⟫⟫ = ⟪{{{b}}}, ⟪{x}, l⟫⟫)
9998eleq1d 2419 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (t = {{{b}}} → (⟪t, ⟪{x}, l⟫⟫ ( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) “k 111c)) ↔ ⟪{{{b}}}, ⟪{x}, l⟫⟫ ( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) “k 111c))))
10097, 99ceqsexv 2894 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (t(t = {{{b}}} t, ⟪{x}, l⟫⟫ ( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) “k 111c))) ↔ ⟪{{{b}}}, ⟪{x}, l⟫⟫ ( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) “k 111c)))
101 elin 3219 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (⟪{{{b}}}, ⟪{x}, l⟫⟫ ( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) “k 111c)) ↔ (⟪{{{b}}}, ⟪{x}, l⟫⟫ Ins2k Sk ⟪{{{b}}}, ⟪{x}, l⟫⟫ Ins3k SIk ∼ (( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) “k 111c)))
102 snex 4111 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 {b} V
103102, 20, 6otkelins2k 4255 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (⟪{{{b}}}, ⟪{x}, l⟫⟫ Ins2k Sk ↔ ⟪{b}, l Sk )
104 vex 2862 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 b V
105104, 6elssetk 4270 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (⟪{b}, l Skb l)
106103, 105bitri 240 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (⟪{{{b}}}, ⟪{x}, l⟫⟫ Ins2k Skb l)
107102, 20, 6otkelins3k 4256 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (⟪{{{b}}}, ⟪{x}, l⟫⟫ Ins3k SIk ∼ (( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) “k 111c) ↔ ⟪{b}, {x}⟫ SIk ∼ (( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) “k 111c))
108104, 28opksnelsik 4265 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (⟪{b}, {x}⟫ SIk ∼ (( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) “k 111c) ↔ ⟪b, x ∼ (( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) “k 111c))
109 alex 1572 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (z(z xz (b ∪ {y})) ↔ ¬ z ¬ (z xz (b ∪ {y})))
110 dfcleq 2347 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (x = (b ∪ {y}) ↔ z(z xz (b ∪ {y})))
111 opkex 4113 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 b, x V
112111elcompl 3225 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (⟪b, x ∼ (( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) “k 111c) ↔ ¬ ⟪b, x (( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) “k 111c))
113111elimak 4259 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (⟪b, x (( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) “k 111c) ↔ t 1 11ct, ⟪b, x⟫⟫ ( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))))
11452anbi1i 676 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((t 111c t, ⟪b, x⟫⟫ ( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V)))) ↔ (z t = {{{z}}} t, ⟪b, x⟫⟫ ( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V)))))
115 19.41v 1901 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (z(t = {{{z}}} t, ⟪b, x⟫⟫ ( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V)))) ↔ (z t = {{{z}}} t, ⟪b, x⟫⟫ ( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V)))))
116114, 115bitr4i 243 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((t 111c t, ⟪b, x⟫⟫ ( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V)))) ↔ z(t = {{{z}}} t, ⟪b, x⟫⟫ ( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V)))))
117116exbii 1582 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (t(t 111c t, ⟪b, x⟫⟫ ( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V)))) ↔ tz(t = {{{z}}} t, ⟪b, x⟫⟫ ( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V)))))
118 df-rex 2620 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (t 1 11ct, ⟪b, x⟫⟫ ( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) ↔ t(t 111c t, ⟪b, x⟫⟫ ( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V)))))
119 excom 1741 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (zt(t = {{{z}}} t, ⟪b, x⟫⟫ ( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V)))) ↔ tz(t = {{{z}}} t, ⟪b, x⟫⟫ ( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V)))))
120117, 118, 1193bitr4i 268 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (t 1 11ct, ⟪b, x⟫⟫ ( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) ↔ zt(t = {{{z}}} t, ⟪b, x⟫⟫ ( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V)))))
121 opkeq1 4059 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (t = {{{z}}} → ⟪t, ⟪b, x⟫⟫ = ⟪{{{z}}}, ⟪b, x⟫⟫)
122121eleq1d 2419 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (t = {{{z}}} → (⟪t, ⟪b, x⟫⟫ ( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) ↔ ⟪{{{z}}}, ⟪b, x⟫⟫ ( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V)))))
12360, 122ceqsexv 2894 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (t(t = {{{z}}} t, ⟪b, x⟫⟫ ( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V)))) ↔ ⟪{{{z}}}, ⟪b, x⟫⟫ ( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))))
124 elsymdif 3223 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (⟪{{{z}}}, ⟪b, x⟫⟫ ( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) ↔ ¬ (⟪{{{z}}}, ⟪b, x⟫⟫ Ins2k Sk ↔ ⟪{{{z}}}, ⟪b, x⟫⟫ Ins3k ( Sk ∪ ({{y}} ×k V))))
12565, 104, 28otkelins2k 4255 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (⟪{{{z}}}, ⟪b, x⟫⟫ Ins2k Sk ↔ ⟪{z}, x Sk )
12667, 28elssetk 4270 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (⟪{z}, x Skz x)
127125, 126bitri 240 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (⟪{{{z}}}, ⟪b, x⟫⟫ Ins2k Skz x)
12865, 104, 28otkelins3k 4256 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (⟪{{{z}}}, ⟪b, x⟫⟫ Ins3k ( Sk ∪ ({{y}} ×k V)) ↔ ⟪{z}, b ( Sk ∪ ({{y}} ×k V)))
12967, 104elssetk 4270 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (⟪{z}, b Skz b)
13065elsnc 3756 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ({z} {{y}} ↔ {z} = {y})
13167sneqb 3876 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ({z} = {y} ↔ z = y)
132130, 131bitri 240 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ({z} {{y}} ↔ z = y)
13365, 104opkelxpk 4248 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (⟪{z}, b ({{y}} ×k V) ↔ ({z} {{y}} b V))
134104, 133mpbiran2 885 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (⟪{z}, b ({{y}} ×k V) ↔ {z} {{y}})
13567elsnc 3756 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (z {y} ↔ z = y)
136132, 134, 1353bitr4i 268 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (⟪{z}, b ({{y}} ×k V) ↔ z {y})
137129, 136orbi12i 507 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((⟪{z}, b Sk ⟪{z}, b ({{y}} ×k V)) ↔ (z b z {y}))
138 elun 3220 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (⟪{z}, b ( Sk ∪ ({{y}} ×k V)) ↔ (⟪{z}, b Sk ⟪{z}, b ({{y}} ×k V)))
139 elun 3220 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (z (b ∪ {y}) ↔ (z b z {y}))
140137, 138, 1393bitr4i 268 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (⟪{z}, b ( Sk ∪ ({{y}} ×k V)) ↔ z (b ∪ {y}))
141128, 140bitri 240 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (⟪{{{z}}}, ⟪b, x⟫⟫ Ins3k ( Sk ∪ ({{y}} ×k V)) ↔ z (b ∪ {y}))
142127, 141bibi12i 306 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((⟪{{{z}}}, ⟪b, x⟫⟫ Ins2k Sk ↔ ⟪{{{z}}}, ⟪b, x⟫⟫ Ins3k ( Sk ∪ ({{y}} ×k V))) ↔ (z xz (b ∪ {y})))
143124, 142xchbinx 301 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (⟪{{{z}}}, ⟪b, x⟫⟫ ( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) ↔ ¬ (z xz (b ∪ {y})))
144123, 143bitri 240 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (t(t = {{{z}}} t, ⟪b, x⟫⟫ ( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V)))) ↔ ¬ (z xz (b ∪ {y})))
145144exbii 1582 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (zt(t = {{{z}}} t, ⟪b, x⟫⟫ ( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V)))) ↔ z ¬ (z xz (b ∪ {y})))
146113, 120, 1453bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (⟪b, x (( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) “k 111c) ↔ z ¬ (z xz (b ∪ {y})))
147112, 146xchbinx 301 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (⟪b, x ∼ (( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) “k 111c) ↔ ¬ z ¬ (z xz (b ∪ {y})))
148109, 110, 1473bitr4ri 269 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (⟪b, x ∼ (( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) “k 111c) ↔ x = (b ∪ {y}))
149107, 108, 1483bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (⟪{{{b}}}, ⟪{x}, l⟫⟫ Ins3k SIk ∼ (( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) “k 111c) ↔ x = (b ∪ {y}))
150106, 149anbi12i 678 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((⟪{{{b}}}, ⟪{x}, l⟫⟫ Ins2k Sk ⟪{{{b}}}, ⟪{x}, l⟫⟫ Ins3k SIk ∼ (( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) “k 111c)) ↔ (b l x = (b ∪ {y})))
151100, 101, 1503bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (t(t = {{{b}}} t, ⟪{x}, l⟫⟫ ( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) “k 111c))) ↔ (b l x = (b ∪ {y})))
152151exbii 1582 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (bt(t = {{{b}}} t, ⟪{x}, l⟫⟫ ( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) “k 111c))) ↔ b(b l x = (b ∪ {y})))
15388, 96, 1523bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (⟪{x}, l (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) “k 111c)) “k 111c) ↔ b(b l x = (b ∪ {y})))
15420, 67, 6otkelins2k 4255 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (⟪{{{x}}}, ⟪z, l⟫⟫ Ins2k (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) “k 111c)) “k 111c) ↔ ⟪{x}, l (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) “k 111c)) “k 111c))
155 df-rex 2620 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (b l x = (b ∪ {y}) ↔ b(b l x = (b ∪ {y})))
156153, 154, 1553bitr4i 268 . . . . . . . . . . . . . . . . . . . . . . . . 25 (⟪{{{x}}}, ⟪z, l⟫⟫ Ins2k (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) “k 111c)) “k 111c) ↔ b l x = (b ∪ {y}))
15786, 156bibi12i 306 . . . . . . . . . . . . . . . . . . . . . . . 24 ((⟪{{{x}}}, ⟪z, l⟫⟫ Ins3k Sk ↔ ⟪{{{x}}}, ⟪z, l⟫⟫ Ins2k (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) “k 111c)) “k 111c)) ↔ (x zb l x = (b ∪ {y})))
15883, 157xchbinx 301 . . . . . . . . . . . . . . . . . . . . . . 23 (⟪{{{x}}}, ⟪z, l⟫⟫ ( Ins3k SkIns2k (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) “k 111c)) “k 111c)) ↔ ¬ (x zb l x = (b ∪ {y})))
15982, 158bitri 240 . . . . . . . . . . . . . . . . . . . . . 22 (t(t = {{{x}}} t, ⟪z, l⟫⟫ ( Ins3k SkIns2k (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) “k 111c)) “k 111c))) ↔ ¬ (x zb l x = (b ∪ {y})))
160159exbii 1582 . . . . . . . . . . . . . . . . . . . . 21 (xt(t = {{{x}}} t, ⟪z, l⟫⟫ ( Ins3k SkIns2k (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) “k 111c)) “k 111c))) ↔ x ¬ (x zb l x = (b ∪ {y})))
16170, 78, 1603bitri 262 . . . . . . . . . . . . . . . . . . . 20 (⟪z, l (( Ins3k SkIns2k (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) “k 111c)) “k 111c)) “k 111c) ↔ x ¬ (x zb l x = (b ∪ {y})))
162161notbii 287 . . . . . . . . . . . . . . . . . . 19 (¬ ⟪z, l (( Ins3k SkIns2k (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) “k 111c)) “k 111c)) “k 111c) ↔ ¬ x ¬ (x zb l x = (b ∪ {y})))
16369elcompl 3225 . . . . . . . . . . . . . . . . . . 19 (⟪z, l ∼ (( Ins3k SkIns2k (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) “k 111c)) “k 111c)) “k 111c) ↔ ¬ ⟪z, l (( Ins3k SkIns2k (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) “k 111c)) “k 111c)) “k 111c))
164 alex 1572 . . . . . . . . . . . . . . . . . . 19 (x(x zb l x = (b ∪ {y})) ↔ ¬ x ¬ (x zb l x = (b ∪ {y})))
165162, 163, 1643bitr4i 268 . . . . . . . . . . . . . . . . . 18 (⟪z, l ∼ (( Ins3k SkIns2k (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) “k 111c)) “k 111c)) “k 111c) ↔ x(x zb l x = (b ∪ {y})))
16666, 68, 1653bitri 262 . . . . . . . . . . . . . . . . 17 (⟪{{{z}}}, ⟪{l}, n⟫⟫ Ins3k SIk ∼ (( Ins3k SkIns2k (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) “k 111c)) “k 111c)) “k 111c) ↔ x(x zb l x = (b ∪ {y})))
16765, 1, 7otkelins2k 4255 . . . . . . . . . . . . . . . . . 18 (⟪{{{z}}}, ⟪{l}, n⟫⟫ Ins2k Sk ↔ ⟪{z}, n Sk )
16867, 7elssetk 4270 . . . . . . . . . . . . . . . . . 18 (⟪{z}, n Skz n)
169167, 168bitri 240 . . . . . . . . . . . . . . . . 17 (⟪{{{z}}}, ⟪{l}, n⟫⟫ Ins2k Skz n)
170166, 169anbi12i 678 . . . . . . . . . . . . . . . 16 ((⟪{{{z}}}, ⟪{l}, n⟫⟫ Ins3k SIk ∼ (( Ins3k SkIns2k (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) “k 111c)) “k 111c)) “k 111c) ⟪{{{z}}}, ⟪{l}, n⟫⟫ Ins2k Sk ) ↔ (x(x zb l x = (b ∪ {y})) z n))
17163, 64, 1703bitri 262 . . . . . . . . . . . . . . 15 (t(t = {{{z}}} t, ⟪{l}, n⟫⟫ ( Ins3k SIk ∼ (( Ins3k SkIns2k (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) “k 111c)) “k 111c)) “k 111c) ∩ Ins2k Sk )) ↔ (x(x zb l x = (b ∪ {y})) z n))
172171exbii 1582 . . . . . . . . . . . . . 14 (zt(t = {{{z}}} t, ⟪{l}, n⟫⟫ ( Ins3k SIk ∼ (( Ins3k SkIns2k (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) “k 111c)) “k 111c)) “k 111c) ∩ Ins2k Sk )) ↔ z(x(x zb l x = (b ∪ {y})) z n))
17351, 59, 1723bitri 262 . . . . . . . . . . . . 13 (⟪{l}, n (( Ins3k SIk ∼ (( Ins3k SkIns2k (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) “k 111c)) “k 111c)) “k 111c) ∩ Ins2k Sk ) “k 111c) ↔ z(x(x zb l x = (b ∪ {y})) z n))
17448, 49, 1733bitr4ri 269 . . . . . . . . . . . 12 (⟪{l}, n (( Ins3k SIk ∼ (( Ins3k SkIns2k (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) “k 111c)) “k 111c)) “k 111c) ∩ Ins2k Sk ) “k 111c) ↔ {x b l x = (b ∪ {y})} n)
175174notbii 287 . . . . . . . . . . 11 (¬ ⟪{l}, n (( Ins3k SIk ∼ (( Ins3k SkIns2k (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) “k 111c)) “k 111c)) “k 111c) ∩ Ins2k Sk ) “k 111c) ↔ ¬ {x b l x = (b ∪ {y})} n)
17645, 175anbi12i 678 . . . . . . . . . 10 ((⟪{l}, n ( ∼ 1(((1{z y z} ×k V) ∩ Sk ) “k 1c) ×k V) ¬ ⟪{l}, n (( Ins3k SIk ∼ (( Ins3k SkIns2k (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) “k 111c)) “k 111c)) “k 111c) ∩ Ins2k Sk ) “k 111c)) ↔ (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))
1789, 176, 1773bitri 262 . . . . . . . . 9 (⟪{l}, n (( ∼ 1(((1{z y z} ×k V) ∩ Sk ) “k 1c) ×k V) (( Ins3k SIk ∼ (( Ins3k SkIns2k (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) “k 111c)) “k 111c)) “k 111c) ∩ Ins2k Sk ) “k 111c)) ↔ ¬ (y l → {x b l x = (b ∪ {y})} n))
1798, 178anbi12i 678 . . . . . . . 8 ((⟪{l}, n Sk ⟪{l}, n (( ∼ 1(((1{z y z} ×k V) ∩ Sk ) “k 1c) ×k V) (( Ins3k SIk ∼ (( Ins3k SkIns2k (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) “k 111c)) “k 111c)) “k 111c) ∩ Ins2k Sk ) “k 111c))) ↔ (l n ¬ (y l → {x b l x = (b ∪ {y})} n)))
1804, 5, 1793bitri 262 . . . . . . 7 (t(t = {l} t, n ( Sk ∩ (( ∼ 1(((1{z y z} ×k V) ∩ Sk ) “k 1c) ×k V) (( Ins3k SIk ∼ (( Ins3k SkIns2k (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) “k 111c)) “k 111c)) “k 111c) ∩ Ins2k Sk ) “k 111c)))) ↔ (l n ¬ (y l → {x b l x = (b ∪ {y})} n)))
181180exbii 1582 . . . . . 6 (lt(t = {l} t, n ( Sk ∩ (( ∼ 1(((1{z y z} ×k V) ∩ Sk ) “k 1c) ×k V) (( Ins3k SIk ∼ (( Ins3k SkIns2k (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) “k 111c)) “k 111c)) “k 111c) ∩ Ins2k Sk ) “k 111c)))) ↔ l(l n ¬ (y l → {x b l x = (b ∪ {y})} n)))
1827elimak 4259 . . . . . . 7 (n (( Sk ∩ (( ∼ 1(((1{z y z} ×k V) ∩ Sk ) “k 1c) ×k V) (( Ins3k SIk ∼ (( Ins3k SkIns2k (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) “k 111c)) “k 111c)) “k 111c) ∩ Ins2k Sk ) “k 111c))) “k 1c) ↔ t 1ct, n ( Sk ∩ (( ∼ 1(((1{z y z} ×k V) ∩ Sk ) “k 1c) ×k V) (( Ins3k SIk ∼ (( Ins3k SkIns2k (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) “k 111c)) “k 111c)) “k 111c) ∩ Ins2k Sk ) “k 111c))))
183 el1c 4139 . . . . . . . . . . 11 (t 1cl t = {l})
184183anbi1i 676 . . . . . . . . . 10 ((t 1c t, n ( Sk ∩ (( ∼ 1(((1{z y z} ×k V) ∩ Sk ) “k 1c) ×k V) (( Ins3k SIk ∼ (( Ins3k SkIns2k (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) “k 111c)) “k 111c)) “k 111c) ∩ Ins2k Sk ) “k 111c)))) ↔ (l t = {l} t, n ( Sk ∩ (( ∼ 1(((1{z y z} ×k V) ∩ Sk ) “k 1c) ×k V) (( Ins3k SIk ∼ (( Ins3k SkIns2k (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) “k 111c)) “k 111c)) “k 111c) ∩ Ins2k Sk ) “k 111c)))))
185 19.41v 1901 . . . . . . . . . 10 (l(t = {l} t, n ( Sk ∩ (( ∼ 1(((1{z y z} ×k V) ∩ Sk ) “k 1c) ×k V) (( Ins3k SIk ∼ (( Ins3k SkIns2k (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) “k 111c)) “k 111c)) “k 111c) ∩ Ins2k Sk ) “k 111c)))) ↔ (l t = {l} t, n ( Sk ∩ (( ∼ 1(((1{z y z} ×k V) ∩ Sk ) “k 1c) ×k V) (( Ins3k SIk ∼ (( Ins3k SkIns2k (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) “k 111c)) “k 111c)) “k 111c) ∩ Ins2k Sk ) “k 111c)))))
186184, 185bitr4i 243 . . . . . . . . 9 ((t 1c t, n ( Sk ∩ (( ∼ 1(((1{z y z} ×k V) ∩ Sk ) “k 1c) ×k V) (( Ins3k SIk ∼ (( Ins3k SkIns2k (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) “k 111c)) “k 111c)) “k 111c) ∩ Ins2k Sk ) “k 111c)))) ↔ l(t = {l} t, n ( Sk ∩ (( ∼ 1(((1{z y z} ×k V) ∩ Sk ) “k 1c) ×k V) (( Ins3k SIk ∼ (( Ins3k SkIns2k (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) “k 111c)) “k 111c)) “k 111c) ∩ Ins2k Sk ) “k 111c)))))
187186exbii 1582 . . . . . . . 8 (t(t 1c t, n ( Sk ∩ (( ∼ 1(((1{z y z} ×k V) ∩ Sk ) “k 1c) ×k V) (( Ins3k SIk ∼ (( Ins3k SkIns2k (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) “k 111c)) “k 111c)) “k 111c) ∩ Ins2k Sk ) “k 111c)))) ↔ tl(t = {l} t, n ( Sk ∩ (( ∼ 1(((1{z y z} ×k V) ∩ Sk ) “k 1c) ×k V) (( Ins3k SIk ∼ (( Ins3k SkIns2k (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) “k 111c)) “k 111c)) “k 111c) ∩ Ins2k Sk ) “k 111c)))))
188 df-rex 2620 . . . . . . . 8 (t 1ct, n ( Sk ∩ (( ∼ 1(((1{z y z} ×k V) ∩ Sk ) “k 1c) ×k V) (( Ins3k SIk ∼ (( Ins3k SkIns2k (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) “k 111c)) “k 111c)) “k 111c) ∩ Ins2k Sk ) “k 111c))) ↔ t(t 1c t, n ( Sk ∩ (( ∼ 1(((1{z y z} ×k V) ∩ Sk ) “k 1c) ×k V) (( Ins3k SIk ∼ (( Ins3k SkIns2k (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) “k 111c)) “k 111c)) “k 111c) ∩ Ins2k Sk ) “k 111c)))))
189 excom 1741 . . . . . . . 8 (lt(t = {l} t, n ( Sk ∩ (( ∼ 1(((1{z y z} ×k V) ∩ Sk ) “k 1c) ×k V) (( Ins3k SIk ∼ (( Ins3k SkIns2k (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) “k 111c)) “k 111c)) “k 111c) ∩ Ins2k Sk ) “k 111c)))) ↔ tl(t = {l} t, n ( Sk ∩ (( ∼ 1(((1{z y z} ×k V) ∩ Sk ) “k 1c) ×k V) (( Ins3k SIk ∼ (( Ins3k SkIns2k (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) “k 111c)) “k 111c)) “k 111c) ∩ Ins2k Sk ) “k 111c)))))
190187, 188, 1893bitr4i 268 . . . . . . 7 (t 1ct, n ( Sk ∩ (( ∼ 1(((1{z y z} ×k V) ∩ Sk ) “k 1c) ×k V) (( Ins3k SIk ∼ (( Ins3k SkIns2k (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) “k 111c)) “k 111c)) “k 111c) ∩ Ins2k Sk ) “k 111c))) ↔ lt(t = {l} t, n ( Sk ∩ (( ∼ 1(((1{z y z} ×k V) ∩ Sk ) “k 1c) ×k V) (( Ins3k SIk ∼ (( Ins3k SkIns2k (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) “k 111c)) “k 111c)) “k 111c) ∩ Ins2k Sk ) “k 111c)))))
191182, 190bitri 240 . . . . . 6 (n (( Sk ∩ (( ∼ 1(((1{z y z} ×k V) ∩ Sk ) “k 1c) ×k V) (( Ins3k SIk ∼ (( Ins3k SkIns2k (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) “k 111c)) “k 111c)) “k 111c) ∩ Ins2k Sk ) “k 111c))) “k 1c) ↔ lt(t = {l} t, n ( Sk ∩ (( ∼ 1(((1{z y z} ×k V) ∩ Sk ) “k 1c) ×k V) (( Ins3k SIk ∼ (( Ins3k SkIns2k (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) “k 111c)) “k 111c)) “k 111c) ∩ Ins2k Sk ) “k 111c)))))
192 df-rex 2620 . . . . . 6 (l n ¬ (y l → {x b l x = (b ∪ {y})} n) ↔ l(l n ¬ (y l → {x b l x = (b ∪ {y})} n)))
193181, 191, 1923bitr4i 268 . . . . 5 (n (( Sk ∩ (( ∼ 1(((1{z y z} ×k V) ∩ Sk ) “k 1c) ×k V) (( Ins3k SIk ∼ (( Ins3k SkIns2k (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) “k 111c)) “k 111c)) “k 111c) ∩ Ins2k Sk ) “k 111c))) “k 1c) ↔ l n ¬ (y l → {x b l x = (b ∪ {y})} n))
194193notbii 287 . . . 4 n (( Sk ∩ (( ∼ 1(((1{z y z} ×k V) ∩ Sk ) “k 1c) ×k V) (( Ins3k SIk ∼ (( Ins3k SkIns2k (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) “k 111c)) “k 111c)) “k 111c) ∩ Ins2k Sk ) “k 111c))) “k 1c) ↔ ¬ l n ¬ (y l → {x b l x = (b ∪ {y})} n))
1957elcompl 3225 . . . 4 (n ∼ (( Sk ∩ (( ∼ 1(((1{z y z} ×k V) ∩ Sk ) “k 1c) ×k V) (( Ins3k SIk ∼ (( Ins3k SkIns2k (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) “k 111c)) “k 111c)) “k 111c) ∩ Ins2k Sk ) “k 111c))) “k 1c) ↔ ¬ n (( Sk ∩ (( ∼ 1(((1{z y z} ×k V) ∩ Sk ) “k 1c) ×k V) (( Ins3k SIk ∼ (( Ins3k SkIns2k (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) “k 111c)) “k 111c)) “k 111c) ∩ Ins2k Sk ) “k 111c))) “k 1c))
196 dfral2 2626 . . . 4 (l n (y l → {x b l x = (b ∪ {y})} n) ↔ ¬ l n ¬ (y l → {x b l x = (b ∪ {y})} n))
197194, 195, 1963bitr4i 268 . . 3 (n ∼ (( Sk ∩ (( ∼ 1(((1{z y z} ×k V) ∩ Sk ) “k 1c) ×k V) (( Ins3k SIk ∼ (( Ins3k SkIns2k (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) “k 111c)) “k 111c)) “k 111c) ∩ Ins2k Sk ) “k 111c))) “k 1c) ↔ l n (y l → {x b l x = (b ∪ {y})} n))
198197abbi2i 2464 . 2 ∼ (( Sk ∩ (( ∼ 1(((1{z y z} ×k V) ∩ Sk ) “k 1c) ×k V) (( Ins3k SIk ∼ (( Ins3k SkIns2k (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) “k 111c)) “k 111c)) “k 111c) ∩ Ins2k Sk ) “k 111c))) “k 1c) = {n l n (y l → {x b l x = (b ∪ {y})} n)}
199 ssetkex 4294 . . . . 5 Sk V
200 setswithex 4322 . . . . . . . . . . . . 13 {z y z} V
201200pw1ex 4303 . . . . . . . . . . . 12 1{z y z} V
202 vvex 4109 . . . . . . . . . . . 12 V V
203201, 202xpkex 4289 . . . . . . . . . . 11 (1{z y z} ×k V) V
204203, 199inex 4105 . . . . . . . . . 10 ((1{z y z} ×k V) ∩ Sk ) V
205 1cex 4142 . . . . . . . . . 10 1c V
206204, 205imakex 4300 . . . . . . . . 9 (((1{z y z} ×k V) ∩ Sk ) “k 1c) V
207206pw1ex 4303 . . . . . . . 8 1(((1{z y z} ×k V) ∩ Sk ) “k 1c) V
208207complex 4104 . . . . . . 7 1(((1{z y z} ×k V) ∩ Sk ) “k 1c) V
209208, 202xpkex 4289 . . . . . 6 ( ∼ 1(((1{z y z} ×k V) ∩ Sk ) “k 1c) ×k V) V
210199ins3kex 4308 . . . . . . . . . . . . 13 Ins3k Sk V
211199ins2kex 4307 . . . . . . . . . . . . . . . 16 Ins2k Sk V
212 snex 4111 . . . . . . . . . . . . . . . . . . . . . . . 24 {{y}} V
213212, 202xpkex 4289 . . . . . . . . . . . . . . . . . . . . . . 23 ({{y}} ×k V) V
214199, 213unex 4106 . . . . . . . . . . . . . . . . . . . . . 22 ( Sk ∪ ({{y}} ×k V)) V
215214ins3kex 4308 . . . . . . . . . . . . . . . . . . . . 21 Ins3k ( Sk ∪ ({{y}} ×k V)) V
216211, 215symdifex 4108 . . . . . . . . . . . . . . . . . . . 20 ( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) V
217205pw1ex 4303 . . . . . . . . . . . . . . . . . . . . 21 11c V
218217pw1ex 4303 . . . . . . . . . . . . . . . . . . . 20 111c V
219216, 218imakex 4300 . . . . . . . . . . . . . . . . . . 19 (( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) “k 111c) V
220219complex 4104 . . . . . . . . . . . . . . . . . 18 ∼ (( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) “k 111c) V
221220sikex 4297 . . . . . . . . . . . . . . . . 17 SIk ∼ (( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) “k 111c) V
222221ins3kex 4308 . . . . . . . . . . . . . . . 16 Ins3k SIk ∼ (( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) “k 111c) V
223211, 222inex 4105 . . . . . . . . . . . . . . 15 ( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) “k 111c)) V
224223, 218imakex 4300 . . . . . . . . . . . . . 14 (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) “k 111c)) “k 111c) V
225224ins2kex 4307 . . . . . . . . . . . . 13 Ins2k (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) “k 111c)) “k 111c) V
226210, 225symdifex 4108 . . . . . . . . . . . 12 ( Ins3k SkIns2k (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) “k 111c)) “k 111c)) V
227226, 218imakex 4300 . . . . . . . . . . 11 (( Ins3k SkIns2k (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) “k 111c)) “k 111c)) “k 111c) V
228227complex 4104 . . . . . . . . . 10 ∼ (( Ins3k SkIns2k (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) “k 111c)) “k 111c)) “k 111c) V
229228sikex 4297 . . . . . . . . 9 SIk ∼ (( Ins3k SkIns2k (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) “k 111c)) “k 111c)) “k 111c) V
230229ins3kex 4308 . . . . . . . 8 Ins3k SIk ∼ (( Ins3k SkIns2k (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) “k 111c)) “k 111c)) “k 111c) V
231230, 211inex 4105 . . . . . . 7 ( Ins3k SIk ∼ (( Ins3k SkIns2k (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) “k 111c)) “k 111c)) “k 111c) ∩ Ins2k Sk ) V
232231, 218imakex 4300 . . . . . 6 (( Ins3k SIk ∼ (( Ins3k SkIns2k (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) “k 111c)) “k 111c)) “k 111c) ∩ Ins2k Sk ) “k 111c) V
233209, 232difex 4107 . . . . 5 (( ∼ 1(((1{z y z} ×k V) ∩ Sk ) “k 1c) ×k V) (( Ins3k SIk ∼ (( Ins3k SkIns2k (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) “k 111c)) “k 111c)) “k 111c) ∩ Ins2k Sk ) “k 111c)) V
234199, 233inex 4105 . . . 4 ( Sk ∩ (( ∼ 1(((1{z y z} ×k V) ∩ Sk ) “k 1c) ×k V) (( Ins3k SIk ∼ (( Ins3k SkIns2k (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) “k 111c)) “k 111c)) “k 111c) ∩ Ins2k Sk ) “k 111c))) V
235234, 205imakex 4300 . . 3 (( Sk ∩ (( ∼ 1(((1{z y z} ×k V) ∩ Sk ) “k 1c) ×k V) (( Ins3k SIk ∼ (( Ins3k SkIns2k (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) “k 111c)) “k 111c)) “k 111c) ∩ Ins2k Sk ) “k 111c))) “k 1c) V
236235complex 4104 . 2 ∼ (( Sk ∩ (( ∼ 1(((1{z y z} ×k V) ∩ Sk ) “k 1c) ×k V) (( Ins3k SIk ∼ (( Ins3k SkIns2k (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ( Sk ∪ ({{y}} ×k V))) “k 111c)) “k 111c)) “k 111c) ∩ Ins2k Sk ) “k 111c))) “k 1c) V
237198, 236eqeltrri 2424 1 {n l n (y l → {x b l x = (b ∪ {y})} n)} V
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 176   ∨ wo 357   ∧ wa 358  ∀wal 1540  ∃wex 1541   = wceq 1642   ∈ wcel 1710  {cab 2339  ∀wral 2614  ∃wrex 2615  Vcvv 2859   ∼ ccompl 3205   ∖ cdif 3206   ∪ cun 3207   ∩ cin 3208   ⊕ csymdif 3209  {csn 3737  ∪cuni 3891  ⟪copk 4057  1cc1c 4134  ℘1cpw1 4135   ×k cxpk 4174   Ins2k cins2k 4176   Ins3k cins3k 4177   “k cimak 4179   SIk csik 4181   Sk cssetk 4183 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 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 4078  ax-xp 4079  ax-cnv 4080  ax-1c 4081  ax-sset 4082  ax-si 4083  ax-ins2 4084  ax-ins3 4085  ax-typlower 4086  ax-sn 4087 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 2478  df-ne 2518  df-ral 2619  df-rex 2620  df-v 2861  df-sbc 3047  df-nin 3211  df-compl 3212  df-in 3213  df-un 3214  df-dif 3215  df-symdif 3216  df-ss 3259  df-nul 3551  df-if 3663  df-pw 3724  df-sn 3741  df-pr 3742  df-uni 3892  df-opk 4058  df-1c 4136  df-pw1 4137  df-xpk 4185  df-cnvk 4186  df-ins2k 4187  df-ins3k 4188  df-imak 4189  df-p6 4191  df-sik 4192  df-ssetk 4193 This theorem is referenced by:  nnadjoin  4520
 Copyright terms: Public domain W3C validator