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

Theorem oddfinex 4504
Description: The set of all odd naturals exists. (Contributed by SF, 20-Jan-2015.)
Assertion
Ref Expression
oddfinex Oddfin V

Proof of Theorem oddfinex
Dummy variables a b c n t x y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-oddfin 4445 . . 3 Oddfin = {x (n Nn x = ((n +c n) +c 1c) x)}
2 eldifsn 3839 . . . . 5 (x (( ∼ (( Ins2k SkIns3k (((( Ins2k Ins2k (((( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c) “k 111c) ∩ Ins3k k SIk SIk SIkSk ) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k Ik )) “k 11111111c)) “k 11111c) “k 1111c)) “k 111c) “k Nn ) {}) ↔ (x ( ∼ (( Ins2k SkIns3k (((( Ins2k Ins2k (((( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c) “k 111c) ∩ Ins3k k SIk SIk SIkSk ) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k Ik )) “k 11111111c)) “k 11111c) “k 1111c)) “k 111c) “k Nn ) x))
3 vex 2862 . . . . . . . 8 x V
43elimak 4259 . . . . . . 7 (x ( ∼ (( Ins2k SkIns3k (((( Ins2k Ins2k (((( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c) “k 111c) ∩ Ins3k k SIk SIk SIkSk ) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k Ik )) “k 11111111c)) “k 11111c) “k 1111c)) “k 111c) “k Nn ) ↔ n Nnn, x ∼ (( Ins2k SkIns3k (((( Ins2k Ins2k (((( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c) “k 111c) ∩ Ins3k k SIk SIk SIkSk ) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k Ik )) “k 11111111c)) “k 11111c) “k 1111c)) “k 111c))
5 opkex 4113 . . . . . . . . . . . 12 n, x V
65elimak 4259 . . . . . . . . . . 11 (⟪n, x (( Ins2k SkIns3k (((( Ins2k Ins2k (((( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c) “k 111c) ∩ Ins3k k SIk SIk SIkSk ) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k Ik )) “k 11111111c)) “k 11111c) “k 1111c)) “k 111c) ↔ t 1 11ct, ⟪n, x⟫⟫ ( Ins2k SkIns3k (((( Ins2k Ins2k (((( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c) “k 111c) ∩ Ins3k k SIk SIk SIkSk ) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k Ik )) “k 11111111c)) “k 11111c) “k 1111c)))
7 elpw121c 4148 . . . . . . . . . . . . . . 15 (t 111ca t = {{{a}}})
87anbi1i 676 . . . . . . . . . . . . . 14 ((t 111c t, ⟪n, x⟫⟫ ( Ins2k SkIns3k (((( Ins2k Ins2k (((( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c) “k 111c) ∩ Ins3k k SIk SIk SIkSk ) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k Ik )) “k 11111111c)) “k 11111c) “k 1111c))) ↔ (a t = {{{a}}} t, ⟪n, x⟫⟫ ( Ins2k SkIns3k (((( Ins2k Ins2k (((( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c) “k 111c) ∩ Ins3k k SIk SIk SIkSk ) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k Ik )) “k 11111111c)) “k 11111c) “k 1111c))))
9 19.41v 1901 . . . . . . . . . . . . . 14 (a(t = {{{a}}} t, ⟪n, x⟫⟫ ( Ins2k SkIns3k (((( Ins2k Ins2k (((( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c) “k 111c) ∩ Ins3k k SIk SIk SIkSk ) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k Ik )) “k 11111111c)) “k 11111c) “k 1111c))) ↔ (a t = {{{a}}} t, ⟪n, x⟫⟫ ( Ins2k SkIns3k (((( Ins2k Ins2k (((( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c) “k 111c) ∩ Ins3k k SIk SIk SIkSk ) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k Ik )) “k 11111111c)) “k 11111c) “k 1111c))))
108, 9bitr4i 243 . . . . . . . . . . . . 13 ((t 111c t, ⟪n, x⟫⟫ ( Ins2k SkIns3k (((( Ins2k Ins2k (((( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c) “k 111c) ∩ Ins3k k SIk SIk SIkSk ) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k Ik )) “k 11111111c)) “k 11111c) “k 1111c))) ↔ a(t = {{{a}}} t, ⟪n, x⟫⟫ ( Ins2k SkIns3k (((( Ins2k Ins2k (((( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c) “k 111c) ∩ Ins3k k SIk SIk SIkSk ) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k Ik )) “k 11111111c)) “k 11111c) “k 1111c))))
1110exbii 1582 . . . . . . . . . . . 12 (t(t 111c t, ⟪n, x⟫⟫ ( Ins2k SkIns3k (((( Ins2k Ins2k (((( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c) “k 111c) ∩ Ins3k k SIk SIk SIkSk ) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k Ik )) “k 11111111c)) “k 11111c) “k 1111c))) ↔ ta(t = {{{a}}} t, ⟪n, x⟫⟫ ( Ins2k SkIns3k (((( Ins2k Ins2k (((( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c) “k 111c) ∩ Ins3k k SIk SIk SIkSk ) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k Ik )) “k 11111111c)) “k 11111c) “k 1111c))))
12 df-rex 2620 . . . . . . . . . . . 12 (t 1 11ct, ⟪n, x⟫⟫ ( Ins2k SkIns3k (((( Ins2k Ins2k (((( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c) “k 111c) ∩ Ins3k k SIk SIk SIkSk ) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k Ik )) “k 11111111c)) “k 11111c) “k 1111c)) ↔ t(t 111c t, ⟪n, x⟫⟫ ( Ins2k SkIns3k (((( Ins2k Ins2k (((( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c) “k 111c) ∩ Ins3k k SIk SIk SIkSk ) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k Ik )) “k 11111111c)) “k 11111c) “k 1111c))))
13 excom 1741 . . . . . . . . . . . 12 (at(t = {{{a}}} t, ⟪n, x⟫⟫ ( Ins2k SkIns3k (((( Ins2k Ins2k (((( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c) “k 111c) ∩ Ins3k k SIk SIk SIkSk ) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k Ik )) “k 11111111c)) “k 11111c) “k 1111c))) ↔ ta(t = {{{a}}} t, ⟪n, x⟫⟫ ( Ins2k SkIns3k (((( Ins2k Ins2k (((( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c) “k 111c) ∩ Ins3k k SIk SIk SIkSk ) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k Ik )) “k 11111111c)) “k 11111c) “k 1111c))))
1411, 12, 133bitr4i 268 . . . . . . . . . . 11 (t 1 11ct, ⟪n, x⟫⟫ ( Ins2k SkIns3k (((( Ins2k Ins2k (((( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c) “k 111c) ∩ Ins3k k SIk SIk SIkSk ) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k Ik )) “k 11111111c)) “k 11111c) “k 1111c)) ↔ at(t = {{{a}}} t, ⟪n, x⟫⟫ ( Ins2k SkIns3k (((( Ins2k Ins2k (((( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c) “k 111c) ∩ Ins3k k SIk SIk SIkSk ) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k Ik )) “k 11111111c)) “k 11111c) “k 1111c))))
15 snex 4111 . . . . . . . . . . . . . 14 {{{a}}} V
16 opkeq1 4059 . . . . . . . . . . . . . . 15 (t = {{{a}}} → ⟪t, ⟪n, x⟫⟫ = ⟪{{{a}}}, ⟪n, x⟫⟫)
1716eleq1d 2419 . . . . . . . . . . . . . 14 (t = {{{a}}} → (⟪t, ⟪n, x⟫⟫ ( Ins2k SkIns3k (((( Ins2k Ins2k (((( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c) “k 111c) ∩ Ins3k k SIk SIk SIkSk ) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k Ik )) “k 11111111c)) “k 11111c) “k 1111c)) ↔ ⟪{{{a}}}, ⟪n, x⟫⟫ ( Ins2k SkIns3k (((( Ins2k Ins2k (((( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c) “k 111c) ∩ Ins3k k SIk SIk SIkSk ) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k Ik )) “k 11111111c)) “k 11111c) “k 1111c))))
1815, 17ceqsexv 2894 . . . . . . . . . . . . 13 (t(t = {{{a}}} t, ⟪n, x⟫⟫ ( Ins2k SkIns3k (((( Ins2k Ins2k (((( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c) “k 111c) ∩ Ins3k k SIk SIk SIkSk ) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k Ik )) “k 11111111c)) “k 11111c) “k 1111c))) ↔ ⟪{{{a}}}, ⟪n, x⟫⟫ ( Ins2k SkIns3k (((( Ins2k Ins2k (((( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c) “k 111c) ∩ Ins3k k SIk SIk SIkSk ) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k Ik )) “k 11111111c)) “k 11111c) “k 1111c)))
19 elsymdif 3223 . . . . . . . . . . . . 13 (⟪{{{a}}}, ⟪n, x⟫⟫ ( Ins2k SkIns3k (((( Ins2k Ins2k (((( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c) “k 111c) ∩ Ins3k k SIk SIk SIkSk ) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k Ik )) “k 11111111c)) “k 11111c) “k 1111c)) ↔ ¬ (⟪{{{a}}}, ⟪n, x⟫⟫ Ins2k Sk ↔ ⟪{{{a}}}, ⟪n, x⟫⟫ Ins3k (((( Ins2k Ins2k (((( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c) “k 111c) ∩ Ins3k k SIk SIk SIkSk ) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k Ik )) “k 11111111c)) “k 11111c) “k 1111c)))
20 snex 4111 . . . . . . . . . . . . . . . . 17 {a} V
21 vex 2862 . . . . . . . . . . . . . . . . 17 n V
2220, 21, 3otkelins2k 4255 . . . . . . . . . . . . . . . 16 (⟪{{{a}}}, ⟪n, x⟫⟫ Ins2k Sk ↔ ⟪{a}, x Sk )
23 vex 2862 . . . . . . . . . . . . . . . . 17 a V
2423, 3elssetk 4270 . . . . . . . . . . . . . . . 16 (⟪{a}, x Ska x)
2522, 24bitri 240 . . . . . . . . . . . . . . 15 (⟪{{{a}}}, ⟪n, x⟫⟫ Ins2k Ska x)
26 opkex 4113 . . . . . . . . . . . . . . . . . 18 ⟪{a}, n V
2726elimak 4259 . . . . . . . . . . . . . . . . 17 (⟪{a}, n (((( Ins2k Ins2k (((( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c) “k 111c) ∩ Ins3k k SIk SIk SIkSk ) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k Ik )) “k 11111111c)) “k 11111c) “k 1111c) ↔ t 1 111ct, ⟪{a}, n⟫⟫ ((( Ins2k Ins2k (((( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c) “k 111c) ∩ Ins3k k SIk SIk SIkSk ) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k Ik )) “k 11111111c)) “k 11111c))
28 df-rex 2620 . . . . . . . . . . . . . . . . . 18 (t 1 111ct, ⟪{a}, n⟫⟫ ((( Ins2k Ins2k (((( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c) “k 111c) ∩ Ins3k k SIk SIk SIkSk ) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k Ik )) “k 11111111c)) “k 11111c) ↔ t(t 1111c t, ⟪{a}, n⟫⟫ ((( Ins2k Ins2k (((( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c) “k 111c) ∩ Ins3k k SIk SIk SIkSk ) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k Ik )) “k 11111111c)) “k 11111c)))
29 elpw131c 4149 . . . . . . . . . . . . . . . . . . . . 21 (t 1111cx t = {{{{x}}}})
3029anbi1i 676 . . . . . . . . . . . . . . . . . . . 20 ((t 1111c t, ⟪{a}, n⟫⟫ ((( Ins2k Ins2k (((( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c) “k 111c) ∩ Ins3k k SIk SIk SIkSk ) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k Ik )) “k 11111111c)) “k 11111c)) ↔ (x t = {{{{x}}}} t, ⟪{a}, n⟫⟫ ((( Ins2k Ins2k (((( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c) “k 111c) ∩ Ins3k k SIk SIk SIkSk ) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k Ik )) “k 11111111c)) “k 11111c)))
31 19.41v 1901 . . . . . . . . . . . . . . . . . . . 20 (x(t = {{{{x}}}} t, ⟪{a}, n⟫⟫ ((( Ins2k Ins2k (((( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c) “k 111c) ∩ Ins3k k SIk SIk SIkSk ) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k Ik )) “k 11111111c)) “k 11111c)) ↔ (x t = {{{{x}}}} t, ⟪{a}, n⟫⟫ ((( Ins2k Ins2k (((( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c) “k 111c) ∩ Ins3k k SIk SIk SIkSk ) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k Ik )) “k 11111111c)) “k 11111c)))
3230, 31bitr4i 243 . . . . . . . . . . . . . . . . . . 19 ((t 1111c t, ⟪{a}, n⟫⟫ ((( Ins2k Ins2k (((( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c) “k 111c) ∩ Ins3k k SIk SIk SIkSk ) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k Ik )) “k 11111111c)) “k 11111c)) ↔ x(t = {{{{x}}}} t, ⟪{a}, n⟫⟫ ((( Ins2k Ins2k (((( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c) “k 111c) ∩ Ins3k k SIk SIk SIkSk ) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k Ik )) “k 11111111c)) “k 11111c)))
3332exbii 1582 . . . . . . . . . . . . . . . . . 18 (t(t 1111c t, ⟪{a}, n⟫⟫ ((( Ins2k Ins2k (((( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c) “k 111c) ∩ Ins3k k SIk SIk SIkSk ) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k Ik )) “k 11111111c)) “k 11111c)) ↔ tx(t = {{{{x}}}} t, ⟪{a}, n⟫⟫ ((( Ins2k Ins2k (((( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c) “k 111c) ∩ Ins3k k SIk SIk SIkSk ) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k Ik )) “k 11111111c)) “k 11111c)))
34 excom 1741 . . . . . . . . . . . . . . . . . 18 (tx(t = {{{{x}}}} t, ⟪{a}, n⟫⟫ ((( Ins2k Ins2k (((( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c) “k 111c) ∩ Ins3k k SIk SIk SIkSk ) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k Ik )) “k 11111111c)) “k 11111c)) ↔ xt(t = {{{{x}}}} t, ⟪{a}, n⟫⟫ ((( Ins2k Ins2k (((( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c) “k 111c) ∩ Ins3k k SIk SIk SIkSk ) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k Ik )) “k 11111111c)) “k 11111c)))
3528, 33, 343bitri 262 . . . . . . . . . . . . . . . . 17 (t 1 111ct, ⟪{a}, n⟫⟫ ((( Ins2k Ins2k (((( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c) “k 111c) ∩ Ins3k k SIk SIk SIkSk ) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k Ik )) “k 11111111c)) “k 11111c) ↔ xt(t = {{{{x}}}} t, ⟪{a}, n⟫⟫ ((( Ins2k Ins2k (((( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c) “k 111c) ∩ Ins3k k SIk SIk SIkSk ) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k Ik )) “k 11111111c)) “k 11111c)))
36 snex 4111 . . . . . . . . . . . . . . . . . . . 20 {{{{x}}}} V
37 opkeq1 4059 . . . . . . . . . . . . . . . . . . . . 21 (t = {{{{x}}}} → ⟪t, ⟪{a}, n⟫⟫ = ⟪{{{{x}}}}, ⟪{a}, n⟫⟫)
3837eleq1d 2419 . . . . . . . . . . . . . . . . . . . 20 (t = {{{{x}}}} → (⟪t, ⟪{a}, n⟫⟫ ((( Ins2k Ins2k (((( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c) “k 111c) ∩ Ins3k k SIk SIk SIkSk ) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k Ik )) “k 11111111c)) “k 11111c) ↔ ⟪{{{{x}}}}, ⟪{a}, n⟫⟫ ((( Ins2k Ins2k (((( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c) “k 111c) ∩ Ins3k k SIk SIk SIkSk ) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k Ik )) “k 11111111c)) “k 11111c)))
3936, 38ceqsexv 2894 . . . . . . . . . . . . . . . . . . 19 (t(t = {{{{x}}}} t, ⟪{a}, n⟫⟫ ((( Ins2k Ins2k (((( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c) “k 111c) ∩ Ins3k k SIk SIk SIkSk ) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k Ik )) “k 11111111c)) “k 11111c)) ↔ ⟪{{{{x}}}}, ⟪{a}, n⟫⟫ ((( Ins2k Ins2k (((( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c) “k 111c) ∩ Ins3k k SIk SIk SIkSk ) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k Ik )) “k 11111111c)) “k 11111c))
40 opkex 4113 . . . . . . . . . . . . . . . . . . . . 21 ⟪{{{{x}}}}, ⟪{a}, n⟫⟫ V
4140elimak 4259 . . . . . . . . . . . . . . . . . . . 20 (⟪{{{{x}}}}, ⟪{a}, n⟫⟫ ((( Ins2k Ins2k (((( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c) “k 111c) ∩ Ins3k k SIk SIk SIkSk ) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k Ik )) “k 11111111c)) “k 11111c) ↔ t 1 1111ct, ⟪{{{{x}}}}, ⟪{a}, n⟫⟫⟫ (( Ins2k Ins2k (((( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c) “k 111c) ∩ Ins3k k SIk SIk SIkSk ) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k Ik )) “k 11111111c)))
42 df-rex 2620 . . . . . . . . . . . . . . . . . . . 20 (t 1 1111ct, ⟪{{{{x}}}}, ⟪{a}, n⟫⟫⟫ (( Ins2k Ins2k (((( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c) “k 111c) ∩ Ins3k k SIk SIk SIkSk ) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k Ik )) “k 11111111c)) ↔ t(t 11111c t, ⟪{{{{x}}}}, ⟪{a}, n⟫⟫⟫ (( Ins2k Ins2k (((( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c) “k 111c) ∩ Ins3k k SIk SIk SIkSk ) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k Ik )) “k 11111111c))))
43 elpw141c 4150 . . . . . . . . . . . . . . . . . . . . . . . 24 (t 11111cb t = {{{{{b}}}}})
4443anbi1i 676 . . . . . . . . . . . . . . . . . . . . . . 23 ((t 11111c t, ⟪{{{{x}}}}, ⟪{a}, n⟫⟫⟫ (( Ins2k Ins2k (((( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c) “k 111c) ∩ Ins3k k SIk SIk SIkSk ) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k Ik )) “k 11111111c))) ↔ (b t = {{{{{b}}}}} t, ⟪{{{{x}}}}, ⟪{a}, n⟫⟫⟫ (( Ins2k Ins2k (((( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c) “k 111c) ∩ Ins3k k SIk SIk SIkSk ) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k Ik )) “k 11111111c))))
45 19.41v 1901 . . . . . . . . . . . . . . . . . . . . . . 23 (b(t = {{{{{b}}}}} t, ⟪{{{{x}}}}, ⟪{a}, n⟫⟫⟫ (( Ins2k Ins2k (((( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c) “k 111c) ∩ Ins3k k SIk SIk SIkSk ) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k Ik )) “k 11111111c))) ↔ (b t = {{{{{b}}}}} t, ⟪{{{{x}}}}, ⟪{a}, n⟫⟫⟫ (( Ins2k Ins2k (((( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c) “k 111c) ∩ Ins3k k SIk SIk SIkSk ) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k Ik )) “k 11111111c))))
4644, 45bitr4i 243 . . . . . . . . . . . . . . . . . . . . . 22 ((t 11111c t, ⟪{{{{x}}}}, ⟪{a}, n⟫⟫⟫ (( Ins2k Ins2k (((( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c) “k 111c) ∩ Ins3k k SIk SIk SIkSk ) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k Ik )) “k 11111111c))) ↔ b(t = {{{{{b}}}}} t, ⟪{{{{x}}}}, ⟪{a}, n⟫⟫⟫ (( Ins2k Ins2k (((( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c) “k 111c) ∩ Ins3k k SIk SIk SIkSk ) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k Ik )) “k 11111111c))))
4746exbii 1582 . . . . . . . . . . . . . . . . . . . . 21 (t(t 11111c t, ⟪{{{{x}}}}, ⟪{a}, n⟫⟫⟫ (( Ins2k Ins2k (((( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c) “k 111c) ∩ Ins3k k SIk SIk SIkSk ) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k Ik )) “k 11111111c))) ↔ tb(t = {{{{{b}}}}} t, ⟪{{{{x}}}}, ⟪{a}, n⟫⟫⟫ (( Ins2k Ins2k (((( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c) “k 111c) ∩ Ins3k k SIk SIk SIkSk ) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k Ik )) “k 11111111c))))
48 excom 1741 . . . . . . . . . . . . . . . . . . . . 21 (bt(t = {{{{{b}}}}} t, ⟪{{{{x}}}}, ⟪{a}, n⟫⟫⟫ (( Ins2k Ins2k (((( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c) “k 111c) ∩ Ins3k k SIk SIk SIkSk ) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k Ik )) “k 11111111c))) ↔ tb(t = {{{{{b}}}}} t, ⟪{{{{x}}}}, ⟪{a}, n⟫⟫⟫ (( Ins2k Ins2k (((( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c) “k 111c) ∩ Ins3k k SIk SIk SIkSk ) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k Ik )) “k 11111111c))))
4947, 48bitr4i 243 . . . . . . . . . . . . . . . . . . . 20 (t(t 11111c t, ⟪{{{{x}}}}, ⟪{a}, n⟫⟫⟫ (( Ins2k Ins2k (((( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c) “k 111c) ∩ Ins3k k SIk SIk SIkSk ) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k Ik )) “k 11111111c))) ↔ bt(t = {{{{{b}}}}} t, ⟪{{{{x}}}}, ⟪{a}, n⟫⟫⟫ (( Ins2k Ins2k (((( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c) “k 111c) ∩ Ins3k k SIk SIk SIkSk ) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k Ik )) “k 11111111c))))
5041, 42, 493bitri 262 . . . . . . . . . . . . . . . . . . 19 (⟪{{{{x}}}}, ⟪{a}, n⟫⟫ ((( Ins2k Ins2k (((( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c) “k 111c) ∩ Ins3k k SIk SIk SIkSk ) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k Ik )) “k 11111111c)) “k 11111c) ↔ bt(t = {{{{{b}}}}} t, ⟪{{{{x}}}}, ⟪{a}, n⟫⟫⟫ (( Ins2k Ins2k (((( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c) “k 111c) ∩ Ins3k k SIk SIk SIkSk ) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k Ik )) “k 11111111c))))
51 snex 4111 . . . . . . . . . . . . . . . . . . . . . 22 {{{{{b}}}}} V
52 opkeq1 4059 . . . . . . . . . . . . . . . . . . . . . . 23 (t = {{{{{b}}}}} → ⟪t, ⟪{{{{x}}}}, ⟪{a}, n⟫⟫⟫ = ⟪{{{{{b}}}}}, ⟪{{{{x}}}}, ⟪{a}, n⟫⟫⟫)
5352eleq1d 2419 . . . . . . . . . . . . . . . . . . . . . 22 (t = {{{{{b}}}}} → (⟪t, ⟪{{{{x}}}}, ⟪{a}, n⟫⟫⟫ (( Ins2k Ins2k (((( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c) “k 111c) ∩ Ins3k k SIk SIk SIkSk ) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k Ik )) “k 11111111c)) ↔ ⟪{{{{{b}}}}}, ⟪{{{{x}}}}, ⟪{a}, n⟫⟫⟫ (( Ins2k Ins2k (((( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c) “k 111c) ∩ Ins3k k SIk SIk SIkSk ) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k Ik )) “k 11111111c))))
5451, 53ceqsexv 2894 . . . . . . . . . . . . . . . . . . . . 21 (t(t = {{{{{b}}}}} t, ⟪{{{{x}}}}, ⟪{a}, n⟫⟫⟫ (( Ins2k Ins2k (((( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c) “k 111c) ∩ Ins3k k SIk SIk SIkSk ) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k Ik )) “k 11111111c))) ↔ ⟪{{{{{b}}}}}, ⟪{{{{x}}}}, ⟪{a}, n⟫⟫⟫ (( Ins2k Ins2k (((( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c) “k 111c) ∩ Ins3k k SIk SIk SIkSk ) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k Ik )) “k 11111111c)))
55 elin 3219 . . . . . . . . . . . . . . . . . . . . 21 (⟪{{{{{b}}}}}, ⟪{{{{x}}}}, ⟪{a}, n⟫⟫⟫ (( Ins2k Ins2k (((( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c) “k 111c) ∩ Ins3k k SIk SIk SIkSk ) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k Ik )) “k 11111111c)) ↔ (⟪{{{{{b}}}}}, ⟪{{{{x}}}}, ⟪{a}, n⟫⟫⟫ ( Ins2k Ins2k (((( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c) “k 111c) ∩ Ins3k k SIk SIk SIkSk ) ⟪{{{{{b}}}}}, ⟪{{{{x}}}}, ⟪{a}, n⟫⟫⟫ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k Ik )) “k 11111111c)))
56 elin 3219 . . . . . . . . . . . . . . . . . . . . . . 23 (⟪{{{{{b}}}}}, ⟪{{{{x}}}}, ⟪{a}, n⟫⟫⟫ ( Ins2k Ins2k (((( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c) “k 111c) ∩ Ins3k k SIk SIk SIkSk ) ↔ (⟪{{{{{b}}}}}, ⟪{{{{x}}}}, ⟪{a}, n⟫⟫⟫ Ins2k Ins2k (((( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c) “k 111c) ⟪{{{{{b}}}}}, ⟪{{{{x}}}}, ⟪{a}, n⟫⟫⟫ Ins3k k SIk SIk SIkSk ))
57 snex 4111 . . . . . . . . . . . . . . . . . . . . . . . . . 26 {{{b}}} V
5857, 36, 26otkelins2k 4255 . . . . . . . . . . . . . . . . . . . . . . . . 25 (⟪{{{{{b}}}}}, ⟪{{{{x}}}}, ⟪{a}, n⟫⟫⟫ Ins2k Ins2k (((( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c) “k 111c) ↔ ⟪{{{b}}}, ⟪{a}, n⟫⟫ Ins2k (((( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c) “k 111c))
59 snex 4111 . . . . . . . . . . . . . . . . . . . . . . . . . 26 {b} V
6059, 20, 21otkelins2k 4255 . . . . . . . . . . . . . . . . . . . . . . . . 25 (⟪{{{b}}}, ⟪{a}, n⟫⟫ Ins2k (((( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c) “k 111c) ↔ ⟪{b}, n (((( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c) “k 111c))
61 opkex 4113 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⟪{b}, n V
6261elimak 4259 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (⟪{b}, n (((( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c) “k 111c) ↔ t 1 11ct, ⟪{b}, n⟫⟫ ((( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c))
63 elpw121c 4148 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (t 111cc t = {{{c}}})
6463anbi1i 676 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((t 111c t, ⟪{b}, n⟫⟫ ((( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c)) ↔ (c t = {{{c}}} t, ⟪{b}, n⟫⟫ ((( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c)))
65 19.41v 1901 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (c(t = {{{c}}} t, ⟪{b}, n⟫⟫ ((( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c)) ↔ (c t = {{{c}}} t, ⟪{b}, n⟫⟫ ((( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c)))
6664, 65bitr4i 243 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((t 111c t, ⟪{b}, n⟫⟫ ((( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c)) ↔ c(t = {{{c}}} t, ⟪{b}, n⟫⟫ ((( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c)))
6766exbii 1582 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (t(t 111c t, ⟪{b}, n⟫⟫ ((( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c)) ↔ tc(t = {{{c}}} t, ⟪{b}, n⟫⟫ ((( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c)))
68 df-rex 2620 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (t 1 11ct, ⟪{b}, n⟫⟫ ((( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c) ↔ t(t 111c t, ⟪{b}, n⟫⟫ ((( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c)))
69 excom 1741 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (ct(t = {{{c}}} t, ⟪{b}, n⟫⟫ ((( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c)) ↔ tc(t = {{{c}}} t, ⟪{b}, n⟫⟫ ((( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c)))
7067, 68, 693bitr4i 268 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (t 1 11ct, ⟪{b}, n⟫⟫ ((( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c) ↔ ct(t = {{{c}}} t, ⟪{b}, n⟫⟫ ((( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c)))
71 snex 4111 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 {{{c}}} V
72 opkeq1 4059 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (t = {{{c}}} → ⟪t, ⟪{b}, n⟫⟫ = ⟪{{{c}}}, ⟪{b}, n⟫⟫)
7372eleq1d 2419 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (t = {{{c}}} → (⟪t, ⟪{b}, n⟫⟫ ((( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c) ↔ ⟪{{{c}}}, ⟪{b}, n⟫⟫ ((( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c)))
7471, 73ceqsexv 2894 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (t(t = {{{c}}} t, ⟪{b}, n⟫⟫ ((( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c)) ↔ ⟪{{{c}}}, ⟪{b}, n⟫⟫ ((( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c))
75 opkex 4113 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⟪{{{c}}}, ⟪{b}, n⟫⟫ V
7675elimak 4259 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (⟪{{{c}}}, ⟪{b}, n⟫⟫ ((( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c) ↔ t 1 1111ct, ⟪{{{c}}}, ⟪{b}, n⟫⟫⟫ (( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))))
77 df-rex 2620 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (t 1 1111ct, ⟪{{{c}}}, ⟪{b}, n⟫⟫⟫ (( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) ↔ t(t 11111c t, ⟪{{{c}}}, ⟪{b}, n⟫⟫⟫ (( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c)))))
78 elpw141c 4150 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (t 11111ca t = {{{{{a}}}}})
7978anbi1i 676 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((t 11111c t, ⟪{{{c}}}, ⟪{b}, n⟫⟫⟫ (( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c)))) ↔ (a t = {{{{{a}}}}} t, ⟪{{{c}}}, ⟪{b}, n⟫⟫⟫ (( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c)))))
80 19.41v 1901 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (a(t = {{{{{a}}}}} t, ⟪{{{c}}}, ⟪{b}, n⟫⟫⟫ (( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c)))) ↔ (a t = {{{{{a}}}}} t, ⟪{{{c}}}, ⟪{b}, n⟫⟫⟫ (( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c)))))
8179, 80bitr4i 243 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((t 11111c t, ⟪{{{c}}}, ⟪{b}, n⟫⟫⟫ (( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c)))) ↔ a(t = {{{{{a}}}}} t, ⟪{{{c}}}, ⟪{b}, n⟫⟫⟫ (( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c)))))
8281exbii 1582 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (t(t 11111c t, ⟪{{{c}}}, ⟪{b}, n⟫⟫⟫ (( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c)))) ↔ ta(t = {{{{{a}}}}} t, ⟪{{{c}}}, ⟪{b}, n⟫⟫⟫ (( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c)))))
83 excom 1741 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (at(t = {{{{{a}}}}} t, ⟪{{{c}}}, ⟪{b}, n⟫⟫⟫ (( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c)))) ↔ ta(t = {{{{{a}}}}} t, ⟪{{{c}}}, ⟪{b}, n⟫⟫⟫ (( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c)))))
8482, 83bitr4i 243 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (t(t 11111c t, ⟪{{{c}}}, ⟪{b}, n⟫⟫⟫ (( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c)))) ↔ at(t = {{{{{a}}}}} t, ⟪{{{c}}}, ⟪{b}, n⟫⟫⟫ (( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c)))))
8576, 77, 843bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (⟪{{{c}}}, ⟪{b}, n⟫⟫ ((( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c) ↔ at(t = {{{{{a}}}}} t, ⟪{{{c}}}, ⟪{b}, n⟫⟫⟫ (( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c)))))
86 snex 4111 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 {{{{{a}}}}} V
87 opkeq1 4059 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (t = {{{{{a}}}}} → ⟪t, ⟪{{{c}}}, ⟪{b}, n⟫⟫⟫ = ⟪{{{{{a}}}}}, ⟪{{{c}}}, ⟪{b}, n⟫⟫⟫)
8887eleq1d 2419 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (t = {{{{{a}}}}} → (⟪t, ⟪{{{c}}}, ⟪{b}, n⟫⟫⟫ (( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) ↔ ⟪{{{{{a}}}}}, ⟪{{{c}}}, ⟪{b}, n⟫⟫⟫ (( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c)))))
8986, 88ceqsexv 2894 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (t(t = {{{{{a}}}}} t, ⟪{{{c}}}, ⟪{b}, n⟫⟫⟫ (( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c)))) ↔ ⟪{{{{{a}}}}}, ⟪{{{c}}}, ⟪{b}, n⟫⟫⟫ (( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))))
90 elin 3219 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (⟪{{{{{a}}}}}, ⟪{{{c}}}, ⟪{b}, n⟫⟫⟫ (( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) ↔ (⟪{{{{{a}}}}}, ⟪{{{c}}}, ⟪{b}, n⟫⟫⟫ ( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ⟪{{{{{a}}}}}, ⟪{{{c}}}, ⟪{b}, n⟫⟫⟫ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))))
91 elin 3219 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (⟪{{{{{a}}}}}, ⟪{{{c}}}, ⟪{b}, n⟫⟫⟫ ( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ↔ (⟪{{{{{a}}}}}, ⟪{{{c}}}, ⟪{b}, n⟫⟫⟫ Ins2k Ins2k Sk ⟪{{{{{a}}}}}, ⟪{{{c}}}, ⟪{b}, n⟫⟫⟫ (V ×k Ins2k Sk )))
9215, 71, 61otkelins2k 4255 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (⟪{{{{{a}}}}}, ⟪{{{c}}}, ⟪{b}, n⟫⟫⟫ Ins2k Ins2k Sk ↔ ⟪{{{a}}}, ⟪{b}, n⟫⟫ Ins2k Sk )
9320, 59, 21otkelins2k 4255 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (⟪{{{a}}}, ⟪{b}, n⟫⟫ Ins2k Sk ↔ ⟪{a}, n Sk )
9423, 21elssetk 4270 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (⟪{a}, n Ska n)
9592, 93, 943bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (⟪{{{{{a}}}}}, ⟪{{{c}}}, ⟪{b}, n⟫⟫⟫ Ins2k Ins2k Ska n)
9686, 75opkelxpk 4248 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (⟪{{{{{a}}}}}, ⟪{{{c}}}, ⟪{b}, n⟫⟫⟫ (V ×k Ins2k Sk ) ↔ ({{{{{a}}}}} V ⟪{{{c}}}, ⟪{b}, n⟫⟫ Ins2k Sk ))
9786, 96mpbiran 884 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (⟪{{{{{a}}}}}, ⟪{{{c}}}, ⟪{b}, n⟫⟫⟫ (V ×k Ins2k Sk ) ↔ ⟪{{{c}}}, ⟪{b}, n⟫⟫ Ins2k Sk )
98 snex 4111 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 {c} V
9998, 59, 21otkelins2k 4255 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (⟪{{{c}}}, ⟪{b}, n⟫⟫ Ins2k Sk ↔ ⟪{c}, n Sk )
100 vex 2862 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 c V
101100, 21elssetk 4270 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (⟪{c}, n Skc n)
10297, 99, 1013bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (⟪{{{{{a}}}}}, ⟪{{{c}}}, ⟪{b}, n⟫⟫⟫ (V ×k Ins2k Sk ) ↔ c n)
10395, 102anbi12i 678 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((⟪{{{{{a}}}}}, ⟪{{{c}}}, ⟪{b}, n⟫⟫⟫ Ins2k Ins2k Sk ⟪{{{{{a}}}}}, ⟪{{{c}}}, ⟪{b}, n⟫⟫⟫ (V ×k Ins2k Sk )) ↔ (a n c n))
10491, 103bitri 240 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (⟪{{{{{a}}}}}, ⟪{{{c}}}, ⟪{b}, n⟫⟫⟫ ( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ↔ (a n c n))
105 elin 3219 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (⟪{{{{{a}}}}}, ⟪{{{c}}}, ⟪{b}, n⟫⟫⟫ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c)) ↔ (⟪{{{{{a}}}}}, ⟪{{{c}}}, ⟪{b}, n⟫⟫⟫ Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ⟪{{{{{a}}}}}, ⟪{{{c}}}, ⟪{b}, n⟫⟫⟫ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c)))
10615, 71, 61otkelins3k 4256 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (⟪{{{{{a}}}}}, ⟪{{{c}}}, ⟪{b}, n⟫⟫⟫ Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ↔ ⟪{{{a}}}, {{{c}}}⟫ SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c))
107 snex 4111 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 {{a}} V
108 snex 4111 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 {{c}} V
109107, 108opksnelsik 4265 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (⟪{{{a}}}, {{{c}}}⟫ SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ↔ ⟪{{a}}, {{c}}⟫ SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c))
11020, 98opksnelsik 4265 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (⟪{{a}}, {{c}}⟫ SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ↔ ⟪{a}, {c}⟫ SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c))
11123, 100opksnelsik 4265 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (⟪{a}, {c}⟫ SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ↔ ⟪a, c ∼ (( Ins3k SkIns2k Sk ) “k 111c))
11223, 100ndisjrelk 4323 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (⟪a, c (( Ins3k SkIns2k Sk ) “k 111c) ↔ (ac) ≠ )
113112notbii 287 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (¬ ⟪a, c (( Ins3k SkIns2k Sk ) “k 111c) ↔ ¬ (ac) ≠ )
114 opkex 4113 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 a, c V
115114elcompl 3225 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (⟪a, c ∼ (( Ins3k SkIns2k Sk ) “k 111c) ↔ ¬ ⟪a, c (( Ins3k SkIns2k Sk ) “k 111c))
116 df-ne 2518 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((ac) ≠ ↔ ¬ (ac) = )
117116con2bii 322 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((ac) = ↔ ¬ (ac) ≠ )
118113, 115, 1173bitr4i 268 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (⟪a, c ∼ (( Ins3k SkIns2k Sk ) “k 111c) ↔ (ac) = )
119110, 111, 1183bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (⟪{{a}}, {{c}}⟫ SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ↔ (ac) = )
120106, 109, 1193bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (⟪{{{{{a}}}}}, ⟪{{{c}}}, ⟪{b}, n⟫⟫⟫ Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ↔ (ac) = )
121 opkex 4113 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⟪{{{{{a}}}}}, ⟪{{{c}}}, ⟪{b}, n⟫⟫⟫ V
122121elimak 4259 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (⟪{{{{{a}}}}}, ⟪{{{c}}}, ⟪{b}, n⟫⟫⟫ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c) ↔ t 1 1111111ct, ⟪{{{{{a}}}}}, ⟪{{{c}}}, ⟪{b}, n⟫⟫⟫⟫ ( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )))
123 elpw171c 4153 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (t 11111111cx t = {{{{{{{{x}}}}}}}})
124123anbi1i 676 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((t 11111111c t, ⟪{{{{{a}}}}}, ⟪{{{c}}}, ⟪{b}, n⟫⟫⟫⟫ ( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk ))) ↔ (x t = {{{{{{{{x}}}}}}}} t, ⟪{{{{{a}}}}}, ⟪{{{c}}}, ⟪{b}, n⟫⟫⟫⟫ ( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk ))))
125 19.41v 1901 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (x(t = {{{{{{{{x}}}}}}}} t, ⟪{{{{{a}}}}}, ⟪{{{c}}}, ⟪{b}, n⟫⟫⟫⟫ ( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk ))) ↔ (x t = {{{{{{{{x}}}}}}}} t, ⟪{{{{{a}}}}}, ⟪{{{c}}}, ⟪{b}, n⟫⟫⟫⟫ ( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk ))))
126124, 125bitr4i 243 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((t 11111111c t, ⟪{{{{{a}}}}}, ⟪{{{c}}}, ⟪{b}, n⟫⟫⟫⟫ ( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk ))) ↔ x(t = {{{{{{{{x}}}}}}}} t, ⟪{{{{{a}}}}}, ⟪{{{c}}}, ⟪{b}, n⟫⟫⟫⟫ ( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk ))))
127126exbii 1582 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (t(t 11111111c t, ⟪{{{{{a}}}}}, ⟪{{{c}}}, ⟪{b}, n⟫⟫⟫⟫ ( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk ))) ↔ tx(t = {{{{{{{{x}}}}}}}} t, ⟪{{{{{a}}}}}, ⟪{{{c}}}, ⟪{b}, n⟫⟫⟫⟫ ( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk ))))
128 df-rex 2620 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (t 1 1111111ct, ⟪{{{{{a}}}}}, ⟪{{{c}}}, ⟪{b}, n⟫⟫⟫⟫ ( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) ↔ t(t 11111111c t, ⟪{{{{{a}}}}}, ⟪{{{c}}}, ⟪{b}, n⟫⟫⟫⟫ ( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk ))))
129 excom 1741 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (xt(t = {{{{{{{{x}}}}}}}} t, ⟪{{{{{a}}}}}, ⟪{{{c}}}, ⟪{b}, n⟫⟫⟫⟫ ( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk ))) ↔ tx(t = {{{{{{{{x}}}}}}}} t, ⟪{{{{{a}}}}}, ⟪{{{c}}}, ⟪{b}, n⟫⟫⟫⟫ ( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk ))))
130127, 128, 1293bitr4i 268 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (t 1 1111111ct, ⟪{{{{{a}}}}}, ⟪{{{c}}}, ⟪{b}, n⟫⟫⟫⟫ ( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) ↔ xt(t = {{{{{{{{x}}}}}}}} t, ⟪{{{{{a}}}}}, ⟪{{{c}}}, ⟪{b}, n⟫⟫⟫⟫ ( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk ))))
131 snex 4111 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 {{{{{{{{x}}}}}}}} V
132 opkeq1 4059 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (t = {{{{{{{{x}}}}}}}} → ⟪t, ⟪{{{{{a}}}}}, ⟪{{{c}}}, ⟪{b}, n⟫⟫⟫⟫ = ⟪{{{{{{{{x}}}}}}}}, ⟪{{{{{a}}}}}, ⟪{{{c}}}, ⟪{b}, n⟫⟫⟫⟫)
133132eleq1d 2419 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (t = {{{{{{{{x}}}}}}}} → (⟪t, ⟪{{{{{a}}}}}, ⟪{{{c}}}, ⟪{b}, n⟫⟫⟫⟫ ( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) ↔ ⟪{{{{{{{{x}}}}}}}}, ⟪{{{{{a}}}}}, ⟪{{{c}}}, ⟪{b}, n⟫⟫⟫⟫ ( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk ))))
134131, 133ceqsexv 2894 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (t(t = {{{{{{{{x}}}}}}}} t, ⟪{{{{{a}}}}}, ⟪{{{c}}}, ⟪{b}, n⟫⟫⟫⟫ ( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk ))) ↔ ⟪{{{{{{{{x}}}}}}}}, ⟪{{{{{a}}}}}, ⟪{{{c}}}, ⟪{b}, n⟫⟫⟫⟫ ( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )))
135 elsymdif 3223 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (⟪{{{{{{{{x}}}}}}}}, ⟪{{{{{a}}}}}, ⟪{{{c}}}, ⟪{b}, n⟫⟫⟫⟫ ( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) ↔ ¬ (⟪{{{{{{{{x}}}}}}}}, ⟪{{{{{a}}}}}, ⟪{{{c}}}, ⟪{b}, n⟫⟫⟫⟫ Ins2k Ins2k Ins3k SIk Sk ↔ ⟪{{{{{{{{x}}}}}}}}, ⟪{{{{{a}}}}}, ⟪{{{c}}}, ⟪{b}, n⟫⟫⟫⟫ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )))
136 snex 4111 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 {{{{{{x}}}}}} V
137136, 86, 75otkelins2k 4255 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (⟪{{{{{{{{x}}}}}}}}, ⟪{{{{{a}}}}}, ⟪{{{c}}}, ⟪{b}, n⟫⟫⟫⟫ Ins2k Ins2k Ins3k SIk Sk ↔ ⟪{{{{{{x}}}}}}, ⟪{{{c}}}, ⟪{b}, n⟫⟫⟫ Ins2k Ins3k SIk Sk )
13836, 71, 61otkelins2k 4255 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (⟪{{{{{{x}}}}}}, ⟪{{{c}}}, ⟪{b}, n⟫⟫⟫ Ins2k Ins3k SIk Sk ↔ ⟪{{{{x}}}}, ⟪{b}, n⟫⟫ Ins3k SIk Sk )
139 snex 4111 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 {{x}} V
140139, 59, 21otkelins3k 4256 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (⟪{{{{x}}}}, ⟪{b}, n⟫⟫ Ins3k SIk Sk ↔ ⟪{{x}}, {b}⟫ SIk Sk )
141 snex 4111 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 {x} V
142 vex 2862 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 b V
143141, 142opksnelsik 4265 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (⟪{{x}}, {b}⟫ SIk Sk ↔ ⟪{x}, b Sk )
1443, 142elssetk 4270 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (⟪{x}, b Skx b)
145140, 143, 1443bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (⟪{{{{x}}}}, ⟪{b}, n⟫⟫ Ins3k SIk Skx b)
146137, 138, 1453bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (⟪{{{{{{{{x}}}}}}}}, ⟪{{{{{a}}}}}, ⟪{{{c}}}, ⟪{b}, n⟫⟫⟫⟫ Ins2k Ins2k Ins3k SIk Skx b)
147136, 86, 75otkelins3k 4256 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (⟪{{{{{{{{x}}}}}}}}, ⟪{{{{{a}}}}}, ⟪{{{c}}}, ⟪{b}, n⟫⟫⟫⟫ Ins3k SIk SIk SIk SIk SIk Sk ↔ ⟪{{{{{{x}}}}}}, {{{{{a}}}}}⟫ SIk SIk SIk SIk SIk Sk )
148 snex 4111 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 {{{{{x}}}}} V
149 snex 4111 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 {{{{a}}}} V
150148, 149opksnelsik 4265 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (⟪{{{{{{x}}}}}}, {{{{{a}}}}}⟫ SIk SIk SIk SIk SIk Sk ↔ ⟪{{{{{x}}}}}, {{{{a}}}}⟫ SIk SIk SIk SIk Sk )
15136, 15opksnelsik 4265 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 (⟪{{{{{x}}}}}, {{{{a}}}}⟫ SIk SIk SIk SIk Sk ↔ ⟪{{{{x}}}}, {{{a}}}⟫ SIk SIk SIk Sk )
152 snex 4111 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 {{{x}}} V
153152, 107opksnelsik 4265 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 (⟪{{{{x}}}}, {{{a}}}⟫ SIk SIk SIk Sk ↔ ⟪{{{x}}}, {{a}}⟫ SIk SIk Sk )
154139, 20opksnelsik 4265 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 (⟪{{{x}}}, {{a}}⟫ SIk SIk Sk ↔ ⟪{{x}}, {a}⟫ SIk Sk )
155141, 23opksnelsik 4265 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 (⟪{{x}}, {a}⟫ SIk Sk ↔ ⟪{x}, a Sk )
1563, 23elssetk 4270 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 (⟪{x}, a Skx a)
157154, 155, 1563bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 (⟪{{{x}}}, {{a}}⟫ SIk SIk Skx a)
158151, 153, 1573bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (⟪{{{{{x}}}}}, {{{{a}}}}⟫ SIk SIk SIk SIk Skx a)
159147, 150, 1583bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (⟪{{{{{{{{x}}}}}}}}, ⟪{{{{{a}}}}}, ⟪{{{c}}}, ⟪{b}, n⟫⟫⟫⟫ Ins3k SIk SIk SIk SIk SIk Skx a)
160136, 86, 75otkelins2k 4255 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (⟪{{{{{{{{x}}}}}}}}, ⟪{{{{{a}}}}}, ⟪{{{c}}}, ⟪{b}, n⟫⟫⟫⟫ Ins2k Ins3k SIk SIk SIk Sk ↔ ⟪{{{{{{x}}}}}}, ⟪{{{c}}}, ⟪{b}, n⟫⟫⟫ Ins3k SIk SIk SIk Sk )
16136, 71, 61otkelins3k 4256 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (⟪{{{{{{x}}}}}}, ⟪{{{c}}}, ⟪{b}, n⟫⟫⟫ Ins3k SIk SIk SIk Sk ↔ ⟪{{{{x}}}}, {{{c}}}⟫ SIk SIk SIk Sk )
162152, 108opksnelsik 4265 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 (⟪{{{{x}}}}, {{{c}}}⟫ SIk SIk SIk Sk ↔ ⟪{{{x}}}, {{c}}⟫ SIk SIk Sk )
163139, 98opksnelsik 4265 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 (⟪{{{x}}}, {{c}}⟫ SIk SIk Sk ↔ ⟪{{x}}, {c}⟫ SIk Sk )
164141, 100opksnelsik 4265 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 (⟪{{x}}, {c}⟫ SIk Sk ↔ ⟪{x}, c Sk )
1653, 100elssetk 4270 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 (⟪{x}, c Skx c)
166164, 165bitri 240 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 (⟪{{x}}, {c}⟫ SIk Skx c)
167162, 163, 1663bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (⟪{{{{x}}}}, {{{c}}}⟫ SIk SIk SIk Skx c)
168160, 161, 1673bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (⟪{{{{{{{{x}}}}}}}}, ⟪{{{{{a}}}}}, ⟪{{{c}}}, ⟪{b}, n⟫⟫⟫⟫ Ins2k Ins3k SIk SIk SIk Skx c)
169159, 168orbi12i 507 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((⟪{{{{{{{{x}}}}}}}}, ⟪{{{{{a}}}}}, ⟪{{{c}}}, ⟪{b}, n⟫⟫⟫⟫ Ins3k SIk SIk SIk SIk SIk Sk ⟪{{{{{{{{x}}}}}}}}, ⟪{{{{{a}}}}}, ⟪{{{c}}}, ⟪{b}, n⟫⟫⟫⟫ Ins2k Ins3k SIk SIk SIk Sk ) ↔ (x a x c))
170 elun 3220 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (⟪{{{{{{{{x}}}}}}}}, ⟪{{{{{a}}}}}, ⟪{{{c}}}, ⟪{b}, n⟫⟫⟫⟫ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk ) ↔ (⟪{{{{{{{{x}}}}}}}}, ⟪{{{{{a}}}}}, ⟪{{{c}}}, ⟪{b}, n⟫⟫⟫⟫ Ins3k SIk SIk SIk SIk SIk Sk ⟪{{{{{{{{x}}}}}}}}, ⟪{{{{{a}}}}}, ⟪{{{c}}}, ⟪{b}, n⟫⟫⟫⟫ Ins2k Ins3k SIk SIk SIk Sk ))
171 elun 3220 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (x (ac) ↔ (x a x c))
172169, 170, 1713bitr4i 268 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (⟪{{{{{{{{x}}}}}}}}, ⟪{{{{{a}}}}}, ⟪{{{c}}}, ⟪{b}, n⟫⟫⟫⟫ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk ) ↔ x (ac))
173146, 172bibi12i 306 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((⟪{{{{{{{{x}}}}}}}}, ⟪{{{{{a}}}}}, ⟪{{{c}}}, ⟪{b}, n⟫⟫⟫⟫ Ins2k Ins2k Ins3k SIk Sk ↔ ⟪{{{{{{{{x}}}}}}}}, ⟪{{{{{a}}}}}, ⟪{{{c}}}, ⟪{b}, n⟫⟫⟫⟫ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) ↔ (x bx (ac)))
174173notbii 287 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (¬ (⟪{{{{{{{{x}}}}}}}}, ⟪{{{{{a}}}}}, ⟪{{{c}}}, ⟪{b}, n⟫⟫⟫⟫ Ins2k Ins2k Ins3k SIk Sk ↔ ⟪{{{{{{{{x}}}}}}}}, ⟪{{{{{a}}}}}, ⟪{{{c}}}, ⟪{b}, n⟫⟫⟫⟫ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) ↔ ¬ (x bx (ac)))
175134, 135, 1743bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (t(t = {{{{{{{{x}}}}}}}} t, ⟪{{{{{a}}}}}, ⟪{{{c}}}, ⟪{b}, n⟫⟫⟫⟫ ( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk ))) ↔ ¬ (x bx (ac)))
176175exbii 1582 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (xt(t = {{{{{{{{x}}}}}}}} t, ⟪{{{{{a}}}}}, ⟪{{{c}}}, ⟪{b}, n⟫⟫⟫⟫ ( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk ))) ↔ x ¬ (x bx (ac)))
177122, 130, 1763bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (⟪{{{{{a}}}}}, ⟪{{{c}}}, ⟪{b}, n⟫⟫⟫ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c) ↔ x ¬ (x bx (ac)))
178177notbii 287 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (¬ ⟪{{{{{a}}}}}, ⟪{{{c}}}, ⟪{b}, n⟫⟫⟫ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c) ↔ ¬ x ¬ (x bx (ac)))
179121elcompl 3225 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (⟪{{{{{a}}}}}, ⟪{{{c}}}, ⟪{b}, n⟫⟫⟫ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c) ↔ ¬ ⟪{{{{{a}}}}}, ⟪{{{c}}}, ⟪{b}, n⟫⟫⟫ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))
180 dfcleq 2347 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (b = (ac) ↔ x(x bx (ac)))
181 alex 1572 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (x(x bx (ac)) ↔ ¬ x ¬ (x bx (ac)))
182180, 181bitri 240 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (b = (ac) ↔ ¬ x ¬ (x bx (ac)))
183178, 179, 1823bitr4i 268 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (⟪{{{{{a}}}}}, ⟪{{{c}}}, ⟪{b}, n⟫⟫⟫ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c) ↔ b = (ac))
184120, 183anbi12i 678 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((⟪{{{{{a}}}}}, ⟪{{{c}}}, ⟪{b}, n⟫⟫⟫ Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ⟪{{{{{a}}}}}, ⟪{{{c}}}, ⟪{b}, n⟫⟫⟫ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c)) ↔ ((ac) = b = (ac)))
185105, 184bitri 240 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (⟪{{{{{a}}}}}, ⟪{{{c}}}, ⟪{b}, n⟫⟫⟫ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c)) ↔ ((ac) = b = (ac)))
186104, 185anbi12i 678 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((⟪{{{{{a}}}}}, ⟪{{{c}}}, ⟪{b}, n⟫⟫⟫ ( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ⟪{{{{{a}}}}}, ⟪{{{c}}}, ⟪{b}, n⟫⟫⟫ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) ↔ ((a n c n) ((ac) = b = (ac))))
18789, 90, 1863bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (t(t = {{{{{a}}}}} t, ⟪{{{c}}}, ⟪{b}, n⟫⟫⟫ (( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c)))) ↔ ((a n c n) ((ac) = b = (ac))))
188187exbii 1582 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (at(t = {{{{{a}}}}} t, ⟪{{{c}}}, ⟪{b}, n⟫⟫⟫ (( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c)))) ↔ a((a n c n) ((ac) = b = (ac))))
18974, 85, 1883bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (t(t = {{{c}}} t, ⟪{b}, n⟫⟫ ((( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c)) ↔ a((a n c n) ((ac) = b = (ac))))
190189exbii 1582 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (ct(t = {{{c}}} t, ⟪{b}, n⟫⟫ ((( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c)) ↔ ca((a n c n) ((ac) = b = (ac))))
19162, 70, 1903bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (⟪{b}, n (((( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c) “k 111c) ↔ ca((a n c n) ((ac) = b = (ac))))
192 eladdc 4398 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (b (n +c n) ↔ a n c n ((ac) = b = (ac)))
193 r2ex 2652 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (a n c n ((ac) = b = (ac)) ↔ ac((a n c n) ((ac) = b = (ac))))
194 excom 1741 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (ac((a n c n) ((ac) = b = (ac))) ↔ ca((a n c n) ((ac) = b = (ac))))
195192, 193, 1943bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (b (n +c n) ↔ ca((a n c n) ((ac) = b = (ac))))
196191, 195bitr4i 243 . . . . . . . . . . . . . . . . . . . . . . . . 25 (⟪{b}, n (((( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c) “k 111c) ↔ b (n +c n))
19758, 60, 1963bitri 262 . . . . . . . . . . . . . . . . . . . . . . . 24 (⟪{{{{{b}}}}}, ⟪{{{{x}}}}, ⟪{a}, n⟫⟫⟫ Ins2k Ins2k (((( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c) “k 111c) ↔ b (n +c n))
19857, 36, 26otkelins3k 4256 . . . . . . . . . . . . . . . . . . . . . . . . 25 (⟪{{{{{b}}}}}, ⟪{{{{x}}}}, ⟪{a}, n⟫⟫⟫ Ins3k k SIk SIk SIkSk ↔ ⟪{{{b}}}, {{{{x}}}}⟫ k SIk SIk SIkSk )
19957, 36opkelcnvk 4250 . . . . . . . . . . . . . . . . . . . . . . . . 25 (⟪{{{b}}}, {{{{x}}}}⟫ k SIk SIk SIkSk ↔ ⟪{{{{x}}}}, {{{b}}}⟫ SIk SIk SIkSk )
200 snex 4111 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 {{b}} V
201152, 200opksnelsik 4265 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (⟪{{{{x}}}}, {{{b}}}⟫ SIk SIk SIkSk ↔ ⟪{{{x}}}, {{b}}⟫ SIk SIkSk )
202139, 59opksnelsik 4265 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (⟪{{{x}}}, {{b}}⟫ SIk SIkSk ↔ ⟪{{x}}, {b}⟫ SIkSk )
203141, 142opksnelsik 4265 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (⟪{{x}}, {b}⟫ SIkSk ↔ ⟪{x}, bSk )
204144notbii 287 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (¬ ⟪{x}, b Sk ↔ ¬ x b)
205 opkex 4113 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⟪{x}, b V
206205elcompl 3225 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (⟪{x}, bSk ↔ ¬ ⟪{x}, b Sk )
2073elcompl 3225 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (x b ↔ ¬ x b)
208204, 206, 2073bitr4i 268 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (⟪{x}, bSkx b)
209203, 208bitri 240 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (⟪{{x}}, {b}⟫ SIkSkx b)
210201, 202, 2093bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . 25 (⟪{{{{x}}}}, {{{b}}}⟫ SIk SIk SIkSkx b)
211198, 199, 2103bitri 262 . . . . . . . . . . . . . . . . . . . . . . . 24 (⟪{{{{{b}}}}}, ⟪{{{{x}}}}, ⟪{a}, n⟫⟫⟫ Ins3k k SIk SIk SIkSkx b)
212197, 211anbi12i 678 . . . . . . . . . . . . . . . . . . . . . . 23 ((⟪{{{{{b}}}}}, ⟪{{{{x}}}}, ⟪{a}, n⟫⟫⟫ Ins2k Ins2k (((( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c) “k 111c) ⟪{{{{{b}}}}}, ⟪{{{{x}}}}, ⟪{a}, n⟫⟫⟫ Ins3k k SIk SIk SIkSk ) ↔ (b (n +c n) x b))
21356, 212bitri 240 . . . . . . . . . . . . . . . . . . . . . 22 (⟪{{{{{b}}}}}, ⟪{{{{x}}}}, ⟪{a}, n⟫⟫⟫ ( Ins2k Ins2k (((( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c) “k 111c) ∩ Ins3k k SIk SIk SIkSk ) ↔ (b (n +c n) x b))
214 opkex 4113 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ⟪{{{{{b}}}}}, ⟪{{{{x}}}}, ⟪{a}, n⟫⟫⟫ V
215214elimak 4259 . . . . . . . . . . . . . . . . . . . . . . . . 25 (⟪{{{{{b}}}}}, ⟪{{{{x}}}}, ⟪{a}, n⟫⟫⟫ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k Ik )) “k 11111111c) ↔ t 1 1111111ct, ⟪{{{{{b}}}}}, ⟪{{{{x}}}}, ⟪{a}, n⟫⟫⟫⟫ ( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k Ik )))
216 elpw171c 4153 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (t 11111111cy t = {{{{{{{{y}}}}}}}})
217216anbi1i 676 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((t 11111111c t, ⟪{{{{{b}}}}}, ⟪{{{{x}}}}, ⟪{a}, n⟫⟫⟫⟫ ( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k Ik ))) ↔ (y t = {{{{{{{{y}}}}}}}} t, ⟪{{{{{b}}}}}, ⟪{{{{x}}}}, ⟪{a}, n⟫⟫⟫⟫ ( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k Ik ))))
218 19.41v 1901 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (y(t = {{{{{{{{y}}}}}}}} t, ⟪{{{{{b}}}}}, ⟪{{{{x}}}}, ⟪{a}, n⟫⟫⟫⟫ ( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k Ik ))) ↔ (y t = {{{{{{{{y}}}}}}}} t, ⟪{{{{{b}}}}}, ⟪{{{{x}}}}, ⟪{a}, n⟫⟫⟫⟫ ( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k Ik ))))
219217, 218bitr4i 243 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((t 11111111c t, ⟪{{{{{b}}}}}, ⟪{{{{x}}}}, ⟪{a}, n⟫⟫⟫⟫ ( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k Ik ))) ↔ y(t = {{{{{{{{y}}}}}}}} t, ⟪{{{{{b}}}}}, ⟪{{{{x}}}}, ⟪{a}, n⟫⟫⟫⟫ ( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k Ik ))))
220219exbii 1582 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (t(t 11111111c t, ⟪{{{{{b}}}}}, ⟪{{{{x}}}}, ⟪{a}, n⟫⟫⟫⟫ ( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k Ik ))) ↔ ty(t = {{{{{{{{y}}}}}}}} t, ⟪{{{{{b}}}}}, ⟪{{{{x}}}}, ⟪{a}, n⟫⟫⟫⟫ ( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k Ik ))))
221 df-rex 2620 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (t 1 1111111ct, ⟪{{{{{b}}}}}, ⟪{{{{x}}}}, ⟪{a}, n⟫⟫⟫⟫ ( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k Ik )) ↔ t(t 11111111c t, ⟪{{{{{b}}}}}, ⟪{{{{x}}}}, ⟪{a}, n⟫⟫⟫⟫ ( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k Ik ))))
222 excom 1741 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (yt(t = {{{{{{{{y}}}}}}}} t, ⟪{{{{{b}}}}}, ⟪{{{{x}}}}, ⟪{a}, n⟫⟫⟫⟫ ( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k Ik ))) ↔ ty(t = {{{{{{{{y}}}}}}}} t, ⟪{{{{{b}}}}}, ⟪{{{{x}}}}, ⟪{a}, n⟫⟫⟫⟫ ( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k Ik ))))
223220, 221, 2223bitr4i 268 . . . . . . . . . . . . . . . . . . . . . . . . 25 (t 1 1111111ct, ⟪{{{{{b}}}}}, ⟪{{{{x}}}}, ⟪{a}, n⟫⟫⟫⟫ ( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k Ik )) ↔ yt(t = {{{{{{{{y}}}}}}}} t, ⟪{{{{{b}}}}}, ⟪{{{{x}}}}, ⟪{a}, n⟫⟫⟫⟫ ( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k Ik ))))
224 snex 4111 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 {{{{{{{{y}}}}}}}} V
225 opkeq1 4059 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (t = {{{{{{{{y}}}}}}}} → ⟪t, ⟪{{{{{b}}}}}, ⟪{{{{x}}}}, ⟪{a}, n⟫⟫⟫⟫ = ⟪{{{{{{{{y}}}}}}}}, ⟪{{{{{b}}}}}, ⟪{{{{x}}}}, ⟪{a}, n⟫⟫⟫⟫)
226225eleq1d 2419 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (t = {{{{{{{{y}}}}}}}} → (⟪t, ⟪{{{{{b}}}}}, ⟪{{{{x}}}}, ⟪{a}, n⟫⟫⟫⟫ ( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k Ik )) ↔ ⟪{{{{{{{{y}}}}}}}}, ⟪{{{{{b}}}}}, ⟪{{{{x}}}}, ⟪{a}, n⟫⟫⟫⟫ ( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k Ik ))))
227224, 226ceqsexv 2894 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (t(t = {{{{{{{{y}}}}}}}} t, ⟪{{{{{b}}}}}, ⟪{{{{x}}}}, ⟪{a}, n⟫⟫⟫⟫ ( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k Ik ))) ↔ ⟪{{{{{{{{y}}}}}}}}, ⟪{{{{{b}}}}}, ⟪{{{{x}}}}, ⟪{a}, n⟫⟫⟫⟫ ( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k Ik )))
228 elsymdif 3223 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (⟪{{{{{{{{y}}}}}}}}, ⟪{{{{{b}}}}}, ⟪{{{{x}}}}, ⟪{a}, n⟫⟫⟫⟫ ( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k Ik )) ↔ ¬ (⟪{{{{{{{{y}}}}}}}}, ⟪{{{{{b}}}}}, ⟪{{{{x}}}}, ⟪{a}, n⟫⟫⟫⟫ Ins2k Ins2k Ins3k SIk Sk ↔ ⟪{{{{{{{{y}}}}}}}}, ⟪{{{{{b}}}}}, ⟪{{{{x}}}}, ⟪{a}, n⟫⟫⟫⟫ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k Ik )))
229 snex 4111 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 {{{{{{y}}}}}} V
230229, 51, 40otkelins2k 4255 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (⟪{{{{{{{{y}}}}}}}}, ⟪{{{{{b}}}}}, ⟪{{{{x}}}}, ⟪{a}, n⟫⟫⟫⟫ Ins2k Ins2k Ins3k SIk Sk ↔ ⟪{{{{{{y}}}}}}, ⟪{{{{x}}}}, ⟪{a}, n⟫⟫⟫ Ins2k Ins3k SIk Sk )
231 snex 4111 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 {{{{y}}}} V
232231, 36, 26otkelins2k 4255 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (⟪{{{{{{y}}}}}}, ⟪{{{{x}}}}, ⟪{a}, n⟫⟫⟫ Ins2k Ins3k SIk Sk ↔ ⟪{{{{y}}}}, ⟪{a}, n⟫⟫ Ins3k SIk Sk )
233 snex 4111 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 {{y}} V
234233, 20, 21otkelins3k 4256 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (⟪{{{{y}}}}, ⟪{a}, n⟫⟫ Ins3k SIk Sk ↔ ⟪{{y}}, {a}⟫ SIk Sk )
235 snex 4111 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 {y} V
236235, 23opksnelsik 4265 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (⟪{{y}}, {a}⟫ SIk Sk ↔ ⟪{y}, a Sk )
237 vex 2862 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 y V
238237, 23elssetk 4270 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (⟪{y}, a Sky a)
239234, 236, 2383bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (⟪{{{{y}}}}, ⟪{a}, n⟫⟫ Ins3k SIk Sky a)
240230, 232, 2393bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (⟪{{{{{{{{y}}}}}}}}, ⟪{{{{{b}}}}}, ⟪{{{{x}}}}, ⟪{a}, n⟫⟫⟫⟫ Ins2k Ins2k Ins3k SIk Sky a)
241229, 51, 40otkelins3k 4256 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (⟪{{{{{{{{y}}}}}}}}, ⟪{{{{{b}}}}}, ⟪{{{{x}}}}, ⟪{a}, n⟫⟫⟫⟫ Ins3k SIk SIk SIk SIk SIk Sk ↔ ⟪{{{{{{y}}}}}}, {{{{{b}}}}}⟫ SIk SIk SIk SIk SIk Sk )
242 snex 4111 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 {{{{{y}}}}} V
243 snex 4111 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 {{{{b}}}} V
244242, 243opksnelsik 4265 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (⟪{{{{{{y}}}}}}, {{{{{b}}}}}⟫ SIk SIk SIk SIk SIk Sk ↔ ⟪{{{{{y}}}}}, {{{{b}}}}⟫ SIk SIk SIk SIk Sk )
245231, 57opksnelsik 4265 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (⟪{{{{{y}}}}}, {{{{b}}}}⟫ SIk SIk SIk SIk Sk ↔ ⟪{{{{y}}}}, {{{b}}}⟫ SIk SIk SIk Sk )
246 snex 4111 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 {{{y}}} V
247246, 200opksnelsik 4265 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (⟪{{{{y}}}}, {{{b}}}⟫ SIk SIk SIk Sk ↔ ⟪{{{y}}}, {{b}}⟫ SIk SIk Sk )
248233, 59opksnelsik 4265 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (⟪{{{y}}}, {{b}}⟫ SIk SIk Sk ↔ ⟪{{y}}, {b}⟫ SIk Sk )
249235, 142opksnelsik 4265 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (⟪{{y}}, {b}⟫ SIk Sk ↔ ⟪{y}, b Sk )
250237, 142elssetk 4270 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (⟪{y}, b Sky b)
251248, 249, 2503bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (⟪{{{y}}}, {{b}}⟫ SIk SIk Sky b)
252245, 247, 2513bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (⟪{{{{{y}}}}}, {{{{b}}}}⟫ SIk SIk SIk SIk Sky b)
253241, 244, 2523bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (⟪{{{{{{{{y}}}}}}}}, ⟪{{{{{b}}}}}, ⟪{{{{x}}}}, ⟪{a}, n⟫⟫⟫⟫ Ins3k SIk SIk SIk SIk SIk Sky b)
254229, 51, 40otkelins2k 4255 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (⟪{{{{{{{{y}}}}}}}}, ⟪{{{{{b}}}}}, ⟪{{{{x}}}}, ⟪{a}, n⟫⟫⟫⟫ Ins2k Ins3k Ik ↔ ⟪{{{{{{y}}}}}}, ⟪{{{{x}}}}, ⟪{a}, n⟫⟫⟫ Ins3k Ik )
255231, 36, 26otkelins3k 4256 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (⟪{{{{{{y}}}}}}, ⟪{{{{x}}}}, ⟪{a}, n⟫⟫⟫ Ins3k Ik ↔ ⟪{{{{y}}}}, {{{{x}}}}⟫ Ik )
256246sneqb 3876 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ({{{{y}}}} = {{{{x}}}} ↔ {{{y}}} = {{{x}}})
257233sneqb 3876 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ({{{y}}} = {{{x}}} ↔ {{y}} = {{x}})
258235sneqb 3876 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ({{y}} = {{x}} ↔ {y} = {x})
259237sneqb 3876 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ({y} = {x} ↔ y = x)
260258, 259bitri 240 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ({{y}} = {{x}} ↔ y = x)
261256, 257, 2603bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ({{{{y}}}} = {{{{x}}}} ↔ y = x)
262 opkelidkg 4274 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (({{{{y}}}} V {{{{x}}}} V) → (⟪{{{{y}}}}, {{{{x}}}}⟫ Ik ↔ {{{{y}}}} = {{{{x}}}}))
263231, 36, 262mp2an 653 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (⟪{{{{y}}}}, {{{{x}}}}⟫ Ik ↔ {{{{y}}}} = {{{{x}}}})
264237elsnc 3756 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (y {x} ↔ y = x)
265261, 263, 2643bitr4i 268 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (⟪{{{{y}}}}, {{{{x}}}}⟫ Iky {x})
266254, 255, 2653bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (⟪{{{{{{{{y}}}}}}}}, ⟪{{{{{b}}}}}, ⟪{{{{x}}}}, ⟪{a}, n⟫⟫⟫⟫ Ins2k Ins3k Iky {x})
267253, 266orbi12i 507 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((⟪{{{{{{{{y}}}}}}}}, ⟪{{{{{b}}}}}, ⟪{{{{x}}}}, ⟪{a}, n⟫⟫⟫⟫ Ins3k SIk SIk SIk SIk SIk Sk ⟪{{{{{{{{y}}}}}}}}, ⟪{{{{{b}}}}}, ⟪{{{{x}}}}, ⟪{a}, n⟫⟫⟫⟫ Ins2k Ins3k Ik ) ↔ (y b y {x}))
268 elun 3220 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (⟪{{{{{{{{y}}}}}}}}, ⟪{{{{{b}}}}}, ⟪{{{{x}}}}, ⟪{a}, n⟫⟫⟫⟫ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k Ik ) ↔ (⟪{{{{{{{{y}}}}}}}}, ⟪{{{{{b}}}}}, ⟪{{{{x}}}}, ⟪{a}, n⟫⟫⟫⟫ Ins3k SIk SIk SIk SIk SIk Sk ⟪{{{{{{{{y}}}}}}}}, ⟪{{{{{b}}}}}, ⟪{{{{x}}}}, ⟪{a}, n⟫⟫⟫⟫ Ins2k Ins3k Ik ))
269 elun 3220 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (y (b ∪ {x}) ↔ (y b y {x}))
270267, 268, 2693bitr4i 268 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (⟪{{{{{{{{y}}}}}}}}, ⟪{{{{{b}}}}}, ⟪{{{{x}}}}, ⟪{a}, n⟫⟫⟫⟫ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k Ik ) ↔ y (b ∪ {x}))
271240, 270bibi12i 306 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((⟪{{{{{{{{y}}}}}}}}, ⟪{{{{{b}}}}}, ⟪{{{{x}}}}, ⟪{a}, n⟫⟫⟫⟫ Ins2k Ins2k Ins3k SIk Sk ↔ ⟪{{{{{{{{y}}}}}}}}, ⟪{{{{{b}}}}}, ⟪{{{{x}}}}, ⟪{a}, n⟫⟫⟫⟫ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k Ik )) ↔ (y ay (b ∪ {x})))
272271notbii 287 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (¬ (⟪{{{{{{{{y}}}}}}}}, ⟪{{{{{b}}}}}, ⟪{{{{x}}}}, ⟪{a}, n⟫⟫⟫⟫ Ins2k Ins2k Ins3k SIk Sk ↔ ⟪{{{{{{{{y}}}}}}}}, ⟪{{{{{b}}}}}, ⟪{{{{x}}}}, ⟪{a}, n⟫⟫⟫⟫ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k Ik )) ↔ ¬ (y ay (b ∪ {x})))
273227, 228, 2723bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (t(t = {{{{{{{{y}}}}}}}} t, ⟪{{{{{b}}}}}, ⟪{{{{x}}}}, ⟪{a}, n⟫⟫⟫⟫ ( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k Ik ))) ↔ ¬ (y ay (b ∪ {x})))
274273exbii 1582 . . . . . . . . . . . . . . . . . . . . . . . . 25 (yt(t = {{{{{{{{y}}}}}}}} t, ⟪{{{{{b}}}}}, ⟪{{{{x}}}}, ⟪{a}, n⟫⟫⟫⟫ ( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k Ik ))) ↔ y ¬ (y ay (b ∪ {x})))
275215, 223, 2743bitri 262 . . . . . . . . . . . . . . . . . . . . . . . 24 (⟪{{{{{b}}}}}, ⟪{{{{x}}}}, ⟪{a}, n⟫⟫⟫ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k Ik )) “k 11111111c) ↔ y ¬ (y ay (b ∪ {x})))
276275notbii 287 . . . . . . . . . . . . . . . . . . . . . . 23 (¬ ⟪{{{{{b}}}}}, ⟪{{{{x}}}}, ⟪{a}, n⟫⟫⟫ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k Ik )) “k 11111111c) ↔ ¬ y ¬ (y ay (b ∪ {x})))
277214elcompl 3225 . . . . . . . . . . . . . . . . . . . . . . 23 (⟪{{{{{b}}}}}, ⟪{{{{x}}}}, ⟪{a}, n⟫⟫⟫ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k Ik )) “k 11111111c) ↔ ¬ ⟪{{{{{b}}}}}, ⟪{{{{x}}}}, ⟪{a}, n⟫⟫⟫ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k Ik )) “k 11111111c))
278 dfcleq 2347 . . . . . . . . . . . . . . . . . . . . . . . 24 (a = (b ∪ {x}) ↔ y(y ay (b ∪ {x})))
279 alex 1572 . . . . . . . . . . . . . . . . . . . . . . . 24 (y(y ay (b ∪ {x})) ↔ ¬ y ¬ (y ay (b ∪ {x})))
280278, 279bitri 240 . . . . . . . . . . . . . . . . . . . . . . 23 (a = (b ∪ {x}) ↔ ¬ y ¬ (y ay (b ∪ {x})))
281276, 277, 2803bitr4i 268 . . . . . . . . . . . . . . . . . . . . . 22 (⟪{{{{{b}}}}}, ⟪{{{{x}}}}, ⟪{a}, n⟫⟫⟫ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k Ik )) “k 11111111c) ↔ a = (b ∪ {x}))
282213, 281anbi12i 678 . . . . . . . . . . . . . . . . . . . . 21 ((⟪{{{{{b}}}}}, ⟪{{{{x}}}}, ⟪{a}, n⟫⟫⟫ ( Ins2k Ins2k (((( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c) “k 111c) ∩ Ins3k k SIk SIk SIkSk ) ⟪{{{{{b}}}}}, ⟪{{{{x}}}}, ⟪{a}, n⟫⟫⟫ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k Ik )) “k 11111111c)) ↔ ((b (n +c n) x b) a = (b ∪ {x})))
28354, 55, 2823bitri 262 . . . . . . . . . . . . . . . . . . . 20 (t(t = {{{{{b}}}}} t, ⟪{{{{x}}}}, ⟪{a}, n⟫⟫⟫ (( Ins2k Ins2k (((( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c) “k 111c) ∩ Ins3k k SIk SIk SIkSk ) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k Ik )) “k 11111111c))) ↔ ((b (n +c n) x b) a = (b ∪ {x})))
284283exbii 1582 . . . . . . . . . . . . . . . . . . 19 (bt(t = {{{{{b}}}}} t, ⟪{{{{x}}}}, ⟪{a}, n⟫⟫⟫ (( Ins2k Ins2k (((( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c) “k 111c) ∩ Ins3k k SIk SIk SIkSk ) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k Ik )) “k 11111111c))) ↔ b((b (n +c n) x b) a = (b ∪ {x})))
28539, 50, 2843bitri 262 . . . . . . . . . . . . . . . . . 18 (t(t = {{{{x}}}} t, ⟪{a}, n⟫⟫ ((( Ins2k Ins2k (((( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c) “k 111c) ∩ Ins3k k SIk SIk SIkSk ) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k Ik )) “k 11111111c)) “k 11111c)) ↔ b((b (n +c n) x b) a = (b ∪ {x})))
286285exbii 1582 . . . . . . . . . . . . . . . . 17 (xt(t = {{{{x}}}} t, ⟪{a}, n⟫⟫ ((( Ins2k Ins2k (((( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c) “k 111c) ∩ Ins3k k SIk SIk SIkSk ) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k Ik )) “k 11111111c)) “k 11111c)) ↔ xb((b (n +c n) x b) a = (b ∪ {x})))
28727, 35, 2863bitri 262 . . . . . . . . . . . . . . . 16 (⟪{a}, n (((( Ins2k Ins2k (((( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c) “k 111c) ∩ Ins3k k SIk SIk SIkSk ) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k Ik )) “k 11111111c)) “k 11111c) “k 1111c) ↔ xb((b (n +c n) x b) a = (b ∪ {x})))
28820, 21, 3otkelins3k 4256 . . . . . . . . . . . . . . . 16 (⟪{{{a}}}, ⟪n, x⟫⟫ Ins3k (((( Ins2k Ins2k (((( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c) “k 111c) ∩ Ins3k k SIk SIk SIkSk ) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k Ik )) “k 11111111c)) “k 11111c) “k 1111c) ↔ ⟪{a}, n (((( Ins2k Ins2k (((( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c) “k 111c) ∩ Ins3k k SIk SIk SIkSk ) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k Ik )) “k 11111111c)) “k 11111c) “k 1111c))
289 elsuc 4413 . . . . . . . . . . . . . . . . 17 (a ((n +c n) +c 1c) ↔ b (n +c n)x ba = (b ∪ {x}))
290 r2ex 2652 . . . . . . . . . . . . . . . . 17 (b (n +c n)x ba = (b ∪ {x}) ↔ bx((b (n +c n) x b) a = (b ∪ {x})))
291 excom 1741 . . . . . . . . . . . . . . . . 17 (bx((b (n +c n) x b) a = (b ∪ {x})) ↔ xb((b (n +c n) x b) a = (b ∪ {x})))
292289, 290, 2913bitri 262 . . . . . . . . . . . . . . . 16 (a ((n +c n) +c 1c) ↔ xb((b (n +c n) x b) a = (b ∪ {x})))
293287, 288, 2923bitr4i 268 . . . . . . . . . . . . . . 15 (⟪{{{a}}}, ⟪n, x⟫⟫ Ins3k (((( Ins2k Ins2k (((( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c) “k 111c) ∩ Ins3k k SIk SIk SIkSk ) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k Ik )) “k 11111111c)) “k 11111c) “k 1111c) ↔ a ((n +c n) +c 1c))
29425, 293bibi12i 306 . . . . . . . . . . . . . 14 ((⟪{{{a}}}, ⟪n, x⟫⟫ Ins2k Sk ↔ ⟪{{{a}}}, ⟪n, x⟫⟫ Ins3k (((( Ins2k Ins2k (((( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c) “k 111c) ∩ Ins3k k SIk SIk SIkSk ) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k Ik )) “k 11111111c)) “k 11111c) “k 1111c)) ↔ (a xa ((n +c n) +c 1c)))
295294notbii 287 . . . . . . . . . . . . 13 (¬ (⟪{{{a}}}, ⟪n, x⟫⟫ Ins2k Sk ↔ ⟪{{{a}}}, ⟪n, x⟫⟫ Ins3k (((( Ins2k Ins2k (((( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c) “k 111c) ∩ Ins3k k SIk SIk SIkSk ) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k Ik )) “k 11111111c)) “k 11111c) “k 1111c)) ↔ ¬ (a xa ((n +c n) +c 1c)))
29618, 19, 2953bitri 262 . . . . . . . . . . . 12 (t(t = {{{a}}} t, ⟪n, x⟫⟫ ( Ins2k SkIns3k (((( Ins2k Ins2k (((( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c) “k 111c) ∩ Ins3k k SIk SIk SIkSk ) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k Ik )) “k 11111111c)) “k 11111c) “k 1111c))) ↔ ¬ (a xa ((n +c n) +c 1c)))
297296exbii 1582 . . . . . . . . . . 11 (at(t = {{{a}}} t, ⟪n, x⟫⟫ ( Ins2k SkIns3k (((( Ins2k Ins2k (((( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c) “k 111c) ∩ Ins3k k SIk SIk SIkSk ) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k Ik )) “k 11111111c)) “k 11111c) “k 1111c))) ↔ a ¬ (a xa ((n +c n) +c 1c)))
2986, 14, 2973bitri 262 . . . . . . . . . 10 (⟪n, x (( Ins2k SkIns3k (((( Ins2k Ins2k (((( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c) “k 111c) ∩ Ins3k k SIk SIk SIkSk ) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k Ik )) “k 11111111c)) “k 11111c) “k 1111c)) “k 111c) ↔ a ¬ (a xa ((n +c n) +c 1c)))
299298notbii 287 . . . . . . . . 9 (¬ ⟪n, x (( Ins2k SkIns3k (((( Ins2k Ins2k (((( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c) “k 111c) ∩ Ins3k k SIk SIk SIkSk ) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k Ik )) “k 11111111c)) “k 11111c) “k 1111c)) “k 111c) ↔ ¬ a ¬ (a xa ((n +c n) +c 1c)))
3005elcompl 3225 . . . . . . . . 9 (⟪n, x ∼ (( Ins2k SkIns3k (((( Ins2k Ins2k (((( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c) “k 111c) ∩ Ins3k k SIk SIk SIkSk ) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k Ik )) “k 11111111c)) “k 11111c) “k 1111c)) “k 111c) ↔ ¬ ⟪n, x (( Ins2k SkIns3k (((( Ins2k Ins2k (((( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c) “k 111c) ∩ Ins3k k SIk SIk SIkSk ) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k Ik )) “k 11111111c)) “k 11111c) “k 1111c)) “k 111c))
301 dfcleq 2347 . . . . . . . . . 10 (x = ((n +c n) +c 1c) ↔ a(a xa ((n +c n) +c 1c)))
302 alex 1572 . . . . . . . . . 10 (a(a xa ((n +c n) +c 1c)) ↔ ¬ a ¬ (a xa ((n +c n) +c 1c)))
303301, 302bitri 240 . . . . . . . . 9 (x = ((n +c n) +c 1c) ↔ ¬ a ¬ (a xa ((n +c n) +c 1c)))
304299, 300, 3033bitr4i 268 . . . . . . . 8 (⟪n, x ∼ (( Ins2k SkIns3k (((( Ins2k Ins2k (((( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c) “k 111c) ∩ Ins3k k SIk SIk SIkSk ) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k Ik )) “k 11111111c)) “k 11111c) “k 1111c)) “k 111c) ↔ x = ((n +c n) +c 1c))
305304rexbii 2639 . . . . . . 7 (n Nnn, x ∼ (( Ins2k SkIns3k (((( Ins2k Ins2k (((( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c) “k 111c) ∩ Ins3k k SIk SIk SIkSk ) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k Ik )) “k 11111111c)) “k 11111c) “k 1111c)) “k 111c) ↔ n Nn x = ((n +c n) +c 1c))
3064, 305bitri 240 . . . . . 6 (x ( ∼ (( Ins2k SkIns3k (((( Ins2k Ins2k (((( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c) “k 111c) ∩ Ins3k k SIk SIk SIkSk ) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k Ik )) “k 11111111c)) “k 11111c) “k 1111c)) “k 111c) “k Nn ) ↔ n Nn x = ((n +c n) +c 1c))
307306anbi1i 676 . . . . 5 ((x ( ∼ (( Ins2k SkIns3k (((( Ins2k Ins2k (((( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c) “k 111c) ∩ Ins3k k SIk SIk SIkSk ) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k Ik )) “k 11111111c)) “k 11111c) “k 1111c)) “k 111c) “k Nn ) x) ↔ (n Nn x = ((n +c n) +c 1c) x))
3082, 307bitri 240 . . . 4 (x (( ∼ (( Ins2k SkIns3k (((( Ins2k Ins2k (((( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c) “k 111c) ∩ Ins3k k SIk SIk SIkSk ) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k Ik )) “k 11111111c)) “k 11111c) “k 1111c)) “k 111c) “k Nn ) {}) ↔ (n Nn x = ((n +c n) +c 1c) x))
309308abbi2i 2464 . . 3 (( ∼ (( Ins2k SkIns3k (((( Ins2k Ins2k (((( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c) “k 111c) ∩ Ins3k k SIk SIk SIkSk ) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k Ik )) “k 11111111c)) “k 11111c) “k 1111c)) “k 111c) “k Nn ) {}) = {x (n Nn x = ((n +c n) +c 1c) x)}
3101, 309eqtr4i 2376 . 2 Oddfin = (( ∼ (( Ins2k SkIns3k (((( Ins2k Ins2k (((( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c) “k 111c) ∩ Ins3k k SIk SIk SIkSk ) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k Ik )) “k 11111111c)) “k 11111c) “k 1111c)) “k 111c) “k Nn ) {})
311 ssetkex 4294 . . . . . . . 8 Sk V
312311ins2kex 4307 . . . . . . 7 Ins2k Sk V
313312ins2kex 4307 . . . . . . . . . . . . . . . . . 18 Ins2k Ins2k Sk V
314 vvex 4109 . . . . . . . . . . . . . . . . . . 19 V V
315314, 312xpkex 4289 . . . . . . . . . . . . . . . . . 18 (V ×k Ins2k Sk ) V
316313, 315inex 4105 . . . . . . . . . . . . . . . . 17 ( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) V
317311ins3kex 4308 . . . . . . . . . . . . . . . . . . . . . . . . 25 Ins3k Sk V
318317, 312inex 4105 . . . . . . . . . . . . . . . . . . . . . . . 24 ( Ins3k SkIns2k Sk ) V
319 1cex 4142 . . . . . . . . . . . . . . . . . . . . . . . . . 26 1c V
320319pw1ex 4303 . . . . . . . . . . . . . . . . . . . . . . . . 25 11c V
321320pw1ex 4303 . . . . . . . . . . . . . . . . . . . . . . . 24 111c V
322318, 321imakex 4300 . . . . . . . . . . . . . . . . . . . . . . 23 (( Ins3k SkIns2k Sk ) “k 111c) V
323322complex 4104 . . . . . . . . . . . . . . . . . . . . . 22 ∼ (( Ins3k SkIns2k Sk ) “k 111c) V
324323sikex 4297 . . . . . . . . . . . . . . . . . . . . 21 SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) V
325324sikex 4297 . . . . . . . . . . . . . . . . . . . 20 SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) V
326325sikex 4297 . . . . . . . . . . . . . . . . . . 19 SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) V
327326ins3kex 4308 . . . . . . . . . . . . . . . . . 18 Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) V
328311sikex 4297 . . . . . . . . . . . . . . . . . . . . . . . 24 SIk Sk V
329328ins3kex 4308 . . . . . . . . . . . . . . . . . . . . . . 23 Ins3k SIk Sk V
330329ins2kex 4307 . . . . . . . . . . . . . . . . . . . . . 22 Ins2k Ins3k SIk Sk V
331330ins2kex 4307 . . . . . . . . . . . . . . . . . . . . 21 Ins2k Ins2k Ins3k SIk Sk V
332328sikex 4297 . . . . . . . . . . . . . . . . . . . . . . . . . 26 SIk SIk Sk V
333332sikex 4297 . . . . . . . . . . . . . . . . . . . . . . . . 25 SIk SIk SIk Sk V
334333sikex 4297 . . . . . . . . . . . . . . . . . . . . . . . 24 SIk SIk SIk SIk Sk V
335334sikex 4297 . . . . . . . . . . . . . . . . . . . . . . 23 SIk SIk SIk SIk SIk Sk V
336335ins3kex 4308 . . . . . . . . . . . . . . . . . . . . . 22 Ins3k SIk SIk SIk SIk SIk Sk V
337333ins3kex 4308 . . . . . . . . . . . . . . . . . . . . . . 23 Ins3k SIk SIk SIk Sk V
338337ins2kex 4307 . . . . . . . . . . . . . . . . . . . . . 22 Ins2k Ins3k SIk SIk SIk Sk V
339336, 338unex 4106 . . . . . . . . . . . . . . . . . . . . 21 ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk ) V
340331, 339symdifex 4108 . . . . . . . . . . . . . . . . . . . 20 ( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) V
341321pw1ex 4303 . . . . . . . . . . . . . . . . . . . . . . . 24 1111c V
342341pw1ex 4303 . . . . . . . . . . . . . . . . . . . . . . 23 11111c V
343342pw1ex 4303 . . . . . . . . . . . . . . . . . . . . . 22 111111c V
344343pw1ex 4303 . . . . . . . . . . . . . . . . . . . . 21 1111111c V
345344pw1ex 4303 . . . . . . . . . . . . . . . . . . . 20 11111111c V
346340, 345imakex 4300 . . . . . . . . . . . . . . . . . . 19 (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c) V
347346complex 4104 . . . . . . . . . . . . . . . . . 18 ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c) V
348327, 347inex 4105 . . . . . . . . . . . . . . . . 17 ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c)) V
349316, 348inex 4105 . . . . . . . . . . . . . . . 16 (( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) V
350349, 342imakex 4300 . . . . . . . . . . . . . . 15 ((( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c) V
351350, 321imakex 4300 . . . . . . . . . . . . . 14 (((( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c) “k 111c) V
352351ins2kex 4307 . . . . . . . . . . . . 13 Ins2k (((( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c) “k 111c) V
353352ins2kex 4307 . . . . . . . . . . . 12 Ins2k Ins2k (((( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c) “k 111c) V
354311complex 4104 . . . . . . . . . . . . . . . . 17 Sk V
355354sikex 4297 . . . . . . . . . . . . . . . 16 SIkSk V
356355sikex 4297 . . . . . . . . . . . . . . 15 SIk SIkSk V
357356sikex 4297 . . . . . . . . . . . . . 14 SIk SIk SIkSk V
358357cnvkex 4287 . . . . . . . . . . . . 13 k SIk SIk SIkSk V
359358ins3kex 4308 . . . . . . . . . . . 12 Ins3k k SIk SIk SIkSk V
360353, 359inex 4105 . . . . . . . . . . 11 ( Ins2k Ins2k (((( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c) “k 111c) ∩ Ins3k k SIk SIk SIkSk ) V
361 idkex 4314 . . . . . . . . . . . . . . . . 17 Ik V
362361ins3kex 4308 . . . . . . . . . . . . . . . 16 Ins3k Ik V
363362ins2kex 4307 . . . . . . . . . . . . . . 15 Ins2k Ins3k Ik V
364336, 363unex 4106 . . . . . . . . . . . . . 14 ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k Ik ) V
365331, 364symdifex 4108 . . . . . . . . . . . . 13 ( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k Ik )) V
366365, 345imakex 4300 . . . . . . . . . . . 12 (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k Ik )) “k 11111111c) V
367366complex 4104 . . . . . . . . . . 11 ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k Ik )) “k 11111111c) V
368360, 367inex 4105 . . . . . . . . . 10 (( Ins2k Ins2k (((( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c) “k 111c) ∩ Ins3k k SIk SIk SIkSk ) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k Ik )) “k 11111111c)) V
369368, 342imakex 4300 . . . . . . . . 9 ((( Ins2k Ins2k (((( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c) “k 111c) ∩ Ins3k k SIk SIk SIkSk ) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k Ik )) “k 11111111c)) “k 11111c) V
370369, 341imakex 4300 . . . . . . . 8 (((( Ins2k Ins2k (((( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c) “k 111c) ∩ Ins3k k SIk SIk SIkSk ) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k Ik )) “k 11111111c)) “k 11111c) “k 1111c) V
371370ins3kex 4308 . . . . . . 7 Ins3k (((( Ins2k Ins2k (((( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c) “k 111c) ∩ Ins3k k SIk SIk SIkSk ) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k Ik )) “k 11111111c)) “k 11111c) “k 1111c) V
372312, 371symdifex 4108 . . . . . 6 ( Ins2k SkIns3k (((( Ins2k Ins2k (((( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c) “k 111c) ∩ Ins3k k SIk SIk SIkSk ) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k Ik )) “k 11111111c)) “k 11111c) “k 1111c)) V
373372, 321imakex 4300 . . . . 5 (( Ins2k SkIns3k (((( Ins2k Ins2k (((( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c) “k 111c) ∩ Ins3k k SIk SIk SIkSk ) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k Ik )) “k 11111111c)) “k 11111c) “k 1111c)) “k 111c) V
374373complex 4104 . . . 4 ∼ (( Ins2k SkIns3k (((( Ins2k Ins2k (((( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c) “k 111c) ∩ Ins3k k SIk SIk SIkSk ) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k Ik )) “k 11111111c)) “k 11111c) “k 1111c)) “k 111c) V
375 nncex 4396 . . . 4 Nn V
376374, 375imakex 4300 . . 3 ( ∼ (( Ins2k SkIns3k (((( Ins2k Ins2k (((( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c) “k 111c) ∩ Ins3k k SIk SIk SIkSk ) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k Ik )) “k 11111111c)) “k 11111c) “k 1111c)) “k 111c) “k Nn ) V
377 snex 4111 . . 3 {} V
378376, 377difex 4107 . 2 (( ∼ (( Ins2k SkIns3k (((( Ins2k Ins2k (((( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ∩ ( Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))) “k 11111c) “k 111c) ∩ Ins3k k SIk SIk SIkSk ) ∩ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k Ik )) “k 11111111c)) “k 11111c) “k 1111c)) “k 111c) “k Nn ) {}) V
379310, 378eqeltri 2423 1 Oddfin V
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 176   wo 357   wa 358  wal 1540  wex 1541   = wceq 1642   wcel 1710  {cab 2339  wne 2516  wrex 2615  Vcvv 2859  ccompl 3205   cdif 3206  cun 3207  cin 3208  csymdif 3209  c0 3550  {csn 3737  copk 4057  1cc1c 4134  1cpw1 4135   ×k cxpk 4174  kccnvk 4175   Ins2k cins2k 4176   Ins3k cins3k 4177  k cimak 4179   SIk csik 4181   Sk cssetk 4183   Ik cidk 4184   Nn cnnc 4373   +c cplc 4375   Oddfin coddfin 4437
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 4078  ax-xp 4079  ax-cnv 4080  ax-1c 4081  ax-sset 4082  ax-si 4083  ax-ins2 4084  ax-ins3 4085  ax-typlower 4086  ax-sn 4087
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-nan 1288  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2340  df-cleq 2346  df-clel 2349  df-nfc 2478  df-ne 2518  df-ral 2619  df-rex 2620  df-v 2861  df-sbc 3047  df-nin 3211  df-compl 3212  df-in 3213  df-un 3214  df-dif 3215  df-symdif 3216  df-ss 3259  df-nul 3551  df-if 3663  df-pw 3724  df-sn 3741  df-pr 3742  df-uni 3892  df-int 3927  df-opk 4058  df-1c 4136  df-pw1 4137  df-uni1 4138  df-xpk 4185  df-cnvk 4186  df-ins2k 4187  df-ins3k 4188  df-imak 4189  df-cok 4190  df-p6 4191  df-sik 4192  df-ssetk 4193  df-imagek 4194  df-idk 4195  df-addc 4378  df-nnc 4379  df-oddfin 4445
This theorem is referenced by:  evenoddnnnul  4514
  Copyright terms: Public domain W3C validator