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

Theorem evenodddisjlem1 4515
Description: Lemma for evenodddisj 4516. Establish stratification for induction. (Contributed by SF, 25-Jan-2015.)
Assertion
Ref Expression
evenodddisjlem1 {j ((j +c j) ≠ n Nn (((n +c n) +c 1c) ≠ → (j +c j) ≠ ((n +c n) +c 1c)))} V
Distinct variable group:   j,n

Proof of Theorem evenodddisjlem1
Dummy variables x a b y t are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-or 359 . . . 4 (((j +c j) = n Nn (((n +c n) +c 1c) ≠ → (j +c j) ≠ ((n +c n) +c 1c))) ↔ (¬ (j +c j) = n Nn (((n +c n) +c 1c) ≠ → (j +c j) ≠ ((n +c n) +c 1c))))
2 vex 2862 . . . . . 6 j V
32elimakv 4260 . . . . 5 (j (( ∼ (( Ins3k SkIns2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c)) “k 111c)) “k 111c) ∩ (({} ∪ ∼ ((( Ins3k (( Ins2k ∼ (( Ins3k SkIns2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k k SIk SIk SIk (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk SkIns3k SIk SIk SIk SIk SIk Sk )) “k 11111111c))) “k 11111c)) “k 111c)) “k 111c) ∩ Ins3k Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c)) “k 11c) ∩ Ins2k ( Ik ({} ×k V))) “k 11c) “k Nn )) ×k V)) “k V) ↔ xx, j ( ∼ (( Ins3k SkIns2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c)) “k 111c)) “k 111c) ∩ (({} ∪ ∼ ((( Ins3k (( Ins2k ∼ (( Ins3k SkIns2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k k SIk SIk SIk (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk SkIns3k SIk SIk SIk SIk SIk Sk )) “k 11111111c))) “k 11111c)) “k 111c)) “k 111c) ∩ Ins3k Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c)) “k 11c) ∩ Ins2k ( Ik ({} ×k V))) “k 11c) “k Nn )) ×k V)))
4 elin 3219 . . . . . . 7 (⟪x, j ( ∼ (( Ins3k SkIns2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c)) “k 111c)) “k 111c) ∩ (({} ∪ ∼ ((( Ins3k (( Ins2k ∼ (( Ins3k SkIns2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k k SIk SIk SIk (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk SkIns3k SIk SIk SIk SIk SIk Sk )) “k 11111111c))) “k 11111c)) “k 111c)) “k 111c) ∩ Ins3k Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c)) “k 11c) ∩ Ins2k ( Ik ({} ×k V))) “k 11c) “k Nn )) ×k V)) ↔ (⟪x, j ∼ (( Ins3k SkIns2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c)) “k 111c)) “k 111c) x, j (({} ∪ ∼ ((( Ins3k (( Ins2k ∼ (( Ins3k SkIns2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k k SIk SIk SIk (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk SkIns3k SIk SIk SIk SIk SIk Sk )) “k 11111111c))) “k 11111c)) “k 111c)) “k 111c) ∩ Ins3k Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c)) “k 11c) ∩ Ins2k ( Ik ({} ×k V))) “k 11c) “k Nn )) ×k V)))
5 opkex 4113 . . . . . . . . . . . . 13 x, j V
65elimak 4259 . . . . . . . . . . . 12 (⟪x, j (( Ins3k SkIns2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c)) “k 111c)) “k 111c) ↔ t 1 11ct, ⟪x, j⟫⟫ ( Ins3k SkIns2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c)) “k 111c)))
7 elpw121c 4148 . . . . . . . . . . . . . . . 16 (t 111cy t = {{{y}}})
87anbi1i 676 . . . . . . . . . . . . . . 15 ((t 111c t, ⟪x, j⟫⟫ ( Ins3k SkIns2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c)) “k 111c))) ↔ (y t = {{{y}}} t, ⟪x, j⟫⟫ ( Ins3k SkIns2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c)) “k 111c))))
9 19.41v 1901 . . . . . . . . . . . . . . 15 (y(t = {{{y}}} t, ⟪x, j⟫⟫ ( Ins3k SkIns2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c)) “k 111c))) ↔ (y t = {{{y}}} t, ⟪x, j⟫⟫ ( Ins3k SkIns2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c)) “k 111c))))
108, 9bitr4i 243 . . . . . . . . . . . . . 14 ((t 111c t, ⟪x, j⟫⟫ ( Ins3k SkIns2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c)) “k 111c))) ↔ y(t = {{{y}}} t, ⟪x, j⟫⟫ ( Ins3k SkIns2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c)) “k 111c))))
1110exbii 1582 . . . . . . . . . . . . 13 (t(t 111c t, ⟪x, j⟫⟫ ( Ins3k SkIns2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c)) “k 111c))) ↔ ty(t = {{{y}}} t, ⟪x, j⟫⟫ ( Ins3k SkIns2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c)) “k 111c))))
12 df-rex 2620 . . . . . . . . . . . . 13 (t 1 11ct, ⟪x, j⟫⟫ ( Ins3k SkIns2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c)) “k 111c)) ↔ t(t 111c t, ⟪x, j⟫⟫ ( Ins3k SkIns2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c)) “k 111c))))
13 excom 1741 . . . . . . . . . . . . 13 (yt(t = {{{y}}} t, ⟪x, j⟫⟫ ( Ins3k SkIns2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c)) “k 111c))) ↔ ty(t = {{{y}}} t, ⟪x, j⟫⟫ ( Ins3k SkIns2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c)) “k 111c))))
1411, 12, 133bitr4i 268 . . . . . . . . . . . 12 (t 1 11ct, ⟪x, j⟫⟫ ( Ins3k SkIns2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c)) “k 111c)) ↔ yt(t = {{{y}}} t, ⟪x, j⟫⟫ ( Ins3k SkIns2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c)) “k 111c))))
15 snex 4111 . . . . . . . . . . . . . . 15 {{{y}}} V
16 opkeq1 4059 . . . . . . . . . . . . . . . 16 (t = {{{y}}} → ⟪t, ⟪x, j⟫⟫ = ⟪{{{y}}}, ⟪x, j⟫⟫)
1716eleq1d 2419 . . . . . . . . . . . . . . 15 (t = {{{y}}} → (⟪t, ⟪x, j⟫⟫ ( Ins3k SkIns2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c)) “k 111c)) ↔ ⟪{{{y}}}, ⟪x, j⟫⟫ ( Ins3k SkIns2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c)) “k 111c))))
1815, 17ceqsexv 2894 . . . . . . . . . . . . . 14 (t(t = {{{y}}} t, ⟪x, j⟫⟫ ( Ins3k SkIns2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c)) “k 111c))) ↔ ⟪{{{y}}}, ⟪x, j⟫⟫ ( Ins3k SkIns2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c)) “k 111c)))
19 elsymdif 3223 . . . . . . . . . . . . . 14 (⟪{{{y}}}, ⟪x, j⟫⟫ ( Ins3k SkIns2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c)) “k 111c)) ↔ ¬ (⟪{{{y}}}, ⟪x, j⟫⟫ Ins3k Sk ↔ ⟪{{{y}}}, ⟪x, j⟫⟫ Ins2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c)) “k 111c)))
20 snex 4111 . . . . . . . . . . . . . . . . . 18 {y} V
21 vex 2862 . . . . . . . . . . . . . . . . . 18 x V
2220, 21, 2otkelins3k 4256 . . . . . . . . . . . . . . . . 17 (⟪{{{y}}}, ⟪x, j⟫⟫ Ins3k Sk ↔ ⟪{y}, x Sk )
23 vex 2862 . . . . . . . . . . . . . . . . . 18 y V
2423, 21elssetk 4270 . . . . . . . . . . . . . . . . 17 (⟪{y}, x Sky x)
2522, 24bitri 240 . . . . . . . . . . . . . . . 16 (⟪{{{y}}}, ⟪x, j⟫⟫ Ins3k Sky x)
2620, 21, 2otkelins2k 4255 . . . . . . . . . . . . . . . . 17 (⟪{{{y}}}, ⟪x, j⟫⟫ Ins2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c)) “k 111c) ↔ ⟪{y}, j (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c)) “k 111c))
27 opkex 4113 . . . . . . . . . . . . . . . . . . . 20 ⟪{y}, j V
2827elimak 4259 . . . . . . . . . . . . . . . . . . 19 (⟪{y}, j (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c)) “k 111c) ↔ t 1 11ct, ⟪{y}, j⟫⟫ ( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c)))
29 elpw121c 4148 . . . . . . . . . . . . . . . . . . . . . . 23 (t 111cb t = {{{b}}})
3029anbi1i 676 . . . . . . . . . . . . . . . . . . . . . 22 ((t 111c t, ⟪{y}, j⟫⟫ ( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c))) ↔ (b t = {{{b}}} t, ⟪{y}, j⟫⟫ ( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c))))
31 19.41v 1901 . . . . . . . . . . . . . . . . . . . . . 22 (b(t = {{{b}}} t, ⟪{y}, j⟫⟫ ( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c))) ↔ (b t = {{{b}}} t, ⟪{y}, j⟫⟫ ( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c))))
3230, 31bitr4i 243 . . . . . . . . . . . . . . . . . . . . 21 ((t 111c t, ⟪{y}, j⟫⟫ ( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c))) ↔ b(t = {{{b}}} t, ⟪{y}, j⟫⟫ ( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c))))
3332exbii 1582 . . . . . . . . . . . . . . . . . . . 20 (t(t 111c t, ⟪{y}, j⟫⟫ ( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c))) ↔ tb(t = {{{b}}} t, ⟪{y}, j⟫⟫ ( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c))))
34 df-rex 2620 . . . . . . . . . . . . . . . . . . . 20 (t 1 11ct, ⟪{y}, j⟫⟫ ( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c)) ↔ t(t 111c t, ⟪{y}, j⟫⟫ ( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c))))
35 excom 1741 . . . . . . . . . . . . . . . . . . . 20 (bt(t = {{{b}}} t, ⟪{y}, j⟫⟫ ( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c))) ↔ tb(t = {{{b}}} t, ⟪{y}, j⟫⟫ ( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c))))
3633, 34, 353bitr4i 268 . . . . . . . . . . . . . . . . . . 19 (t 1 11ct, ⟪{y}, j⟫⟫ ( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c)) ↔ bt(t = {{{b}}} t, ⟪{y}, j⟫⟫ ( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c))))
37 snex 4111 . . . . . . . . . . . . . . . . . . . . . 22 {{{b}}} V
38 opkeq1 4059 . . . . . . . . . . . . . . . . . . . . . . 23 (t = {{{b}}} → ⟪t, ⟪{y}, j⟫⟫ = ⟪{{{b}}}, ⟪{y}, j⟫⟫)
3938eleq1d 2419 . . . . . . . . . . . . . . . . . . . . . 22 (t = {{{b}}} → (⟪t, ⟪{y}, j⟫⟫ ( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c)) ↔ ⟪{{{b}}}, ⟪{y}, j⟫⟫ ( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c))))
4037, 39ceqsexv 2894 . . . . . . . . . . . . . . . . . . . . 21 (t(t = {{{b}}} t, ⟪{y}, j⟫⟫ ( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c))) ↔ ⟪{{{b}}}, ⟪{y}, j⟫⟫ ( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c)))
41 elin 3219 . . . . . . . . . . . . . . . . . . . . 21 (⟪{{{b}}}, ⟪{y}, j⟫⟫ ( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c)) ↔ (⟪{{{b}}}, ⟪{y}, j⟫⟫ Ins2k Sk ⟪{{{b}}}, ⟪{y}, j⟫⟫ (( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c)))
42 snex 4111 . . . . . . . . . . . . . . . . . . . . . . . 24 {b} V
4342, 20, 2otkelins2k 4255 . . . . . . . . . . . . . . . . . . . . . . 23 (⟪{{{b}}}, ⟪{y}, j⟫⟫ Ins2k Sk ↔ ⟪{b}, j Sk )
44 vex 2862 . . . . . . . . . . . . . . . . . . . . . . . 24 b V
4544, 2elssetk 4270 . . . . . . . . . . . . . . . . . . . . . . 23 (⟪{b}, j Skb j)
4643, 45bitri 240 . . . . . . . . . . . . . . . . . . . . . 22 (⟪{{{b}}}, ⟪{y}, j⟫⟫ Ins2k Skb j)
47 opkex 4113 . . . . . . . . . . . . . . . . . . . . . . . . 25 ⟪{{{b}}}, ⟪{y}, j⟫⟫ V
4847elimak 4259 . . . . . . . . . . . . . . . . . . . . . . . 24 (⟪{{{b}}}, ⟪{y}, j⟫⟫ (( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c) ↔ t 1 1111ct, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫ ( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))))
49 elpw141c 4150 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (t 11111ca t = {{{{{a}}}}})
5049anbi1i 676 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((t 11111c t, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫ ( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c)))) ↔ (a t = {{{{{a}}}}} t, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫ ( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c)))))
51 19.41v 1901 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (a(t = {{{{{a}}}}} t, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫ ( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c)))) ↔ (a t = {{{{{a}}}}} t, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫ ( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c)))))
5250, 51bitr4i 243 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((t 11111c t, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫ ( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c)))) ↔ a(t = {{{{{a}}}}} t, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫ ( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c)))))
5352exbii 1582 . . . . . . . . . . . . . . . . . . . . . . . . 25 (t(t 11111c t, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫ ( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c)))) ↔ ta(t = {{{{{a}}}}} t, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫ ( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c)))))
54 df-rex 2620 . . . . . . . . . . . . . . . . . . . . . . . . 25 (t 1 1111ct, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫ ( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) ↔ t(t 11111c t, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫ ( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c)))))
55 excom 1741 . . . . . . . . . . . . . . . . . . . . . . . . 25 (at(t = {{{{{a}}}}} t, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫ ( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c)))) ↔ ta(t = {{{{{a}}}}} t, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫ ( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c)))))
5653, 54, 553bitr4i 268 . . . . . . . . . . . . . . . . . . . . . . . 24 (t 1 1111ct, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫ ( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) ↔ at(t = {{{{{a}}}}} t, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫ ( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c)))))
57 snex 4111 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 {{{{{a}}}}} V
58 opkeq1 4059 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (t = {{{{{a}}}}} → ⟪t, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫ = ⟪{{{{{a}}}}}, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫)
5958eleq1d 2419 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (t = {{{{{a}}}}} → (⟪t, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫ ( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) ↔ ⟪{{{{{a}}}}}, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫ ( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c)))))
6057, 59ceqsexv 2894 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (t(t = {{{{{a}}}}} t, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫ ( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c)))) ↔ ⟪{{{{{a}}}}}, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫ ( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))))
61 elin 3219 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (⟪{{{{{a}}}}}, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫ ( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) ↔ (⟪{{{{{a}}}}}, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫ Ins2k Ins2k Sk ⟪{{{{{a}}}}}, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))))
62 snex 4111 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 {{{a}}} V
6362, 37, 27otkelins2k 4255 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (⟪{{{{{a}}}}}, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫ Ins2k Ins2k Sk ↔ ⟪{{{a}}}, ⟪{y}, j⟫⟫ Ins2k Sk )
64 snex 4111 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 {a} V
6564, 20, 2otkelins2k 4255 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (⟪{{{a}}}, ⟪{y}, j⟫⟫ Ins2k Sk ↔ ⟪{a}, j Sk )
66 vex 2862 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 a V
6766, 2elssetk 4270 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (⟪{a}, j Ska j)
6863, 65, 673bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (⟪{{{{{a}}}}}, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫ Ins2k Ins2k Ska j)
69 elin 3219 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (⟪{{{{{a}}}}}, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c)) ↔ (⟪{{{{{a}}}}}, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫ Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ⟪{{{{{a}}}}}, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c)))
7062, 37, 27otkelins3k 4256 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (⟪{{{{{a}}}}}, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫ Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ↔ ⟪{{{a}}}, {{{b}}}⟫ SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c))
71 snex 4111 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 {{a}} V
72 snex 4111 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 {{b}} V
7371, 72opksnelsik 4265 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (⟪{{{a}}}, {{{b}}}⟫ SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ↔ ⟪{{a}}, {{b}}⟫ SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c))
7464, 42opksnelsik 4265 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (⟪{{a}}, {{b}}⟫ SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ↔ ⟪{a}, {b}⟫ SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c))
7566, 44opksnelsik 4265 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (⟪{a}, {b}⟫ SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ↔ ⟪a, b ∼ (( Ins3k SkIns2k Sk ) “k 111c))
7666, 44ndisjrelk 4323 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (⟪a, b (( Ins3k SkIns2k Sk ) “k 111c) ↔ (ab) ≠ )
7776notbii 287 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (¬ ⟪a, b (( Ins3k SkIns2k Sk ) “k 111c) ↔ ¬ (ab) ≠ )
78 opkex 4113 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 a, b V
7978elcompl 3225 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (⟪a, b ∼ (( Ins3k SkIns2k Sk ) “k 111c) ↔ ¬ ⟪a, b (( Ins3k SkIns2k Sk ) “k 111c))
80 df-ne 2518 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((ab) ≠ ↔ ¬ (ab) = )
8180con2bii 322 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((ab) = ↔ ¬ (ab) ≠ )
8277, 79, 813bitr4i 268 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (⟪a, b ∼ (( Ins3k SkIns2k Sk ) “k 111c) ↔ (ab) = )
8374, 75, 823bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (⟪{{a}}, {{b}}⟫ SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ↔ (ab) = )
8470, 73, 833bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (⟪{{{{{a}}}}}, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫ Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ↔ (ab) = )
85 opkex 4113 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⟪{{{{{a}}}}}, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫ V
8685elimak 4259 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (⟪{{{{{a}}}}}, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c) ↔ t 1 1111111ct, ⟪{{{{{a}}}}}, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫⟫ ( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )))
87 elpw171c 4153 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (t 11111111cx t = {{{{{{{{x}}}}}}}})
8887anbi1i 676 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((t 11111111c t, ⟪{{{{{a}}}}}, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫⟫ ( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk ))) ↔ (x t = {{{{{{{{x}}}}}}}} t, ⟪{{{{{a}}}}}, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫⟫ ( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk ))))
89 19.41v 1901 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (x(t = {{{{{{{{x}}}}}}}} t, ⟪{{{{{a}}}}}, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫⟫ ( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk ))) ↔ (x t = {{{{{{{{x}}}}}}}} t, ⟪{{{{{a}}}}}, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫⟫ ( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk ))))
9088, 89bitr4i 243 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((t 11111111c t, ⟪{{{{{a}}}}}, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫⟫ ( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk ))) ↔ x(t = {{{{{{{{x}}}}}}}} t, ⟪{{{{{a}}}}}, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫⟫ ( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk ))))
9190exbii 1582 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (t(t 11111111c t, ⟪{{{{{a}}}}}, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫⟫ ( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk ))) ↔ tx(t = {{{{{{{{x}}}}}}}} t, ⟪{{{{{a}}}}}, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫⟫ ( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk ))))
92 df-rex 2620 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (t 1 1111111ct, ⟪{{{{{a}}}}}, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫⟫ ( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) ↔ t(t 11111111c t, ⟪{{{{{a}}}}}, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫⟫ ( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk ))))
93 excom 1741 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (xt(t = {{{{{{{{x}}}}}}}} t, ⟪{{{{{a}}}}}, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫⟫ ( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk ))) ↔ tx(t = {{{{{{{{x}}}}}}}} t, ⟪{{{{{a}}}}}, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫⟫ ( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk ))))
9491, 92, 933bitr4i 268 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (t 1 1111111ct, ⟪{{{{{a}}}}}, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫⟫ ( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) ↔ xt(t = {{{{{{{{x}}}}}}}} t, ⟪{{{{{a}}}}}, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫⟫ ( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk ))))
95 snex 4111 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 {{{{{{{{x}}}}}}}} V
96 opkeq1 4059 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (t = {{{{{{{{x}}}}}}}} → ⟪t, ⟪{{{{{a}}}}}, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫⟫ = ⟪{{{{{{{{x}}}}}}}}, ⟪{{{{{a}}}}}, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫⟫)
9796eleq1d 2419 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (t = {{{{{{{{x}}}}}}}} → (⟪t, ⟪{{{{{a}}}}}, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫⟫ ( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) ↔ ⟪{{{{{{{{x}}}}}}}}, ⟪{{{{{a}}}}}, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫⟫ ( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk ))))
9895, 97ceqsexv 2894 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (t(t = {{{{{{{{x}}}}}}}} t, ⟪{{{{{a}}}}}, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫⟫ ( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk ))) ↔ ⟪{{{{{{{{x}}}}}}}}, ⟪{{{{{a}}}}}, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫⟫ ( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )))
99 elsymdif 3223 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (⟪{{{{{{{{x}}}}}}}}, ⟪{{{{{a}}}}}, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫⟫ ( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) ↔ ¬ (⟪{{{{{{{{x}}}}}}}}, ⟪{{{{{a}}}}}, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫⟫ Ins2k Ins2k Ins3k SIk Sk ↔ ⟪{{{{{{{{x}}}}}}}}, ⟪{{{{{a}}}}}, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫⟫ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )))
100 snex 4111 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 {{{{{{x}}}}}} V
101100, 57, 47otkelins2k 4255 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (⟪{{{{{{{{x}}}}}}}}, ⟪{{{{{a}}}}}, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫⟫ Ins2k Ins2k Ins3k SIk Sk ↔ ⟪{{{{{{x}}}}}}, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫ Ins2k Ins3k SIk Sk )
102 snex 4111 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 {{{{x}}}} V
103102, 37, 27otkelins2k 4255 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (⟪{{{{{{x}}}}}}, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫ Ins2k Ins3k SIk Sk ↔ ⟪{{{{x}}}}, ⟪{y}, j⟫⟫ Ins3k SIk Sk )
104 snex 4111 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 {{x}} V
105104, 20, 2otkelins3k 4256 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (⟪{{{{x}}}}, ⟪{y}, j⟫⟫ Ins3k SIk Sk ↔ ⟪{{x}}, {y}⟫ SIk Sk )
106 snex 4111 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 {x} V
107106, 23opksnelsik 4265 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (⟪{{x}}, {y}⟫ SIk Sk ↔ ⟪{x}, y Sk )
10821, 23elssetk 4270 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (⟪{x}, y Skx y)
109105, 107, 1083bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (⟪{{{{x}}}}, ⟪{y}, j⟫⟫ Ins3k SIk Skx y)
110101, 103, 1093bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (⟪{{{{{{{{x}}}}}}}}, ⟪{{{{{a}}}}}, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫⟫ Ins2k Ins2k Ins3k SIk Skx y)
111100, 57, 47otkelins3k 4256 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (⟪{{{{{{{{x}}}}}}}}, ⟪{{{{{a}}}}}, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫⟫ Ins3k SIk SIk SIk SIk SIk Sk ↔ ⟪{{{{{{x}}}}}}, {{{{{a}}}}}⟫ SIk SIk SIk SIk SIk Sk )
112 snex 4111 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 {{{{{x}}}}} V
113 snex 4111 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 {{{{a}}}} V
114112, 113opksnelsik 4265 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (⟪{{{{{{x}}}}}}, {{{{{a}}}}}⟫ SIk SIk SIk SIk SIk Sk ↔ ⟪{{{{{x}}}}}, {{{{a}}}}⟫ SIk SIk SIk SIk Sk )
115102, 62opksnelsik 4265 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (⟪{{{{{x}}}}}, {{{{a}}}}⟫ SIk SIk SIk SIk Sk ↔ ⟪{{{{x}}}}, {{{a}}}⟫ SIk SIk SIk Sk )
116 snex 4111 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 {{{x}}} V
117116, 71opksnelsik 4265 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (⟪{{{{x}}}}, {{{a}}}⟫ SIk SIk SIk Sk ↔ ⟪{{{x}}}, {{a}}⟫ SIk SIk Sk )
118104, 64opksnelsik 4265 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (⟪{{{x}}}, {{a}}⟫ SIk SIk Sk ↔ ⟪{{x}}, {a}⟫ SIk Sk )
119106, 66opksnelsik 4265 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (⟪{{x}}, {a}⟫ SIk Sk ↔ ⟪{x}, a Sk )
12021, 66elssetk 4270 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (⟪{x}, a Skx a)
121118, 119, 1203bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (⟪{{{x}}}, {{a}}⟫ SIk SIk Skx a)
122115, 117, 1213bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (⟪{{{{{x}}}}}, {{{{a}}}}⟫ SIk SIk SIk SIk Skx a)
123111, 114, 1223bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (⟪{{{{{{{{x}}}}}}}}, ⟪{{{{{a}}}}}, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫⟫ Ins3k SIk SIk SIk SIk SIk Skx a)
124100, 57, 47otkelins2k 4255 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (⟪{{{{{{{{x}}}}}}}}, ⟪{{{{{a}}}}}, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫⟫ Ins2k Ins3k SIk SIk SIk Sk ↔ ⟪{{{{{{x}}}}}}, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫ Ins3k SIk SIk SIk Sk )
125102, 37, 27otkelins3k 4256 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (⟪{{{{{{x}}}}}}, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫ Ins3k SIk SIk SIk Sk ↔ ⟪{{{{x}}}}, {{{b}}}⟫ SIk SIk SIk Sk )
126116, 72opksnelsik 4265 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (⟪{{{{x}}}}, {{{b}}}⟫ SIk SIk SIk Sk ↔ ⟪{{{x}}}, {{b}}⟫ SIk SIk Sk )
127104, 42opksnelsik 4265 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (⟪{{{x}}}, {{b}}⟫ SIk SIk Sk ↔ ⟪{{x}}, {b}⟫ SIk Sk )
128106, 44opksnelsik 4265 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (⟪{{x}}, {b}⟫ SIk Sk ↔ ⟪{x}, b Sk )
12921, 44elssetk 4270 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (⟪{x}, b Skx b)
130128, 129bitri 240 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (⟪{{x}}, {b}⟫ SIk Skx b)
131126, 127, 1303bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (⟪{{{{x}}}}, {{{b}}}⟫ SIk SIk SIk Skx b)
132124, 125, 1313bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (⟪{{{{{{{{x}}}}}}}}, ⟪{{{{{a}}}}}, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫⟫ Ins2k Ins3k SIk SIk SIk Skx b)
133123, 132orbi12i 507 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((⟪{{{{{{{{x}}}}}}}}, ⟪{{{{{a}}}}}, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫⟫ Ins3k SIk SIk SIk SIk SIk Sk ⟪{{{{{{{{x}}}}}}}}, ⟪{{{{{a}}}}}, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫⟫ Ins2k Ins3k SIk SIk SIk Sk ) ↔ (x a x b))
134 elun 3220 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (⟪{{{{{{{{x}}}}}}}}, ⟪{{{{{a}}}}}, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫⟫ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk ) ↔ (⟪{{{{{{{{x}}}}}}}}, ⟪{{{{{a}}}}}, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫⟫ Ins3k SIk SIk SIk SIk SIk Sk ⟪{{{{{{{{x}}}}}}}}, ⟪{{{{{a}}}}}, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫⟫ Ins2k Ins3k SIk SIk SIk Sk ))
135 elun 3220 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (x (ab) ↔ (x a x b))
136133, 134, 1353bitr4i 268 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (⟪{{{{{{{{x}}}}}}}}, ⟪{{{{{a}}}}}, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫⟫ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk ) ↔ x (ab))
137110, 136bibi12i 306 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((⟪{{{{{{{{x}}}}}}}}, ⟪{{{{{a}}}}}, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫⟫ Ins2k Ins2k Ins3k SIk Sk ↔ ⟪{{{{{{{{x}}}}}}}}, ⟪{{{{{a}}}}}, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫⟫ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) ↔ (x yx (ab)))
138137notbii 287 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (¬ (⟪{{{{{{{{x}}}}}}}}, ⟪{{{{{a}}}}}, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫⟫ Ins2k Ins2k Ins3k SIk Sk ↔ ⟪{{{{{{{{x}}}}}}}}, ⟪{{{{{a}}}}}, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫⟫ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) ↔ ¬ (x yx (ab)))
13998, 99, 1383bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (t(t = {{{{{{{{x}}}}}}}} t, ⟪{{{{{a}}}}}, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫⟫ ( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk ))) ↔ ¬ (x yx (ab)))
140139exbii 1582 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (xt(t = {{{{{{{{x}}}}}}}} t, ⟪{{{{{a}}}}}, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫⟫ ( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk ))) ↔ x ¬ (x yx (ab)))
14186, 94, 1403bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (⟪{{{{{a}}}}}, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c) ↔ x ¬ (x yx (ab)))
142141notbii 287 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (¬ ⟪{{{{{a}}}}}, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c) ↔ ¬ x ¬ (x yx (ab)))
14385elcompl 3225 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (⟪{{{{{a}}}}}, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c) ↔ ¬ ⟪{{{{{a}}}}}, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))
144 dfcleq 2347 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (y = (ab) ↔ x(x yx (ab)))
145 alex 1572 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (x(x yx (ab)) ↔ ¬ x ¬ (x yx (ab)))
146144, 145bitri 240 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (y = (ab) ↔ ¬ x ¬ (x yx (ab)))
147142, 143, 1463bitr4i 268 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (⟪{{{{{a}}}}}, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c) ↔ y = (ab))
14884, 147anbi12i 678 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((⟪{{{{{a}}}}}, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫ Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ⟪{{{{{a}}}}}, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c)) ↔ ((ab) = y = (ab)))
14969, 148bitri 240 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (⟪{{{{{a}}}}}, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c)) ↔ ((ab) = y = (ab)))
15068, 149anbi12i 678 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((⟪{{{{{a}}}}}, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫ Ins2k Ins2k Sk ⟪{{{{{a}}}}}, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) ↔ (a j ((ab) = y = (ab))))
15160, 61, 1503bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . 25 (t(t = {{{{{a}}}}} t, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫ ( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c)))) ↔ (a j ((ab) = y = (ab))))
152151exbii 1582 . . . . . . . . . . . . . . . . . . . . . . . 24 (at(t = {{{{{a}}}}} t, ⟪{{{b}}}, ⟪{y}, j⟫⟫⟫ ( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c)))) ↔ a(a j ((ab) = y = (ab))))
15348, 56, 1523bitri 262 . . . . . . . . . . . . . . . . . . . . . . 23 (⟪{{{b}}}, ⟪{y}, j⟫⟫ (( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c) ↔ a(a j ((ab) = y = (ab))))
154 df-rex 2620 . . . . . . . . . . . . . . . . . . . . . . 23 (a j ((ab) = y = (ab)) ↔ a(a j ((ab) = y = (ab))))
155153, 154bitr4i 243 . . . . . . . . . . . . . . . . . . . . . 22 (⟪{{{b}}}, ⟪{y}, j⟫⟫ (( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c) ↔ a j ((ab) = y = (ab)))
15646, 155anbi12i 678 . . . . . . . . . . . . . . . . . . . . 21 ((⟪{{{b}}}, ⟪{y}, j⟫⟫ Ins2k Sk ⟪{{{b}}}, ⟪{y}, j⟫⟫ (( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c)) ↔ (b j a j ((ab) = y = (ab))))
15740, 41, 1563bitri 262 . . . . . . . . . . . . . . . . . . . 20 (t(t = {{{b}}} t, ⟪{y}, j⟫⟫ ( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c))) ↔ (b j a j ((ab) = y = (ab))))
158157exbii 1582 . . . . . . . . . . . . . . . . . . 19 (bt(t = {{{b}}} t, ⟪{y}, j⟫⟫ ( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c))) ↔ b(b j a j ((ab) = y = (ab))))
15928, 36, 1583bitri 262 . . . . . . . . . . . . . . . . . 18 (⟪{y}, j (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c)) “k 111c) ↔ b(b j a j ((ab) = y = (ab))))
160 df-rex 2620 . . . . . . . . . . . . . . . . . 18 (b j a j ((ab) = y = (ab)) ↔ b(b j a j ((ab) = y = (ab))))
161159, 160bitr4i 243 . . . . . . . . . . . . . . . . 17 (⟪{y}, j (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c)) “k 111c) ↔ b j a j ((ab) = y = (ab)))
162 rexcom 2772 . . . . . . . . . . . . . . . . 17 (b j a j ((ab) = y = (ab)) ↔ a j b j ((ab) = y = (ab)))
16326, 161, 1623bitri 262 . . . . . . . . . . . . . . . 16 (⟪{{{y}}}, ⟪x, j⟫⟫ Ins2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c)) “k 111c) ↔ a j b j ((ab) = y = (ab)))
16425, 163bibi12i 306 . . . . . . . . . . . . . . 15 ((⟪{{{y}}}, ⟪x, j⟫⟫ Ins3k Sk ↔ ⟪{{{y}}}, ⟪x, j⟫⟫ Ins2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c)) “k 111c)) ↔ (y xa j b j ((ab) = y = (ab))))
165164notbii 287 . . . . . . . . . . . . . 14 (¬ (⟪{{{y}}}, ⟪x, j⟫⟫ Ins3k Sk ↔ ⟪{{{y}}}, ⟪x, j⟫⟫ Ins2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c)) “k 111c)) ↔ ¬ (y xa j b j ((ab) = y = (ab))))
16618, 19, 1653bitri 262 . . . . . . . . . . . . 13 (t(t = {{{y}}} t, ⟪x, j⟫⟫ ( Ins3k SkIns2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c)) “k 111c))) ↔ ¬ (y xa j b j ((ab) = y = (ab))))
167166exbii 1582 . . . . . . . . . . . 12 (yt(t = {{{y}}} t, ⟪x, j⟫⟫ ( Ins3k SkIns2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c)) “k 111c))) ↔ y ¬ (y xa j b j ((ab) = y = (ab))))
1686, 14, 1673bitri 262 . . . . . . . . . . 11 (⟪x, j (( Ins3k SkIns2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c)) “k 111c)) “k 111c) ↔ y ¬ (y xa j b j ((ab) = y = (ab))))
169168notbii 287 . . . . . . . . . 10 (¬ ⟪x, j (( Ins3k SkIns2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c)) “k 111c)) “k 111c) ↔ ¬ y ¬ (y xa j b j ((ab) = y = (ab))))
1705elcompl 3225 . . . . . . . . . 10 (⟪x, j ∼ (( Ins3k SkIns2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c)) “k 111c)) “k 111c) ↔ ¬ ⟪x, j (( Ins3k SkIns2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c)) “k 111c)) “k 111c))
171 alex 1572 . . . . . . . . . 10 (y(y xa j b j ((ab) = y = (ab))) ↔ ¬ y ¬ (y xa j b j ((ab) = y = (ab))))
172169, 170, 1713bitr4i 268 . . . . . . . . 9 (⟪x, j ∼ (( Ins3k SkIns2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c)) “k 111c)) “k 111c) ↔ y(y xa j b j ((ab) = y = (ab))))
173 df-addc 4378 . . . . . . . . . . 11 (j +c j) = {y a j b j ((ab) = y = (ab))}
174173eqeq2i 2363 . . . . . . . . . 10 (x = (j +c j) ↔ x = {y a j b j ((ab) = y = (ab))})
175 abeq2 2458 . . . . . . . . . 10 (x = {y a j b j ((ab) = y = (ab))} ↔ y(y xa j b j ((ab) = y = (ab))))
176174, 175bitri 240 . . . . . . . . 9 (x = (j +c j) ↔ y(y xa j b j ((ab) = y = (ab))))
177172, 176bitr4i 243 . . . . . . . 8 (⟪x, j ∼ (( Ins3k SkIns2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c)) “k 111c)) “k 111c) ↔ x = (j +c j))
17821, 2opkelxpk 4248 . . . . . . . . . 10 (⟪x, j (({} ∪ ∼ ((( Ins3k (( Ins2k ∼ (( Ins3k SkIns2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k k SIk SIk SIk (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk SkIns3k SIk SIk SIk SIk SIk Sk )) “k 11111111c))) “k 11111c)) “k 111c)) “k 111c) ∩ Ins3k Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c)) “k 11c) ∩ Ins2k ( Ik ({} ×k V))) “k 11c) “k Nn )) ×k V) ↔ (x ({} ∪ ∼ ((( Ins3k (( Ins2k ∼ (( Ins3k SkIns2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k k SIk SIk SIk (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk SkIns3k SIk SIk SIk SIk SIk Sk )) “k 11111111c))) “k 11111c)) “k 111c)) “k 111c) ∩ Ins3k Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c)) “k 11c) ∩ Ins2k ( Ik ({} ×k V))) “k 11c) “k Nn )) j V))
1792, 178mpbiran2 885 . . . . . . . . 9 (⟪x, j (({} ∪ ∼ ((( Ins3k (( Ins2k ∼ (( Ins3k SkIns2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k k SIk SIk SIk (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk SkIns3k SIk SIk SIk SIk SIk Sk )) “k 11111111c))) “k 11111c)) “k 111c)) “k 111c) ∩ Ins3k Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c)) “k 11c) ∩ Ins2k ( Ik ({} ×k V))) “k 11c) “k Nn )) ×k V) ↔ x ({} ∪ ∼ ((( Ins3k (( Ins2k ∼ (( Ins3k SkIns2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k k SIk SIk SIk (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk SkIns3k SIk SIk SIk SIk SIk Sk )) “k 11111111c))) “k 11111c)) “k 111c)) “k 111c) ∩ Ins3k Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c)) “k 11c) ∩ Ins2k ( Ik ({} ×k V))) “k 11c) “k Nn )))
180 elun 3220 . . . . . . . . 9 (x ({} ∪ ∼ ((( Ins3k (( Ins2k ∼ (( Ins3k SkIns2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k k SIk SIk SIk (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk SkIns3k SIk SIk SIk SIk SIk Sk )) “k 11111111c))) “k 11111c)) “k 111c)) “k 111c) ∩ Ins3k Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c)) “k 11c) ∩ Ins2k ( Ik ({} ×k V))) “k 11c) “k Nn )) ↔ (x {} x ∼ ((( Ins3k (( Ins2k ∼ (( Ins3k SkIns2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k k SIk SIk SIk (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk SkIns3k SIk SIk SIk SIk SIk Sk )) “k 11111111c))) “k 11111c)) “k 111c)) “k 111c) ∩ Ins3k Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c)) “k 11c) ∩ Ins2k ( Ik ({} ×k V))) “k 11c) “k Nn )))
18121elsnc 3756 . . . . . . . . . 10 (x {} ↔ x = )
18221elimak 4259 . . . . . . . . . . . . 13 (x ((( Ins3k (( Ins2k ∼ (( Ins3k SkIns2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k k SIk SIk SIk (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk SkIns3k SIk SIk SIk SIk SIk Sk )) “k 11111111c))) “k 11111c)) “k 111c)) “k 111c) ∩ Ins3k Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c)) “k 11c) ∩ Ins2k ( Ik ({} ×k V))) “k 11c) “k Nn ) ↔ n Nnn, x (( Ins3k (( Ins2k ∼ (( Ins3k SkIns2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k k SIk SIk SIk (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk SkIns3k SIk SIk SIk SIk SIk Sk )) “k 11111111c))) “k 11111c)) “k 111c)) “k 111c) ∩ Ins3k Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c)) “k 11c) ∩ Ins2k ( Ik ({} ×k V))) “k 11c))
183 opkex 4113 . . . . . . . . . . . . . . . . 17 n, x V
184183elimak 4259 . . . . . . . . . . . . . . . 16 (⟪n, x (( Ins3k (( Ins2k ∼ (( Ins3k SkIns2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k k SIk SIk SIk (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk SkIns3k SIk SIk SIk SIk SIk Sk )) “k 11111111c))) “k 11111c)) “k 111c)) “k 111c) ∩ Ins3k Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c)) “k 11c) ∩ Ins2k ( Ik ({} ×k V))) “k 11c) ↔ t 1 1ct, ⟪n, x⟫⟫ ( Ins3k (( Ins2k ∼ (( Ins3k SkIns2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k k SIk SIk SIk (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk SkIns3k SIk SIk SIk SIk SIk Sk )) “k 11111111c))) “k 11111c)) “k 111c)) “k 111c) ∩ Ins3k Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c)) “k 11c) ∩ Ins2k ( Ik ({} ×k V))))
185 elpw11c 4147 . . . . . . . . . . . . . . . . . . . 20 (t 11cy t = {{y}})
186185anbi1i 676 . . . . . . . . . . . . . . . . . . 19 ((t 11c t, ⟪n, x⟫⟫ ( Ins3k (( Ins2k ∼ (( Ins3k SkIns2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k k SIk SIk SIk (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk SkIns3k SIk SIk SIk SIk SIk Sk )) “k 11111111c))) “k 11111c)) “k 111c)) “k 111c) ∩ Ins3k Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c)) “k 11c) ∩ Ins2k ( Ik ({} ×k V)))) ↔ (y t = {{y}} t, ⟪n, x⟫⟫ ( Ins3k (( Ins2k ∼ (( Ins3k SkIns2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k k SIk SIk SIk (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk SkIns3k SIk SIk SIk SIk SIk Sk )) “k 11111111c))) “k 11111c)) “k 111c)) “k 111c) ∩ Ins3k Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c)) “k 11c) ∩ Ins2k ( Ik ({} ×k V)))))
187 19.41v 1901 . . . . . . . . . . . . . . . . . . 19 (y(t = {{y}} t, ⟪n, x⟫⟫ ( Ins3k (( Ins2k ∼ (( Ins3k SkIns2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k k SIk SIk SIk (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk SkIns3k SIk SIk SIk SIk SIk Sk )) “k 11111111c))) “k 11111c)) “k 111c)) “k 111c) ∩ Ins3k Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c)) “k 11c) ∩ Ins2k ( Ik ({} ×k V)))) ↔ (y t = {{y}} t, ⟪n, x⟫⟫ ( Ins3k (( Ins2k ∼ (( Ins3k SkIns2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k k SIk SIk SIk (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk SkIns3k SIk SIk SIk SIk SIk Sk )) “k 11111111c))) “k 11111c)) “k 111c)) “k 111c) ∩ Ins3k Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c)) “k 11c) ∩ Ins2k ( Ik ({} ×k V)))))
188186, 187bitr4i 243 . . . . . . . . . . . . . . . . . 18 ((t 11c t, ⟪n, x⟫⟫ ( Ins3k (( Ins2k ∼ (( Ins3k SkIns2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k k SIk SIk SIk (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk SkIns3k SIk SIk SIk SIk SIk Sk )) “k 11111111c))) “k 11111c)) “k 111c)) “k 111c) ∩ Ins3k Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c)) “k 11c) ∩ Ins2k ( Ik ({} ×k V)))) ↔ y(t = {{y}} t, ⟪n, x⟫⟫ ( Ins3k (( Ins2k ∼ (( Ins3k SkIns2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k k SIk SIk SIk (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk SkIns3k SIk SIk SIk SIk SIk Sk )) “k 11111111c))) “k 11111c)) “k 111c)) “k 111c) ∩ Ins3k Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c)) “k 11c) ∩ Ins2k ( Ik ({} ×k V)))))
189188exbii 1582 . . . . . . . . . . . . . . . . 17 (t(t 11c t, ⟪n, x⟫⟫ ( Ins3k (( Ins2k ∼ (( Ins3k SkIns2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k k SIk SIk SIk (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk SkIns3k SIk SIk SIk SIk SIk Sk )) “k 11111111c))) “k 11111c)) “k 111c)) “k 111c) ∩ Ins3k Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c)) “k 11c) ∩ Ins2k ( Ik ({} ×k V)))) ↔ ty(t = {{y}} t, ⟪n, x⟫⟫ ( Ins3k (( Ins2k ∼ (( Ins3k SkIns2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k k SIk SIk SIk (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk SkIns3k SIk SIk SIk SIk SIk Sk )) “k 11111111c))) “k 11111c)) “k 111c)) “k 111c) ∩ Ins3k Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c)) “k 11c) ∩ Ins2k ( Ik ({} ×k V)))))
190 df-rex 2620 . . . . . . . . . . . . . . . . 17 (t 1 1ct, ⟪n, x⟫⟫ ( Ins3k (( Ins2k ∼ (( Ins3k SkIns2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k k SIk SIk SIk (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk SkIns3k SIk SIk SIk SIk SIk Sk )) “k 11111111c))) “k 11111c)) “k 111c)) “k 111c) ∩ Ins3k Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c)) “k 11c) ∩ Ins2k ( Ik ({} ×k V))) ↔ t(t 11c t, ⟪n, x⟫⟫ ( Ins3k (( Ins2k ∼ (( Ins3k SkIns2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k k SIk SIk SIk (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk SkIns3k SIk SIk SIk SIk SIk Sk )) “k 11111111c))) “k 11111c)) “k 111c)) “k 111c) ∩ Ins3k Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c)) “k 11c) ∩ Ins2k ( Ik ({} ×k V)))))
191 excom 1741 . . . . . . . . . . . . . . . . 17 (yt(t = {{y}} t, ⟪n, x⟫⟫ ( Ins3k (( Ins2k ∼ (( Ins3k SkIns2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k k SIk SIk SIk (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk SkIns3k SIk SIk SIk SIk SIk Sk )) “k 11111111c))) “k 11111c)) “k 111c)) “k 111c) ∩ Ins3k Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c)) “k 11c) ∩ Ins2k ( Ik ({} ×k V)))) ↔ ty(t = {{y}} t, ⟪n, x⟫⟫ ( Ins3k (( Ins2k ∼ (( Ins3k SkIns2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k k SIk SIk SIk (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk SkIns3k SIk SIk SIk SIk SIk Sk )) “k 11111111c))) “k 11111c)) “k 111c)) “k 111c) ∩ Ins3k Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c)) “k 11c) ∩ Ins2k ( Ik ({} ×k V)))))
192189, 190, 1913bitr4i 268 . . . . . . . . . . . . . . . 16 (t 1 1ct, ⟪n, x⟫⟫ ( Ins3k (( Ins2k ∼ (( Ins3k SkIns2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k k SIk SIk SIk (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk SkIns3k SIk SIk SIk SIk SIk Sk )) “k 11111111c))) “k 11111c)) “k 111c)) “k 111c) ∩ Ins3k Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c)) “k 11c) ∩ Ins2k ( Ik ({} ×k V))) ↔ yt(t = {{y}} t, ⟪n, x⟫⟫ ( Ins3k (( Ins2k ∼ (( Ins3k SkIns2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k k SIk SIk SIk (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk SkIns3k SIk SIk SIk SIk SIk Sk )) “k 11111111c))) “k 11111c)) “k 111c)) “k 111c) ∩ Ins3k Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c)) “k 11c) ∩ Ins2k ( Ik ({} ×k V)))))
193 snex 4111 . . . . . . . . . . . . . . . . . . 19 {{y}} V
194 opkeq1 4059 . . . . . . . . . . . . . . . . . . . 20 (t = {{y}} → ⟪t, ⟪n, x⟫⟫ = ⟪{{y}}, ⟪n, x⟫⟫)
195194eleq1d 2419 . . . . . . . . . . . . . . . . . . 19 (t = {{y}} → (⟪t, ⟪n, x⟫⟫ ( Ins3k (( Ins2k ∼ (( Ins3k SkIns2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k k SIk SIk SIk (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk SkIns3k SIk SIk SIk SIk SIk Sk )) “k 11111111c))) “k 11111c)) “k 111c)) “k 111c) ∩ Ins3k Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c)) “k 11c) ∩ Ins2k ( Ik ({} ×k V))) ↔ ⟪{{y}}, ⟪n, x⟫⟫ ( Ins3k (( Ins2k ∼ (( Ins3k SkIns2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k k SIk SIk SIk (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk SkIns3k SIk SIk SIk SIk SIk Sk )) “k 11111111c))) “k 11111c)) “k 111c)) “k 111c) ∩ Ins3k Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c)) “k 11c) ∩ Ins2k ( Ik ({} ×k V)))))
196193, 195ceqsexv 2894 . . . . . . . . . . . . . . . . . 18 (t(t = {{y}} t, ⟪n, x⟫⟫ ( Ins3k (( Ins2k ∼ (( Ins3k SkIns2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k k SIk SIk SIk (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk SkIns3k SIk SIk SIk SIk SIk Sk )) “k 11111111c))) “k 11111c)) “k 111c)) “k 111c) ∩ Ins3k Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c)) “k 11c) ∩ Ins2k ( Ik ({} ×k V)))) ↔ ⟪{{y}}, ⟪n, x⟫⟫ ( Ins3k (( Ins2k ∼ (( Ins3k SkIns2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k k SIk SIk SIk (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk SkIns3k SIk SIk SIk SIk SIk Sk )) “k 11111111c))) “k 11111c)) “k 111c)) “k 111c) ∩ Ins3k Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c)) “k 11c) ∩ Ins2k ( Ik ({} ×k V))))
197 elin 3219 . . . . . . . . . . . . . . . . . 18 (⟪{{y}}, ⟪n, x⟫⟫ ( Ins3k (( Ins2k ∼ (( Ins3k SkIns2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k k SIk SIk SIk (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk SkIns3k SIk SIk SIk SIk SIk Sk )) “k 11111111c))) “k 11111c)) “k 111c)) “k 111c) ∩ Ins3k Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c)) “k 11c) ∩ Ins2k ( Ik ({} ×k V))) ↔ (⟪{{y}}, ⟪n, x⟫⟫ Ins3k (( Ins2k ∼ (( Ins3k SkIns2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k k SIk SIk SIk (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk SkIns3k SIk SIk SIk SIk SIk Sk )) “k 11111111c))) “k 11111c)) “k 111c)) “k 111c) ∩ Ins3k Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c)) “k 11c) ⟪{{y}}, ⟪n, x⟫⟫ Ins2k ( Ik ({} ×k V))))
198 vex 2862 . . . . . . . . . . . . . . . . . . . . 21 n V
19923, 198, 21otkelins3k 4256 . . . . . . . . . . . . . . . . . . . 20 (⟪{{y}}, ⟪n, x⟫⟫ Ins3k (( Ins2k ∼ (( Ins3k SkIns2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k k SIk SIk SIk (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk SkIns3k SIk SIk SIk SIk SIk Sk )) “k 11111111c))) “k 11111c)) “k 111c)) “k 111c) ∩ Ins3k Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c)) “k 11c) ↔ ⟪y, n (( Ins2k ∼ (( Ins3k SkIns2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k k SIk SIk SIk (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk SkIns3k SIk SIk SIk SIk SIk Sk )) “k 11111111c))) “k 11111c)) “k 111c)) “k 111c) ∩ Ins3k Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c)) “k 11c))
200 opkex 4113 . . . . . . . . . . . . . . . . . . . . . 22 y, n V
201200elimak 4259 . . . . . . . . . . . . . . . . . . . . 21 (⟪y, n (( Ins2k ∼ (( Ins3k SkIns2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k k SIk SIk SIk (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk SkIns3k SIk SIk SIk SIk SIk Sk )) “k 11111111c))) “k 11111c)) “k 111c)) “k 111c) ∩ Ins3k Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c)) “k 11c) ↔ t 1 1ct, ⟪y, n⟫⟫ ( Ins2k ∼ (( Ins3k SkIns2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k k SIk SIk SIk (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk SkIns3k SIk SIk SIk SIk SIk Sk )) “k 11111111c))) “k 11111c)) “k 111c)) “k 111c) ∩ Ins3k Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c)))
202 elpw11c 4147 . . . . . . . . . . . . . . . . . . . . . . . . 25 (t 11cx t = {{x}})
203202anbi1i 676 . . . . . . . . . . . . . . . . . . . . . . . 24 ((t 11c t, ⟪y, n⟫⟫ ( Ins2k ∼ (( Ins3k SkIns2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k k SIk SIk SIk (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk SkIns3k SIk SIk SIk SIk SIk Sk )) “k 11111111c))) “k 11111c)) “k 111c)) “k 111c) ∩ Ins3k Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c))) ↔ (x t = {{x}} t, ⟪y, n⟫⟫ ( Ins2k ∼ (( Ins3k SkIns2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k k SIk SIk SIk (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk SkIns3k SIk SIk SIk SIk SIk Sk )) “k 11111111c))) “k 11111c)) “k 111c)) “k 111c) ∩ Ins3k Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c))))
204 19.41v 1901 . . . . . . . . . . . . . . . . . . . . . . . 24 (x(t = {{x}} t, ⟪y, n⟫⟫ ( Ins2k ∼ (( Ins3k SkIns2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k k SIk SIk SIk (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk SkIns3k SIk SIk SIk SIk SIk Sk )) “k 11111111c))) “k 11111c)) “k 111c)) “k 111c) ∩ Ins3k Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c))) ↔ (x t = {{x}} t, ⟪y, n⟫⟫ ( Ins2k ∼ (( Ins3k SkIns2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k k SIk SIk SIk (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk SkIns3k SIk SIk SIk SIk SIk Sk )) “k 11111111c))) “k 11111c)) “k 111c)) “k 111c) ∩ Ins3k Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c))))
205203, 204bitr4i 243 . . . . . . . . . . . . . . . . . . . . . . 23 ((t 11c t, ⟪y, n⟫⟫ ( Ins2k ∼ (( Ins3k SkIns2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k k SIk SIk SIk (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk SkIns3k SIk SIk SIk SIk SIk Sk )) “k 11111111c))) “k 11111c)) “k 111c)) “k 111c) ∩ Ins3k Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c))) ↔ x(t = {{x}} t, ⟪y, n⟫⟫ ( Ins2k ∼ (( Ins3k SkIns2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k k SIk SIk SIk (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk SkIns3k SIk SIk SIk SIk SIk Sk )) “k 11111111c))) “k 11111c)) “k 111c)) “k 111c) ∩ Ins3k Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c))))
206205exbii 1582 . . . . . . . . . . . . . . . . . . . . . 22 (t(t 11c t, ⟪y, n⟫⟫ ( Ins2k ∼ (( Ins3k SkIns2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k k SIk SIk SIk (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk SkIns3k SIk SIk SIk SIk SIk Sk )) “k 11111111c))) “k 11111c)) “k 111c)) “k 111c) ∩ Ins3k Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c))) ↔ tx(t = {{x}} t, ⟪y, n⟫⟫ ( Ins2k ∼ (( Ins3k SkIns2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k k SIk SIk SIk (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk SkIns3k SIk SIk SIk SIk SIk Sk )) “k 11111111c))) “k 11111c)) “k 111c)) “k 111c) ∩ Ins3k Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c))))
207 df-rex 2620 . . . . . . . . . . . . . . . . . . . . . 22 (t 1 1ct, ⟪y, n⟫⟫ ( Ins2k ∼ (( Ins3k SkIns2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k k SIk SIk SIk (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk SkIns3k SIk SIk SIk SIk SIk Sk )) “k 11111111c))) “k 11111c)) “k 111c)) “k 111c) ∩ Ins3k Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c)) ↔ t(t 11c t, ⟪y, n⟫⟫ ( Ins2k ∼ (( Ins3k SkIns2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k k SIk SIk SIk (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk SkIns3k SIk SIk SIk SIk SIk Sk )) “k 11111111c))) “k 11111c)) “k 111c)) “k 111c) ∩ Ins3k Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c))))
208 excom 1741 . . . . . . . . . . . . . . . . . . . . . 22 (xt(t = {{x}} t, ⟪y, n⟫⟫ ( Ins2k ∼ (( Ins3k SkIns2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k k SIk SIk SIk (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk SkIns3k SIk SIk SIk SIk SIk Sk )) “k 11111111c))) “k 11111c)) “k 111c)) “k 111c) ∩ Ins3k Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c))) ↔ tx(t = {{x}} t, ⟪y, n⟫⟫ ( Ins2k ∼ (( Ins3k SkIns2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k k SIk SIk SIk (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk SkIns3k SIk SIk SIk SIk SIk Sk )) “k 11111111c))) “k 11111c)) “k 111c)) “k 111c) ∩ Ins3k Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c))))
209206, 207, 2083bitr4i 268 . . . . . . . . . . . . . . . . . . . . 21 (t 1 1ct, ⟪y, n⟫⟫ ( Ins2k ∼ (( Ins3k SkIns2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k k SIk SIk SIk (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk SkIns3k SIk SIk SIk SIk SIk Sk )) “k 11111111c))) “k 11111c)) “k 111c)) “k 111c) ∩ Ins3k Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c)) ↔ xt(t = {{x}} t, ⟪y, n⟫⟫ ( Ins2k ∼ (( Ins3k SkIns2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k k SIk SIk SIk (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk SkIns3k SIk SIk SIk SIk SIk Sk )) “k 11111111c))) “k 11111c)) “k 111c)) “k 111c) ∩ Ins3k Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c))))
210 opkeq1 4059 . . . . . . . . . . . . . . . . . . . . . . . . 25 (t = {{x}} → ⟪t, ⟪y, n⟫⟫ = ⟪{{x}}, ⟪y, n⟫⟫)
211210eleq1d 2419 . . . . . . . . . . . . . . . . . . . . . . . 24 (t = {{x}} → (⟪t, ⟪y, n⟫⟫ ( Ins2k ∼ (( Ins3k SkIns2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k k SIk SIk SIk (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk SkIns3k SIk SIk SIk SIk SIk Sk )) “k 11111111c))) “k 11111c)) “k 111c)) “k 111c) ∩ Ins3k Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c)) ↔ ⟪{{x}}, ⟪y, n⟫⟫ ( Ins2k ∼ (( Ins3k SkIns2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k k SIk SIk SIk (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk SkIns3k SIk SIk SIk SIk SIk Sk )) “k 11111111c))) “k 11111c)) “k 111c)) “k 111c) ∩ Ins3k Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c))))
212104, 211ceqsexv 2894 . . . . . . . . . . . . . . . . . . . . . . 23 (t(t = {{x}} t, ⟪y, n⟫⟫ ( Ins2k ∼ (( Ins3k SkIns2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k k SIk SIk SIk (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk SkIns3k SIk SIk SIk SIk SIk Sk )) “k 11111111c))) “k 11111c)) “k 111c)) “k 111c) ∩ Ins3k Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c))) ↔ ⟪{{x}}, ⟪y, n⟫⟫ ( Ins2k ∼ (( Ins3k SkIns2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k k SIk SIk SIk (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk SkIns3k SIk SIk SIk SIk SIk Sk )) “k 11111111c))) “k 11111c)) “k 111c)) “k 111c) ∩ Ins3k Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c)))
213 elin 3219 . . . . . . . . . . . . . . . . . . . . . . 23 (⟪{{x}}, ⟪y, n⟫⟫ ( Ins2k ∼ (( Ins3k SkIns2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k k SIk SIk SIk (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk SkIns3k SIk SIk SIk SIk SIk Sk )) “k 11111111c))) “k 11111c)) “k 111c)) “k 111c) ∩ Ins3k Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c)) ↔ (⟪{{x}}, ⟪y, n⟫⟫ Ins2k ∼ (( Ins3k SkIns2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k k SIk SIk SIk (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk SkIns3k SIk SIk SIk SIk SIk Sk )) “k 11111111c))) “k 11111c)) “k 111c)) “k 111c) ⟪{{x}}, ⟪y, n⟫⟫ Ins3k Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c)))
214 opkex 4113 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 x, n V
215214elimak 4259 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (⟪x, n (( Ins3k SkIns2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k k SIk SIk SIk (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk SkIns3k SIk SIk SIk SIk SIk Sk )) “k 11111111c))) “k 11111c)) “k 111c)) “k 111c) ↔ t 1 11ct, ⟪x, n⟫⟫ ( Ins3k SkIns2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k k SIk SIk SIk (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk SkIns3k SIk SIk SIk SIk SIk Sk )) “k 11111111c))) “k 11111c)) “k 111c)))
2167anbi1i 676 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((t 111c t, ⟪x, n⟫⟫ ( Ins3k SkIns2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k k SIk SIk SIk (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk SkIns3k SIk SIk SIk SIk SIk Sk )) “k 11111111c))) “k 11111c)) “k 111c))) ↔ (y t = {{{y}}} t, ⟪x, n⟫⟫ ( Ins3k SkIns2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k k SIk SIk SIk (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk SkIns3k SIk SIk SIk SIk SIk Sk )) “k 11111111c))) “k 11111c)) “k 111c))))
217 19.41v 1901 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (y(t = {{{y}}} t, ⟪x, n⟫⟫ ( Ins3k SkIns2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k k SIk SIk SIk (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk SkIns3k SIk SIk SIk SIk SIk Sk )) “k 11111111c))) “k 11111c)) “k 111c))) ↔ (y t = {{{y}}} t, ⟪x, n⟫⟫ ( Ins3k SkIns2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k k SIk SIk SIk (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk SkIns3k SIk SIk SIk SIk SIk Sk )) “k 11111111c))) “k 11111c)) “k 111c))))
218216, 217bitr4i 243 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((t 111c t, ⟪x, n⟫⟫ ( Ins3k SkIns2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k k SIk SIk SIk (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk SkIns3k SIk SIk SIk SIk SIk Sk )) “k 11111111c))) “k 11111c)) “k 111c))) ↔ y(t = {{{y}}} t, ⟪x, n⟫⟫ ( Ins3k SkIns2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k k SIk SIk SIk (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk SkIns3k SIk SIk SIk SIk SIk Sk )) “k 11111111c))) “k 11111c)) “k 111c))))
219218exbii 1582 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (t(t 111c t, ⟪x, n⟫⟫ ( Ins3k SkIns2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k k SIk SIk SIk (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk SkIns3k SIk SIk SIk SIk SIk Sk )) “k 11111111c))) “k 11111c)) “k 111c))) ↔ ty(t = {{{y}}} t, ⟪x, n⟫⟫ ( Ins3k SkIns2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k k SIk SIk SIk (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk SkIns3k SIk SIk SIk SIk SIk Sk )) “k 11111111c))) “k 11111c)) “k 111c))))
220 df-rex 2620 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (t 1 11ct, ⟪x, n⟫⟫ ( Ins3k SkIns2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k k SIk SIk SIk (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk SkIns3k SIk SIk SIk SIk SIk Sk )) “k 11111111c))) “k 11111c)) “k 111c)) ↔ t(t 111c t, ⟪x, n⟫⟫ ( Ins3k SkIns2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k k SIk SIk SIk (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk SkIns3k SIk SIk SIk SIk SIk Sk )) “k 11111111c))) “k 11111c)) “k 111c))))
221 excom 1741 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (yt(t = {{{y}}} t, ⟪x, n⟫⟫ ( Ins3k SkIns2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k k SIk SIk SIk (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk SkIns3k SIk SIk SIk SIk SIk Sk )) “k 11111111c))) “k 11111c)) “k 111c))) ↔ ty(t = {{{y}}} t, ⟪x, n⟫⟫ ( Ins3k SkIns2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k k SIk SIk SIk (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk SkIns3k SIk SIk SIk SIk SIk Sk )) “k 11111111c))) “k 11111c)) “k 111c))))
222219, 220, 2213bitr4i 268 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (t 1 11ct, ⟪x, n⟫⟫ ( Ins3k SkIns2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k k SIk SIk SIk (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk SkIns3k SIk SIk SIk SIk SIk Sk )) “k 11111111c))) “k 11111c)) “k 111c)) ↔ yt(t = {{{y}}} t, ⟪x, n⟫⟫ ( Ins3k SkIns2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k k SIk SIk SIk (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk SkIns3k SIk SIk SIk SIk SIk Sk )) “k 11111111c))) “k 11111c)) “k 111c))))
223 opkeq1 4059 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (t = {{{y}}} → ⟪t, ⟪x, n⟫⟫ = ⟪{{{y}}}, ⟪x, n⟫⟫)
224223eleq1d 2419 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (t = {{{y}}} → (⟪t, ⟪x, n⟫⟫ ( Ins3k SkIns2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k k SIk SIk SIk (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk SkIns3k SIk SIk SIk SIk SIk Sk )) “k 11111111c))) “k 11111c)) “k 111c)) ↔ ⟪{{{y}}}, ⟪x, n⟫⟫ ( Ins3k SkIns2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k k SIk SIk SIk (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk SkIns3k SIk SIk SIk SIk SIk Sk )) “k 11111111c))) “k 11111c)) “k 111c))))
22515, 224ceqsexv 2894 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (t(t = {{{y}}} t, ⟪x, n⟫⟫ ( Ins3k SkIns2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k k SIk SIk SIk (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk SkIns3k SIk SIk SIk SIk SIk Sk )) “k 11111111c))) “k 11111c)) “k 111c))) ↔ ⟪{{{y}}}, ⟪x, n⟫⟫ ( Ins3k SkIns2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k k SIk SIk SIk (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk SkIns3k SIk SIk SIk SIk SIk Sk )) “k 11111111c))) “k 11111c)) “k 111c)))
226 elsymdif 3223 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (⟪{{{y}}}, ⟪x, n⟫⟫ ( Ins3k SkIns2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k k SIk SIk SIk (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk SkIns3k SIk SIk SIk SIk SIk Sk )) “k 11111111c))) “k 11111c)) “k 111c)) ↔ ¬ (⟪{{{y}}}, ⟪x, n⟫⟫ Ins3k Sk ↔ ⟪{{{y}}}, ⟪x, n⟫⟫ Ins2k (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k k SIk SIk SIk (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk SkIns3k SIk SIk SIk SIk SIk Sk )) “k 11111111c))) “k 11111c)) “k 111c)))
22720, 21, 198otkelins3k 4256 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (⟪{{{y}}}, ⟪x, n⟫⟫ Ins3k Sk ↔ ⟪{y}, x Sk )
228227, 24bitri 240 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (⟪{{{y}}}, ⟪x, n⟫⟫ Ins3k Sky x)
229 opkex 4113 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⟪{y}, n V
230229elimak 4259 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (⟪{y}, n (( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k k SIk SIk SIk (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk SkIns3k SIk SIk SIk SIk SIk Sk )) “k 11111111c))) “k 11111c)) “k 111c) ↔ t 1 11ct, ⟪{y}, n⟫⟫ ( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k k SIk SIk SIk (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk SkIns3k SIk SIk SIk SIk SIk Sk )) “k 11111111c))) “k 11111c)))
231 elpw121c 4148 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (t 111ca t = {{{a}}})
232231anbi1i 676 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((t 111c t, ⟪{y}, n⟫⟫ ( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k k SIk SIk SIk (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk SkIns3k SIk SIk SIk SIk SIk Sk )) “k 11111111c))) “k 11111c))) ↔ (a t = {{{a}}} t, ⟪{y}, n⟫⟫ ( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k k SIk SIk SIk (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk SkIns3k SIk SIk SIk SIk SIk Sk )) “k 11111111c))) “k 11111c))))
233 19.41v 1901 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (a(t = {{{a}}} t, ⟪{y}, n⟫⟫ ( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k k SIk SIk SIk (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk SkIns3k SIk SIk SIk SIk SIk Sk )) “k 11111111c))) “k 11111c))) ↔ (a t = {{{a}}} t, ⟪{y}, n⟫⟫ ( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k k SIk SIk SIk (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk SkIns3k SIk SIk SIk SIk SIk Sk )) “k 11111111c))) “k 11111c))))
234232, 233bitr4i 243 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((t 111c t, ⟪{y}, n⟫⟫ ( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k k SIk SIk SIk (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk SkIns3k SIk SIk SIk SIk SIk Sk )) “k 11111111c))) “k 11111c))) ↔ a(t = {{{a}}} t, ⟪{y}, n⟫⟫ ( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k k SIk SIk SIk (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk SkIns3k SIk SIk SIk SIk SIk Sk )) “k 11111111c))) “k 11111c))))
235234exbii 1582 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (t(t 111c t, ⟪{y}, n⟫⟫ ( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k k SIk SIk SIk (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk SkIns3k SIk SIk SIk SIk SIk Sk )) “k 11111111c))) “k 11111c))) ↔ ta(t = {{{a}}} t, ⟪{y}, n⟫⟫ ( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k k SIk SIk SIk (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk SkIns3k SIk SIk SIk SIk SIk Sk )) “k 11111111c))) “k 11111c))))
236 df-rex 2620 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (t 1 11ct, ⟪{y}, n⟫⟫ ( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k k SIk SIk SIk (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk SkIns3k SIk SIk SIk SIk SIk Sk )) “k 11111111c))) “k 11111c)) ↔ t(t 111c t, ⟪{y}, n⟫⟫ ( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k k SIk SIk SIk (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk SkIns3k SIk SIk SIk SIk SIk Sk )) “k 11111111c))) “k 11111c))))
237 excom 1741 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (at(t = {{{a}}} t, ⟪{y}, n⟫⟫ ( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k k SIk SIk SIk (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk SkIns3k SIk SIk SIk SIk SIk Sk )) “k 11111111c))) “k 11111c))) ↔ ta(t = {{{a}}} t, ⟪{y}, n⟫⟫ ( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k k SIk SIk SIk (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk SkIns3k SIk SIk SIk SIk SIk Sk )) “k 11111111c))) “k 11111c))))
238235, 236, 2373bitr4i 268 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (t 1 11ct, ⟪{y}, n⟫⟫ ( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k k SIk SIk SIk (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk SkIns3k SIk SIk SIk SIk SIk Sk )) “k 11111111c))) “k 11111c)) ↔ at(t = {{{a}}} t, ⟪{y}, n⟫⟫ ( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k k SIk SIk SIk (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk SkIns3k SIk SIk SIk SIk SIk Sk )) “k 11111111c))) “k 11111c))))
239 opkeq1 4059 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (t = {{{a}}} → ⟪t, ⟪{y}, n⟫⟫ = ⟪{{{a}}}, ⟪{y}, n⟫⟫)
240239eleq1d 2419 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (t = {{{a}}} → (⟪t, ⟪{y}, n⟫⟫ ( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k k SIk SIk SIk (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk SkIns3k SIk SIk SIk SIk SIk Sk )) “k 11111111c))) “k 11111c)) ↔ ⟪{{{a}}}, ⟪{y}, n⟫⟫ ( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k k SIk SIk SIk (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk SkIns3k SIk SIk SIk SIk SIk Sk )) “k 11111111c))) “k 11111c))))
24162, 240ceqsexv 2894 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (t(t = {{{a}}} t, ⟪{y}, n⟫⟫ ( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k k SIk SIk SIk (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk SkIns3k SIk SIk SIk SIk SIk Sk )) “k 11111111c))) “k 11111c))) ↔ ⟪{{{a}}}, ⟪{y}, n⟫⟫ ( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k k SIk SIk SIk (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk SkIns3k SIk SIk SIk SIk SIk Sk )) “k 11111111c))) “k 11111c)))
242 elin 3219 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (⟪{{{a}}}, ⟪{y}, n⟫⟫ ( Ins2k Sk ∩ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k k SIk SIk SIk (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk SkIns3k SIk SIk SIk SIk SIk Sk )) “k 11111111c))) “k 11111c)) ↔ (⟪{{{a}}}, ⟪{y}, n⟫⟫ Ins2k Sk ⟪{{{a}}}, ⟪{y}, n⟫⟫ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k k SIk SIk SIk (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk SkIns3k SIk SIk SIk SIk SIk Sk )) “k 11111111c))) “k 11111c)))
24364, 20, 198otkelins2k 4255 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (⟪{{{a}}}, ⟪{y}, n⟫⟫ Ins2k Sk ↔ ⟪{a}, n Sk )
24466, 198elssetk 4270 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (⟪{a}, n Ska n)
245243, 244bitri 240 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (⟪{{{a}}}, ⟪{y}, n⟫⟫ Ins2k Ska n)
246 opkex 4113 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⟪{{{a}}}, ⟪{y}, n⟫⟫ V
247246elimak 4259 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (⟪{{{a}}}, ⟪{y}, n⟫⟫ (( Ins2k Ins2k Sk ∩ ( ∼ Ins3k k SIk SIk SIk (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk SkIns3k SIk SIk SIk SIk SIk Sk )) “k 11111111c))) “k 11111c) ↔ t 1 1111ct, ⟪{{{a}}}, ⟪{y}, n⟫⟫⟫ ( Ins2k Ins2k Sk ∩ ( ∼ Ins3k k SIk SIk SIk (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk SkIns3k SIk SIk SIk SIk SIk Sk )) “k 11111111c))))
248 elpw141c 4150 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (t 11111cb t = {{{{{b}}}}})
249248anbi1i 676 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((t 11111c t, ⟪{{{a}}}, ⟪{y}, n⟫⟫⟫ ( Ins2k Ins2k Sk ∩ ( ∼ Ins3k k SIk SIk SIk (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk SkIns3k SIk SIk SIk SIk SIk Sk )) “k 11111111c)))) ↔ (b t = {{{{{b}}}}} t, ⟪{{{a}}}, ⟪{y}, n⟫⟫⟫ ( Ins2k Ins2k Sk ∩ ( ∼ Ins3k k SIk SIk SIk (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk SkIns3k SIk SIk SIk SIk SIk Sk )) “k 11111111c)))))
250 19.41v 1901 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (b(t = {{{{{b}}}}} t, ⟪{{{a}}}, ⟪{y}, n⟫⟫⟫ ( Ins2k Ins2k Sk ∩ ( ∼ Ins3k k SIk SIk SIk (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk SkIns3k SIk SIk SIk SIk SIk Sk )) “k 11111111c)))) ↔ (b t = {{{{{b}}}}} t, ⟪{{{a}}}, ⟪{y}, n⟫⟫⟫ ( Ins2k Ins2k Sk ∩ ( ∼ Ins3k k SIk SIk SIk (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk SkIns3k SIk SIk SIk SIk SIk Sk )) “k 11111111c)))))
251249, 250bitr4i 243 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((t 11111c t, ⟪{{{a}}}, ⟪{y}, n⟫⟫⟫ ( Ins2k Ins2k Sk ∩ ( ∼ Ins3k k SIk SIk SIk (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk SkIns3k SIk SIk SIk SIk SIk Sk )) “k 11111111c)))) ↔ b(t = {{{{{b}}}}} t, ⟪{{{a}}}, ⟪{y}, n⟫⟫⟫ ( Ins2k Ins2k Sk ∩ ( ∼ Ins3k k SIk SIk SIk (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk SkIns3k SIk SIk SIk SIk SIk Sk )) “k 11111111c)))))
252251exbii 1582 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (t(t 11111c t, ⟪{{{a}}}, ⟪{y}, n⟫⟫⟫ ( Ins2k Ins2k Sk ∩ ( ∼ Ins3k k SIk SIk SIk (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk SkIns3k SIk SIk SIk SIk SIk Sk )) “k 11111111c)))) ↔ tb(t = {{{{{b}}}}} t, ⟪{{{a}}}, ⟪{y}, n⟫⟫⟫ ( Ins2k Ins2k Sk ∩ ( ∼ Ins3k k SIk SIk SIk (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk SkIns3k SIk SIk SIk SIk SIk Sk )) “k 11111111c)))))
253 df-rex 2620 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (t 1 1111ct, ⟪{{{a}}}, ⟪{y}, n⟫⟫⟫ ( Ins2k Ins2k Sk ∩ ( ∼ Ins3k k SIk SIk SIk (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk SkIns3k SIk SIk SIk SIk SIk Sk )) “k 11111111c))) ↔ t(t 11111c t, ⟪{{{a}}}, ⟪{y}, n⟫⟫⟫ ( Ins2k Ins2k Sk ∩ ( ∼ Ins3k k SIk SIk SIk (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk SkIns3k SIk SIk SIk SIk SIk Sk )) “k 11111111c)))))
254 excom 1741 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (bt(t = {{{{{b}}}}} t, ⟪{{{a}}}, ⟪{y}, n⟫⟫⟫ ( Ins2k Ins2k Sk ∩ ( ∼ Ins3k k SIk SIk SIk (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk SkIns3k SIk SIk SIk SIk SIk Sk )) “k 11111111c)))) ↔ tb(t = {{{{{b}}}}} t, ⟪{{{a}}}, ⟪{y}, n⟫⟫⟫ ( Ins2k Ins2k Sk ∩ ( ∼ Ins3k k SIk SIk SIk (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk SkIns3k SIk SIk SIk SIk SIk Sk )) “k 11111111c)))))
255252, 253, 2543bitr4i 268 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (t 1 1111ct, ⟪{{{a}}}, ⟪{y}, n⟫⟫⟫ ( Ins2k Ins2k Sk ∩ ( ∼ Ins3k k SIk SIk SIk (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk SkIns3k SIk SIk SIk SIk SIk Sk )) “k 11111111c))) ↔ bt(t = {{{{{b}}}}} t, ⟪{{{a}}}, ⟪{y}, n⟫⟫⟫ ( Ins2k Ins2k Sk ∩ ( ∼ Ins3k k SIk SIk SIk (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk SkIns3k SIk SIk SIk SIk SIk Sk )) “k 11111111c)))))
256 snex 4111 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 {{{{{b}}}}} V
257 opkeq1 4059 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (t = {{{{{b}}}}} → ⟪t, ⟪{{{a}}}, ⟪{y}, n⟫⟫⟫ = ⟪{{{{{b}}}}}, ⟪{{{a}}}, ⟪{y}, n⟫⟫⟫)
258257eleq1d 2419 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (t = {{{{{b}}}}} → (⟪t, ⟪{{{a}}}, ⟪{y}, n⟫⟫⟫ ( Ins2k Ins2k Sk ∩ ( ∼ Ins3k k SIk SIk SIk (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk SkIns3k SIk SIk SIk SIk SIk Sk )) “k 11111111c))) ↔ ⟪{{{{{b}}}}}, ⟪{{{a}}}, ⟪{y}, n⟫⟫⟫ ( Ins2k Ins2k Sk ∩ ( ∼ Ins3k k SIk SIk SIk (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk SkIns3k SIk SIk SIk SIk SIk Sk )) “k 11111111c)))))
259256, 258ceqsexv 2894 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (t(t = {{{{{b}}}}} t, ⟪{{{a}}}, ⟪{y}, n⟫⟫⟫ ( Ins2k Ins2k Sk ∩ ( ∼ Ins3k k SIk SIk SIk (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk SkIns3k SIk SIk SIk SIk SIk Sk )) “k 11111111c)))) ↔ ⟪{{{{{b}}}}}, ⟪{{{a}}}, ⟪{y}, n⟫⟫⟫ ( Ins2k Ins2k Sk ∩ ( ∼ Ins3k k SIk SIk SIk (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk SkIns3k SIk SIk SIk SIk SIk Sk )) “k 11111111c))))
260 elin 3219 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (⟪{{{{{b}}}}}, ⟪{{{a}}}, ⟪{y}, n⟫⟫⟫ ( Ins2k Ins2k Sk ∩ ( ∼ Ins3k k SIk SIk SIk (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk SkIns3k SIk SIk SIk SIk SIk Sk )) “k 11111111c))) ↔ (⟪{{{{{b}}}}}, ⟪{{{a}}}, ⟪{y}, n⟫⟫⟫ Ins2k Ins2k Sk ⟪{{{{{b}}}}}, ⟪{{{a}}}, ⟪{y}, n⟫⟫⟫ ( ∼ Ins3k k SIk SIk SIk (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk SkIns3k SIk SIk SIk SIk SIk Sk )) “k 11111111c))))
26137, 62, 229otkelins2k 4255 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (⟪{{{{{b}}}}}, ⟪{{{a}}}, ⟪{y}, n⟫⟫⟫ Ins2k Ins2k Sk ↔ ⟪{{{b}}}, ⟪{y}, n⟫⟫ Ins2k Sk )
26242, 20, 198otkelins2k 4255 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (⟪{{{b}}}, ⟪{y}, n⟫⟫ Ins2k Sk ↔ ⟪{b}, n Sk )
26344, 198elssetk 4270 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (⟪{b}, n Skb n)
264261, 262, 2633bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (⟪{{{{{b}}}}}, ⟪{{{a}}}, ⟪{y}, n⟫⟫⟫ Ins2k Ins2k Skb n)
265 elin 3219 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (⟪{{{{{b}}}}}, ⟪{{{a}}}, ⟪{y}, n⟫⟫⟫ ( ∼ Ins3k k SIk SIk SIk (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk SkIns3k SIk SIk SIk SIk SIk Sk )) “k 11111111c)) ↔ (⟪{{{{{b}}}}}, ⟪{{{a}}}, ⟪{y}, n⟫⟫⟫ Ins3k k SIk SIk SIk (( Ins3k SkIns2k Sk ) “k 111c) ⟪{{{{{b}}}}}, ⟪{{{a}}}, ⟪{y}, n⟫⟫⟫ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk SkIns3k SIk SIk SIk SIk SIk Sk )) “k 11111111c)))
26637, 62, 229otkelins3k 4256 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 (⟪{{{{{b}}}}}, ⟪{{{a}}}, ⟪{y}, n⟫⟫⟫ Ins3k k SIk SIk SIk (( Ins3k SkIns2k Sk ) “k 111c) ↔ ⟪{{{b}}}, {{{a}}}⟫ k SIk SIk SIk (( Ins3k SkIns2k Sk ) “k 111c))
26737, 62opkelcnvk 4250 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 (⟪{{{b}}}, {{{a}}}⟫ k SIk SIk SIk (( Ins3k SkIns2k Sk ) “k 111c) ↔ ⟪{{{a}}}, {{{b}}}⟫ SIk SIk SIk (( Ins3k SkIns2k Sk ) “k 111c))
26871, 72opksnelsik 4265 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 (⟪{{{a}}}, {{{b}}}⟫ SIk SIk SIk (( Ins3k SkIns2k Sk ) “k 111c) ↔ ⟪{{a}}, {{b}}⟫ SIk SIk (( Ins3k SkIns2k Sk ) “k 111c))
26964, 42opksnelsik 4265 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 (⟪{{a}}, {{b}}⟫ SIk SIk (( Ins3k SkIns2k Sk ) “k 111c) ↔ ⟪{a}, {b}⟫ SIk (( Ins3k SkIns2k Sk ) “k 111c))
27066, 44opksnelsik 4265 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 (⟪{a}, {b}⟫ SIk (( Ins3k SkIns2k Sk ) “k 111c) ↔ ⟪a, b (( Ins3k SkIns2k Sk ) “k 111c))
271270, 76bitri 240 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 (⟪{a}, {b}⟫ SIk (( Ins3k SkIns2k Sk ) “k 111c) ↔ (ab) ≠ )
272268, 269, 2713bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 (⟪{{{a}}}, {{{b}}}⟫ SIk SIk SIk (( Ins3k SkIns2k Sk ) “k 111c) ↔ (ab) ≠ )
273266, 267, 2723bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 (⟪{{{{{b}}}}}, ⟪{{{a}}}, ⟪{y}, n⟫⟫⟫ Ins3k k SIk SIk SIk (( Ins3k SkIns2k Sk ) “k 111c) ↔ (ab) ≠ )
274273notbii 287 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 (¬ ⟪{{{{{b}}}}}, ⟪{{{a}}}, ⟪{y}, n⟫⟫⟫ Ins3k k SIk SIk SIk (( Ins3k SkIns2k Sk ) “k 111c) ↔ ¬ (ab) ≠ )
275 opkex 4113 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⟪{{{{{b}}}}}, ⟪{{{a}}}, ⟪{y}, n⟫⟫⟫ V
276275elcompl 3225 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 (⟪{{{{{b}}}}}, ⟪{{{a}}}, ⟪{y}, n⟫⟫⟫ Ins3k k SIk SIk SIk (( Ins3k SkIns2k Sk ) “k 111c) ↔ ¬ ⟪{{{{{b}}}}}, ⟪{{{a}}}, ⟪{y}, n⟫⟫⟫ Ins3k k SIk SIk SIk (( Ins3k SkIns2k Sk ) “k 111c))
277274, 276, 813bitr4i 268 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (⟪{{{{{b}}}}}, ⟪{{{a}}}, ⟪{y}, n⟫⟫⟫ Ins3k k SIk SIk SIk (( Ins3k SkIns2k Sk ) “k 111c) ↔ (ab) = )
278275elimak 4259 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 (⟪{{{{{b}}}}}, ⟪{{{a}}}, ⟪{y}, n⟫⟫⟫ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk SkIns3k SIk SIk SIk SIk SIk Sk )) “k 11111111c) ↔ t 1 1111111ct, ⟪{{{{{b}}}}}, ⟪{{{a}}}, ⟪{y}, n⟫⟫⟫⟫ ( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk SkIns3k SIk SIk SIk SIk SIk Sk )))
27987anbi1i 676 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 ((t 11111111c t, ⟪{{{{{b}}}}}, ⟪{{{a}}}, ⟪{y}, n⟫⟫⟫⟫ ( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk SkIns3k SIk SIk SIk SIk SIk Sk ))) ↔ (x t = {{{{{{{{x}}}}}}}} t, ⟪{{{{{b}}}}}, ⟪{{{a}}}, ⟪{y}, n⟫⟫⟫⟫ ( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk SkIns3k SIk SIk SIk SIk SIk Sk ))))
280 19.41v 1901 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 (x(t = {{{{{{{{x}}}}}}}} t, ⟪{{{{{b}}}}}, ⟪{{{a}}}, ⟪{y}, n⟫⟫⟫⟫ ( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk SkIns3k SIk SIk SIk SIk SIk Sk ))) ↔ (x t = {{{{{{{{x}}}}}}}} t, ⟪{{{{{b}}}}}, ⟪{{{a}}}, ⟪{y}, n⟫⟫⟫⟫ ( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk SkIns3k SIk SIk SIk SIk SIk Sk ))))
281279, 280bitr4i 243 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 ((t 11111111c t, ⟪{{{{{b}}}}}, ⟪{{{a}}}, ⟪{y}, n⟫⟫⟫⟫ ( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk SkIns3k SIk SIk SIk SIk SIk Sk ))) ↔ x(t = {{{{{{{{x}}}}}}}} t, ⟪{{{{{b}}}}}, ⟪{{{a}}}, ⟪{y}, n⟫⟫⟫⟫ ( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk SkIns3k SIk SIk SIk SIk SIk Sk ))))
282281exbii 1582 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 (t(t 11111111c t, ⟪{{{{{b}}}}}, ⟪{{{a}}}, ⟪{y}, n⟫⟫⟫⟫ ( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk SkIns3k SIk SIk SIk SIk SIk Sk ))) ↔ tx(t = {{{{{{{{x}}}}}}}} t, ⟪{{{{{b}}}}}, ⟪{{{a}}}, ⟪{y}, n⟫⟫⟫⟫ ( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins2k Ins3k SIk SIk SIk SkIns3k SIk SIk SIk SIk SIk Sk ))))
283 df-rex 2620 . . . . . . . . . . . . . . . . . . . .