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

Theorem evenfinex 4503
Description: The set of all even naturals exists. (Contributed by SF, 20-Jan-2015.)
Assertion
Ref Expression
evenfinex Evenfin V

Proof of Theorem evenfinex
Dummy variables a b c n t x are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-evenfin 4444 . . 3 Evenfin = {x (n Nn x = (n +c n) x)}
2 eldifsn 3839 . . . . 5 (x (( ∼ (( Ins2k SkIns3k (((( 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)) “k 111c) “k Nn ) {}) ↔ (x ( ∼ (( Ins2k SkIns3k (((( 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)) “k 111c) “k Nn ) x))
3 vex 2862 . . . . . . . 8 x V
43elimak 4259 . . . . . . 7 (x ( ∼ (( Ins2k SkIns3k (((( 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)) “k 111c) “k Nn ) ↔ n Nnn, x ∼ (( Ins2k SkIns3k (((( 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)) “k 111c))
5 opkex 4113 . . . . . . . . . . . 12 n, x V
65elimak 4259 . . . . . . . . . . 11 (⟪n, x (( Ins2k SkIns3k (((( 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)) “k 111c) ↔ t 1 11ct, ⟪n, x⟫⟫ ( Ins2k SkIns3k (((( 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)))
7 elpw121c 4148 . . . . . . . . . . . . . . 15 (t 111ca t = {{{a}}})
87anbi1i 676 . . . . . . . . . . . . . 14 ((t 111c t, ⟪n, x⟫⟫ ( Ins2k SkIns3k (((( 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))) ↔ (a t = {{{a}}} t, ⟪n, x⟫⟫ ( Ins2k SkIns3k (((( 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))))
9 19.41v 1901 . . . . . . . . . . . . . 14 (a(t = {{{a}}} t, ⟪n, x⟫⟫ ( Ins2k SkIns3k (((( 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))) ↔ (a t = {{{a}}} t, ⟪n, x⟫⟫ ( Ins2k SkIns3k (((( 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))))
108, 9bitr4i 243 . . . . . . . . . . . . 13 ((t 111c t, ⟪n, x⟫⟫ ( Ins2k SkIns3k (((( 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))) ↔ a(t = {{{a}}} t, ⟪n, x⟫⟫ ( Ins2k SkIns3k (((( 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))))
1110exbii 1582 . . . . . . . . . . . 12 (t(t 111c t, ⟪n, x⟫⟫ ( Ins2k SkIns3k (((( 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))) ↔ ta(t = {{{a}}} t, ⟪n, x⟫⟫ ( Ins2k SkIns3k (((( 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))))
12 df-rex 2620 . . . . . . . . . . . 12 (t 1 11ct, ⟪n, x⟫⟫ ( Ins2k SkIns3k (((( 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(t 111c t, ⟪n, x⟫⟫ ( Ins2k SkIns3k (((( 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))))
13 excom 1741 . . . . . . . . . . . 12 (at(t = {{{a}}} t, ⟪n, x⟫⟫ ( Ins2k SkIns3k (((( 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))) ↔ ta(t = {{{a}}} t, ⟪n, x⟫⟫ ( Ins2k SkIns3k (((( 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))))
1411, 12, 133bitr4i 268 . . . . . . . . . . 11 (t 1 11ct, ⟪n, x⟫⟫ ( Ins2k SkIns3k (((( 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)) ↔ at(t = {{{a}}} t, ⟪n, x⟫⟫ ( Ins2k SkIns3k (((( 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))))
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 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)) ↔ ⟪{{{a}}}, ⟪n, x⟫⟫ ( Ins2k SkIns3k (((( 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))))
1815, 17ceqsexv 2894 . . . . . . . . . . . . 13 (t(t = {{{a}}} t, ⟪n, x⟫⟫ ( Ins2k SkIns3k (((( 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))) ↔ ⟪{{{a}}}, ⟪n, x⟫⟫ ( Ins2k SkIns3k (((( 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)))
19 elsymdif 3223 . . . . . . . . . . . . 13 (⟪{{{a}}}, ⟪n, x⟫⟫ ( Ins2k SkIns3k (((( 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)) ↔ ¬ (⟪{{{a}}}, ⟪n, x⟫⟫ Ins2k Sk ↔ ⟪{{{a}}}, ⟪n, x⟫⟫ Ins3k (((( 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)))
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 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, ⟪{a}, 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))
28 df-rex 2620 . . . . . . . . . . . . . . . . 17 (t 1 11ct, ⟪{a}, 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, ⟪{a}, 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)))
29 elpw121c 4148 . . . . . . . . . . . . . . . . . . . . 21 (t 111cc t = {{{c}}})
3029anbi1i 676 . . . . . . . . . . . . . . . . . . . 20 ((t 111c t, ⟪{a}, 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, ⟪{a}, 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)))
31 19.41v 1901 . . . . . . . . . . . . . . . . . . . 20 (c(t = {{{c}}} t, ⟪{a}, 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, ⟪{a}, 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)))
3230, 31bitr4i 243 . . . . . . . . . . . . . . . . . . 19 ((t 111c t, ⟪{a}, 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, ⟪{a}, 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)))
3332exbii 1582 . . . . . . . . . . . . . . . . . 18 (t(t 111c t, ⟪{a}, 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, ⟪{a}, 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)))
34 excom 1741 . . . . . . . . . . . . . . . . . 18 (ct(t = {{{c}}} t, ⟪{a}, 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, ⟪{a}, 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)))
3533, 34bitr4i 243 . . . . . . . . . . . . . . . . 17 (t(t 111c t, ⟪{a}, 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, ⟪{a}, 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)))
3627, 28, 353bitri 262 . . . . . . . . . . . . . . . 16 (⟪{a}, 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) ↔ ct(t = {{{c}}} t, ⟪{a}, 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)))
3720, 21, 3otkelins3k 4256 . . . . . . . . . . . . . . . 16 (⟪{{{a}}}, ⟪n, x⟫⟫ Ins3k (((( 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) ↔ ⟪{a}, 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))
38 eladdc 4398 . . . . . . . . . . . . . . . . 17 (a (n +c n) ↔ b n c n ((bc) = a = (bc)))
39 r2ex 2652 . . . . . . . . . . . . . . . . 17 (b n c n ((bc) = a = (bc)) ↔ bc((b n c n) ((bc) = a = (bc))))
40 excom 1741 . . . . . . . . . . . . . . . . . 18 (bc((b n c n) ((bc) = a = (bc))) ↔ cb((b n c n) ((bc) = a = (bc))))
41 snex 4111 . . . . . . . . . . . . . . . . . . . . 21 {{{c}}} V
42 opkeq1 4059 . . . . . . . . . . . . . . . . . . . . . 22 (t = {{{c}}} → ⟪t, ⟪{a}, n⟫⟫ = ⟪{{{c}}}, ⟪{a}, n⟫⟫)
4342eleq1d 2419 . . . . . . . . . . . . . . . . . . . . 21 (t = {{{c}}} → (⟪t, ⟪{a}, 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}}}, ⟪{a}, 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)))
4441, 43ceqsexv 2894 . . . . . . . . . . . . . . . . . . . 20 (t(t = {{{c}}} t, ⟪{a}, 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}}}, ⟪{a}, 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))
45 opkex 4113 . . . . . . . . . . . . . . . . . . . . . 22 ⟪{{{c}}}, ⟪{a}, n⟫⟫ V
4645elimak 4259 . . . . . . . . . . . . . . . . . . . . 21 (⟪{{{c}}}, ⟪{a}, 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}}}, ⟪{a}, 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))))
47 df-rex 2620 . . . . . . . . . . . . . . . . . . . . 21 (t 1 1111ct, ⟪{{{c}}}, ⟪{a}, 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}}}, ⟪{a}, 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)))))
48 elpw141c 4150 . . . . . . . . . . . . . . . . . . . . . . . . 25 (t 11111cb t = {{{{{b}}}}})
4948anbi1i 676 . . . . . . . . . . . . . . . . . . . . . . . 24 ((t 11111c t, ⟪{{{c}}}, ⟪{a}, 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)))) ↔ (b t = {{{{{b}}}}} t, ⟪{{{c}}}, ⟪{a}, 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)))))
50 19.41v 1901 . . . . . . . . . . . . . . . . . . . . . . . 24 (b(t = {{{{{b}}}}} t, ⟪{{{c}}}, ⟪{a}, 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)))) ↔ (b t = {{{{{b}}}}} t, ⟪{{{c}}}, ⟪{a}, 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)))))
5149, 50bitr4i 243 . . . . . . . . . . . . . . . . . . . . . . 23 ((t 11111c t, ⟪{{{c}}}, ⟪{a}, 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)))) ↔ b(t = {{{{{b}}}}} t, ⟪{{{c}}}, ⟪{a}, 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)))))
5251exbii 1582 . . . . . . . . . . . . . . . . . . . . . 22 (t(t 11111c t, ⟪{{{c}}}, ⟪{a}, 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)))) ↔ tb(t = {{{{{b}}}}} t, ⟪{{{c}}}, ⟪{a}, 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)))))
53 excom 1741 . . . . . . . . . . . . . . . . . . . . . 22 (bt(t = {{{{{b}}}}} t, ⟪{{{c}}}, ⟪{a}, 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)))) ↔ tb(t = {{{{{b}}}}} t, ⟪{{{c}}}, ⟪{a}, 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)))))
5452, 53bitr4i 243 . . . . . . . . . . . . . . . . . . . . 21 (t(t 11111c t, ⟪{{{c}}}, ⟪{a}, 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)))) ↔ bt(t = {{{{{b}}}}} t, ⟪{{{c}}}, ⟪{a}, 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)))))
5546, 47, 543bitri 262 . . . . . . . . . . . . . . . . . . . 20 (⟪{{{c}}}, ⟪{a}, 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) ↔ bt(t = {{{{{b}}}}} t, ⟪{{{c}}}, ⟪{a}, 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)))))
56 snex 4111 . . . . . . . . . . . . . . . . . . . . . . 23 {{{{{b}}}}} V
57 opkeq1 4059 . . . . . . . . . . . . . . . . . . . . . . . 24 (t = {{{{{b}}}}} → ⟪t, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫ = ⟪{{{{{b}}}}}, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫)
5857eleq1d 2419 . . . . . . . . . . . . . . . . . . . . . . 23 (t = {{{{{b}}}}} → (⟪t, ⟪{{{c}}}, ⟪{a}, 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))) ↔ ⟪{{{{{b}}}}}, ⟪{{{c}}}, ⟪{a}, 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)))))
5956, 58ceqsexv 2894 . . . . . . . . . . . . . . . . . . . . . 22 (t(t = {{{{{b}}}}} t, ⟪{{{c}}}, ⟪{a}, 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)))) ↔ ⟪{{{{{b}}}}}, ⟪{{{c}}}, ⟪{a}, 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))))
60 elin 3219 . . . . . . . . . . . . . . . . . . . . . 22 (⟪{{{{{b}}}}}, ⟪{{{c}}}, ⟪{a}, 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))) ↔ (⟪{{{{{b}}}}}, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫ ( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ⟪{{{{{b}}}}}, ⟪{{{c}}}, ⟪{a}, 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))))
61 elin 3219 . . . . . . . . . . . . . . . . . . . . . . . 24 (⟪{{{{{b}}}}}, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫ ( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ↔ (⟪{{{{{b}}}}}, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫ Ins2k Ins2k Sk ⟪{{{{{b}}}}}, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫ (V ×k Ins2k Sk )))
62 snex 4111 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 {{{b}}} V
6362, 41, 26otkelins2k 4255 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (⟪{{{{{b}}}}}, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫ Ins2k Ins2k Sk ↔ ⟪{{{b}}}, ⟪{a}, n⟫⟫ Ins2k Sk )
64 snex 4111 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 {b} V
6564, 20, 21otkelins2k 4255 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (⟪{{{b}}}, ⟪{a}, n⟫⟫ Ins2k Sk ↔ ⟪{b}, n Sk )
66 vex 2862 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 b V
6766, 21elssetk 4270 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (⟪{b}, n Skb n)
6863, 65, 673bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . 25 (⟪{{{{{b}}}}}, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫ Ins2k Ins2k Skb n)
6956, 45opkelxpk 4248 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (⟪{{{{{b}}}}}, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫ (V ×k Ins2k Sk ) ↔ ({{{{{b}}}}} V ⟪{{{c}}}, ⟪{a}, n⟫⟫ Ins2k Sk ))
7056, 69mpbiran 884 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (⟪{{{{{b}}}}}, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫ (V ×k Ins2k Sk ) ↔ ⟪{{{c}}}, ⟪{a}, n⟫⟫ Ins2k Sk )
71 snex 4111 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 {c} V
7271, 20, 21otkelins2k 4255 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (⟪{{{c}}}, ⟪{a}, n⟫⟫ Ins2k Sk ↔ ⟪{c}, n Sk )
73 vex 2862 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 c V
7473, 21elssetk 4270 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (⟪{c}, n Skc n)
7570, 72, 743bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . 25 (⟪{{{{{b}}}}}, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫ (V ×k Ins2k Sk ) ↔ c n)
7668, 75anbi12i 678 . . . . . . . . . . . . . . . . . . . . . . . 24 ((⟪{{{{{b}}}}}, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫ Ins2k Ins2k Sk ⟪{{{{{b}}}}}, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫ (V ×k Ins2k Sk )) ↔ (b n c n))
7761, 76bitri 240 . . . . . . . . . . . . . . . . . . . . . . 23 (⟪{{{{{b}}}}}, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫ ( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ↔ (b n c n))
78 elin 3219 . . . . . . . . . . . . . . . . . . . . . . . 24 (⟪{{{{{b}}}}}, ⟪{{{c}}}, ⟪{a}, 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)) ↔ (⟪{{{{{b}}}}}, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫ Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ⟪{{{{{b}}}}}, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c)))
7962, 41, 26otkelins3k 4256 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (⟪{{{{{b}}}}}, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫ Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ↔ ⟪{{{b}}}, {{{c}}}⟫ SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c))
80 snex 4111 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 {{b}} V
81 snex 4111 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 {{c}} V
8280, 81opksnelsik 4265 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (⟪{{{b}}}, {{{c}}}⟫ SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ↔ ⟪{{b}}, {{c}}⟫ SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c))
8364, 71opksnelsik 4265 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (⟪{{b}}, {{c}}⟫ SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ↔ ⟪{b}, {c}⟫ SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c))
8466, 73opksnelsik 4265 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (⟪{b}, {c}⟫ SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ↔ ⟪b, c ∼ (( Ins3k SkIns2k Sk ) “k 111c))
8566, 73ndisjrelk 4323 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (⟪b, c (( Ins3k SkIns2k Sk ) “k 111c) ↔ (bc) ≠ )
8685notbii 287 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (¬ ⟪b, c (( Ins3k SkIns2k Sk ) “k 111c) ↔ ¬ (bc) ≠ )
87 opkex 4113 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 b, c V
8887elcompl 3225 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (⟪b, c ∼ (( Ins3k SkIns2k Sk ) “k 111c) ↔ ¬ ⟪b, c (( Ins3k SkIns2k Sk ) “k 111c))
89 df-ne 2518 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((bc) ≠ ↔ ¬ (bc) = )
9089con2bii 322 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((bc) = ↔ ¬ (bc) ≠ )
9186, 88, 903bitr4i 268 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (⟪b, c ∼ (( Ins3k SkIns2k Sk ) “k 111c) ↔ (bc) = )
9283, 84, 913bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (⟪{{b}}, {{c}}⟫ SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ↔ (bc) = )
9379, 82, 923bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . 25 (⟪{{{{{b}}}}}, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫ Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ↔ (bc) = )
94 opkex 4113 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⟪{{{{{b}}}}}, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫ V
9594elimak 4259 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (⟪{{{{{b}}}}}, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c) ↔ t 1 1111111ct, ⟪{{{{{b}}}}}, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫⟫ ( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )))
96 elpw171c 4153 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (t 11111111cx t = {{{{{{{{x}}}}}}}})
9796anbi1i 676 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((t 11111111c t, ⟪{{{{{b}}}}}, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫⟫ ( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk ))) ↔ (x t = {{{{{{{{x}}}}}}}} t, ⟪{{{{{b}}}}}, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫⟫ ( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk ))))
98 19.41v 1901 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (x(t = {{{{{{{{x}}}}}}}} t, ⟪{{{{{b}}}}}, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫⟫ ( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk ))) ↔ (x t = {{{{{{{{x}}}}}}}} t, ⟪{{{{{b}}}}}, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫⟫ ( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk ))))
9997, 98bitr4i 243 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((t 11111111c t, ⟪{{{{{b}}}}}, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫⟫ ( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk ))) ↔ x(t = {{{{{{{{x}}}}}}}} t, ⟪{{{{{b}}}}}, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫⟫ ( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk ))))
10099exbii 1582 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (t(t 11111111c t, ⟪{{{{{b}}}}}, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫⟫ ( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk ))) ↔ tx(t = {{{{{{{{x}}}}}}}} t, ⟪{{{{{b}}}}}, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫⟫ ( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk ))))
101 df-rex 2620 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (t 1 1111111ct, ⟪{{{{{b}}}}}, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫⟫ ( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) ↔ t(t 11111111c t, ⟪{{{{{b}}}}}, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫⟫ ( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk ))))
102 excom 1741 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (xt(t = {{{{{{{{x}}}}}}}} t, ⟪{{{{{b}}}}}, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫⟫ ( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk ))) ↔ tx(t = {{{{{{{{x}}}}}}}} t, ⟪{{{{{b}}}}}, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫⟫ ( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk ))))
103100, 101, 1023bitr4i 268 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (t 1 1111111ct, ⟪{{{{{b}}}}}, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫⟫ ( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) ↔ xt(t = {{{{{{{{x}}}}}}}} t, ⟪{{{{{b}}}}}, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫⟫ ( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk ))))
104 snex 4111 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 {{{{{{{{x}}}}}}}} V
105 opkeq1 4059 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (t = {{{{{{{{x}}}}}}}} → ⟪t, ⟪{{{{{b}}}}}, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫⟫ = ⟪{{{{{{{{x}}}}}}}}, ⟪{{{{{b}}}}}, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫⟫)
106105eleq1d 2419 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (t = {{{{{{{{x}}}}}}}} → (⟪t, ⟪{{{{{b}}}}}, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫⟫ ( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) ↔ ⟪{{{{{{{{x}}}}}}}}, ⟪{{{{{b}}}}}, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫⟫ ( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk ))))
107104, 106ceqsexv 2894 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (t(t = {{{{{{{{x}}}}}}}} t, ⟪{{{{{b}}}}}, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫⟫ ( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk ))) ↔ ⟪{{{{{{{{x}}}}}}}}, ⟪{{{{{b}}}}}, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫⟫ ( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )))
108 elsymdif 3223 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (⟪{{{{{{{{x}}}}}}}}, ⟪{{{{{b}}}}}, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫⟫ ( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) ↔ ¬ (⟪{{{{{{{{x}}}}}}}}, ⟪{{{{{b}}}}}, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫⟫ Ins2k Ins2k Ins3k SIk Sk ↔ ⟪{{{{{{{{x}}}}}}}}, ⟪{{{{{b}}}}}, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫⟫ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )))
109 snex 4111 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 {{{{{{x}}}}}} V
110109, 56, 45otkelins2k 4255 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (⟪{{{{{{{{x}}}}}}}}, ⟪{{{{{b}}}}}, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫⟫ Ins2k Ins2k Ins3k SIk Sk ↔ ⟪{{{{{{x}}}}}}, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫ Ins2k Ins3k SIk Sk )
111 snex 4111 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 {{{{x}}}} V
112111, 41, 26otkelins2k 4255 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (⟪{{{{{{x}}}}}}, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫ Ins2k Ins3k SIk Sk ↔ ⟪{{{{x}}}}, ⟪{a}, n⟫⟫ Ins3k SIk Sk )
113 snex 4111 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 {{x}} V
114113, 20, 21otkelins3k 4256 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (⟪{{{{x}}}}, ⟪{a}, n⟫⟫ Ins3k SIk Sk ↔ ⟪{{x}}, {a}⟫ SIk Sk )
115 snex 4111 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 {x} V
116115, 23opksnelsik 4265 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (⟪{{x}}, {a}⟫ SIk Sk ↔ ⟪{x}, a Sk )
1173, 23elssetk 4270 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (⟪{x}, a Skx a)
118114, 116, 1173bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (⟪{{{{x}}}}, ⟪{a}, n⟫⟫ Ins3k SIk Skx a)
119110, 112, 1183bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (⟪{{{{{{{{x}}}}}}}}, ⟪{{{{{b}}}}}, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫⟫ Ins2k Ins2k Ins3k SIk Skx a)
120109, 56, 45otkelins3k 4256 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (⟪{{{{{{{{x}}}}}}}}, ⟪{{{{{b}}}}}, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫⟫ Ins3k SIk SIk SIk SIk SIk Sk ↔ ⟪{{{{{{x}}}}}}, {{{{{b}}}}}⟫ SIk SIk SIk SIk SIk Sk )
121 snex 4111 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 {{{{{x}}}}} V
122 snex 4111 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 {{{{b}}}} V
123121, 122opksnelsik 4265 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (⟪{{{{{{x}}}}}}, {{{{{b}}}}}⟫ SIk SIk SIk SIk SIk Sk ↔ ⟪{{{{{x}}}}}, {{{{b}}}}⟫ SIk SIk SIk SIk Sk )
124111, 62opksnelsik 4265 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (⟪{{{{{x}}}}}, {{{{b}}}}⟫ SIk SIk SIk SIk Sk ↔ ⟪{{{{x}}}}, {{{b}}}⟫ SIk SIk SIk Sk )
125 snex 4111 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 {{{x}}} V
126125, 80opksnelsik 4265 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (⟪{{{{x}}}}, {{{b}}}⟫ SIk SIk SIk Sk ↔ ⟪{{{x}}}, {{b}}⟫ SIk SIk Sk )
127113, 64opksnelsik 4265 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (⟪{{{x}}}, {{b}}⟫ SIk SIk Sk ↔ ⟪{{x}}, {b}⟫ SIk Sk )
128115, 66opksnelsik 4265 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (⟪{{x}}, {b}⟫ SIk Sk ↔ ⟪{x}, b Sk )
1293, 66elssetk 4270 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (⟪{x}, b Skx b)
130127, 128, 1293bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (⟪{{{x}}}, {{b}}⟫ SIk SIk Skx b)
131124, 126, 1303bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (⟪{{{{{x}}}}}, {{{{b}}}}⟫ SIk SIk SIk SIk Skx b)
132120, 123, 1313bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (⟪{{{{{{{{x}}}}}}}}, ⟪{{{{{b}}}}}, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫⟫ Ins3k SIk SIk SIk SIk SIk Skx b)
133109, 56, 45otkelins2k 4255 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (⟪{{{{{{{{x}}}}}}}}, ⟪{{{{{b}}}}}, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫⟫ Ins2k Ins3k SIk SIk SIk Sk ↔ ⟪{{{{{{x}}}}}}, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫ Ins3k SIk SIk SIk Sk )
134111, 41, 26otkelins3k 4256 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (⟪{{{{{{x}}}}}}, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫ Ins3k SIk SIk SIk Sk ↔ ⟪{{{{x}}}}, {{{c}}}⟫ SIk SIk SIk Sk )
135125, 81opksnelsik 4265 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (⟪{{{{x}}}}, {{{c}}}⟫ SIk SIk SIk Sk ↔ ⟪{{{x}}}, {{c}}⟫ SIk SIk Sk )
136113, 71opksnelsik 4265 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (⟪{{{x}}}, {{c}}⟫ SIk SIk Sk ↔ ⟪{{x}}, {c}⟫ SIk Sk )
137115, 73opksnelsik 4265 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (⟪{{x}}, {c}⟫ SIk Sk ↔ ⟪{x}, c Sk )
1383, 73elssetk 4270 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (⟪{x}, c Skx c)
139137, 138bitri 240 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (⟪{{x}}, {c}⟫ SIk Skx c)
140135, 136, 1393bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (⟪{{{{x}}}}, {{{c}}}⟫ SIk SIk SIk Skx c)
141133, 134, 1403bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (⟪{{{{{{{{x}}}}}}}}, ⟪{{{{{b}}}}}, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫⟫ Ins2k Ins3k SIk SIk SIk Skx c)
142132, 141orbi12i 507 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((⟪{{{{{{{{x}}}}}}}}, ⟪{{{{{b}}}}}, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫⟫ Ins3k SIk SIk SIk SIk SIk Sk ⟪{{{{{{{{x}}}}}}}}, ⟪{{{{{b}}}}}, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫⟫ Ins2k Ins3k SIk SIk SIk Sk ) ↔ (x b x c))
143 elun 3220 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (⟪{{{{{{{{x}}}}}}}}, ⟪{{{{{b}}}}}, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫⟫ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk ) ↔ (⟪{{{{{{{{x}}}}}}}}, ⟪{{{{{b}}}}}, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫⟫ Ins3k SIk SIk SIk SIk SIk Sk ⟪{{{{{{{{x}}}}}}}}, ⟪{{{{{b}}}}}, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫⟫ Ins2k Ins3k SIk SIk SIk Sk ))
144 elun 3220 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (x (bc) ↔ (x b x c))
145142, 143, 1443bitr4i 268 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (⟪{{{{{{{{x}}}}}}}}, ⟪{{{{{b}}}}}, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫⟫ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk ) ↔ x (bc))
146119, 145bibi12i 306 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((⟪{{{{{{{{x}}}}}}}}, ⟪{{{{{b}}}}}, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫⟫ Ins2k Ins2k Ins3k SIk Sk ↔ ⟪{{{{{{{{x}}}}}}}}, ⟪{{{{{b}}}}}, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫⟫ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) ↔ (x ax (bc)))
147146notbii 287 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (¬ (⟪{{{{{{{{x}}}}}}}}, ⟪{{{{{b}}}}}, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫⟫ Ins2k Ins2k Ins3k SIk Sk ↔ ⟪{{{{{{{{x}}}}}}}}, ⟪{{{{{b}}}}}, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫⟫ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) ↔ ¬ (x ax (bc)))
148107, 108, 1473bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (t(t = {{{{{{{{x}}}}}}}} t, ⟪{{{{{b}}}}}, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫⟫ ( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk ))) ↔ ¬ (x ax (bc)))
149148exbii 1582 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (xt(t = {{{{{{{{x}}}}}}}} t, ⟪{{{{{b}}}}}, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫⟫ ( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk ))) ↔ x ¬ (x ax (bc)))
15095, 103, 1493bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (⟪{{{{{b}}}}}, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c) ↔ x ¬ (x ax (bc)))
151150notbii 287 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (¬ ⟪{{{{{b}}}}}, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c) ↔ ¬ x ¬ (x ax (bc)))
15294elcompl 3225 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (⟪{{{{{b}}}}}, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c) ↔ ¬ ⟪{{{{{b}}}}}, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c))
153 dfcleq 2347 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (a = (bc) ↔ x(x ax (bc)))
154 alex 1572 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (x(x ax (bc)) ↔ ¬ x ¬ (x ax (bc)))
155153, 154bitri 240 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (a = (bc) ↔ ¬ x ¬ (x ax (bc)))
156151, 152, 1553bitr4i 268 . . . . . . . . . . . . . . . . . . . . . . . . 25 (⟪{{{{{b}}}}}, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c) ↔ a = (bc))
15793, 156anbi12i 678 . . . . . . . . . . . . . . . . . . . . . . . 24 ((⟪{{{{{b}}}}}, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫ Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) ⟪{{{{{b}}}}}, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫ ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c)) ↔ ((bc) = a = (bc)))
15878, 157bitri 240 . . . . . . . . . . . . . . . . . . . . . . 23 (⟪{{{{{b}}}}}, ⟪{{{c}}}, ⟪{a}, 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)) ↔ ((bc) = a = (bc)))
15977, 158anbi12i 678 . . . . . . . . . . . . . . . . . . . . . 22 ((⟪{{{{{b}}}}}, ⟪{{{c}}}, ⟪{a}, n⟫⟫⟫ ( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) ⟪{{{{{b}}}}}, ⟪{{{c}}}, ⟪{a}, 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))) ↔ ((b n c n) ((bc) = a = (bc))))
16059, 60, 1593bitri 262 . . . . . . . . . . . . . . . . . . . . 21 (t(t = {{{{{b}}}}} t, ⟪{{{c}}}, ⟪{a}, 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)))) ↔ ((b n c n) ((bc) = a = (bc))))
161160exbii 1582 . . . . . . . . . . . . . . . . . . . 20 (bt(t = {{{{{b}}}}} t, ⟪{{{c}}}, ⟪{a}, 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)))) ↔ b((b n c n) ((bc) = a = (bc))))
16244, 55, 1613bitri 262 . . . . . . . . . . . . . . . . . . 19 (t(t = {{{c}}} t, ⟪{a}, 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)) ↔ b((b n c n) ((bc) = a = (bc))))
163162exbii 1582 . . . . . . . . . . . . . . . . . 18 (ct(t = {{{c}}} t, ⟪{a}, 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)) ↔ cb((b n c n) ((bc) = a = (bc))))
16440, 163bitr4i 243 . . . . . . . . . . . . . . . . 17 (bc((b n c n) ((bc) = a = (bc))) ↔ ct(t = {{{c}}} t, ⟪{a}, 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)))
16538, 39, 1643bitri 262 . . . . . . . . . . . . . . . 16 (a (n +c n) ↔ ct(t = {{{c}}} t, ⟪{a}, 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)))
16636, 37, 1653bitr4i 268 . . . . . . . . . . . . . . 15 (⟪{{{a}}}, ⟪n, x⟫⟫ Ins3k (((( 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) ↔ a (n +c n))
16725, 166bibi12i 306 . . . . . . . . . . . . . 14 ((⟪{{{a}}}, ⟪n, x⟫⟫ Ins2k Sk ↔ ⟪{{{a}}}, ⟪n, x⟫⟫ Ins3k (((( 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)) ↔ (a xa (n +c n)))
168167notbii 287 . . . . . . . . . . . . 13 (¬ (⟪{{{a}}}, ⟪n, x⟫⟫ Ins2k Sk ↔ ⟪{{{a}}}, ⟪n, x⟫⟫ Ins3k (((( 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)) ↔ ¬ (a xa (n +c n)))
16918, 19, 1683bitri 262 . . . . . . . . . . . 12 (t(t = {{{a}}} t, ⟪n, x⟫⟫ ( Ins2k SkIns3k (((( 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))) ↔ ¬ (a xa (n +c n)))
170169exbii 1582 . . . . . . . . . . 11 (at(t = {{{a}}} t, ⟪n, x⟫⟫ ( Ins2k SkIns3k (((( 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))) ↔ a ¬ (a xa (n +c n)))
1716, 14, 1703bitri 262 . . . . . . . . . 10 (⟪n, x (( Ins2k SkIns3k (((( 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)) “k 111c) ↔ a ¬ (a xa (n +c n)))
172171notbii 287 . . . . . . . . 9 (¬ ⟪n, x (( Ins2k SkIns3k (((( 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)) “k 111c) ↔ ¬ a ¬ (a xa (n +c n)))
1735elcompl 3225 . . . . . . . . 9 (⟪n, x ∼ (( Ins2k SkIns3k (((( 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)) “k 111c) ↔ ¬ ⟪n, x (( Ins2k SkIns3k (((( 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)) “k 111c))
174 dfcleq 2347 . . . . . . . . . 10 (x = (n +c n) ↔ a(a xa (n +c n)))
175 alex 1572 . . . . . . . . . 10 (a(a xa (n +c n)) ↔ ¬ a ¬ (a xa (n +c n)))
176174, 175bitri 240 . . . . . . . . 9 (x = (n +c n) ↔ ¬ a ¬ (a xa (n +c n)))
177172, 173, 1763bitr4i 268 . . . . . . . 8 (⟪n, x ∼ (( Ins2k SkIns3k (((( 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)) “k 111c) ↔ x = (n +c n))
178177rexbii 2639 . . . . . . 7 (n Nnn, x ∼ (( Ins2k SkIns3k (((( 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)) “k 111c) ↔ n Nn x = (n +c n))
1794, 178bitri 240 . . . . . 6 (x ( ∼ (( Ins2k SkIns3k (((( 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)) “k 111c) “k Nn ) ↔ n Nn x = (n +c n))
180179anbi1i 676 . . . . 5 ((x ( ∼ (( Ins2k SkIns3k (((( 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)) “k 111c) “k Nn ) x) ↔ (n Nn x = (n +c n) x))
1812, 180bitri 240 . . . 4 (x (( ∼ (( Ins2k SkIns3k (((( 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)) “k 111c) “k Nn ) {}) ↔ (n Nn x = (n +c n) x))
182181abbi2i 2464 . . 3 (( ∼ (( Ins2k SkIns3k (((( 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)) “k 111c) “k Nn ) {}) = {x (n Nn x = (n +c n) x)}
1831, 182eqtr4i 2376 . 2 Evenfin = (( ∼ (( Ins2k SkIns3k (((( 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)) “k 111c) “k Nn ) {})
184 ssetkex 4294 . . . . . . . 8 Sk V
185184ins2kex 4307 . . . . . . 7 Ins2k Sk V
186185ins2kex 4307 . . . . . . . . . . . 12 Ins2k Ins2k Sk V
187 vvex 4109 . . . . . . . . . . . . 13 V V
188187, 185xpkex 4289 . . . . . . . . . . . 12 (V ×k Ins2k Sk ) V
189186, 188inex 4105 . . . . . . . . . . 11 ( Ins2k Ins2k Sk ∩ (V ×k Ins2k Sk )) V
190184ins3kex 4308 . . . . . . . . . . . . . . . . . . 19 Ins3k Sk V
191190, 185inex 4105 . . . . . . . . . . . . . . . . . 18 ( Ins3k SkIns2k Sk ) V
192 1cex 4142 . . . . . . . . . . . . . . . . . . . 20 1c V
193192pw1ex 4303 . . . . . . . . . . . . . . . . . . 19 11c V
194193pw1ex 4303 . . . . . . . . . . . . . . . . . 18 111c V
195191, 194imakex 4300 . . . . . . . . . . . . . . . . 17 (( Ins3k SkIns2k Sk ) “k 111c) V
196195complex 4104 . . . . . . . . . . . . . . . 16 ∼ (( Ins3k SkIns2k Sk ) “k 111c) V
197196sikex 4297 . . . . . . . . . . . . . . 15 SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) V
198197sikex 4297 . . . . . . . . . . . . . 14 SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) V
199198sikex 4297 . . . . . . . . . . . . 13 SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) V
200199ins3kex 4308 . . . . . . . . . . . 12 Ins3k SIk SIk SIk ∼ (( Ins3k SkIns2k Sk ) “k 111c) V
201184sikex 4297 . . . . . . . . . . . . . . . . . 18 SIk Sk V
202201ins3kex 4308 . . . . . . . . . . . . . . . . 17 Ins3k SIk Sk V
203202ins2kex 4307 . . . . . . . . . . . . . . . 16 Ins2k Ins3k SIk Sk V
204203ins2kex 4307 . . . . . . . . . . . . . . 15 Ins2k Ins2k Ins3k SIk Sk V
205201sikex 4297 . . . . . . . . . . . . . . . . . . . 20 SIk SIk Sk V
206205sikex 4297 . . . . . . . . . . . . . . . . . . 19 SIk SIk SIk Sk V
207206sikex 4297 . . . . . . . . . . . . . . . . . 18 SIk SIk SIk SIk Sk V
208207sikex 4297 . . . . . . . . . . . . . . . . 17 SIk SIk SIk SIk SIk Sk V
209208ins3kex 4308 . . . . . . . . . . . . . . . 16 Ins3k SIk SIk SIk SIk SIk Sk V
210206ins3kex 4308 . . . . . . . . . . . . . . . . 17 Ins3k SIk SIk SIk Sk V
211210ins2kex 4307 . . . . . . . . . . . . . . . 16 Ins2k Ins3k SIk SIk SIk Sk V
212209, 211unex 4106 . . . . . . . . . . . . . . 15 ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk ) V
213204, 212symdifex 4108 . . . . . . . . . . . . . 14 ( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) V
214194pw1ex 4303 . . . . . . . . . . . . . . . . . 18 1111c V
215214pw1ex 4303 . . . . . . . . . . . . . . . . 17 11111c V
216215pw1ex 4303 . . . . . . . . . . . . . . . 16 111111c V
217216pw1ex 4303 . . . . . . . . . . . . . . 15 1111111c V
218217pw1ex 4303 . . . . . . . . . . . . . 14 11111111c V
219213, 218imakex 4300 . . . . . . . . . . . . 13 (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c) V
220219complex 4104 . . . . . . . . . . . 12 ∼ (( Ins2k Ins2k Ins3k SIk Sk ⊕ ( Ins3k SIk SIk SIk SIk SIk SkIns2k Ins3k SIk SIk SIk Sk )) “k 11111111c) V
221200, 220inex 4105 . . . . . . . . . . 11 ( Ins3k SIk SIk SIk ∼ (( 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
222189, 221inex 4105 . . . . . . . . . 10 (( 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
223222, 215imakex 4300 . . . . . . . . 9 ((( 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
224223, 194imakex 4300 . . . . . . . 8 (((( 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
225224ins3kex 4308 . . . . . . 7 Ins3k (((( 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
226185, 225symdifex 4108 . . . . . 6 ( Ins2k SkIns3k (((( 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
227226, 194imakex 4300 . . . . 5 (( Ins2k SkIns3k (((( 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)) “k 111c) V
228227complex 4104 . . . 4 ∼ (( Ins2k SkIns3k (((( 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)) “k 111c) V
229 nncex 4396 . . . 4 Nn V
230228, 229imakex 4300 . . 3 ( ∼ (( Ins2k SkIns3k (((( 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)) “k 111c) “k Nn ) V
231 snex 4111 . . 3 {} V
232230, 231difex 4107 . 2 (( ∼ (( Ins2k SkIns3k (((( 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)) “k 111c) “k Nn ) {}) V
233183, 232eqeltri 2423 1 Evenfin V
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 176   wo 357   wa 358  wal 1540  wex 1541   = wceq 1642   wcel 1710  {cab 2339  wne 2516  wrex 2615  Vcvv 2859  ccompl 3205   cdif 3206  cun 3207  cin 3208  csymdif 3209  c0 3550  {csn 3737  copk 4057  1cc1c 4134  1cpw1 4135   ×k cxpk 4174   Ins2k cins2k 4176   Ins3k cins3k 4177  k cimak 4179   SIk csik 4181   Sk cssetk 4183   Nn cnnc 4373   +c cplc 4375   Evenfin cevenfin 4436
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-ext 2334  ax-nin 4078  ax-xp 4079  ax-cnv 4080  ax-1c 4081  ax-sset 4082  ax-si 4083  ax-ins2 4084  ax-ins3 4085  ax-typlower 4086  ax-sn 4087
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-nan 1288  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2340  df-cleq 2346  df-clel 2349  df-nfc 2478  df-ne 2518  df-ral 2619  df-rex 2620  df-v 2861  df-sbc 3047  df-nin 3211  df-compl 3212  df-in 3213  df-un 3214  df-dif 3215  df-symdif 3216  df-ss 3259  df-nul 3551  df-if 3663  df-pw 3724  df-sn 3741  df-pr 3742  df-uni 3892  df-int 3927  df-opk 4058  df-1c 4136  df-pw1 4137  df-uni1 4138  df-xpk 4185  df-cnvk 4186  df-ins2k 4187  df-ins3k 4188  df-imak 4189  df-cok 4190  df-p6 4191  df-sik 4192  df-ssetk 4193  df-imagek 4194  df-addc 4378  df-nnc 4379  df-evenfin 4444
This theorem is referenced by:  evenoddnnnul  4514
  Copyright terms: Public domain W3C validator