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

Theorem ltfinex 4465
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 4442 . . 3 <fin = {x yz(x = ⟪y, z (y w Nn z = ((y +c w) +c 1c)))}
2 elin 3220 . . . . 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 4208 . . . . . 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 4114 . . . . . . . . . . . . 13 y, z V
87elimak 4260 . . . . . . . . . . . 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 4146 . . . . . . . . . . . . . . . 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 2765 . . . . . . . . . . . . . . 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 2621 . . . . . . . . . . . . 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 2879 . . . . . . . . . . . . 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 4112 . . . . . . . . . . . . . . 15 {{w}} V
18 opkeq1 4060 . . . . . . . . . . . . . . . 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 2895 . . . . . . . . . . . . . 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 4114 . . . . . . . . . . . . . . . 16 ⟪{{w}}, ⟪y, z⟫⟫ V
2221elimak 4260 . . . . . . . . . . . . . . 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 4150 . . . . . . . . . . . . . . . . . . 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 2621 . . . . . . . . . . . . . . . 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 4112 . . . . . . . . . . . . . . . . . 18 {{{{x}}}} V
32 opkeq1 4060 . . . . . . . . . . . . . . . . . . 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 2895 . . . . . . . . . . . . . . . . 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 3220 . . . . . . . . . . . . . . . . 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 4114 . . . . . . . . . . . . . . . . . . . . . 22 ⟪{{{{x}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫ V
3736elimak 4260 . . . . . . . . . . . . . . . . . . . . 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 4153 . . . . . . . . . . . . . . . . . . . . . . . . 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 2621 . . . . . . . . . . . . . . . . . . . . . 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 4112 . . . . . . . . . . . . . . . . . . . . . . . 24 {{{{{{{c}}}}}}} V
47 opkeq1 4060 . . . . . . . . . . . . . . . . . . . . . . . . 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 2895 . . . . . . . . . . . . . . . . . . . . . . 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 3224 . . . . . . . . . . . . . . . . . . . . . . 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 4112 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 {{{{{c}}}}} V
5251, 31, 21otkelins3k 4257 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (⟪{{{{{{{c}}}}}}}, ⟪{{{{x}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫ Ins3k SIk SIk SIk SIk Sk ↔ ⟪{{{{{c}}}}}, {{{{x}}}}⟫ SIk SIk SIk SIk Sk )
53 snex 4112 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 {{{{c}}}} V
54 snex 4112 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 {{{x}}} V
5553, 54opksnelsik 4266 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (⟪{{{{{c}}}}}, {{{{x}}}}⟫ SIk SIk SIk SIk Sk ↔ ⟪{{{{c}}}}, {{{x}}}⟫ SIk SIk SIk Sk )
56 snex 4112 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 {{{c}}} V
57 snex 4112 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 {{x}} V
5856, 57opksnelsik 4266 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (⟪{{{{c}}}}, {{{x}}}⟫ SIk SIk SIk Sk ↔ ⟪{{{c}}}, {{x}}⟫ SIk SIk Sk )
59 snex 4112 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 {{c}} V
60 snex 4112 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 {x} V
6159, 60opksnelsik 4266 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (⟪{{{c}}}, {{x}}⟫ SIk SIk Sk ↔ ⟪{{c}}, {x}⟫ SIk Sk )
62 snex 4112 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 {c} V
63 vex 2863 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 x V
6462, 63opksnelsik 4266 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (⟪{{c}}, {x}⟫ SIk Sk ↔ ⟪{c}, x Sk )
65 vex 2863 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 c V
6665, 63elssetk 4271 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4114 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⟪{{{{{c}}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫ V
7170elimak 4260 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4153 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2621 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4112 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 {{{{{{{b}}}}}}} V
81 opkeq1 4060 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2895 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3220 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4112 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 {{{{{b}}}}} V
8685, 51, 21otkelins2k 4256 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (⟪{{{{{{{b}}}}}}}, ⟪{{{{{c}}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫ Ins2k Ins3k SIk SIk Sk ↔ ⟪{{{{{b}}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫ Ins3k SIk SIk Sk )
87 snex 4112 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 {{{b}}} V
8887, 17, 7otkelins3k 4257 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (⟪{{{{{b}}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫ Ins3k SIk SIk Sk ↔ ⟪{{{b}}}, {{w}}⟫ SIk SIk Sk )
89 snex 4112 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 {{b}} V
90 snex 4112 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 {w} V
9189, 90opksnelsik 4266 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (⟪{{{b}}}, {{w}}⟫ SIk SIk Sk ↔ ⟪{{b}}, {w}⟫ SIk Sk )
92 snex 4112 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 {b} V
93 vex 2863 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 w V
9492, 93opksnelsik 4266 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (⟪{{b}}, {w}⟫ SIk Sk ↔ ⟪{b}, w Sk )
95 vex 2863 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 b V
9695, 93elssetk 4271 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4114 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⟪{{{{{{{b}}}}}}}, ⟪{{{{{c}}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫ V
10099elimak 4260 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4155 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2621 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4112 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 {{{{{{{{{a}}}}}}}}} V
110 opkeq1 4060 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2895 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3220 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4112 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 {{{{{{{a}}}}}}} V
115114, 80, 70otkelins2k 4256 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (⟪{{{{{{{{{a}}}}}}}}}, ⟪{{{{{{{b}}}}}}}, ⟪{{{{{c}}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫⟫ Ins2k Ins2k Ins2k Ins3k Sk ↔ ⟪{{{{{{{a}}}}}}}, ⟪{{{{{c}}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫ Ins2k Ins2k Ins3k Sk )
116 snex 4112 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 {{{{{a}}}}} V
117116, 51, 21otkelins2k 4256 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (⟪{{{{{{{a}}}}}}}, ⟪{{{{{c}}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫ Ins2k Ins2k Ins3k Sk ↔ ⟪{{{{{a}}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫ Ins2k Ins3k Sk )
118 snex 4112 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 {{{a}}} V
119118, 17, 7otkelins2k 4256 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (⟪{{{{{a}}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫ Ins2k Ins3k Sk ↔ ⟪{{{a}}}, ⟪y, z⟫⟫ Ins3k Sk )
120 snex 4112 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 {a} V
121 vex 2863 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 y V
122 vex 2863 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 z V
123120, 121, 122otkelins3k 4257 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (⟪{{{a}}}, ⟪y, z⟫⟫ Ins3k Sk ↔ ⟪{a}, y Sk )
124 vex 2863 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 a V
125124, 121elssetk 4271 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3220 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4257 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4112 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 {{{{{{a}}}}}} V
131 snex 4112 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 {{{{{{b}}}}}} V
132130, 131opksnelsik 4266 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4266 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4112 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 {{{{a}}}} V
135 snex 4112 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 {{{{b}}}} V
136134, 135opksnelsik 4266 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4266 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (⟪{{{{a}}}}, {{{{b}}}}⟫ SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ↔ ⟪{{{a}}}, {{{b}}}⟫ SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c))
138 snex 4112 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 {{a}} V
139138, 89opksnelsik 4266 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (⟪{{{a}}}, {{{b}}}⟫ SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ↔ ⟪{{a}}, {{b}}⟫ SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c))
140120, 92opksnelsik 4266 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (⟪{{a}}, {{b}}⟫ SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ↔ ⟪{a}, {b}⟫ SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c))
141124, 95opksnelsik 4266 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (⟪{a}, {b}⟫ SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ↔ ⟪a, b ∼ (( Ins3k SkIns2k Sk ) “k 111c))
142124, 95ndisjrelk 4324 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (⟪a, b (( Ins3k SkIns2k Sk ) “k 111c) ↔ (ab) ≠ )
143142notbii 287 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (¬ ⟪a, b (( Ins3k SkIns2k Sk ) “k 111c) ↔ ¬ (ab) ≠ )
144 opkex 4114 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 a, b V
145144elcompl 3226 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (⟪a, b ∼ (( Ins3k SkIns2k Sk ) “k 111c) ↔ ¬ ⟪a, b (( Ins3k SkIns2k Sk ) “k 111c))
146 df-ne 2519 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4114 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⟪{{{{{{{{{a}}}}}}}}}, ⟪{{{{{{{b}}}}}}}, ⟪{{{{{c}}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫⟫ V
154153elimak 4260 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4158 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2621 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4112 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 {{{{{{{{{{{{d}}}}}}}}}}}} V
164 opkeq1 4060 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2895 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3224 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4112 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 {{{{{{{{{{d}}}}}}}}}} V
169168, 109, 99otkelins2k 4256 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4112 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 {{{{{{{{d}}}}}}}} V
171170, 80, 70otkelins2k 4256 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4112 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 {{{{{{d}}}}}} V
173172, 51, 21otkelins3k 4257 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 (⟪{{{{{{{{d}}}}}}}}, ⟪{{{{{c}}}}}, ⟪{{w}}, ⟪y, z⟫⟫⟫⟫ Ins3k SIk SIk SIk SIk SIk Sk ↔ ⟪{{{{{{d}}}}}}, {{{{{c}}}}}⟫ SIk SIk SIk SIk SIk Sk )
174 snex 4112 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 {{{{{d}}}}} V
175174, 53opksnelsik 4266 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 (⟪{{{{{{d}}}}}}, {{{{{c}}}}}⟫ SIk SIk SIk SIk SIk Sk ↔ ⟪{{{{{d}}}}}, {{{{c}}}}⟫ SIk SIk SIk SIk Sk )
176 snex 4112 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 {{{{d}}}} V
177176, 56opksnelsik 4266 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 (⟪{{{{{d}}}}}, {{{{c}}}}⟫ SIk SIk SIk SIk Sk ↔ ⟪{{{{d}}}}, {{{c}}}⟫ SIk SIk SIk Sk )
178 snex 4112 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 {{{d}}} V
179178, 59opksnelsik 4266 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 (⟪{{{{d}}}}, {{{c}}}⟫ SIk SIk SIk Sk ↔ ⟪{{{d}}}, {{c}}⟫ SIk SIk Sk )
180 snex 4112 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 {{d}} V
181180, 62opksnelsik 4266 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 (⟪{{{d}}}, {{c}}⟫ SIk SIk Sk ↔ ⟪{{d}}, {c}⟫ SIk Sk )
182 snex 4112 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 {d} V
183182, 65opksnelsik 4266 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 (⟪{{d}}, {c}⟫ SIk Sk ↔ ⟪{d}, c Sk )
184 vex 2863 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 d V
185184, 65elssetk 4271 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4257 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4112 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 {{{{{{{{{d}}}}}}}}} V
192 snex 4112 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 {{{{{{{{a}}}}}}}} V
193191, 192opksnelsik 4266 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4266 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 (⟪{{{{{{{{{d}}}}}}}}}, {{{{{{{{a}}}}}}}}⟫ SIk SIk SIk SIk SIk SIk SIk SIk Sk ↔ ⟪{{{{{{{{d}}}}}}}}, {{{{{{{a}}}}}}}⟫ SIk SIk SIk SIk SIk SIk SIk Sk )
195 snex 4112 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 {{{{{{{d}}}}}}} V
196195, 130opksnelsik 4266 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 (⟪{{{{{{{{d}}}}}}}}, {{{{{{{a}}}}}}}⟫ SIk SIk SIk SIk SIk SIk SIk Sk ↔ ⟪{{{{{{{d}}}}}}}, {{{{{{a}}}}}}⟫ SIk SIk SIk SIk SIk SIk Sk )
197172, 116opksnelsik 4266 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 (⟪{{{{{{{d}}}}}}}, {{{{{{a}}}}}}⟫ SIk SIk SIk SIk SIk SIk Sk ↔ ⟪{{{{{{d}}}}}}, {{{{{a}}}}}⟫ SIk SIk SIk SIk SIk Sk )
198174, 134opksnelsik 4266 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 (⟪{{{{{{d}}}}}}, {{{{{a}}}}}⟫ SIk SIk SIk SIk SIk Sk ↔ ⟪{{{{{d}}}}}, {{{{a}}}}⟫ SIk SIk SIk SIk Sk )
199176, 118opksnelsik 4266 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 (⟪{{{{{d}}}}}, {{{{a}}}}⟫ SIk SIk SIk SIk Sk ↔ ⟪{{{{d}}}}, {{{a}}}⟫ SIk SIk SIk Sk )
200178, 138opksnelsik 4266 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 (⟪{{{{d}}}}, {{{a}}}⟫ SIk SIk SIk Sk ↔ ⟪{{{d}}}, {{a}}⟫ SIk SIk Sk )
201180, 120opksnelsik 4266 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 (⟪{{{d}}}, {{a}}⟫ SIk SIk Sk ↔ ⟪{{d}}, {a}⟫ SIk Sk )
202182, 124opksnelsik 4266 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 (⟪{{d}}, {a}⟫ SIk Sk ↔ ⟪{d}, a Sk )
203184, 124elssetk 4271 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4256 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4257 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4266 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 (⟪{{{{{{{{d}}}}}}}}, {{{{{{{b}}}}}}}⟫ SIk SIk SIk SIk SIk SIk SIk Sk ↔ ⟪{{{{{{{d}}}}}}}, {{{{{{b}}}}}}⟫ SIk SIk SIk SIk SIk SIk Sk )
212172, 85opksnelsik 4266 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 (⟪{{{{{{{d}}}}}}}, {{{{{{b}}}}}}⟫ SIk SIk SIk SIk SIk SIk Sk ↔ ⟪{{{{{{d}}}}}}, {{{{{b}}}}}⟫ SIk SIk SIk SIk SIk Sk )
213174, 135opksnelsik 4266 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 (⟪{{{{{{d}}}}}}, {{{{{b}}}}}⟫ SIk SIk SIk SIk SIk Sk ↔ ⟪{{{{{d}}}}}, {{{{b}}}}⟫ SIk SIk SIk SIk Sk )
214176, 87opksnelsik 4266 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 (⟪{{{{{d}}}}}, {{{{b}}}}⟫ SIk SIk SIk SIk Sk ↔ ⟪{{{{d}}}}, {{{b}}}⟫ SIk SIk SIk Sk )
215178, 89opksnelsik 4266 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 (⟪{{{{d}}}}, {{{b}}}⟫ SIk SIk SIk Sk ↔ ⟪{{{d}}}, {{b}}⟫ SIk SIk Sk )
216180, 92opksnelsik 4266 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 (⟪{{{d}}}, {{b}}⟫ SIk SIk Sk ↔ ⟪{{d}}, {b}⟫ SIk Sk )
217182, 95opksnelsik 4266 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 (⟪{{d}}, {b}⟫ SIk Sk ↔ ⟪{d}, b Sk )
218184, 95elssetk 4271 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3221 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3221 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3226 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2621 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4256 . . . . . . . . . . . . . . . . . . . . . . . . . 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 2773 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (a y b w ((ab) = c = (ab)) ↔ b w a y ((ab) = c = (ab)))
253 df-rex 2621 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3226 . . . . . . . . . . . . . . . . . . 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 4379 . . . . . . . . . . . . . . . . . . . . 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 2459 . . . . . . . . . . . . . . . . . . . 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 4256 . . . . . . . . . . . . . . . . . . 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 4256 . . . . . . . . . . . . . . . . . . 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 4273 . . . . . . . . . . . . . . . . . . . 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 4382 . . . . . . . . . . . . . . . . . . . . 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 4395 . . . . . . . . . . . . . . 15 (y +c w) V
281 addceq1 4384 . . . . . . . . . . . . . . . 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 2895 . . . . . . . . . . . . . 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 2640 . . . . . . . . . . . 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 4249 . . . . . . . . . . . . . 14 (⟪y, z ({} ×k V) ↔ (y {} z V))
288122, 287mpbiran2 885 . . . . . . . . . . . . 13 (⟪y, z ({} ×k V) ↔ y {})
289121elsnc 3757 . . . . . . . . . . . . 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 3222 . . . . . . . . . 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 2519 . . . . . . . . . . . 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 2465 . . 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 4110 . . . 4 V V
307306, 306xpkex 4290 . . 3 (V ×k V) V
308 ssetkex 4295 . . . . . . . . . . . . . . 15 Sk V
309308sikex 4298 . . . . . . . . . . . . . 14 SIk Sk V
310309sikex 4298 . . . . . . . . . . . . 13 SIk SIk Sk V
311310sikex 4298 . . . . . . . . . . . 12 SIk SIk SIk Sk V
312311sikex 4298 . . . . . . . . . . 11 SIk SIk SIk SIk Sk V
313312ins3kex 4309 . . . . . . . . . 10 Ins3k SIk SIk SIk SIk Sk V
314310ins3kex 4309 . . . . . . . . . . . . . 14 Ins3k SIk SIk Sk V
315314ins2kex 4308 . . . . . . . . . . . . 13 Ins2k Ins3k SIk SIk Sk V
316308ins3kex 4309 . . . . . . . . . . . . . . . . . 18 Ins3k Sk V
317316ins2kex 4308 . . . . . . . . . . . . . . . . 17 Ins2k Ins3k Sk V
318317ins2kex 4308 . . . . . . . . . . . . . . . 16 Ins2k Ins2k Ins3k Sk V
319318ins2kex 4308 . . . . . . . . . . . . . . 15 Ins2k Ins2k Ins2k Ins3k Sk V
320308ins2kex 4308 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 Ins2k Sk V
321316, 320inex 4106 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ( Ins3k SkIns2k Sk ) V
322 1cex 4143 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 1c V
323322pw1ex 4304 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 11c V
324323pw1ex 4304 . . . . . . . . . . . . . . . . . . . . . . . . . 26 111c V
325321, 324imakex 4301 . . . . . . . . . . . . . . . . . . . . . . . . 25 (( Ins3k SkIns2k Sk ) “k 111c) V
326325complex 4105 . . . . . . . . . . . . . . . . . . . . . . . 24 ∼ (( Ins3k SkIns2k Sk ) “k 111c) V
327326sikex 4298 . . . . . . . . . . . . . . . . . . . . . . 23 SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) V
328327sikex 4298 . . . . . . . . . . . . . . . . . . . . . 22 SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) V
329328sikex 4298 . . . . . . . . . . . . . . . . . . . . 21 SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) V
330329sikex 4298 . . . . . . . . . . . . . . . . . . . 20 SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) V
331330sikex 4298 . . . . . . . . . . . . . . . . . . 19 SIk SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) V
332331sikex 4298 . . . . . . . . . . . . . . . . . 18 SIk SIk SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) V
333332sikex 4298 . . . . . . . . . . . . . . . . 17 SIk SIk SIk SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) V
334333ins3kex 4309 . . . . . . . . . . . . . . . 16 Ins3k SIk SIk SIk SIk SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) V
335312sikex 4298 . . . . . . . . . . . . . . . . . . . . . 22 SIk SIk SIk SIk SIk Sk V
336335ins3kex 4309 . . . . . . . . . . . . . . . . . . . . 21 Ins3k SIk SIk SIk SIk SIk Sk V
337336ins2kex 4308 . . . . . . . . . . . . . . . . . . . 20 Ins2k Ins3k SIk SIk SIk SIk SIk Sk V
338337ins2kex 4308 . . . . . . . . . . . . . . . . . . 19 Ins2k Ins2k Ins3k SIk SIk SIk SIk SIk Sk V
339335sikex 4298 . . . . . . . . . . . . . . . . . . . . . . . 24 SIk SIk SIk SIk SIk SIk Sk V
340339sikex 4298 . . . . . . . . . . . . . . . . . . . . . . 23 SIk SIk SIk SIk SIk SIk SIk Sk V
341340sikex 4298 . . . . . . . . . . . . . . . . . . . . . 22 SIk SIk SIk SIk SIk SIk SIk SIk Sk V
342341sikex 4298 . . . . . . . . . . . . . . . . . . . . 21 SIk SIk SIk SIk SIk SIk SIk SIk SIk Sk V
343342ins3kex 4309 . . . . . . . . . . . . . . . . . . . 20 Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk Sk V
344340ins3kex 4309 . . . . . . . . . . . . . . . . . . . . 21 Ins3k SIk SIk SIk SIk SIk SIk SIk Sk V
345344ins2kex 4308 . . . . . . . . . . . . . . . . . . . 20 Ins2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk V
346343, 345unex 4107 . . . . . . . . . . . . . . . . . . 19 ( Ins3k SIk SIk SIk SIk SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk SIk SIk SIk SIk Sk ) V
347338, 346symdifex 4109 . . . . . . . . . . . . . . . . . 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 4304 . . . . . . . . . . . . . . . . . . . . . . . . . 26 1111c V
349348pw1ex 4304 . . . . . . . . . . . . . . . . . . . . . . . . 25 11111c V
350349pw1ex 4304 . . . . . . . . . . . . . . . . . . . . . . . 24 111111c V
351350pw1ex 4304 . . . . . . . . . . . . . . . . . . . . . . 23 1111111c V
352351pw1ex 4304 . . . . . . . . . . . . . . . . . . . . . 22 11111111c V
353352pw1ex 4304 . . . . . . . . . . . . . . . . . . . . 21 111111111c V
354353pw1ex 4304 . . . . . . . . . . . . . . . . . . . 20 1111111111c V
355354pw1ex 4304 . . . . . . . . . . . . . . . . . . 19 11111111111c V
356355pw1ex 4304 . . . . . . . . . . . . . . . . . 18 111111111111c V
357347, 356imakex 4301 . . . . . . . . . . . . . . . . 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 4105 . . . . . . . . . . . . . . . 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 4106 . . . . . . . . . . . . . . 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 4106 . . . . . . . . . . . . . 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 4301 . . . . . . . . . . . . 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 4106 . . . . . . . . . . . 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 4301 . . . . . . . . . . 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 4308 . . . . . . . . . 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 4109 . . . . . . . . 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 4301 . . . . . . . 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 4105 . . . . . . 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 4383 . . . . . . . . . . 11 ( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) V
369368, 324imakex 4301 . . . . . . . . . 10 (( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) V
370369imagekex 4313 . . . . . . . . 9 Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) V
371370ins2kex 4308 . . . . . . . 8 Ins2k Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) V
372371ins2kex 4308 . . . . . . 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 4106 . . . . . 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 4301 . . . . 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 4397 . . . . . . 7 Nn V
376375pw1ex 4304 . . . . . 6 1 Nn V
377376pw1ex 4304 . . . . 5 11 Nn V
378374, 377imakex 4301 . . . 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 4112 . . . . 5 {} V
380379, 306xpkex 4290 . . . 4 ({} ×k V) V
381378, 380difex 4108 . . 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 4106 . 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 2517  wrex 2616  Vcvv 2860  ccompl 3206   cdif 3207  cun 3208  cin 3209  csymdif 3210  c0 3551  {csn 3738  copk 4058  1cc1c 4135  1cpw1 4136   ×k cxpk 4175   Ins2k cins2k 4177   Ins3k cins3k 4178  k cimak 4180   SIk csik 4182  Imagekcimagek 4183   Sk cssetk 4184   Nn cnnc 4374   +c cplc 4376   <fin cltfin 4434
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-ext 2334  ax-nin 4079  ax-xp 4080  ax-cnv 4081  ax-1c 4082  ax-sset 4083  ax-si 4084  ax-ins2 4085  ax-ins3 4086  ax-typlower 4087  ax-sn 4088
This 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 2479  df-ne 2519  df-ral 2620  df-rex 2621  df-v 2862  df-sbc 3048  df-nin 3212  df-compl 3213  df-in 3214  df-un 3215  df-dif 3216  df-symdif 3217  df-ss 3260  df-nul 3552  df-if 3664  df-pw 3725  df-sn 3742  df-pr 3743  df-uni 3893  df-int 3928  df-opk 4059  df-1c 4137  df-pw1 4138  df-uni1 4139  df-xpk 4186  df-cnvk 4187  df-ins2k 4188  df-ins3k 4189  df-imak 4190  df-cok 4191  df-p6 4192  df-sik 4193  df-ssetk 4194  df-imagek 4195  df-addc 4379  df-nnc 4380  df-ltfin 4442
This theorem is referenced by:  ltfintrilem1  4466
  Copyright terms: Public domain W3C validator