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) = c = (ab))))
261260notbii 287 . . . . . . . . . . . . . . . . . . 19 (¬ ⟪{{{{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) = c = (ab))))
26236elcompl 3225 . . . . . . . . . . . . . . . . . . 19 (⟪{{{{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⟫⟫⟫ (( 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))
263 df-addc 4378 . . . . . . . . . . . . . . . . . . . . 21 (y +c w) = {c a y b w ((ab) = c = (ab))}
264263eqeq2i 2363 . . . . . . . . . . . . . . . . . . . 20 (x = (y +c w) ↔ x = {c a y b w ((ab) = c = (ab))})
265 abeq2 2458 . . . . . . . . . . . . . . . . . . . 20 (x = {c a y b w ((ab) = c = (ab))} ↔ c(c xa y b w ((ab) = c = (ab))))
266 alex 1572 . . . . . . . . . . . . . . . . . . . 20 (c(c xa y b w ((ab) = c = (ab))) ↔ ¬ c ¬ (c xa y b w ((ab) = c = (ab))))
267264, 265, 2663bitri 262 . . . . . . . . . . . . . . . . . . 19 (x = (y +c w) ↔ ¬ c ¬ (c xa y b w ((ab) = c = (ab))))
268261, 262, 2673bitr4i 268 . . . . . . . . . . . . . . . . . 18 (⟪{{{{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 = (y +c w))
26957, 17, 7otkelins2k 4255 . . . . . . . . . . . . . . . . . . 19 (⟪{{{{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) ↔ ⟪{{x}}, ⟪y, z⟫⟫ Ins2k Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c))
27063, 121, 122otkelins2k 4255 . . . . . . . . . . . . . . . . . . 19 (⟪{{x}}, ⟪y, z⟫⟫ Ins2k Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ↔ ⟪x, z Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c))
27163, 122opkelimagek 4272 . . . . . . . . . . . . . . . . . . . 20 (⟪x, z Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ↔ z = ((( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) “k x))
272 dfaddc2 4381 . . . . . . . . . . . . . . . . . . . . 21 (x +c 1c) = ((( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) “k x)
273272eqeq2i 2363 . . . . . . . . . . . . . . . . . . . 20 (z = (x +c 1c) ↔ z = ((( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) “k x))
274271, 273bitr4i 243 . . . . . . . . . . . . . . . . . . 19 (⟪x, z Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ↔ z = (x +c 1c))
275269, 270, 2743bitri 262 . . . . . . . . . . . . . . . . . 18 (⟪{{{{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) ↔ z = (x +c 1c))
276268, 275anbi12i 678 . . . . . . . . . . . . . . . . 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) ⟪{{{{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)) ↔ (x = (y +c w) z = (x +c 1c)))
27734, 35, 2763bitri 262 . . . . . . . . . . . . . . . 16 (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 = (y +c w) z = (x +c 1c)))
278277exbii 1582 . . . . . . . . . . . . . . 15 (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))) ↔ x(x = (y +c w) z = (x +c 1c)))
27922, 30, 2783bitri 262 . . . . . . . . . . . . . 14 (⟪{{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) ↔ x(x = (y +c w) z = (x +c 1c)))
280121, 93addcex 4394 . . . . . . . . . . . . . . 15 (y +c w) V
281 addceq1 4383 . . . . . . . . . . . . . . . 16 (x = (y +c w) → (x +c 1c) = ((y +c w) +c 1c))
282281eqeq2d 2364 . . . . . . . . . . . . . . 15 (x = (y +c w) → (z = (x +c 1c) ↔ z = ((y +c w) +c 1c)))
283280, 282ceqsexv 2894 . . . . . . . . . . . . . 14 (x(x = (y +c w) z = (x +c 1c)) ↔ z = ((y +c w) +c 1c))
28420, 279, 2833bitri 262 . . . . . . . . . . . . 13 (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)) ↔ z = ((y +c w) +c 1c))
285284rexbii 2639 . . . . . . . . . . . 12 (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)) ↔ w Nn z = ((y +c w) +c 1c))
2868, 16, 2853bitri 262 . . . . . . . . . . 11 (⟪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 ) ↔ w Nn z = ((y +c w) +c 1c))
287121, 122opkelxpk 4248 . . . . . . . . . . . . . 14 (⟪y, z ({} ×k V) ↔ (y {} z V))
288122, 287mpbiran2 885 . . . . . . . . . . . . 13 (⟪y, z ({} ×k V) ↔ y {})
289121elsnc 3756 . . . . . . . . . . . . 13 (y {} ↔ y = )
290288, 289bitri 240 . . . . . . . . . . . 12 (⟪y, z ({} ×k V) ↔ y = )
291290notbii 287 . . . . . . . . . . 11 (¬ ⟪y, z ({} ×k V) ↔ ¬ y = )
292286, 291anbi12i 678 . . . . . . . . . 10 ((⟪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 ) ¬ ⟪y, z ({} ×k V)) ↔ (w Nn z = ((y +c w) +c 1c) ¬ y = ))
293 eldif 3221 . . . . . . . . . 10 (⟪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)) ↔ (⟪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 ) ¬ ⟪y, z ({} ×k V)))
294 ancom 437 . . . . . . . . . . 11 ((y w Nn z = ((y +c w) +c 1c)) ↔ (w Nn z = ((y +c w) +c 1c) y))
295 df-ne 2518 . . . . . . . . . . . 12 (y ↔ ¬ y = )
296295anbi2i 675 . . . . . . . . . . 11 ((w Nn z = ((y +c w) +c 1c) y) ↔ (w Nn z = ((y +c w) +c 1c) ¬ y = ))
297294, 296bitri 240 . . . . . . . . . 10 ((y w Nn z = ((y +c w) +c 1c)) ↔ (w Nn z = ((y +c w) +c 1c) ¬ y = ))
298292, 293, 2973bitr4i 268 . . . . . . . . 9 (⟪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)) ↔ (y w Nn z = ((y +c w) +c 1c)))
2996, 298syl6bb 252 . . . . . . . 8 (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 w Nn z = ((y +c w) +c 1c))))
300299pm5.32i 618 . . . . . . 7 ((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))) ↔ (x = ⟪y, z (y w Nn z = ((y +c w) +c 1c))))
3013002exbii 1583 . . . . . 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 (y w Nn z = ((y +c w) +c 1c))))
3025, 301bitr3i 242 . . . . 5 ((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 (y w Nn z = ((y +c w) +c 1c))))
3032, 4, 3023bitri 262 . . . 4 (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))) ↔ yz(x = ⟪y, z (y w Nn z = ((y +c w) +c 1c))))
304303abbi2i 2464 . . 3 ((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 yz(x = ⟪y, z (y w Nn z = ((y +c w) +c 1c)))}
3051, 304eqtr4i 2376 . 2 <fin = ((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)))
306 vvex 4109 . . . 4 V V
307306, 306xpkex 4289 . . 3 (V ×k V) V
308 ssetkex 4294 . . . . . . . . . . . . . . 15 Sk V
309308sikex 4297 . . . . . . . . . . . . . 14 SIk Sk V
310309sikex 4297 . . . . . . . . . . . . 13 SIk SIk Sk V
311310sikex 4297 . . . . . . . . . . . 12 SIk SIk SIk Sk V
312311sikex 4297 . . . . . . . . . . 11 SIk SIk SIk SIk Sk V
313312ins3kex 4308 . . . . . . . . . 10 Ins3k SIk SIk SIk SIk Sk V
314310ins3kex 4308 . . . . . . . . . . . . . 14 Ins3k SIk SIk Sk V
315314ins2kex 4307 . . . . . . . . . . . . 13 Ins2k Ins3k SIk SIk Sk V
316308ins3kex 4308 . . . . . . . . . . . . . . . . . 18 Ins3k Sk V
317316ins2kex 4307 . . . . . . . . . . . . . . . . 17 Ins2k Ins3k Sk V
318317ins2kex 4307 . . . . . . . . . . . . . . . 16 Ins2k Ins2k Ins3k Sk V
319318ins2kex 4307 . . . . . . . . . . . . . . 15 Ins2k Ins2k Ins2k Ins3k Sk V
320308ins2kex 4307 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 Ins2k Sk V
321316, 320inex 4105 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ( Ins3k SkIns2k Sk ) V
322 1cex 4142 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 1c V
323322pw1ex 4303 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 11c V
324323pw1ex 4303 . . . . . . . . . . . . . . . . . . . . . . . . . 26 111c V
325321, 324imakex 4300 . . . . . . . . . . . . . . . . . . . . . . . . 25 (( Ins3k SkIns2k Sk ) “k 111c) V
326325complex 4104 . . . . . . . . . . . . . . . . . . . . . . . 24 ∼ (( Ins3k SkIns2k Sk ) “k 111c) V
327326sikex 4297 . . . . . . . . . . . . . . . . . . . . . . 23 SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) V
328327sikex 4297 . . . . . . . . . . . . . . . . . . . . . 22 SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) V
329328sikex 4297 . . . . . . . . . . . . . . . . . . . . 21 SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) V
330329sikex 4297 . . . . . . . . . . . . . . . . . . . 20 SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) V
331330sikex 4297 . . . . . . . . . . . . . . . . . . 19 SIk SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) V
332331sikex 4297 . . . . . . . . . . . . . . . . . 18 SIk SIk SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) V
333332sikex 4297 . . . . . . . . . . . . . . . . 17 SIk SIk SIk SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) V
334333ins3kex 4308 . . . . . . . . . . . . . . . 16 Ins3k SIk SIk SIk SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) V
335312sikex 4297 . . . . . . . . . . . . . . . . . . . . . 22 SIk SIk SIk SIk SIk Sk V
336335ins3kex 4308 . . . . . . . . . . . . . . . . . . . . 21 Ins3k SIk SIk SIk SIk SIk Sk V
337336ins2kex 4307 . . . . . . . . . . . . . . . . . . . 20 Ins2k Ins3k SIk SIk SIk SIk SIk Sk V
338337ins2kex 4307 . . . . . . . . . . . . . . . . . . 19 Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk V
339335sikex 4297 . . . . . . . . . . . . . . . . . . . . . . . 24 SIk SIk SIk SIk SIk SIk Sk V
340339sikex 4297 . . . . . . . . . . . . . . . . . . . . . . 23 SIk SIk SIk SIk SIk SIk SIk Sk V
341340sikex 4297 . . . . . . . . . . . . . . . . . . . . . 22 SIk SIk SIk SIk SIk SIk SIk SIk Sk V
342341sikex 4297 . . . . . . . . . . . . . . . . . . . . 21 SIk SIk SIk SIk SIk SIk SIk SIk SIk Sk V
343342ins3kex 4308 . . . . . . . . . . . . . . . . . . . 20 Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk Sk V
344340ins3kex 4308 . . . . . . . . . . . . . . . . . . . . 21 Ins3k SIk SIk SIk SIk SIk SIk SIk Sk V
345344ins2kex 4307 . . . . . . . . . . . . . . . . . . . 20 Ins2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk V
346343, 345unex 4106 . . . . . . . . . . . . . . . . . . 19 ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk ) V
347338, 346symdifex 4108 . . . . . . . . . . . . . . . . . 18 ( 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 )) V
348324pw1ex 4303 . . . . . . . . . . . . . . . . . . . . . . . . . 26 1111c V
349348pw1ex 4303 . . . . . . . . . . . . . . . . . . . . . . . . 25 11111c V
350349pw1ex 4303 . . . . . . . . . . . . . . . . . . . . . . . 24 111111c V
351350pw1ex 4303 . . . . . . . . . . . . . . . . . . . . . . 23 1111111c V
352351pw1ex 4303 . . . . . . . . . . . . . . . . . . . . . 22 11111111c V
353352pw1ex 4303 . . . . . . . . . . . . . . . . . . . . 21 111111111c V
354353pw1ex 4303 . . . . . . . . . . . . . . . . . . . 20 1111111111c V
355354pw1ex 4303 . . . . . . . . . . . . . . . . . . 19 11111111111c V
356355pw1ex 4303 . . . . . . . . . . . . . . . . . 18 111111111111c V
357347, 356imakex 4300 . . . . . . . . . . . . . . . . 17 (( 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) V
358357complex 4104 . . . . . . . . . . . . . . . 16 ∼ (( 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) V
359334, 358inex 4105 . . . . . . . . . . . . . . 15 ( 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)) V
360319, 359inex 4105 . . . . . . . . . . . . . 14 ( 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))) V
361360, 353imakex 4300 . . . . . . . . . . . . 13 (( 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) V
362315, 361inex 4105 . . . . . . . . . . . 12 ( 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)) V
363362, 351imakex 4300 . . . . . . . . . . 11 (( 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) V
364363ins2kex 4307 . . . . . . . . . 10 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) V
365313, 364symdifex 4108 . . . . . . . . 9 ( 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)) V
366365, 351imakex 4300 . . . . . . . 8 (( 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) V
367366complex 4104 . . . . . . 7 ∼ (( 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) V
368 addcexlem 4382 . . . . . . . . . . 11 ( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) V
369368, 324imakex 4300 . . . . . . . . . 10 (( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) V
370369imagekex 4312 . . . . . . . . 9 Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) V
371370ins2kex 4307 . . . . . . . 8 Ins2k Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) V
372371ins2kex 4307 . . . . . . 7 Ins2k Ins2k Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) V
373367, 372inex 4105 . . . . . 6 ( ∼ (( 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)) V
374373, 348imakex 4300 . . . . 5 (( ∼ (( 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) V
375 nncex 4396 . . . . . . 7 Nn V
376375pw1ex 4303 . . . . . 6 1 Nn V
377376pw1ex 4303 . . . . 5 11 Nn V
378374, 377imakex 4300 . . . 4 ((( ∼ (( 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 ) V
379 snex 4111 . . . . 5 {} V
380379, 306xpkex 4289 . . . 4 ({} ×k V) V
381378, 380difex 4107 . . 3 (((( ∼ (( 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)) V
382307, 381inex 4105 . 2 ((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))) V
383305, 382eqeltri 2423 1 <fin V
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 176   wo 357   wa 358  wal 1540  wex 1541   = wceq 1642   wcel 1710  {cab 2339  wne 2516  wrex 2615  Vcvv 2859  ccompl 3205   cdif 3206  cun 3207  cin 3208  csymdif 3209  c0 3550  {csn 3737  copk 4057  1cc1c 4134  1cpw1 4135   ×k cxpk 4174   Ins2k cins2k 4176   Ins3k cins3k 4177  k cimak 4179   SIk csik 4181  Imagekcimagek 4182   Sk cssetk 4183   Nn cnnc 4373   +c cplc 4375   <fin cltfin 4433
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-ext 2334  ax-nin 4078  ax-xp 4079  ax-cnv 4080  ax-1c 4081  ax-sset 4082  ax-si 4083  ax-ins2 4084  ax-ins3 4085  ax-typlower 4086  ax-sn 4087
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-nan 1288  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2340  df-cleq 2346  df-clel 2349  df-nfc 2478  df-ne 2518  df-ral 2619  df-rex 2620  df-v 2861  df-sbc 3047  df-nin 3211  df-compl 3212  df-in 3213  df-un 3214  df-dif 3215  df-symdif 3216  df-ss 3259  df-nul 3551  df-if 3663  df-pw 3724  df-sn 3741  df-pr 3742  df-uni 3892  df-int 3927  df-opk 4058  df-1c 4136  df-pw1 4137  df-uni1 4138  df-xpk 4185  df-cnvk 4186  df-ins2k 4187  df-ins3k 4188  df-imak 4189  df-cok 4190  df-p6 4191  df-sik 4192  df-ssetk 4193  df-imagek 4194  df-addc 4378  df-nnc 4379  df-ltfin 4441
This theorem is referenced by:  ltfintrilem1  4465
  Copyright terms: Public domain W3C validator