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

Theorem ltfinex 4464
Description: Finite less than is stratified. (Contributed by SF, 29-Jan-2015.)
Assertion
Ref Expression
ltfinex <fin V

Proof of Theorem ltfinex
Dummy variables a b c d t w y z x are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-ltfin 4441 . . 3 <fin = {x yz(x = ⟪y, z (y w Nn z = ((y +c w) +c 1c)))}
2 elin 3219 . . . . 5 (x ((V ×k V) ∩ (((( ∼ (( Ins3k SIk SIk SIk SIk SkIns2k (( Ins2k Ins3k SIk SIk Sk ∩ (( Ins2k Ins2k Ins2k Ins3k Sk ∩ ( Ins3k SIk SIk SIk SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk )) “k 111111111111c))) “k 111111111c)) “k 1111111c)) “k 1111111c) ∩ Ins2k Ins2k Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c)) “k 1111c) “k 11 Nn ) ({} ×k V))) ↔ (x (V ×k V) x (((( ∼ (( Ins3k SIk SIk SIk SIk SkIns2k (( Ins2k Ins3k SIk SIk Sk ∩ (( Ins2k Ins2k Ins2k Ins3k Sk ∩ ( Ins3k SIk SIk SIk SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk )) “k 111111111111c))) “k 111111111c)) “k 1111111c)) “k 1111111c) ∩ Ins2k Ins2k Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c)) “k 1111c) “k 11 Nn ) ({} ×k V))))
3 elvvk 4207 . . . . . 6 (x (V ×k V) ↔ yz x = ⟪y, z⟫)
43anbi1i 676 . . . . 5 ((x (V ×k V) x (((( ∼ (( Ins3k SIk SIk SIk SIk SkIns2k (( Ins2k Ins3k SIk SIk Sk ∩ (( Ins2k Ins2k Ins2k Ins3k Sk ∩ ( Ins3k SIk SIk SIk SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk )) “k 111111111111c))) “k 111111111c)) “k 1111111c)) “k 1111111c) ∩ Ins2k Ins2k Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c)) “k 1111c) “k 11 Nn ) ({} ×k V))) ↔ (yz x = ⟪y, z x (((( ∼ (( Ins3k SIk SIk SIk SIk SkIns2k (( Ins2k Ins3k SIk SIk Sk ∩ (( Ins2k Ins2k Ins2k Ins3k Sk ∩ ( Ins3k SIk SIk SIk SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk )) “k 111111111111c))) “k 111111111c)) “k 1111111c)) “k 1111111c) ∩ Ins2k Ins2k Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c)) “k 1111c) “k 11 Nn ) ({} ×k V))))
5 19.41vv 1902 . . . . . 6 (yz(x = ⟪y, z x (((( ∼ (( Ins3k SIk SIk SIk SIk SkIns2k (( Ins2k Ins3k SIk SIk Sk ∩ (( Ins2k Ins2k Ins2k Ins3k Sk ∩ ( Ins3k SIk SIk SIk SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk )) “k 111111111111c))) “k 111111111c)) “k 1111111c)) “k 1111111c) ∩ Ins2k Ins2k Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c)) “k 1111c) “k 11 Nn ) ({} ×k V))) ↔ (yz x = ⟪y, z x (((( ∼ (( Ins3k SIk SIk SIk SIk SkIns2k (( Ins2k Ins3k SIk SIk Sk ∩ (( Ins2k Ins2k Ins2k Ins3k Sk ∩ ( Ins3k SIk SIk SIk SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk )) “k 111111111111c))) “k 111111111c)) “k 1111111c)) “k 1111111c) ∩ Ins2k Ins2k Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c)) “k 1111c) “k 11 Nn ) ({} ×k V))))
6 eleq1 2413 . . . . . . . . 9 (x = ⟪y, z⟫ → (x (((( ∼ (( Ins3k SIk SIk SIk SIk SkIns2k (( Ins2k Ins3k SIk SIk Sk ∩ (( Ins2k Ins2k Ins2k Ins3k Sk ∩ ( Ins3k SIk SIk SIk SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk )) “k 111111111111c))) “k 111111111c)) “k 1111111c)) “k 1111111c) ∩ Ins2k Ins2k Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c)) “k 1111c) “k 11 Nn ) ({} ×k V)) ↔ ⟪y, z (((( ∼ (( Ins3k SIk SIk SIk SIk SkIns2k (( Ins2k Ins3k SIk SIk Sk ∩ (( Ins2k Ins2k Ins2k Ins3k Sk ∩ ( Ins3k SIk SIk SIk SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk )) “k 111111111111c))) “k 111111111c)) “k 1111111c)) “k 1111111c) ∩ Ins2k Ins2k Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c)) “k 1111c) “k 11 Nn ) ({} ×k V))))
7 opkex 4113 . . . . . . . . . . . . 13 y, z V
87elimak 4259 . . . . . . . . . . . 12 (⟪y, z ((( ∼ (( Ins3k SIk SIk SIk SIk SkIns2k (( Ins2k Ins3k SIk SIk Sk ∩ (( Ins2k Ins2k Ins2k Ins3k Sk ∩ ( Ins3k SIk SIk SIk SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk )) “k 111111111111c))) “k 111111111c)) “k 1111111c)) “k 1111111c) ∩ Ins2k Ins2k Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c)) “k 1111c) “k 11 Nn ) ↔ t 1 1 Nnt, ⟪y, z⟫⟫ (( ∼ (( Ins3k SIk SIk SIk SIk SkIns2k (( Ins2k Ins3k SIk SIk Sk ∩ (( Ins2k Ins2k Ins2k Ins3k Sk ∩ ( Ins3k SIk SIk SIk SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk )) “k 111111111111c))) “k 111111111c)) “k 1111111c)) “k 1111111c) ∩ Ins2k Ins2k Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c)) “k 1111c))
9 elpw12 4145 . . . . . . . . . . . . . . . 16 (t 11 Nnw Nn t = {{w}})
109anbi1i 676 . . . . . . . . . . . . . . 15 ((t 11 Nn t, ⟪y, z⟫⟫ (( ∼ (( Ins3k SIk SIk SIk SIk SkIns2k (( Ins2k Ins3k SIk SIk Sk ∩ (( Ins2k Ins2k Ins2k Ins3k Sk ∩ ( Ins3k SIk SIk SIk SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk )) “k 111111111111c))) “k 111111111c)) “k 1111111c)) “k 1111111c) ∩ Ins2k Ins2k Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c)) “k 1111c)) ↔ (w Nn t = {{w}} t, ⟪y, z⟫⟫ (( ∼ (( Ins3k SIk SIk SIk SIk SkIns2k (( Ins2k Ins3k SIk SIk Sk ∩ (( Ins2k Ins2k Ins2k Ins3k Sk ∩ ( Ins3k SIk SIk SIk SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk )) “k 111111111111c))) “k 111111111c)) “k 1111111c)) “k 1111111c) ∩ Ins2k Ins2k Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c)) “k 1111c)))
11 r19.41v 2764 . . . . . . . . . . . . . . 15 (w Nn (t = {{w}} t, ⟪y, z⟫⟫ (( ∼ (( Ins3k SIk SIk SIk SIk SkIns2k (( Ins2k Ins3k SIk SIk Sk ∩ (( Ins2k Ins2k Ins2k Ins3k Sk ∩ ( Ins3k SIk SIk SIk SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk )) “k 111111111111c))) “k 111111111c)) “k 1111111c)) “k 1111111c) ∩ Ins2k Ins2k Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c)) “k 1111c)) ↔ (w Nn t = {{w}} t, ⟪y, z⟫⟫ (( ∼ (( Ins3k SIk SIk SIk SIk SkIns2k (( Ins2k Ins3k SIk SIk Sk ∩ (( Ins2k Ins2k Ins2k Ins3k Sk ∩ ( Ins3k SIk SIk SIk SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk )) “k 111111111111c))) “k 111111111c)) “k 1111111c)) “k 1111111c) ∩ Ins2k Ins2k Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c)) “k 1111c)))
1210, 11bitr4i 243 . . . . . . . . . . . . . 14 ((t 11 Nn t, ⟪y, z⟫⟫ (( ∼ (( Ins3k SIk SIk SIk SIk SkIns2k (( Ins2k Ins3k SIk SIk Sk ∩ (( Ins2k Ins2k Ins2k Ins3k Sk ∩ ( Ins3k SIk SIk SIk SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk )) “k 111111111111c))) “k 111111111c)) “k 1111111c)) “k 1111111c) ∩ Ins2k Ins2k Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c)) “k 1111c)) ↔ w Nn (t = {{w}} t, ⟪y, z⟫⟫ (( ∼ (( Ins3k SIk SIk SIk SIk SkIns2k (( Ins2k Ins3k SIk SIk Sk ∩ (( Ins2k Ins2k Ins2k Ins3k Sk ∩ ( Ins3k SIk SIk SIk SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk )) “k 111111111111c))) “k 111111111c)) “k 1111111c)) “k 1111111c) ∩ Ins2k Ins2k Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c)) “k 1111c)))
1312exbii 1582 . . . . . . . . . . . . 13 (t(t 11 Nn t, ⟪y, z⟫⟫ (( ∼ (( Ins3k SIk SIk SIk SIk SkIns2k (( Ins2k Ins3k SIk SIk Sk ∩ (( Ins2k Ins2k Ins2k Ins3k Sk ∩ ( Ins3k SIk SIk SIk SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk )) “k 111111111111c))) “k 111111111c)) “k 1111111c)) “k 1111111c) ∩ Ins2k Ins2k Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c)) “k 1111c)) ↔ tw Nn (t = {{w}} t, ⟪y, z⟫⟫ (( ∼ (( Ins3k SIk SIk SIk SIk SkIns2k (( Ins2k Ins3k SIk SIk Sk ∩ (( Ins2k Ins2k Ins2k Ins3k Sk ∩ ( Ins3k SIk SIk SIk SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk )) “k 111111111111c))) “k 111111111c)) “k 1111111c)) “k 1111111c) ∩ Ins2k Ins2k Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c)) “k 1111c)))
14 df-rex 2620 . . . . . . . . . . . . 13 (t 1 1 Nnt, ⟪y, z⟫⟫ (( ∼ (( Ins3k SIk SIk SIk SIk SkIns2k (( Ins2k Ins3k SIk SIk Sk ∩ (( Ins2k Ins2k Ins2k Ins3k Sk ∩ ( Ins3k SIk SIk SIk SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk )) “k 111111111111c))) “k 111111111c)) “k 1111111c)) “k 1111111c) ∩ Ins2k Ins2k Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c)) “k 1111c) ↔ t(t 11 Nn t, ⟪y, z⟫⟫ (( ∼ (( Ins3k SIk SIk SIk SIk SkIns2k (( Ins2k Ins3k SIk SIk Sk ∩ (( Ins2k Ins2k Ins2k Ins3k Sk ∩ ( Ins3k SIk SIk SIk SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk )) “k 111111111111c))) “k 111111111c)) “k 1111111c)) “k 1111111c) ∩ Ins2k Ins2k Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c)) “k 1111c)))
15 rexcom4 2878 . . . . . . . . . . . . 13 (w Nn t(t = {{w}} t, ⟪y, z⟫⟫ (( ∼ (( Ins3k SIk SIk SIk SIk SkIns2k (( Ins2k Ins3k SIk SIk Sk ∩ (( Ins2k Ins2k Ins2k Ins3k Sk ∩ ( Ins3k SIk SIk SIk SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk )) “k 111111111111c))) “k 111111111c)) “k 1111111c)) “k 1111111c) ∩ Ins2k Ins2k Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c)) “k 1111c)) ↔ tw Nn (t = {{w}} t, ⟪y, z⟫⟫ (( ∼ (( Ins3k SIk SIk SIk SIk SkIns2k (( Ins2k Ins3k SIk SIk Sk ∩ (( Ins2k Ins2k Ins2k Ins3k Sk ∩ ( Ins3k SIk SIk SIk SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk )) “k 111111111111c))) “k 111111111c)) “k 1111111c)) “k 1111111c) ∩ Ins2k Ins2k Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c)) “k 1111c)))
1613, 14, 153bitr4i 268 . . . . . . . . . . . 12 (t 1 1 Nnt, ⟪y, z⟫⟫ (( ∼ (( Ins3k SIk SIk SIk SIk SkIns2k (( Ins2k Ins3k SIk SIk Sk ∩ (( Ins2k Ins2k Ins2k Ins3k Sk ∩ ( Ins3k SIk SIk SIk SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk )) “k 111111111111c))) “k 111111111c)) “k 1111111c)) “k 1111111c) ∩ Ins2k Ins2k Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c)) “k 1111c) ↔ w Nn t(t = {{w}} t, ⟪y, z⟫⟫ (( ∼ (( Ins3k SIk SIk SIk SIk SkIns2k (( Ins2k Ins3k SIk SIk Sk ∩ (( Ins2k Ins2k Ins2k Ins3k Sk ∩ ( Ins3k SIk SIk SIk SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk )) “k 111111111111c))) “k 111111111c)) “k 1111111c)) “k 1111111c) ∩ Ins2k Ins2k Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c)) “k 1111c)))
17 snex 4111 . . . . . . . . . . . . . . 15 {{w}} V
18 opkeq1 4059 . . . . . . . . . . . . . . . 16 (t = {{w}} → ⟪t, ⟪y, z⟫⟫ = ⟪{{w}}, ⟪y, z⟫⟫)
1918eleq1d 2419 . . . . . . . . . . . . . . 15 (t = {{w}} → (⟪t, ⟪y, z⟫⟫ (( ∼ (( Ins3k SIk SIk SIk SIk SkIns2k (( Ins2k Ins3k SIk SIk Sk ∩ (( Ins2k Ins2k Ins2k Ins3k Sk ∩ ( Ins3k SIk SIk SIk SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk )) “k 111111111111c))) “k 111111111c)) “k 1111111c)) “k 1111111c) ∩ Ins2k Ins2k Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c)) “k 1111c) ↔ ⟪{{w}}, ⟪y, z⟫⟫ (( ∼ (( Ins3k SIk SIk SIk SIk SkIns2k (( Ins2k Ins3k SIk SIk Sk ∩ (( Ins2k Ins2k Ins2k Ins3k Sk ∩ ( Ins3k SIk SIk SIk SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk )) “k 111111111111c))) “k 111111111c)) “k 1111111c)) “k 1111111c) ∩ Ins2k Ins2k Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c)) “k 1111c)))
2017, 19ceqsexv 2894 . . . . . . . . . . . . . 14 (t(t = {{w}} t, ⟪y, z⟫⟫ (( ∼ (( Ins3k SIk SIk SIk SIk SkIns2k (( Ins2k Ins3k SIk SIk Sk ∩ (( Ins2k Ins2k Ins2k Ins3k Sk ∩ ( Ins3k SIk SIk SIk SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk )) “k 111111111111c))) “k 111111111c)) “k 1111111c)) “k 1111111c) ∩ Ins2k Ins2k Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c)) “k 1111c)) ↔ ⟪{{w}}, ⟪y, z⟫⟫ (( ∼ (( Ins3k SIk SIk SIk SIk SkIns2k (( Ins2k Ins3k SIk SIk Sk ∩ (( Ins2k Ins2k Ins2k Ins3k Sk ∩ ( Ins3k SIk SIk SIk SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk )) “k 111111111111c))) “k 111111111c)) “k 1111111c)) “k 1111111c) ∩ Ins2k Ins2k Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c)) “k 1111c))
21 opkex 4113 . . . . . . . . . . . . . . . 16 ⟪{{w}}, ⟪y, z⟫⟫ V
2221elimak 4259 . . . . . . . . . . . . . . 15 (⟪{{w}}, ⟪y, z⟫⟫ (( ∼ (( Ins3k SIk SIk SIk SIk SkIns2k (( Ins2k Ins3k SIk SIk Sk ∩ (( Ins2k Ins2k Ins2k Ins3k Sk ∩ ( Ins3k SIk SIk SIk SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk )) “k 111111111111c))) “k 111111111c)) “k 1111111c)) “k 1111111c) ∩ Ins2k Ins2k Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c)) “k 1111c) ↔ t 1 111ct, ⟪{{w}}, ⟪y, z⟫⟫⟫ ( ∼ (( Ins3k SIk SIk SIk SIk SkIns2k (( Ins2k Ins3k SIk SIk Sk ∩ (( Ins2k Ins2k Ins2k Ins3k Sk ∩ ( Ins3k SIk SIk SIk SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk )) “k 111111111111c))) “k 111111111c)) “k 1111111c)) “k 1111111c) ∩ Ins2k Ins2k Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c)))
23 elpw131c 4149 . . . . . . . . . . . . . . . . . . 19 (t 1111cx t = {{{{x}}}})
2423anbi1i 676 . . . . . . . . . . . . . . . . . 18 ((t 1111c t, ⟪{{w}}, ⟪y, z⟫⟫⟫ ( ∼ (( Ins3k SIk SIk SIk SIk SkIns2k (( Ins2k Ins3k SIk SIk Sk ∩ (( Ins2k Ins2k Ins2k Ins3k Sk ∩ ( Ins3k SIk SIk SIk SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk )) “k 111111111111c))) “k 111111111c)) “k 1111111c)) “k 1111111c) ∩ Ins2k Ins2k Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c))) ↔ (x t = {{{{x}}}} t, ⟪{{w}}, ⟪y, z⟫⟫⟫ ( ∼ (( Ins3k SIk SIk SIk SIk SkIns2k (( Ins2k Ins3k SIk SIk Sk ∩ (( Ins2k Ins2k Ins2k Ins3k Sk ∩ ( Ins3k SIk SIk SIk SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk )) “k 111111111111c))) “k 111111111c)) “k 1111111c)) “k 1111111c) ∩ Ins2k Ins2k Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c))))
25 19.41v 1901 . . . . . . . . . . . . . . . . . 18 (x(t = {{{{x}}}} t, ⟪{{w}}, ⟪y, z⟫⟫⟫ ( ∼ (( Ins3k SIk SIk SIk SIk SkIns2k (( Ins2k Ins3k SIk SIk Sk ∩ (( Ins2k Ins2k Ins2k Ins3k Sk ∩ ( Ins3k SIk SIk SIk SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk )) “k 111111111111c))) “k 111111111c)) “k 1111111c)) “k 1111111c) ∩ Ins2k Ins2k Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c))) ↔ (x t = {{{{x}}}} t, ⟪{{w}}, ⟪y, z⟫⟫⟫ ( ∼ (( Ins3k SIk SIk SIk SIk SkIns2k (( Ins2k Ins3k SIk SIk Sk ∩ (( Ins2k Ins2k Ins2k Ins3k Sk ∩ ( Ins3k SIk SIk SIk SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk )) “k 111111111111c))) “k 111111111c)) “k 1111111c)) “k 1111111c) ∩ Ins2k Ins2k Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c))))
2624, 25bitr4i 243 . . . . . . . . . . . . . . . . 17 ((t 1111c t, ⟪{{w}}, ⟪y, z⟫⟫⟫ ( ∼ (( Ins3k SIk SIk SIk SIk SkIns2k (( Ins2k Ins3k SIk SIk Sk ∩ (( Ins2k Ins2k Ins2k Ins3k Sk ∩ ( Ins3k SIk SIk SIk SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk )) “k 111111111111c))) “k 111111111c)) “k 1111111c)) “k 1111111c) ∩ Ins2k Ins2k Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c))) ↔ x(t = {{{{x}}}} t, ⟪{{w}}, ⟪y, z⟫⟫⟫ ( ∼ (( Ins3k SIk SIk SIk SIk SkIns2k (( Ins2k Ins3k SIk SIk Sk ∩ (( Ins2k Ins2k Ins2k Ins3k Sk ∩ ( Ins3k SIk SIk SIk SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk )) “k 111111111111c))) “k 111111111c)) “k 1111111c)) “k 1111111c) ∩ Ins2k Ins2k Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c))))
2726exbii 1582 . . . . . . . . . . . . . . . 16 (t(t 1111c t, ⟪{{w}}, ⟪y, z⟫⟫⟫ ( ∼ (( Ins3k SIk SIk SIk SIk SkIns2k (( Ins2k Ins3k SIk SIk Sk ∩ (( Ins2k Ins2k Ins2k Ins3k Sk ∩ ( Ins3k SIk SIk SIk SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk )) “k 111111111111c))) “k 111111111c)) “k 1111111c)) “k 1111111c) ∩ Ins2k Ins2k Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c))) ↔ tx(t = {{{{x}}}} t, ⟪{{w}}, ⟪y, z⟫⟫⟫ ( ∼ (( Ins3k SIk SIk SIk SIk SkIns2k (( Ins2k Ins3k SIk SIk Sk ∩ (( Ins2k Ins2k Ins2k Ins3k Sk ∩ ( Ins3k SIk SIk SIk SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk )) “k 111111111111c))) “k 111111111c)) “k 1111111c)) “k 1111111c) ∩ Ins2k Ins2k Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c))))
28 df-rex 2620 . . . . . . . . . . . . . . . 16 (t 1 111ct, ⟪{{w}}, ⟪y, z⟫⟫⟫ ( ∼ (( Ins3k SIk SIk SIk SIk SkIns2k (( Ins2k Ins3k SIk SIk Sk ∩ (( Ins2k Ins2k Ins2k Ins3k Sk ∩ ( Ins3k SIk SIk SIk SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk )) “k 111111111111c))) “k 111111111c)) “k 1111111c)) “k 1111111c) ∩ Ins2k Ins2k Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c)) ↔ t(t 1111c t, ⟪{{w}}, ⟪y, z⟫⟫⟫ ( ∼ (( Ins3k SIk SIk SIk SIk SkIns2k (( Ins2k Ins3k SIk SIk Sk ∩ (( Ins2k Ins2k Ins2k Ins3k Sk ∩ ( Ins3k SIk SIk SIk SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk )) “k 111111111111c))) “k 111111111c)) “k 1111111c)) “k 1111111c) ∩ Ins2k Ins2k Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c))))
29 excom 1741 . . . . . . . . . . . . . . . 16 (xt(t = {{{{x}}}} t, ⟪{{w}}, ⟪y, z⟫⟫⟫ ( ∼ (( Ins3k SIk SIk SIk SIk SkIns2k (( Ins2k Ins3k SIk SIk Sk ∩ (( Ins2k Ins2k Ins2k Ins3k Sk ∩ ( Ins3k SIk SIk SIk SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk )) “k 111111111111c))) “k 111111111c)) “k 1111111c)) “k 1111111c) ∩ Ins2k Ins2k Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c))) ↔ tx(t = {{{{x}}}} t, ⟪{{w}}, ⟪y, z⟫⟫⟫ ( ∼ (( Ins3k SIk SIk SIk SIk SkIns2k (( Ins2k Ins3k SIk SIk Sk ∩ (( Ins2k Ins2k Ins2k Ins3k Sk ∩ ( Ins3k SIk SIk SIk SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk )) “k 111111111111c))) “k 111111111c)) “k 1111111c)) “k 1111111c) ∩ Ins2k Ins2k Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c))))
3027, 28, 293bitr4i 268 . . . . . . . . . . . . . . 15 (t 1 111ct, ⟪{{w}}, ⟪y, z⟫⟫⟫ ( ∼ (( Ins3k SIk SIk SIk SIk SkIns2k (( Ins2k Ins3k SIk SIk Sk ∩ (( Ins2k Ins2k Ins2k Ins3k Sk ∩ ( Ins3k SIk SIk SIk SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk )) “k 111111111111c))) “k 111111111c)) “k 1111111c)) “k 1111111c) ∩ Ins2k Ins2k Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c)) ↔ xt(t = {{{{x}}}} t, ⟪{{w}}, ⟪y, z⟫⟫⟫ ( ∼ (( Ins3k SIk SIk SIk SIk SkIns2k (( Ins2k Ins3k SIk SIk Sk ∩ (( Ins2k Ins2k Ins2k Ins3k Sk ∩ ( Ins3k SIk SIk SIk SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk )) “k 111111111111c))) “k 111111111c)) “k 1111111c)) “k 1111111c) ∩ Ins2k Ins2k Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c))))
31 snex 4111 . . . . . . . . . . . . . . . . . 18 {{{{x}}}} V
32 opkeq1 4059 . . . . . . . . . . . . . . . . . . 19 (t = {{{{x}}}} → ⟪t, ⟪{{w}}, ⟪y, z⟫⟫⟫ = ⟪{{{{x}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫)
3332eleq1d 2419 . . . . . . . . . . . . . . . . . 18 (t = {{{{x}}}} → (⟪t, ⟪{{w}}, ⟪y, z⟫⟫⟫ ( ∼ (( Ins3k SIk SIk SIk SIk SkIns2k (( Ins2k Ins3k SIk SIk Sk ∩ (( Ins2k Ins2k Ins2k Ins3k Sk ∩ ( Ins3k SIk SIk SIk SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk )) “k 111111111111c))) “k 111111111c)) “k 1111111c)) “k 1111111c) ∩ Ins2k Ins2k Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c)) ↔ ⟪{{{{x}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫ ( ∼ (( Ins3k SIk SIk SIk SIk SkIns2k (( Ins2k Ins3k SIk SIk Sk ∩ (( Ins2k Ins2k Ins2k Ins3k Sk ∩ ( Ins3k SIk SIk SIk SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk )) “k 111111111111c))) “k 111111111c)) “k 1111111c)) “k 1111111c) ∩ Ins2k Ins2k Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c))))
3431, 33ceqsexv 2894 . . . . . . . . . . . . . . . . 17 (t(t = {{{{x}}}} t, ⟪{{w}}, ⟪y, z⟫⟫⟫ ( ∼ (( Ins3k SIk SIk SIk SIk SkIns2k (( Ins2k Ins3k SIk SIk Sk ∩ (( Ins2k Ins2k Ins2k Ins3k Sk ∩ ( Ins3k SIk SIk SIk SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk )) “k 111111111111c))) “k 111111111c)) “k 1111111c)) “k 1111111c) ∩ Ins2k Ins2k Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c))) ↔ ⟪{{{{x}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫ ( ∼ (( Ins3k SIk SIk SIk SIk SkIns2k (( Ins2k Ins3k SIk SIk Sk ∩ (( Ins2k Ins2k Ins2k Ins3k Sk ∩ ( Ins3k SIk SIk SIk SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk )) “k 111111111111c))) “k 111111111c)) “k 1111111c)) “k 1111111c) ∩ Ins2k Ins2k Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c)))
35 elin 3219 . . . . . . . . . . . . . . . . 17 (⟪{{{{x}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫ ( ∼ (( Ins3k SIk SIk SIk SIk SkIns2k (( Ins2k Ins3k SIk SIk Sk ∩ (( Ins2k Ins2k Ins2k Ins3k Sk ∩ ( Ins3k SIk SIk SIk SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk )) “k 111111111111c))) “k 111111111c)) “k 1111111c)) “k 1111111c) ∩ Ins2k Ins2k Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c)) ↔ (⟪{{{{x}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫ ∼ (( Ins3k SIk SIk SIk SIk SkIns2k (( Ins2k Ins3k SIk SIk Sk ∩ (( Ins2k Ins2k Ins2k Ins3k Sk ∩ ( Ins3k SIk SIk SIk SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk )) “k 111111111111c))) “k 111111111c)) “k 1111111c)) “k 1111111c) ⟪{{{{x}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫ Ins2k Ins2k Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c)))
36 opkex 4113 . . . . . . . . . . . . . . . . . . . . . 22 ⟪{{{{x}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫ V
3736elimak 4259 . . . . . . . . . . . . . . . . . . . . 21 (⟪{{{{x}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫ (( Ins3k SIk SIk SIk SIk SkIns2k (( Ins2k Ins3k SIk SIk Sk ∩ (( Ins2k Ins2k Ins2k Ins3k Sk ∩ ( Ins3k SIk SIk SIk SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk )) “k 111111111111c))) “k 111111111c)) “k 1111111c)) “k 1111111c) ↔ t 1 111111ct, ⟪{{{{x}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫ ( Ins3k SIk SIk SIk SIk SkIns2k (( Ins2k Ins3k SIk SIk Sk ∩ (( Ins2k Ins2k Ins2k Ins3k Sk ∩ ( Ins3k SIk SIk SIk SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk )) “k 111111111111c))) “k 111111111c)) “k 1111111c)))
38 elpw161c 4152 . . . . . . . . . . . . . . . . . . . . . . . . 25 (t 1111111cc t = {{{{{{{c}}}}}}})
3938anbi1i 676 . . . . . . . . . . . . . . . . . . . . . . . 24 ((t 1111111c t, ⟪{{{{x}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫ ( Ins3k SIk SIk SIk SIk SkIns2k (( Ins2k Ins3k SIk SIk Sk ∩ (( Ins2k Ins2k Ins2k Ins3k Sk ∩ ( Ins3k SIk SIk SIk SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk )) “k 111111111111c))) “k 111111111c)) “k 1111111c))) ↔ (c t = {{{{{{{c}}}}}}} t, ⟪{{{{x}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫ ( Ins3k SIk SIk SIk SIk SkIns2k (( Ins2k Ins3k SIk SIk Sk ∩ (( Ins2k Ins2k Ins2k Ins3k Sk ∩ ( Ins3k SIk SIk SIk SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk )) “k 111111111111c))) “k 111111111c)) “k 1111111c))))
40 19.41v 1901 . . . . . . . . . . . . . . . . . . . . . . . 24 (c(t = {{{{{{{c}}}}}}} t, ⟪{{{{x}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫ ( Ins3k SIk SIk SIk SIk SkIns2k (( Ins2k Ins3k SIk SIk Sk ∩ (( Ins2k Ins2k Ins2k Ins3k Sk ∩ ( Ins3k SIk SIk SIk SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk )) “k 111111111111c))) “k 111111111c)) “k 1111111c))) ↔ (c t = {{{{{{{c}}}}}}} t, ⟪{{{{x}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫ ( Ins3k SIk SIk SIk SIk SkIns2k (( Ins2k Ins3k SIk SIk Sk ∩ (( Ins2k Ins2k Ins2k Ins3k Sk ∩ ( Ins3k SIk SIk SIk SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk )) “k 111111111111c))) “k 111111111c)) “k 1111111c))))
4139, 40bitr4i 243 . . . . . . . . . . . . . . . . . . . . . . 23 ((t 1111111c t, ⟪{{{{x}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫ ( Ins3k SIk SIk SIk SIk SkIns2k (( Ins2k Ins3k SIk SIk Sk ∩ (( Ins2k Ins2k Ins2k Ins3k Sk ∩ ( Ins3k SIk SIk SIk SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk )) “k 111111111111c))) “k 111111111c)) “k 1111111c))) ↔ c(t = {{{{{{{c}}}}}}} t, ⟪{{{{x}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫ ( Ins3k SIk SIk SIk SIk SkIns2k (( Ins2k Ins3k SIk SIk Sk ∩ (( Ins2k Ins2k Ins2k Ins3k Sk ∩ ( Ins3k SIk SIk SIk SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk )) “k 111111111111c))) “k 111111111c)) “k 1111111c))))
4241exbii 1582 . . . . . . . . . . . . . . . . . . . . . 22 (t(t 1111111c t, ⟪{{{{x}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫ ( Ins3k SIk SIk SIk SIk SkIns2k (( Ins2k Ins3k SIk SIk Sk ∩ (( Ins2k Ins2k Ins2k Ins3k Sk ∩ ( Ins3k SIk SIk SIk SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk )) “k 111111111111c))) “k 111111111c)) “k 1111111c))) ↔ tc(t = {{{{{{{c}}}}}}} t, ⟪{{{{x}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫ ( Ins3k SIk SIk SIk SIk SkIns2k (( Ins2k Ins3k SIk SIk Sk ∩ (( Ins2k Ins2k Ins2k Ins3k Sk ∩ ( Ins3k SIk SIk SIk SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk )) “k 111111111111c))) “k 111111111c)) “k 1111111c))))
43 df-rex 2620 . . . . . . . . . . . . . . . . . . . . . 22 (t 1 111111ct, ⟪{{{{x}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫ ( Ins3k SIk SIk SIk SIk SkIns2k (( Ins2k Ins3k SIk SIk Sk ∩ (( Ins2k Ins2k Ins2k Ins3k Sk ∩ ( Ins3k SIk SIk SIk SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk )) “k 111111111111c))) “k 111111111c)) “k 1111111c)) ↔ t(t 1111111c t, ⟪{{{{x}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫ ( Ins3k SIk SIk SIk SIk SkIns2k (( Ins2k Ins3k SIk SIk Sk ∩ (( Ins2k Ins2k Ins2k Ins3k Sk ∩ ( Ins3k SIk SIk SIk SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk )) “k 111111111111c))) “k 111111111c)) “k 1111111c))))
44 excom 1741 . . . . . . . . . . . . . . . . . . . . . 22 (ct(t = {{{{{{{c}}}}}}} t, ⟪{{{{x}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫ ( Ins3k SIk SIk SIk SIk SkIns2k (( Ins2k Ins3k SIk SIk Sk ∩ (( Ins2k Ins2k Ins2k Ins3k Sk ∩ ( Ins3k SIk SIk SIk SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk )) “k 111111111111c))) “k 111111111c)) “k 1111111c))) ↔ tc(t = {{{{{{{c}}}}}}} t, ⟪{{{{x}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫ ( Ins3k SIk SIk SIk SIk SkIns2k (( Ins2k Ins3k SIk SIk Sk ∩ (( Ins2k Ins2k Ins2k Ins3k Sk ∩ ( Ins3k SIk SIk SIk SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk )) “k 111111111111c))) “k 111111111c)) “k 1111111c))))
4542, 43, 443bitr4i 268 . . . . . . . . . . . . . . . . . . . . 21 (t 1 111111ct, ⟪{{{{x}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫ ( Ins3k SIk SIk SIk SIk SkIns2k (( Ins2k Ins3k SIk SIk Sk ∩ (( Ins2k Ins2k Ins2k Ins3k Sk ∩ ( Ins3k SIk SIk SIk SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk )) “k 111111111111c))) “k 111111111c)) “k 1111111c)) ↔ ct(t = {{{{{{{c}}}}}}} t, ⟪{{{{x}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫ ( Ins3k SIk SIk SIk SIk SkIns2k (( Ins2k Ins3k SIk SIk Sk ∩ (( Ins2k Ins2k Ins2k Ins3k Sk ∩ ( Ins3k SIk SIk SIk SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk )) “k 111111111111c))) “k 111111111c)) “k 1111111c))))
46 snex 4111 . . . . . . . . . . . . . . . . . . . . . . . 24 {{{{{{{c}}}}}}} V
47 opkeq1 4059 . . . . . . . . . . . . . . . . . . . . . . . . 25 (t = {{{{{{{c}}}}}}} → ⟪t, ⟪{{{{x}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫ = ⟪{{{{{{{c}}}}}}}, ⟪{{{{x}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫)
4847eleq1d 2419 . . . . . . . . . . . . . . . . . . . . . . . 24 (t = {{{{{{{c}}}}}}} → (⟪t, ⟪{{{{x}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫ ( Ins3k SIk SIk SIk SIk SkIns2k (( Ins2k Ins3k SIk SIk Sk ∩ (( Ins2k Ins2k Ins2k Ins3k Sk ∩ ( Ins3k SIk SIk SIk SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk )) “k 111111111111c))) “k 111111111c)) “k 1111111c)) ↔ ⟪{{{{{{{c}}}}}}}, ⟪{{{{x}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫ ( Ins3k SIk SIk SIk SIk SkIns2k (( Ins2k Ins3k SIk SIk Sk ∩ (( Ins2k Ins2k Ins2k Ins3k Sk ∩ ( Ins3k SIk SIk SIk SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk )) “k 111111111111c))) “k 111111111c)) “k 1111111c))))
4946, 48ceqsexv 2894 . . . . . . . . . . . . . . . . . . . . . . 23 (t(t = {{{{{{{c}}}}}}} t, ⟪{{{{x}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫ ( Ins3k SIk SIk SIk SIk SkIns2k (( Ins2k Ins3k SIk SIk Sk ∩ (( Ins2k Ins2k Ins2k Ins3k Sk ∩ ( Ins3k SIk SIk SIk SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk )) “k 111111111111c))) “k 111111111c)) “k 1111111c))) ↔ ⟪{{{{{{{c}}}}}}}, ⟪{{{{x}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫ ( Ins3k SIk SIk SIk SIk SkIns2k (( Ins2k Ins3k SIk SIk Sk ∩ (( Ins2k Ins2k Ins2k Ins3k Sk ∩ ( Ins3k SIk SIk SIk SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk )) “k 111111111111c))) “k 111111111c)) “k 1111111c)))
50 elsymdif 3223 . . . . . . . . . . . . . . . . . . . . . . 23 (⟪{{{{{{{c}}}}}}}, ⟪{{{{x}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫ ( Ins3k SIk SIk SIk SIk SkIns2k (( Ins2k Ins3k SIk SIk Sk ∩ (( Ins2k Ins2k Ins2k Ins3k Sk ∩ ( Ins3k SIk SIk SIk SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk )) “k 111111111111c))) “k 111111111c)) “k 1111111c)) ↔ ¬ (⟪{{{{{{{c}}}}}}}, ⟪{{{{x}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫ Ins3k SIk SIk SIk SIk Sk ↔ ⟪{{{{{{{c}}}}}}}, ⟪{{{{x}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫ Ins2k (( Ins2k Ins3k SIk SIk Sk ∩ (( Ins2k Ins2k Ins2k Ins3k Sk ∩ ( Ins3k SIk SIk SIk SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk )) “k 111111111111c))) “k 111111111c)) “k 1111111c)))
51 snex 4111 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 {{{{{c}}}}} V
5251, 31, 21otkelins3k 4256 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (⟪{{{{{{{c}}}}}}}, ⟪{{{{x}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫ Ins3k SIk SIk SIk SIk Sk ↔ ⟪{{{{{c}}}}}, {{{{x}}}}⟫ SIk SIk SIk SIk Sk )
53 snex 4111 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 {{{{c}}}} V
54 snex 4111 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 {{{x}}} V
5553, 54opksnelsik 4265 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (⟪{{{{{c}}}}}, {{{{x}}}}⟫ SIk SIk SIk SIk Sk ↔ ⟪{{{{c}}}}, {{{x}}}⟫ SIk SIk SIk Sk )
56 snex 4111 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 {{{c}}} V
57 snex 4111 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 {{x}} V
5856, 57opksnelsik 4265 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (⟪{{{{c}}}}, {{{x}}}⟫ SIk SIk SIk Sk ↔ ⟪{{{c}}}, {{x}}⟫ SIk SIk Sk )
59 snex 4111 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 {{c}} V
60 snex 4111 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 {x} V
6159, 60opksnelsik 4265 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (⟪{{{c}}}, {{x}}⟫ SIk SIk Sk ↔ ⟪{{c}}, {x}⟫ SIk Sk )
62 snex 4111 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 {c} V
63 vex 2862 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 x V
6462, 63opksnelsik 4265 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (⟪{{c}}, {x}⟫ SIk Sk ↔ ⟪{c}, x Sk )
65 vex 2862 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 c V
6665, 63elssetk 4270 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (⟪{c}, x Skc x)
6764, 66bitri 240 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (⟪{{c}}, {x}⟫ SIk Skc x)
6858, 61, 673bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (⟪{{{{c}}}}, {{{x}}}⟫ SIk SIk SIk Skc x)
6952, 55, 683bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . 25 (⟪{{{{{{{c}}}}}}}, ⟪{{{{x}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫ Ins3k SIk SIk SIk SIk Skc x)
70 opkex 4113 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⟪{{{{{c}}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫ V
7170elimak 4259 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (⟪{{{{{c}}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫ (( Ins2k Ins3k SIk SIk Sk ∩ (( Ins2k Ins2k Ins2k Ins3k Sk ∩ ( Ins3k SIk SIk SIk SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk )) “k 111111111111c))) “k 111111111c)) “k 1111111c) ↔ t 1 111111ct, ⟪{{{{{c}}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫ ( Ins2k Ins3k SIk SIk Sk ∩ (( Ins2k Ins2k Ins2k Ins3k Sk ∩ ( Ins3k SIk SIk SIk SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk )) “k 111111111111c))) “k 111111111c)))
72 elpw161c 4152 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (t 1111111cb t = {{{{{{{b}}}}}}})
7372anbi1i 676 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((t 1111111c t, ⟪{{{{{c}}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫ ( Ins2k Ins3k SIk SIk Sk ∩ (( Ins2k Ins2k Ins2k Ins3k Sk ∩ ( Ins3k SIk SIk SIk SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk )) “k 111111111111c))) “k 111111111c))) ↔ (b t = {{{{{{{b}}}}}}} t, ⟪{{{{{c}}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫ ( Ins2k Ins3k SIk SIk Sk ∩ (( Ins2k Ins2k Ins2k Ins3k Sk ∩ ( Ins3k SIk SIk SIk SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk )) “k 111111111111c))) “k 111111111c))))
74 19.41v 1901 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (b(t = {{{{{{{b}}}}}}} t, ⟪{{{{{c}}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫ ( Ins2k Ins3k SIk SIk Sk ∩ (( Ins2k Ins2k Ins2k Ins3k Sk ∩ ( Ins3k SIk SIk SIk SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk )) “k 111111111111c))) “k 111111111c))) ↔ (b t = {{{{{{{b}}}}}}} t, ⟪{{{{{c}}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫ ( Ins2k Ins3k SIk SIk Sk ∩ (( Ins2k Ins2k Ins2k Ins3k Sk ∩ ( Ins3k SIk SIk SIk SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk )) “k 111111111111c))) “k 111111111c))))
7573, 74bitr4i 243 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((t 1111111c t, ⟪{{{{{c}}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫ ( Ins2k Ins3k SIk SIk Sk ∩ (( Ins2k Ins2k Ins2k Ins3k Sk ∩ ( Ins3k SIk SIk SIk SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk )) “k 111111111111c))) “k 111111111c))) ↔ b(t = {{{{{{{b}}}}}}} t, ⟪{{{{{c}}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫ ( Ins2k Ins3k SIk SIk Sk ∩ (( Ins2k Ins2k Ins2k Ins3k Sk ∩ ( Ins3k SIk SIk SIk SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk )) “k 111111111111c))) “k 111111111c))))
7675exbii 1582 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (t(t 1111111c t, ⟪{{{{{c}}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫ ( Ins2k Ins3k SIk SIk Sk ∩ (( Ins2k Ins2k Ins2k Ins3k Sk ∩ ( Ins3k SIk SIk SIk SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk )) “k 111111111111c))) “k 111111111c))) ↔ tb(t = {{{{{{{b}}}}}}} t, ⟪{{{{{c}}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫ ( Ins2k Ins3k SIk SIk Sk ∩ (( Ins2k Ins2k Ins2k Ins3k Sk ∩ ( Ins3k SIk SIk SIk SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk )) “k 111111111111c))) “k 111111111c))))
77 df-rex 2620 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (t 1 111111ct, ⟪{{{{{c}}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫ ( Ins2k Ins3k SIk SIk Sk ∩ (( Ins2k Ins2k Ins2k Ins3k Sk ∩ ( Ins3k SIk SIk SIk SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk )) “k 111111111111c))) “k 111111111c)) ↔ t(t 1111111c t, ⟪{{{{{c}}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫ ( Ins2k Ins3k SIk SIk Sk ∩ (( Ins2k Ins2k Ins2k Ins3k Sk ∩ ( Ins3k SIk SIk SIk SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk )) “k 111111111111c))) “k 111111111c))))
78 excom 1741 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (bt(t = {{{{{{{b}}}}}}} t, ⟪{{{{{c}}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫ ( Ins2k Ins3k SIk SIk Sk ∩ (( Ins2k Ins2k Ins2k Ins3k Sk ∩ ( Ins3k SIk SIk SIk SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk )) “k 111111111111c))) “k 111111111c))) ↔ tb(t = {{{{{{{b}}}}}}} t, ⟪{{{{{c}}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫ ( Ins2k Ins3k SIk SIk Sk ∩ (( Ins2k Ins2k Ins2k Ins3k Sk ∩ ( Ins3k SIk SIk SIk SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk )) “k 111111111111c))) “k 111111111c))))
7976, 77, 783bitr4i 268 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (t 1 111111ct, ⟪{{{{{c}}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫ ( Ins2k Ins3k SIk SIk Sk ∩ (( Ins2k Ins2k Ins2k Ins3k Sk ∩ ( Ins3k SIk SIk SIk SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk )) “k 111111111111c))) “k 111111111c)) ↔ bt(t = {{{{{{{b}}}}}}} t, ⟪{{{{{c}}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫ ( Ins2k Ins3k SIk SIk Sk ∩ (( Ins2k Ins2k Ins2k Ins3k Sk ∩ ( Ins3k SIk SIk SIk SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk )) “k 111111111111c))) “k 111111111c))))
80 snex 4111 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 {{{{{{{b}}}}}}} V
81 opkeq1 4059 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (t = {{{{{{{b}}}}}}} → ⟪t, ⟪{{{{{c}}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫ = ⟪{{{{{{{b}}}}}}}, ⟪{{{{{c}}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫)
8281eleq1d 2419 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (t = {{{{{{{b}}}}}}} → (⟪t, ⟪{{{{{c}}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫ ( Ins2k Ins3k SIk SIk Sk ∩ (( Ins2k Ins2k Ins2k Ins3k Sk ∩ ( Ins3k SIk SIk SIk SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk )) “k 111111111111c))) “k 111111111c)) ↔ ⟪{{{{{{{b}}}}}}}, ⟪{{{{{c}}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫ ( Ins2k Ins3k SIk SIk Sk ∩ (( Ins2k Ins2k Ins2k Ins3k Sk ∩ ( Ins3k SIk SIk SIk SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk )) “k 111111111111c))) “k 111111111c))))
8380, 82ceqsexv 2894 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (t(t = {{{{{{{b}}}}}}} t, ⟪{{{{{c}}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫ ( Ins2k Ins3k SIk SIk Sk ∩ (( Ins2k Ins2k Ins2k Ins3k Sk ∩ ( Ins3k SIk SIk SIk SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk )) “k 111111111111c))) “k 111111111c))) ↔ ⟪{{{{{{{b}}}}}}}, ⟪{{{{{c}}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫ ( Ins2k Ins3k SIk SIk Sk ∩ (( Ins2k Ins2k Ins2k Ins3k Sk ∩ ( Ins3k SIk SIk SIk SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk )) “k 111111111111c))) “k 111111111c)))
84 elin 3219 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (⟪{{{{{{{b}}}}}}}, ⟪{{{{{c}}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫ ( Ins2k Ins3k SIk SIk Sk ∩ (( Ins2k Ins2k Ins2k Ins3k Sk ∩ ( Ins3k SIk SIk SIk SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk )) “k 111111111111c))) “k 111111111c)) ↔ (⟪{{{{{{{b}}}}}}}, ⟪{{{{{c}}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫ Ins2k Ins3k SIk SIk Sk ⟪{{{{{{{b}}}}}}}, ⟪{{{{{c}}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫ (( Ins2k Ins2k Ins2k Ins3k Sk ∩ ( Ins3k SIk SIk SIk SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk )) “k 111111111111c))) “k 111111111c)))
85 snex 4111 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 {{{{{b}}}}} V
8685, 51, 21otkelins2k 4255 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (⟪{{{{{{{b}}}}}}}, ⟪{{{{{c}}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫ Ins2k Ins3k SIk SIk Sk ↔ ⟪{{{{{b}}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫ Ins3k SIk SIk Sk )
87 snex 4111 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 {{{b}}} V
8887, 17, 7otkelins3k 4256 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (⟪{{{{{b}}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫ Ins3k SIk SIk Sk ↔ ⟪{{{b}}}, {{w}}⟫ SIk SIk Sk )
89 snex 4111 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 {{b}} V
90 snex 4111 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 {w} V
9189, 90opksnelsik 4265 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (⟪{{{b}}}, {{w}}⟫ SIk SIk Sk ↔ ⟪{{b}}, {w}⟫ SIk Sk )
92 snex 4111 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 {b} V
93 vex 2862 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 w V
9492, 93opksnelsik 4265 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (⟪{{b}}, {w}⟫ SIk Sk ↔ ⟪{b}, w Sk )
95 vex 2862 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 b V
9695, 93elssetk 4270 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (⟪{b}, w Skb w)
9791, 94, 963bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (⟪{{{b}}}, {{w}}⟫ SIk SIk Skb w)
9886, 88, 973bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (⟪{{{{{{{b}}}}}}}, ⟪{{{{{c}}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫ Ins2k Ins3k SIk SIk Skb w)
99 opkex 4113 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⟪{{{{{{{b}}}}}}}, ⟪{{{{{c}}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫ V
10099elimak 4259 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (⟪{{{{{{{b}}}}}}}, ⟪{{{{{c}}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫ (( Ins2k Ins2k Ins2k Ins3k Sk ∩ ( Ins3k SIk SIk SIk SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk )) “k 111111111111c))) “k 111111111c) ↔ t 1 11111111ct, ⟪{{{{{{{b}}}}}}}, ⟪{{{{{c}}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫⟫ ( Ins2k Ins2k Ins2k Ins3k Sk ∩ ( Ins3k SIk SIk SIk SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk )) “k 111111111111c))))
101 elpw181c 4154 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (t 111111111ca t = {{{{{{{{{a}}}}}}}}})
102101anbi1i 676 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((t 111111111c t, ⟪{{{{{{{b}}}}}}}, ⟪{{{{{c}}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫⟫ ( Ins2k Ins2k Ins2k Ins3k Sk ∩ ( Ins3k SIk SIk SIk SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk )) “k 111111111111c)))) ↔ (a t = {{{{{{{{{a}}}}}}}}} t, ⟪{{{{{{{b}}}}}}}, ⟪{{{{{c}}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫⟫ ( Ins2k Ins2k Ins2k Ins3k Sk ∩ ( Ins3k SIk SIk SIk SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk )) “k 111111111111c)))))
103 19.41v 1901 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (a(t = {{{{{{{{{a}}}}}}}}} t, ⟪{{{{{{{b}}}}}}}, ⟪{{{{{c}}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫⟫ ( Ins2k Ins2k Ins2k Ins3k Sk ∩ ( Ins3k SIk SIk SIk SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk )) “k 111111111111c)))) ↔ (a t = {{{{{{{{{a}}}}}}}}} t, ⟪{{{{{{{b}}}}}}}, ⟪{{{{{c}}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫⟫ ( Ins2k Ins2k Ins2k Ins3k Sk ∩ ( Ins3k SIk SIk SIk SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk )) “k 111111111111c)))))
104102, 103bitr4i 243 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((t 111111111c t, ⟪{{{{{{{b}}}}}}}, ⟪{{{{{c}}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫⟫ ( Ins2k Ins2k Ins2k Ins3k Sk ∩ ( Ins3k SIk SIk SIk SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk )) “k 111111111111c)))) ↔ a(t = {{{{{{{{{a}}}}}}}}} t, ⟪{{{{{{{b}}}}}}}, ⟪{{{{{c}}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫⟫ ( Ins2k Ins2k Ins2k Ins3k Sk ∩ ( Ins3k SIk SIk SIk SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk )) “k 111111111111c)))))
105104exbii 1582 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (t(t 111111111c t, ⟪{{{{{{{b}}}}}}}, ⟪{{{{{c}}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫⟫ ( Ins2k Ins2k Ins2k Ins3k Sk ∩ ( Ins3k SIk SIk SIk SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk )) “k 111111111111c)))) ↔ ta(t = {{{{{{{{{a}}}}}}}}} t, ⟪{{{{{{{b}}}}}}}, ⟪{{{{{c}}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫⟫ ( Ins2k Ins2k Ins2k Ins3k Sk ∩ ( Ins3k SIk SIk SIk SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk )) “k 111111111111c)))))
106 df-rex 2620 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (t 1 11111111ct, ⟪{{{{{{{b}}}}}}}, ⟪{{{{{c}}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫⟫ ( Ins2k Ins2k Ins2k Ins3k Sk ∩ ( Ins3k SIk SIk SIk SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk )) “k 111111111111c))) ↔ t(t 111111111c t, ⟪{{{{{{{b}}}}}}}, ⟪{{{{{c}}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫⟫ ( Ins2k Ins2k Ins2k Ins3k Sk ∩ ( Ins3k SIk SIk SIk SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk )) “k 111111111111c)))))
107 excom 1741 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (at(t = {{{{{{{{{a}}}}}}}}} t, ⟪{{{{{{{b}}}}}}}, ⟪{{{{{c}}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫⟫ ( Ins2k Ins2k Ins2k Ins3k Sk ∩ ( Ins3k SIk SIk SIk SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk )) “k 111111111111c)))) ↔ ta(t = {{{{{{{{{a}}}}}}}}} t, ⟪{{{{{{{b}}}}}}}, ⟪{{{{{c}}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫⟫ ( Ins2k Ins2k Ins2k Ins3k Sk ∩ ( Ins3k SIk SIk SIk SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk )) “k 111111111111c)))))
108105, 106, 1073bitr4i 268 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (t 1 11111111ct, ⟪{{{{{{{b}}}}}}}, ⟪{{{{{c}}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫⟫ ( Ins2k Ins2k Ins2k Ins3k Sk ∩ ( Ins3k SIk SIk SIk SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk )) “k 111111111111c))) ↔ at(t = {{{{{{{{{a}}}}}}}}} t, ⟪{{{{{{{b}}}}}}}, ⟪{{{{{c}}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫⟫ ( Ins2k Ins2k Ins2k Ins3k Sk ∩ ( Ins3k SIk SIk SIk SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk )) “k 111111111111c)))))
109 snex 4111 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 {{{{{{{{{a}}}}}}}}} V
110 opkeq1 4059 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (t = {{{{{{{{{a}}}}}}}}} → ⟪t, ⟪{{{{{{{b}}}}}}}, ⟪{{{{{c}}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫⟫ = ⟪{{{{{{{{{a}}}}}}}}}, ⟪{{{{{{{b}}}}}}}, ⟪{{{{{c}}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫⟫)
111110eleq1d 2419 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (t = {{{{{{{{{a}}}}}}}}} → (⟪t, ⟪{{{{{{{b}}}}}}}, ⟪{{{{{c}}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫⟫ ( Ins2k Ins2k Ins2k Ins3k Sk ∩ ( Ins3k SIk SIk SIk SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk )) “k 111111111111c))) ↔ ⟪{{{{{{{{{a}}}}}}}}}, ⟪{{{{{{{b}}}}}}}, ⟪{{{{{c}}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫⟫ ( Ins2k Ins2k Ins2k Ins3k Sk ∩ ( Ins3k SIk SIk SIk SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk )) “k 111111111111c)))))
112109, 111ceqsexv 2894 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (t(t = {{{{{{{{{a}}}}}}}}} t, ⟪{{{{{{{b}}}}}}}, ⟪{{{{{c}}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫⟫ ( Ins2k Ins2k Ins2k Ins3k Sk ∩ ( Ins3k SIk SIk SIk SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk )) “k 111111111111c)))) ↔ ⟪{{{{{{{{{a}}}}}}}}}, ⟪{{{{{{{b}}}}}}}, ⟪{{{{{c}}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫⟫ ( Ins2k Ins2k Ins2k Ins3k Sk ∩ ( Ins3k SIk SIk SIk SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk )) “k 111111111111c))))
113 elin 3219 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (⟪{{{{{{{{{a}}}}}}}}}, ⟪{{{{{{{b}}}}}}}, ⟪{{{{{c}}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫⟫ ( Ins2k Ins2k Ins2k Ins3k Sk ∩ ( Ins3k SIk SIk SIk SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk )) “k 111111111111c))) ↔ (⟪{{{{{{{{{a}}}}}}}}}, ⟪{{{{{{{b}}}}}}}, ⟪{{{{{c}}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫⟫ Ins2k Ins2k Ins2k Ins3k Sk ⟪{{{{{{{{{a}}}}}}}}}, ⟪{{{{{{{b}}}}}}}, ⟪{{{{{c}}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫⟫ ( Ins3k SIk SIk SIk SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk )) “k 111111111111c))))
114 snex 4111 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 {{{{{{{a}}}}}}} V
115114, 80, 70otkelins2k 4255 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (⟪{{{{{{{{{a}}}}}}}}}, ⟪{{{{{{{b}}}}}}}, ⟪{{{{{c}}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫⟫ Ins2k Ins2k Ins2k Ins3k Sk ↔ ⟪{{{{{{{a}}}}}}}, ⟪{{{{{c}}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫ Ins2k Ins2k Ins3k Sk )
116 snex 4111 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 {{{{{a}}}}} V
117116, 51, 21otkelins2k 4255 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (⟪{{{{{{{a}}}}}}}, ⟪{{{{{c}}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫ Ins2k Ins2k Ins3k Sk ↔ ⟪{{{{{a}}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫ Ins2k Ins3k Sk )
118 snex 4111 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 {{{a}}} V
119118, 17, 7otkelins2k 4255 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (⟪{{{{{a}}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫ Ins2k Ins3k Sk ↔ ⟪{{{a}}}, ⟪y, z⟫⟫ Ins3k Sk )
120 snex 4111 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 {a} V
121 vex 2862 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 y V
122 vex 2862 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 z V
123120, 121, 122otkelins3k 4256 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (⟪{{{a}}}, ⟪y, z⟫⟫ Ins3k Sk ↔ ⟪{a}, y Sk )
124 vex 2862 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 a V
125124, 121elssetk 4270 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (⟪{a}, y Ska y)
126119, 123, 1253bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (⟪{{{{{a}}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫ Ins2k Ins3k Ska y)
127115, 117, 1263bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (⟪{{{{{{{{{a}}}}}}}}}, ⟪{{{{{{{b}}}}}}}, ⟪{{{{{c}}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫⟫ Ins2k Ins2k Ins2k Ins3k Ska y)
128 elin 3219 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (⟪{{{{{{{{{a}}}}}}}}}, ⟪{{{{{{{b}}}}}}}, ⟪{{{{{c}}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫⟫ ( Ins3k SIk SIk SIk SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk )) “k 111111111111c)) ↔ (⟪{{{{{{{{{a}}}}}}}}}, ⟪{{{{{{{b}}}}}}}, ⟪{{{{{c}}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫⟫ Ins3k SIk SIk SIk SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ⟪{{{{{{{{{a}}}}}}}}}, ⟪{{{{{{{b}}}}}}}, ⟪{{{{{c}}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫⟫ ∼ (( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk )) “k 111111111111c)))
129114, 80, 70otkelins3k 4256 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (⟪{{{{{{{{{a}}}}}}}}}, ⟪{{{{{{{b}}}}}}}, ⟪{{{{{c}}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫⟫ Ins3k SIk SIk SIk SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ↔ ⟪{{{{{{{a}}}}}}}, {{{{{{{b}}}}}}}⟫ SIk SIk SIk SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c))
130 snex 4111 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 {{{{{{a}}}}}} V
131 snex 4111 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 {{{{{{b}}}}}} V
132130, 131opksnelsik 4265 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (⟪{{{{{{{a}}}}}}}, {{{{{{{b}}}}}}}⟫ SIk SIk SIk SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ↔ ⟪{{{{{{a}}}}}}, {{{{{{b}}}}}}⟫ SIk SIk SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c))
133116, 85opksnelsik 4265 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (⟪{{{{{{a}}}}}}, {{{{{{b}}}}}}⟫ SIk SIk SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ↔ ⟪{{{{{a}}}}}, {{{{{b}}}}}⟫ SIk SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c))
134 snex 4111 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 {{{{a}}}} V
135 snex 4111 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 {{{{b}}}} V
136134, 135opksnelsik 4265 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (⟪{{{{{a}}}}}, {{{{{b}}}}}⟫ SIk SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ↔ ⟪{{{{a}}}}, {{{{b}}}}⟫ SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c))
137118, 87opksnelsik 4265 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (⟪{{{{a}}}}, {{{{b}}}}⟫ SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ↔ ⟪{{{a}}}, {{{b}}}⟫ SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c))
138 snex 4111 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 {{a}} V
139138, 89opksnelsik 4265 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (⟪{{{a}}}, {{{b}}}⟫ SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ↔ ⟪{{a}}, {{b}}⟫ SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c))
140120, 92opksnelsik 4265 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (⟪{{a}}, {{b}}⟫ SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ↔ ⟪{a}, {b}⟫ SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c))
141124, 95opksnelsik 4265 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (⟪{a}, {b}⟫ SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ↔ ⟪a, b ∼ (( Ins3k SkIns2k Sk ) “k 111c))
142124, 95ndisjrelk 4323 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (⟪a, b (( Ins3k SkIns2k Sk ) “k 111c) ↔ (ab) ≠ )
143142notbii 287 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (¬ ⟪a, b (( Ins3k SkIns2k Sk ) “k 111c) ↔ ¬ (ab) ≠ )
144 opkex 4113 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 a, b V
145144elcompl 3225 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (⟪a, b ∼ (( Ins3k SkIns2k Sk ) “k 111c) ↔ ¬ ⟪a, b (( Ins3k SkIns2k Sk ) “k 111c))
146 df-ne 2518 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ((ab) ≠ ↔ ¬ (ab) = )
147146con2bii 322 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((ab) = ↔ ¬ (ab) ≠ )
148143, 145, 1473bitr4i 268 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (⟪a, b ∼ (( Ins3k SkIns2k Sk ) “k 111c) ↔ (ab) = )
149140, 141, 1483bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (⟪{{a}}, {{b}}⟫ SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ↔ (ab) = )
150137, 139, 1493bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (⟪{{{{a}}}}, {{{{b}}}}⟫ SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ↔ (ab) = )
151133, 136, 1503bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (⟪{{{{{{a}}}}}}, {{{{{{b}}}}}}⟫ SIk SIk SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ↔ (ab) = )
152129, 132, 1513bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (⟪{{{{{{{{{a}}}}}}}}}, ⟪{{{{{{{b}}}}}}}, ⟪{{{{{c}}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫⟫ Ins3k SIk SIk SIk SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ↔ (ab) = )
153 opkex 4113 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⟪{{{{{{{{{a}}}}}}}}}, ⟪{{{{{{{b}}}}}}}, ⟪{{{{{c}}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫⟫ V
154153elimak 4259 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (⟪{{{{{{{{{a}}}}}}}}}, ⟪{{{{{{{b}}}}}}}, ⟪{{{{{c}}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫⟫ (( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk )) “k 111111111111c) ↔ t 1 11111111111ct, ⟪{{{{{{{{{a}}}}}}}}}, ⟪{{{{{{{b}}}}}}}, ⟪{{{{{c}}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫⟫⟫ ( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk )))
155 elpw1111c 4157 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (t 111111111111cd t = {{{{{{{{{{{{d}}}}}}}}}}}})
156155anbi1i 676 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ((t 111111111111c t, ⟪{{{{{{{{{a}}}}}}}}}, ⟪{{{{{{{b}}}}}}}, ⟪{{{{{c}}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫⟫⟫ ( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk ))) ↔ (d t = {{{{{{{{{{{{d}}}}}}}}}}}} t, ⟪{{{{{{{{{a}}}}}}}}}, ⟪{{{{{{{b}}}}}}}, ⟪{{{{{c}}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫⟫⟫ ( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk ))))
157 19.41v 1901 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (d(t = {{{{{{{{{{{{d}}}}}}}}}}}} t, ⟪{{{{{{{{{a}}}}}}}}}, ⟪{{{{{{{b}}}}}}}, ⟪{{{{{c}}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫⟫⟫ ( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk ))) ↔ (d t = {{{{{{{{{{{{d}}}}}}}}}}}} t, ⟪{{{{{{{{{a}}}}}}}}}, ⟪{{{{{{{b}}}}}}}, ⟪{{{{{c}}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫⟫⟫ ( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk ))))
158156, 157bitr4i 243 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((t 111111111111c t, ⟪{{{{{{{{{a}}}}}}}}}, ⟪{{{{{{{b}}}}}}}, ⟪{{{{{c}}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫⟫⟫ ( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk ))) ↔ d(t = {{{{{{{{{{{{d}}}}}}}}}}}} t, ⟪{{{{{{{{{a}}}}}}}}}, ⟪{{{{{{{b}}}}}}}, ⟪{{{{{c}}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫⟫⟫ ( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk ))))
159158exbii 1582 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (t(t 111111111111c t, ⟪{{{{{{{{{a}}}}}}}}}, ⟪{{{{{{{b}}}}}}}, ⟪{{{{{c}}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫⟫⟫ ( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk ))) ↔ td(t = {{{{{{{{{{{{d}}}}}}}}}}}} t, ⟪{{{{{{{{{a}}}}}}}}}, ⟪{{{{{{{b}}}}}}}, ⟪{{{{{c}}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫⟫⟫ ( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk ))))
160 df-rex 2620 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (t 1 11111111111ct, ⟪{{{{{{{{{a}}}}}}}}}, ⟪{{{{{{{b}}}}}}}, ⟪{{{{{c}}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫⟫⟫ ( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk )) ↔ t(t 111111111111c t, ⟪{{{{{{{{{a}}}}}}}}}, ⟪{{{{{{{b}}}}}}}, ⟪{{{{{c}}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫⟫⟫ ( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk ))))
161 excom 1741 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (dt(t = {{{{{{{{{{{{d}}}}}}}}}}}} t, ⟪{{{{{{{{{a}}}}}}}}}, ⟪{{{{{{{b}}}}}}}, ⟪{{{{{c}}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫⟫⟫ ( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk ))) ↔ td(t = {{{{{{{{{{{{d}}}}}}}}}}}} t, ⟪{{{{{{{{{a}}}}}}}}}, ⟪{{{{{{{b}}}}}}}, ⟪{{{{{c}}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫⟫⟫ ( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk ))))
162159, 160, 1613bitr4i 268 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (t 1 11111111111ct, ⟪{{{{{{{{{a}}}}}}}}}, ⟪{{{{{{{b}}}}}}}, ⟪{{{{{c}}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫⟫⟫ ( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk )) ↔ dt(t = {{{{{{{{{{{{d}}}}}}}}}}}} t, ⟪{{{{{{{{{a}}}}}}}}}, ⟪{{{{{{{b}}}}}}}, ⟪{{{{{c}}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫⟫⟫ ( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk ))))
163 snex 4111 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 {{{{{{{{{{{{d}}}}}}}}}}}} V
164 opkeq1 4059 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (t = {{{{{{{{{{{{d}}}}}}}}}}}} → ⟪t, ⟪{{{{{{{{{a}}}}}}}}}, ⟪{{{{{{{b}}}}}}}, ⟪{{{{{c}}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫⟫⟫ = ⟪{{{{{{{{{{{{d}}}}}}}}}}}}, ⟪{{{{{{{{{a}}}}}}}}}, ⟪{{{{{{{b}}}}}}}, ⟪{{{{{c}}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫⟫⟫)
165164eleq1d 2419 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (t = {{{{{{{{{{{{d}}}}}}}}}}}} → (⟪t, ⟪{{{{{{{{{a}}}}}}}}}, ⟪{{{{{{{b}}}}}}}, ⟪{{{{{c}}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫⟫⟫ ( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk )) ↔ ⟪{{{{{{{{{{{{d}}}}}}}}}}}}, ⟪{{{{{{{{{a}}}}}}}}}, ⟪{{{{{{{b}}}}}}}, ⟪{{{{{c}}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫⟫⟫ ( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk ))))
166163, 165ceqsexv 2894 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (t(t = {{{{{{{{{{{{d}}}}}}}}}}}} t, ⟪{{{{{{{{{a}}}}}}}}}, ⟪{{{{{{{b}}}}}}}, ⟪{{{{{c}}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫⟫⟫ ( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk ))) ↔ ⟪{{{{{{{{{{{{d}}}}}}}}}}}}, ⟪{{{{{{{{{a}}}}}}}}}, ⟪{{{{{{{b}}}}}}}, ⟪{{{{{c}}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫⟫⟫ ( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk )))
167 elsymdif 3223 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (⟪{{{{{{{{{{{{d}}}}}}}}}}}}, ⟪{{{{{{{{{a}}}}}}}}}, ⟪{{{{{{{b}}}}}}}, ⟪{{{{{c}}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫⟫⟫ ( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk )) ↔ ¬ (⟪{{{{{{{{{{{{d}}}}}}}}}}}}, ⟪{{{{{{{{{a}}}}}}}}}, ⟪{{{{{{{b}}}}}}}, ⟪{{{{{c}}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫⟫⟫ Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ↔ ⟪{{{{{{{{{{{{d}}}}}}}}}}}}, ⟪{{{{{{{{{a}}}}}}}}}, ⟪{{{{{{{b}}}}}}}, ⟪{{{{{c}}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫⟫⟫ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk )))
168 snex 4111 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 {{{{{{{{{{d}}}}}}}}}} V
169168, 109, 99otkelins2k 4255 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 (⟪{{{{{{{{{{{{d}}}}}}}}}}}}, ⟪{{{{{{{{{a}}}}}}}}}, ⟪{{{{{{{b}}}}}}}, ⟪{{{{{c}}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫⟫⟫ Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ↔ ⟪{{{{{{{{{{d}}}}}}}}}}, ⟪{{{{{{{b}}}}}}}, ⟪{{{{{c}}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫⟫ Ins2k Ins3k SIk SIk SIk SIk SIk Sk )
170 snex 4111 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 {{{{{{{{d}}}}}}}} V
171170, 80, 70otkelins2k 4255 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 (⟪{{{{{{{{{{d}}}}}}}}}}, ⟪{{{{{{{b}}}}}}}, ⟪{{{{{c}}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫⟫ Ins2k Ins3k SIk SIk SIk SIk SIk Sk ↔ ⟪{{{{{{{{d}}}}}}}}, ⟪{{{{{c}}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫ Ins3k SIk SIk SIk SIk SIk Sk )
172 snex 4111 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 {{{{{{d}}}}}} V
173172, 51, 21otkelins3k 4256 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 (⟪{{{{{{{{d}}}}}}}}, ⟪{{{{{c}}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫ Ins3k SIk SIk SIk SIk SIk Sk ↔ ⟪{{{{{{d}}}}}}, {{{{{c}}}}}⟫ SIk SIk SIk SIk SIk Sk )
174 snex 4111 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 {{{{{d}}}}} V
175174, 53opksnelsik 4265 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 (⟪{{{{{{d}}}}}}, {{{{{c}}}}}⟫ SIk SIk SIk SIk SIk Sk ↔ ⟪{{{{{d}}}}}, {{{{c}}}}⟫ SIk SIk SIk SIk Sk )
176 snex 4111 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 {{{{d}}}} V
177176, 56opksnelsik 4265 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 (⟪{{{{{d}}}}}, {{{{c}}}}⟫ SIk SIk SIk SIk Sk ↔ ⟪{{{{d}}}}, {{{c}}}⟫ SIk SIk SIk Sk )
178 snex 4111 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 {{{d}}} V
179178, 59opksnelsik 4265 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 (⟪{{{{d}}}}, {{{c}}}⟫ SIk SIk SIk Sk ↔ ⟪{{{d}}}, {{c}}⟫ SIk SIk Sk )
180 snex 4111 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 {{d}} V
181180, 62opksnelsik 4265 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 (⟪{{{d}}}, {{c}}⟫ SIk SIk Sk ↔ ⟪{{d}}, {c}⟫ SIk Sk )
182 snex 4111 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 {d} V
183182, 65opksnelsik 4265 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 (⟪{{d}}, {c}⟫ SIk Sk ↔ ⟪{d}, c Sk )
184 vex 2862 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 d V
185184, 65elssetk 4270 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 (⟪{d}, c Skd c)
186181, 183, 1853bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 (⟪{{{d}}}, {{c}}⟫ SIk SIk Skd c)
187177, 179, 1863bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 (⟪{{{{{d}}}}}, {{{{c}}}}⟫ SIk SIk SIk SIk Skd c)
188173, 175, 1873bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 (⟪{{{{{{{{d}}}}}}}}, ⟪{{{{{c}}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫ Ins3k SIk SIk SIk SIk SIk Skd c)
189169, 171, 1883bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (⟪{{{{{{{{{{{{d}}}}}}}}}}}}, ⟪{{{{{{{{{a}}}}}}}}}, ⟪{{{{{{{b}}}}}}}, ⟪{{{{{c}}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫⟫⟫ Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Skd c)
190168, 109, 99otkelins3k 4256 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 (⟪{{{{{{{{{{{{d}}}}}}}}}}}}, ⟪{{{{{{{{{a}}}}}}}}}, ⟪{{{{{{{b}}}}}}}, ⟪{{{{{c}}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫⟫⟫ Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk Sk ↔ ⟪{{{{{{{{{{d}}}}}}}}}}, {{{{{{{{{a}}}}}}}}}⟫ SIk SIk SIk SIk SIk SIk SIk SIk SIk Sk )
191 snex 4111 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 {{{{{{{{{d}}}}}}}}} V
192 snex 4111 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 {{{{{{{{a}}}}}}}} V
193191, 192opksnelsik 4265 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 (⟪{{{{{{{{{{d}}}}}}}}}}, {{{{{{{{{a}}}}}}}}}⟫ SIk SIk SIk SIk SIk SIk SIk SIk SIk Sk ↔ ⟪{{{{{{{{{d}}}}}}}}}, {{{{{{{{a}}}}}}}}⟫ SIk SIk SIk SIk SIk SIk SIk SIk Sk )
194170, 114opksnelsik 4265 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 (⟪{{{{{{{{{d}}}}}}}}}, {{{{{{{{a}}}}}}}}⟫ SIk SIk SIk SIk SIk SIk SIk SIk Sk ↔ ⟪{{{{{{{{d}}}}}}}}, {{{{{{{a}}}}}}}⟫ SIk SIk SIk SIk SIk SIk SIk Sk )
195 snex 4111 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 {{{{{{{d}}}}}}} V
196195, 130opksnelsik 4265 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 (⟪{{{{{{{{d}}}}}}}}, {{{{{{{a}}}}}}}⟫ SIk SIk SIk SIk SIk SIk SIk Sk ↔ ⟪{{{{{{{d}}}}}}}, {{{{{{a}}}}}}⟫ SIk SIk SIk SIk SIk SIk Sk )
197172, 116opksnelsik 4265 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 (⟪{{{{{{{d}}}}}}}, {{{{{{a}}}}}}⟫ SIk SIk SIk SIk SIk SIk Sk ↔ ⟪{{{{{{d}}}}}}, {{{{{a}}}}}⟫ SIk SIk SIk SIk SIk Sk )
198174, 134opksnelsik 4265 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 (⟪{{{{{{d}}}}}}, {{{{{a}}}}}⟫ SIk SIk SIk SIk SIk Sk ↔ ⟪{{{{{d}}}}}, {{{{a}}}}⟫ SIk SIk SIk SIk Sk )
199176, 118opksnelsik 4265 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 (⟪{{{{{d}}}}}, {{{{a}}}}⟫ SIk SIk SIk SIk Sk ↔ ⟪{{{{d}}}}, {{{a}}}⟫ SIk SIk SIk Sk )
200178, 138opksnelsik 4265 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 (⟪{{{{d}}}}, {{{a}}}⟫ SIk SIk SIk Sk ↔ ⟪{{{d}}}, {{a}}⟫ SIk SIk Sk )
201180, 120opksnelsik 4265 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 (⟪{{{d}}}, {{a}}⟫ SIk SIk Sk ↔ ⟪{{d}}, {a}⟫ SIk Sk )
202182, 124opksnelsik 4265 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 (⟪{{d}}, {a}⟫ SIk Sk ↔ ⟪{d}, a Sk )
203184, 124elssetk 4270 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 (⟪{d}, a Skd a)
204201, 202, 2033bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 (⟪{{{d}}}, {{a}}⟫ SIk SIk Skd a)
205199, 200, 2043bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 (⟪{{{{{d}}}}}, {{{{a}}}}⟫ SIk SIk SIk SIk Skd a)
206197, 198, 2053bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 (⟪{{{{{{{d}}}}}}}, {{{{{{a}}}}}}⟫ SIk SIk SIk SIk SIk SIk Skd a)
207194, 196, 2063bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 (⟪{{{{{{{{{d}}}}}}}}}, {{{{{{{{a}}}}}}}}⟫ SIk SIk SIk SIk SIk SIk SIk SIk Skd a)
208190, 193, 2073bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 (⟪{{{{{{{{{{{{d}}}}}}}}}}}}, ⟪{{{{{{{{{a}}}}}}}}}, ⟪{{{{{{{b}}}}}}}, ⟪{{{{{c}}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫⟫⟫ Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk Skd a)
209168, 109, 99otkelins2k 4255 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 (⟪{{{{{{{{{{{{d}}}}}}}}}}}}, ⟪{{{{{{{{{a}}}}}}}}}, ⟪{{{{{{{b}}}}}}}, ⟪{{{{{c}}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫⟫⟫ Ins2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk ↔ ⟪{{{{{{{{{{d}}}}}}}}}}, ⟪{{{{{{{b}}}}}}}, ⟪{{{{{c}}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫⟫ Ins3k SIk SIk SIk SIk SIk SIk SIk Sk )
210170, 80, 70otkelins3k 4256 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 (⟪{{{{{{{{{{d}}}}}}}}}}, ⟪{{{{{{{b}}}}}}}, ⟪{{{{{c}}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫⟫ Ins3k SIk SIk SIk SIk SIk SIk SIk Sk ↔ ⟪{{{{{{{{d}}}}}}}}, {{{{{{{b}}}}}}}⟫ SIk SIk SIk SIk SIk SIk SIk Sk )
211195, 131opksnelsik 4265 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 (⟪{{{{{{{{d}}}}}}}}, {{{{{{{b}}}}}}}⟫ SIk SIk SIk SIk SIk SIk SIk Sk ↔ ⟪{{{{{{{d}}}}}}}, {{{{{{b}}}}}}⟫ SIk SIk SIk SIk SIk SIk Sk )
212172, 85opksnelsik 4265 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 (⟪{{{{{{{d}}}}}}}, {{{{{{b}}}}}}⟫ SIk SIk SIk SIk SIk SIk Sk ↔ ⟪{{{{{{d}}}}}}, {{{{{b}}}}}⟫ SIk SIk SIk SIk SIk Sk )
213174, 135opksnelsik 4265 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 (⟪{{{{{{d}}}}}}, {{{{{b}}}}}⟫ SIk SIk SIk SIk SIk Sk ↔ ⟪{{{{{d}}}}}, {{{{b}}}}⟫ SIk SIk SIk SIk Sk )
214176, 87opksnelsik 4265 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 (⟪{{{{{d}}}}}, {{{{b}}}}⟫ SIk SIk SIk SIk Sk ↔ ⟪{{{{d}}}}, {{{b}}}⟫ SIk SIk SIk Sk )
215178, 89opksnelsik 4265 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 (⟪{{{{d}}}}, {{{b}}}⟫ SIk SIk SIk Sk ↔ ⟪{{{d}}}, {{b}}⟫ SIk SIk Sk )
216180, 92opksnelsik 4265 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 (⟪{{{d}}}, {{b}}⟫ SIk SIk Sk ↔ ⟪{{d}}, {b}⟫ SIk Sk )
217182, 95opksnelsik 4265 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 (⟪{{d}}, {b}⟫ SIk Sk ↔ ⟪{d}, b Sk )
218184, 95elssetk 4270 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 (⟪{d}, b Skd b)
219217, 218bitri 240 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 (⟪{{d}}, {b}⟫ SIk Skd b)
220215, 216, 2193bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 (⟪{{{{d}}}}, {{{b}}}⟫ SIk SIk SIk Skd b)
221213, 214, 2203bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 (⟪{{{{{{d}}}}}}, {{{{{b}}}}}⟫ SIk SIk SIk SIk SIk Skd b)
222211, 212, 2213bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 (⟪{{{{{{{{d}}}}}}}}, {{{{{{{b}}}}}}}⟫ SIk SIk SIk SIk SIk SIk SIk Skd b)
223209, 210, 2223bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 (⟪{{{{{{{{{{{{d}}}}}}}}}}}}, ⟪{{{{{{{{{a}}}}}}}}}, ⟪{{{{{{{b}}}}}}}, ⟪{{{{{c}}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫⟫⟫ Ins2k Ins3k SIk SIk SIk SIk SIk SIk SIk Skd b)
224208, 223orbi12i 507 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ((⟪{{{{{{{{{{{{d}}}}}}}}}}}}, ⟪{{{{{{{{{a}}}}}}}}}, ⟪{{{{{{{b}}}}}}}, ⟪{{{{{c}}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫⟫⟫ Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk Sk ⟪{{{{{{{{{{{{d}}}}}}}}}}}}, ⟪{{{{{{{{{a}}}}}}}}}, ⟪{{{{{{{b}}}}}}}, ⟪{{{{{c}}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫⟫⟫ Ins2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk ) ↔ (d a d b))
225 elun 3220 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 (⟪{{{{{{{{{{{{d}}}}}}}}}}}}, ⟪{{{{{{{{{a}}}}}}}}}, ⟪{{{{{{{b}}}}}}}, ⟪{{{{{c}}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫⟫⟫ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk ) ↔ (⟪{{{{{{{{{{{{d}}}}}}}}}}}}, ⟪{{{{{{{{{a}}}}}}}}}, ⟪{{{{{{{b}}}}}}}, ⟪{{{{{c}}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫⟫⟫ Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk Sk ⟪{{{{{{{{{{{{d}}}}}}}}}}}}, ⟪{{{{{{{{{a}}}}}}}}}, ⟪{{{{{{{b}}}}}}}, ⟪{{{{{c}}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫⟫⟫ Ins2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk ))
226 elun 3220 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 (d (ab) ↔ (d a d b))
227224, 225, 2263bitr4i 268 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (⟪{{{{{{{{{{{{d}}}}}}}}}}}}, ⟪{{{{{{{{{a}}}}}}}}}, ⟪{{{{{{{b}}}}}}}, ⟪{{{{{c}}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫⟫⟫ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk ) ↔ d (ab))
228189, 227bibi12i 306 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ((⟪{{{{{{{{{{{{d}}}}}}}}}}}}, ⟪{{{{{{{{{a}}}}}}}}}, ⟪{{{{{{{b}}}}}}}, ⟪{{{{{c}}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫⟫⟫ Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ↔ ⟪{{{{{{{{{{{{d}}}}}}}}}}}}, ⟪{{{{{{{{{a}}}}}}}}}, ⟪{{{{{{{b}}}}}}}, ⟪{{{{{c}}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫⟫⟫ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk )) ↔ (d cd (ab)))
229228notbii 287 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (¬ (⟪{{{{{{{{{{{{d}}}}}}}}}}}}, ⟪{{{{{{{{{a}}}}}}}}}, ⟪{{{{{{{b}}}}}}}, ⟪{{{{{c}}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫⟫⟫ Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ↔ ⟪{{{{{{{{{{{{d}}}}}}}}}}}}, ⟪{{{{{{{{{a}}}}}}}}}, ⟪{{{{{{{b}}}}}}}, ⟪{{{{{c}}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫⟫⟫ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk )) ↔ ¬ (d cd (ab)))
230166, 167, 2293bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (t(t = {{{{{{{{{{{{d}}}}}}}}}}}} t, ⟪{{{{{{{{{a}}}}}}}}}, ⟪{{{{{{{b}}}}}}}, ⟪{{{{{c}}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫⟫⟫ ( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk ))) ↔ ¬ (d cd (ab)))
231230exbii 1582 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (dt(t = {{{{{{{{{{{{d}}}}}}}}}}}} t, ⟪{{{{{{{{{a}}}}}}}}}, ⟪{{{{{{{b}}}}}}}, ⟪{{{{{c}}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫⟫⟫ ( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk ))) ↔ d ¬ (d cd (ab)))
232154, 162, 2313bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (⟪{{{{{{{{{a}}}}}}}}}, ⟪{{{{{{{b}}}}}}}, ⟪{{{{{c}}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫⟫ (( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk )) “k 111111111111c) ↔ d ¬ (d cd (ab)))
233232notbii 287 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (¬ ⟪{{{{{{{{{a}}}}}}}}}, ⟪{{{{{{{b}}}}}}}, ⟪{{{{{c}}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫⟫ (( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk )) “k 111111111111c) ↔ ¬ d ¬ (d cd (ab)))
234153elcompl 3225 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (⟪{{{{{{{{{a}}}}}}}}}, ⟪{{{{{{{b}}}}}}}, ⟪{{{{{c}}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫⟫ ∼ (( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk )) “k 111111111111c) ↔ ¬ ⟪{{{{{{{{{a}}}}}}}}}, ⟪{{{{{{{b}}}}}}}, ⟪{{{{{c}}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫⟫ (( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk )) “k 111111111111c))
235 dfcleq 2347 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (c = (ab) ↔ d(d cd (ab)))
236 alex 1572 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (d(d cd (ab)) ↔ ¬ d ¬ (d cd (ab)))
237235, 236bitri 240 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (c = (ab) ↔ ¬ d ¬ (d cd (ab)))
238233, 234, 2373bitr4i 268 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (⟪{{{{{{{{{a}}}}}}}}}, ⟪{{{{{{{b}}}}}}}, ⟪{{{{{c}}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫⟫ ∼ (( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk )) “k 111111111111c) ↔ c = (ab))
239152, 238anbi12i 678 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((⟪{{{{{{{{{a}}}}}}}}}, ⟪{{{{{{{b}}}}}}}, ⟪{{{{{c}}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫⟫ Ins3k SIk SIk SIk SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ⟪{{{{{{{{{a}}}}}}}}}, ⟪{{{{{{{b}}}}}}}, ⟪{{{{{c}}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫⟫ ∼ (( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk )) “k 111111111111c)) ↔ ((ab) = c = (ab)))
240128, 239bitri 240 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (⟪{{{{{{{{{a}}}}}}}}}, ⟪{{{{{{{b}}}}}}}, ⟪{{{{{c}}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫⟫ ( Ins3k SIk SIk SIk SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk )) “k 111111111111c)) ↔ ((ab) = c = (ab)))
241127, 240anbi12i 678 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((⟪{{{{{{{{{a}}}}}}}}}, ⟪{{{{{{{b}}}}}}}, ⟪{{{{{c}}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫⟫ Ins2k Ins2k Ins2k Ins3k Sk ⟪{{{{{{{{{a}}}}}}}}}, ⟪{{{{{{{b}}}}}}}, ⟪{{{{{c}}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫⟫ ( Ins3k SIk SIk SIk SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk )) “k 111111111111c))) ↔ (a y ((ab) = c = (ab))))
242112, 113, 2413bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (t(t = {{{{{{{{{a}}}}}}}}} t, ⟪{{{{{{{b}}}}}}}, ⟪{{{{{c}}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫⟫ ( Ins2k Ins2k Ins2k Ins3k Sk ∩ ( Ins3k SIk SIk SIk SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk )) “k 111111111111c)))) ↔ (a y ((ab) = c = (ab))))
243242exbii 1582 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (at(t = {{{{{{{{{a}}}}}}}}} t, ⟪{{{{{{{b}}}}}}}, ⟪{{{{{c}}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫⟫ ( Ins2k Ins2k Ins2k Ins3k Sk ∩ ( Ins3k SIk SIk SIk SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk )) “k 111111111111c)))) ↔ a(a y ((ab) = c = (ab))))
244100, 108, 2433bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (⟪{{{{{{{b}}}}}}}, ⟪{{{{{c}}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫ (( Ins2k Ins2k Ins2k Ins3k Sk ∩ ( Ins3k SIk SIk SIk SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk )) “k 111111111111c))) “k 111111111c) ↔ a(a y ((ab) = c = (ab))))
245 df-rex 2620 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (a y ((ab) = c = (ab)) ↔ a(a y ((ab) = c = (ab))))
246244, 245bitr4i 243 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (⟪{{{{{{{b}}}}}}}, ⟪{{{{{c}}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫ (( Ins2k Ins2k Ins2k Ins3k Sk ∩ ( Ins3k SIk SIk SIk SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk )) “k 111111111111c))) “k 111111111c) ↔ a y ((ab) = c = (ab)))
24798, 246anbi12i 678 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((⟪{{{{{{{b}}}}}}}, ⟪{{{{{c}}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫ Ins2k Ins3k SIk SIk Sk ⟪{{{{{{{b}}}}}}}, ⟪{{{{{c}}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫ (( Ins2k Ins2k Ins2k Ins3k Sk ∩ ( Ins3k SIk SIk SIk SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk )) “k 111111111111c))) “k 111111111c)) ↔ (b w a y ((ab) = c = (ab))))
24883, 84, 2473bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (t(t = {{{{{{{b}}}}}}} t, ⟪{{{{{c}}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫ ( Ins2k Ins3k SIk SIk Sk ∩ (( Ins2k Ins2k Ins2k Ins3k Sk ∩ ( Ins3k SIk SIk SIk SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk )) “k 111111111111c))) “k 111111111c))) ↔ (b w a y ((ab) = c = (ab))))
249248exbii 1582 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (bt(t = {{{{{{{b}}}}}}} t, ⟪{{{{{c}}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫ ( Ins2k Ins3k SIk SIk Sk ∩ (( Ins2k Ins2k Ins2k Ins3k Sk ∩ ( Ins3k SIk SIk SIk SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk )) “k 111111111111c))) “k 111111111c))) ↔ b(b w a y ((ab) = c = (ab))))
25071, 79, 2493bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (⟪{{{{{c}}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫ (( Ins2k Ins3k SIk SIk Sk ∩ (( Ins2k Ins2k Ins2k Ins3k Sk ∩ ( Ins3k SIk SIk SIk SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk )) “k 111111111111c))) “k 111111111c)) “k 1111111c) ↔ b(b w a y ((ab) = c = (ab))))
25151, 31, 21otkelins2k 4255 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (⟪{{{{{{{c}}}}}}}, ⟪{{{{x}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫ Ins2k (( Ins2k Ins3k SIk SIk Sk ∩ (( Ins2k Ins2k Ins2k Ins3k Sk ∩ ( Ins3k SIk SIk SIk SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk )) “k 111111111111c))) “k 111111111c)) “k 1111111c) ↔ ⟪{{{{{c}}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫ (( Ins2k Ins3k SIk SIk Sk ∩ (( Ins2k Ins2k Ins2k Ins3k Sk ∩ ( Ins3k SIk SIk SIk SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk )) “k 111111111111c))) “k 111111111c)) “k 1111111c))
252 rexcom 2772 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (a y b w ((ab) = c = (ab)) ↔ b w a y ((ab) = c = (ab)))
253 df-rex 2620 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (b w a y ((ab) = c = (ab)) ↔ b(b w a y ((ab) = c = (ab))))
254252, 253bitri 240 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (a y b w ((ab) = c = (ab)) ↔ b(b w a y ((ab) = c = (ab))))
255250, 251, 2543bitr4i 268 . . . . . . . . . . . . . . . . . . . . . . . . 25 (⟪{{{{{{{c}}}}}}}, ⟪{{{{x}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫ Ins2k (( Ins2k Ins3k SIk SIk Sk ∩ (( Ins2k Ins2k Ins2k Ins3k Sk ∩ ( Ins3k SIk SIk SIk SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk )) “k 111111111111c))) “k 111111111c)) “k 1111111c) ↔ a y b w ((ab) = c = (ab)))
25669, 255bibi12i 306 . . . . . . . . . . . . . . . . . . . . . . . 24 ((⟪{{{{{{{c}}}}}}}, ⟪{{{{x}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫ Ins3k SIk SIk SIk SIk Sk ↔ ⟪{{{{{{{c}}}}}}}, ⟪{{{{x}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫ Ins2k (( Ins2k Ins3k SIk SIk Sk ∩ (( Ins2k Ins2k Ins2k Ins3k Sk ∩ ( Ins3k SIk SIk SIk SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk )) “k 111111111111c))) “k 111111111c)) “k 1111111c)) ↔ (c xa y b w ((ab) = c = (ab))))
257256notbii 287 . . . . . . . . . . . . . . . . . . . . . . 23 (¬ (⟪{{{{{{{c}}}}}}}, ⟪{{{{x}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫ Ins3k SIk SIk SIk SIk Sk ↔ ⟪{{{{{{{c}}}}}}}, ⟪{{{{x}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫ Ins2k (( Ins2k Ins3k SIk SIk Sk ∩ (( Ins2k Ins2k Ins2k Ins3k Sk ∩ ( Ins3k SIk SIk SIk SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk )) “k 111111111111c))) “k 111111111c)) “k 1111111c)) ↔ ¬ (c xa y b w ((ab) = c = (ab))))
25849, 50, 2573bitri 262 . . . . . . . . . . . . . . . . . . . . . 22 (t(t = {{{{{{{c}}}}}}} t, ⟪{{{{x}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫ ( Ins3k SIk SIk SIk SIk SkIns2k (( Ins2k Ins3k SIk SIk Sk ∩ (( Ins2k Ins2k Ins2k Ins3k Sk ∩ ( Ins3k SIk SIk SIk SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk )) “k 111111111111c))) “k 111111111c)) “k 1111111c))) ↔ ¬ (c xa y b w ((ab) = c = (ab))))
259258exbii 1582 . . . . . . . . . . . . . . . . . . . . 21 (ct(t = {{{{{{{c}}}}}}} t, ⟪{{{{x}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫ ( Ins3k SIk SIk SIk SIk SkIns2k (( Ins2k Ins3k SIk SIk Sk ∩ (( Ins2k Ins2k Ins2k Ins3k Sk ∩ ( Ins3k SIk SIk SIk SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk )) “k 111111111111c))) “k 111111111c)) “k 1111111c))) ↔ c ¬ (c xa y b w ((ab) = c = (ab))))
26037, 45, 2593bitri 262 . . . . . . . . . . . . . . . . . . . 20 (⟪{{{{x}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫ (( Ins3k SIk SIk SIk SIk SkIns2k (( Ins2k Ins3k SIk SIk Sk ∩ (( Ins2k Ins2k Ins2k Ins3k Sk ∩ ( Ins3k SIk SIk SIk SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk )) “k 111111111111c))) “k 111111111c)) “k 1111111c)) “k 1111111c) ↔ c ¬ (c xa y b w ((ab) =