Theorem evenfinex 4503

Description: The set of all even naturals exists. (Contributed by SF, 20-Jan-2015.)

Assertion

Ref	Expression
evenfinex	|- Evenfin e. _V

Proof of Theorem evenfinex

Dummy variables a b c n t x are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-evenfin 4444	. . 3 |- Evenfin = {x | (E.n e. Nn x = (n +o n) /\ x =/= (/))}
2		eldifsn 3839	. . . . 5 |- (x e. (( ∼ (( Ins2k Sk (+) Ins3k (((( Ins2k Ins2k Sk i^i (_V X.k Ins2k Sk )) i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))"k~P1 ~P1 ~P1 ~P1 1c)"k~P1 ~P1 1c))"k~P1 ~P1 1c)"k Nn ) \ {(/)}) <-> (x e. ( ∼ (( Ins2k Sk (+) Ins3k (((( Ins2k Ins2k Sk i^i (_V X.k Ins2k Sk )) i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))"k~P1 ~P1 ~P1 ~P1 1c)"k~P1 ~P1 1c))"k~P1 ~P1 1c)"k Nn ) /\ x =/= (/)))
3		vex 2862	. . . . . . . 8 |- x e. _V
4	3	elimak 4259	. . . . . . 7 |- (x e. ( ∼ (( Ins2k Sk (+) Ins3k (((( Ins2k Ins2k Sk i^i (_V X.k Ins2k Sk )) i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))"k~P1 ~P1 ~P1 ~P1 1c)"k~P1 ~P1 1c))"k~P1 ~P1 1c)"k Nn ) <-> E.n e. Nn <<n, x>> e. ∼ (( Ins2k Sk (+) Ins3k (((( Ins2k Ins2k Sk i^i (_V X.k Ins2k Sk )) i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))"k~P1 ~P1 ~P1 ~P1 1c)"k~P1 ~P1 1c))"k~P1 ~P1 1c))
5		opkex 4113	. . . . . . . . . . . 12 |- <<n, x>> e. _V
6	5	elimak 4259	. . . . . . . . . . 11 |- (<<n, x>> e. (( Ins2k Sk (+) Ins3k (((( Ins2k Ins2k Sk i^i (_V X.k Ins2k Sk )) i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))"k~P1 ~P1 ~P1 ~P1 1c)"k~P1 ~P1 1c))"k~P1 ~P1 1c) <-> E.t e. ~P1 ~P1 1c<<t, <<n, x>>>> e. ( Ins2k Sk (+) Ins3k (((( Ins2k Ins2k Sk i^i (_V X.k Ins2k Sk )) i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))"k~P1 ~P1 ~P1 ~P1 1c)"k~P1 ~P1 1c)))
7		elpw121c 4148	. . . . . . . . . . . . . . 15 |- (t e. ~P1 ~P1 1c <-> E.a t = {{{a}}})
8	7	anbi1i 676	. . . . . . . . . . . . . 14 |- ((t e. ~P1 ~P1 1c /\ <<t, <<n, x>>>> e. ( Ins2k Sk (+) Ins3k (((( Ins2k Ins2k Sk i^i (_V X.k Ins2k Sk )) i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))"k~P1 ~P1 ~P1 ~P1 1c)"k~P1 ~P1 1c))) <-> (E.a t = {{{a}}} /\ <<t, <<n, x>>>> e. ( Ins2k Sk (+) Ins3k (((( Ins2k Ins2k Sk i^i (_V X.k Ins2k Sk )) i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))"k~P1 ~P1 ~P1 ~P1 1c)"k~P1 ~P1 1c))))
9		19.41v 1901	. . . . . . . . . . . . . 14 |- (E.a(t = {{{a}}} /\ <<t, <<n, x>>>> e. ( Ins2k Sk (+) Ins3k (((( Ins2k Ins2k Sk i^i (_V X.k Ins2k Sk )) i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))"k~P1 ~P1 ~P1 ~P1 1c)"k~P1 ~P1 1c))) <-> (E.a t = {{{a}}} /\ <<t, <<n, x>>>> e. ( Ins2k Sk (+) Ins3k (((( Ins2k Ins2k Sk i^i (_V X.k Ins2k Sk )) i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))"k~P1 ~P1 ~P1 ~P1 1c)"k~P1 ~P1 1c))))
10	8, 9	bitr4i 243	. . . . . . . . . . . . 13 |- ((t e. ~P1 ~P1 1c /\ <<t, <<n, x>>>> e. ( Ins2k Sk (+) Ins3k (((( Ins2k Ins2k Sk i^i (_V X.k Ins2k Sk )) i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))"k~P1 ~P1 ~P1 ~P1 1c)"k~P1 ~P1 1c))) <-> E.a(t = {{{a}}} /\ <<t, <<n, x>>>> e. ( Ins2k Sk (+) Ins3k (((( Ins2k Ins2k Sk i^i (_V X.k Ins2k Sk )) i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))"k~P1 ~P1 ~P1 ~P1 1c)"k~P1 ~P1 1c))))
11	10	exbii 1582	. . . . . . . . . . . 12 |- (E.t(t e. ~P1 ~P1 1c /\ <<t, <<n, x>>>> e. ( Ins2k Sk (+) Ins3k (((( Ins2k Ins2k Sk i^i (_V X.k Ins2k Sk )) i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))"k~P1 ~P1 ~P1 ~P1 1c)"k~P1 ~P1 1c))) <-> E.tE.a(t = {{{a}}} /\ <<t, <<n, x>>>> e. ( Ins2k Sk (+) Ins3k (((( Ins2k Ins2k Sk i^i (_V X.k Ins2k Sk )) i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))"k~P1 ~P1 ~P1 ~P1 1c)"k~P1 ~P1 1c))))
12		df-rex 2620	. . . . . . . . . . . 12 |- (E.t e. ~P1 ~P1 1c<<t, <<n, x>>>> e. ( Ins2k Sk (+) Ins3k (((( Ins2k Ins2k Sk i^i (_V X.k Ins2k Sk )) i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))"k~P1 ~P1 ~P1 ~P1 1c)"k~P1 ~P1 1c)) <-> E.t(t e. ~P1 ~P1 1c /\ <<t, <<n, x>>>> e. ( Ins2k Sk (+) Ins3k (((( Ins2k Ins2k Sk i^i (_V X.k Ins2k Sk )) i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))"k~P1 ~P1 ~P1 ~P1 1c)"k~P1 ~P1 1c))))
13		excom 1741	. . . . . . . . . . . 12 |- (E.aE.t(t = {{{a}}} /\ <<t, <<n, x>>>> e. ( Ins2k Sk (+) Ins3k (((( Ins2k Ins2k Sk i^i (_V X.k Ins2k Sk )) i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))"k~P1 ~P1 ~P1 ~P1 1c)"k~P1 ~P1 1c))) <-> E.tE.a(t = {{{a}}} /\ <<t, <<n, x>>>> e. ( Ins2k Sk (+) Ins3k (((( Ins2k Ins2k Sk i^i (_V X.k Ins2k Sk )) i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))"k~P1 ~P1 ~P1 ~P1 1c)"k~P1 ~P1 1c))))
14	11, 12, 13	3bitr4i 268	. . . . . . . . . . 11 |- (E.t e. ~P1 ~P1 1c<<t, <<n, x>>>> e. ( Ins2k Sk (+) Ins3k (((( Ins2k Ins2k Sk i^i (_V X.k Ins2k Sk )) i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))"k~P1 ~P1 ~P1 ~P1 1c)"k~P1 ~P1 1c)) <-> E.aE.t(t = {{{a}}} /\ <<t, <<n, x>>>> e. ( Ins2k Sk (+) Ins3k (((( Ins2k Ins2k Sk i^i (_V X.k Ins2k Sk )) i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))"k~P1 ~P1 ~P1 ~P1 1c)"k~P1 ~P1 1c))))
15		snex 4111	. . . . . . . . . . . . . 14 |- {{{a}}} e. _V
16		opkeq1 4059	. . . . . . . . . . . . . . 15 |- (t = {{{a}}} -> <<t, <<n, x>>>> = <<{{{a}}}, <<n, x>>>>)
17	16	eleq1d 2419	. . . . . . . . . . . . . 14 |- (t = {{{a}}} -> (<<t, <<n, x>>>> e. ( Ins2k Sk (+) Ins3k (((( Ins2k Ins2k Sk i^i (_V X.k Ins2k Sk )) i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))"k~P1 ~P1 ~P1 ~P1 1c)"k~P1 ~P1 1c)) <-> <<{{{a}}}, <<n, x>>>> e. ( Ins2k Sk (+) Ins3k (((( Ins2k Ins2k Sk i^i (_V X.k Ins2k Sk )) i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))"k~P1 ~P1 ~P1 ~P1 1c)"k~P1 ~P1 1c))))
18	15, 17	ceqsexv 2894	. . . . . . . . . . . . 13 |- (E.t(t = {{{a}}} /\ <<t, <<n, x>>>> e. ( Ins2k Sk (+) Ins3k (((( Ins2k Ins2k Sk i^i (_V X.k Ins2k Sk )) i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))"k~P1 ~P1 ~P1 ~P1 1c)"k~P1 ~P1 1c))) <-> <<{{{a}}}, <<n, x>>>> e. ( Ins2k Sk (+) Ins3k (((( Ins2k Ins2k Sk i^i (_V X.k Ins2k Sk )) i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))"k~P1 ~P1 ~P1 ~P1 1c)"k~P1 ~P1 1c)))
19		elsymdif 3223	. . . . . . . . . . . . 13 |- (<<{{{a}}}, <<n, x>>>> e. ( Ins2k Sk (+) Ins3k (((( Ins2k Ins2k Sk i^i (_V X.k Ins2k Sk )) i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))"k~P1 ~P1 ~P1 ~P1 1c)"k~P1 ~P1 1c)) <-> -. (<<{{{a}}}, <<n, x>>>> e. Ins2k Sk <-> <<{{{a}}}, <<n, x>>>> e. Ins3k (((( Ins2k Ins2k Sk i^i (_V X.k Ins2k Sk )) i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))"k~P1 ~P1 ~P1 ~P1 1c)"k~P1 ~P1 1c)))
20		snex 4111	. . . . . . . . . . . . . . . . 17 |- {a} e. _V
21		vex 2862	. . . . . . . . . . . . . . . . 17 |- n e. _V
22	20, 21, 3	otkelins2k 4255	. . . . . . . . . . . . . . . 16 |- (<<{{{a}}}, <<n, x>>>> e. Ins2k Sk <-> <<{a}, x>> e. Sk )
23		vex 2862	. . . . . . . . . . . . . . . . 17 |- a e. _V
24	23, 3	elssetk 4270	. . . . . . . . . . . . . . . 16 |- (<<{a}, x>> e. Sk <-> a e. x)
25	22, 24	bitri 240	. . . . . . . . . . . . . . 15 |- (<<{{{a}}}, <<n, x>>>> e. Ins2k Sk <-> a e. x)
26		opkex 4113	. . . . . . . . . . . . . . . . . 18 |- <<{a}, n>> e. _V
27	26	elimak 4259	. . . . . . . . . . . . . . . . 17 |- (<<{a}, n>> e. (((( Ins2k Ins2k Sk i^i (_V X.k Ins2k Sk )) i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))"k~P1 ~P1 ~P1 ~P1 1c)"k~P1 ~P1 1c) <-> E.t e. ~P1 ~P1 1c<<t, <<{a}, n>>>> e. ((( Ins2k Ins2k Sk i^i (_V X.k Ins2k Sk )) i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))"k~P1 ~P1 ~P1 ~P1 1c))
28		df-rex 2620	. . . . . . . . . . . . . . . . 17 |- (E.t e. ~P1 ~P1 1c<<t, <<{a}, n>>>> e. ((( Ins2k Ins2k Sk i^i (_V X.k Ins2k Sk )) i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))"k~P1 ~P1 ~P1 ~P1 1c) <-> E.t(t e. ~P1 ~P1 1c /\ <<t, <<{a}, n>>>> e. ((( Ins2k Ins2k Sk i^i (_V X.k Ins2k Sk )) i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))"k~P1 ~P1 ~P1 ~P1 1c)))
29		elpw121c 4148	. . . . . . . . . . . . . . . . . . . . 21 |- (t e. ~P1 ~P1 1c <-> E.c t = {{{c}}})
30	29	anbi1i 676	. . . . . . . . . . . . . . . . . . . 20 |- ((t e. ~P1 ~P1 1c /\ <<t, <<{a}, n>>>> e. ((( Ins2k Ins2k Sk i^i (_V X.k Ins2k Sk )) i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))"k~P1 ~P1 ~P1 ~P1 1c)) <-> (E.c t = {{{c}}} /\ <<t, <<{a}, n>>>> e. ((( Ins2k Ins2k Sk i^i (_V X.k Ins2k Sk )) i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))"k~P1 ~P1 ~P1 ~P1 1c)))
31		19.41v 1901	. . . . . . . . . . . . . . . . . . . 20 |- (E.c(t = {{{c}}} /\ <<t, <<{a}, n>>>> e. ((( Ins2k Ins2k Sk i^i (_V X.k Ins2k Sk )) i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))"k~P1 ~P1 ~P1 ~P1 1c)) <-> (E.c t = {{{c}}} /\ <<t, <<{a}, n>>>> e. ((( Ins2k Ins2k Sk i^i (_V X.k Ins2k Sk )) i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))"k~P1 ~P1 ~P1 ~P1 1c)))
32	30, 31	bitr4i 243	. . . . . . . . . . . . . . . . . . 19 |- ((t e. ~P1 ~P1 1c /\ <<t, <<{a}, n>>>> e. ((( Ins2k Ins2k Sk i^i (_V X.k Ins2k Sk )) i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))"k~P1 ~P1 ~P1 ~P1 1c)) <-> E.c(t = {{{c}}} /\ <<t, <<{a}, n>>>> e. ((( Ins2k Ins2k Sk i^i (_V X.k Ins2k Sk )) i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))"k~P1 ~P1 ~P1 ~P1 1c)))
33	32	exbii 1582	. . . . . . . . . . . . . . . . . 18 |- (E.t(t e. ~P1 ~P1 1c /\ <<t, <<{a}, n>>>> e. ((( Ins2k Ins2k Sk i^i (_V X.k Ins2k Sk )) i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))"k~P1 ~P1 ~P1 ~P1 1c)) <-> E.tE.c(t = {{{c}}} /\ <<t, <<{a}, n>>>> e. ((( Ins2k Ins2k Sk i^i (_V X.k Ins2k Sk )) i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))"k~P1 ~P1 ~P1 ~P1 1c)))
34		excom 1741	. . . . . . . . . . . . . . . . . 18 |- (E.cE.t(t = {{{c}}} /\ <<t, <<{a}, n>>>> e. ((( Ins2k Ins2k Sk i^i (_V X.k Ins2k Sk )) i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))"k~P1 ~P1 ~P1 ~P1 1c)) <-> E.tE.c(t = {{{c}}} /\ <<t, <<{a}, n>>>> e. ((( Ins2k Ins2k Sk i^i (_V X.k Ins2k Sk )) i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))"k~P1 ~P1 ~P1 ~P1 1c)))
35	33, 34	bitr4i 243	. . . . . . . . . . . . . . . . 17 |- (E.t(t e. ~P1 ~P1 1c /\ <<t, <<{a}, n>>>> e. ((( Ins2k Ins2k Sk i^i (_V X.k Ins2k Sk )) i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))"k~P1 ~P1 ~P1 ~P1 1c)) <-> E.cE.t(t = {{{c}}} /\ <<t, <<{a}, n>>>> e. ((( Ins2k Ins2k Sk i^i (_V X.k Ins2k Sk )) i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))"k~P1 ~P1 ~P1 ~P1 1c)))
36	27, 28, 35	3bitri 262	. . . . . . . . . . . . . . . 16 |- (<<{a}, n>> e. (((( Ins2k Ins2k Sk i^i (_V X.k Ins2k Sk )) i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))"k~P1 ~P1 ~P1 ~P1 1c)"k~P1 ~P1 1c) <-> E.cE.t(t = {{{c}}} /\ <<t, <<{a}, n>>>> e. ((( Ins2k Ins2k Sk i^i (_V X.k Ins2k Sk )) i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))"k~P1 ~P1 ~P1 ~P1 1c)))
37	20, 21, 3	otkelins3k 4256	. . . . . . . . . . . . . . . 16 |- (<<{{{a}}}, <<n, x>>>> e. Ins3k (((( Ins2k Ins2k Sk i^i (_V X.k Ins2k Sk )) i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))"k~P1 ~P1 ~P1 ~P1 1c)"k~P1 ~P1 1c) <-> <<{a}, n>> e. (((( Ins2k Ins2k Sk i^i (_V X.k Ins2k Sk )) i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))"k~P1 ~P1 ~P1 ~P1 1c)"k~P1 ~P1 1c))
38		eladdc 4398	. . . . . . . . . . . . . . . . 17 |- (a e. (n +o n) <-> E.b e. n E.c e. n ((b i^i c) = (/) /\ a = (b u. c)))
39		r2ex 2652	. . . . . . . . . . . . . . . . 17 |- (E.b e. n E.c e. n ((b i^i c) = (/) /\ a = (b u. c)) <-> E.bE.c((b e. n /\ c e. n) /\ ((b i^i c) = (/) /\ a = (b u. c))))
40		excom 1741	. . . . . . . . . . . . . . . . . 18 |- (E.bE.c((b e. n /\ c e. n) /\ ((b i^i c) = (/) /\ a = (b u. c))) <-> E.cE.b((b e. n /\ c e. n) /\ ((b i^i c) = (/) /\ a = (b u. c))))
41		snex 4111	. . . . . . . . . . . . . . . . . . . . 21 |- {{{c}}} e. _V
42		opkeq1 4059	. . . . . . . . . . . . . . . . . . . . . 22 |- (t = {{{c}}} -> <<t, <<{a}, n>>>> = <<{{{c}}}, <<{a}, n>>>>)
43	42	eleq1d 2419	. . . . . . . . . . . . . . . . . . . . 21 |- (t = {{{c}}} -> (<<t, <<{a}, n>>>> e. ((( Ins2k Ins2k Sk i^i (_V X.k Ins2k Sk )) i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))"k~P1 ~P1 ~P1 ~P1 1c) <-> <<{{{c}}}, <<{a}, n>>>> e. ((( Ins2k Ins2k Sk i^i (_V X.k Ins2k Sk )) i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))"k~P1 ~P1 ~P1 ~P1 1c)))
44	41, 43	ceqsexv 2894	. . . . . . . . . . . . . . . . . . . 20 |- (E.t(t = {{{c}}} /\ <<t, <<{a}, n>>>> e. ((( Ins2k Ins2k Sk i^i (_V X.k Ins2k Sk )) i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))"k~P1 ~P1 ~P1 ~P1 1c)) <-> <<{{{c}}}, <<{a}, n>>>> e. ((( Ins2k Ins2k Sk i^i (_V X.k Ins2k Sk )) i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))"k~P1 ~P1 ~P1 ~P1 1c))
45		opkex 4113	. . . . . . . . . . . . . . . . . . . . . 22 |- <<{{{c}}}, <<{a}, n>>>> e. _V
46	45	elimak 4259	. . . . . . . . . . . . . . . . . . . . 21 |- (<<{{{c}}}, <<{a}, n>>>> e. ((( Ins2k Ins2k Sk i^i (_V X.k Ins2k Sk )) i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))"k~P1 ~P1 ~P1 ~P1 1c) <-> E.t e. ~P1 ~P1 ~P1 ~P1 1c<<t, <<{{{c}}}, <<{a}, n>>>>>> e. (( Ins2k Ins2k Sk i^i (_V X.k Ins2k Sk )) i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c))))
47		df-rex 2620	. . . . . . . . . . . . . . . . . . . . 21 |- (E.t e. ~P1 ~P1 ~P1 ~P1 1c<<t, <<{{{c}}}, <<{a}, n>>>>>> e. (( Ins2k Ins2k Sk i^i (_V X.k Ins2k Sk )) i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c))) <-> E.t(t e. ~P1 ~P1 ~P1 ~P1 1c /\ <<t, <<{{{c}}}, <<{a}, n>>>>>> e. (( Ins2k Ins2k Sk i^i (_V X.k Ins2k Sk )) i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))))
48		elpw141c 4150	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (t e. ~P1 ~P1 ~P1 ~P1 1c <-> E.b t = {{{{{b}}}}})
49	48	anbi1i 676	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((t e. ~P1 ~P1 ~P1 ~P1 1c /\ <<t, <<{{{c}}}, <<{a}, n>>>>>> e. (( Ins2k Ins2k Sk i^i (_V X.k Ins2k Sk )) i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))) <-> (E.b t = {{{{{b}}}}} /\ <<t, <<{{{c}}}, <<{a}, n>>>>>> e. (( Ins2k Ins2k Sk i^i (_V X.k Ins2k Sk )) i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))))
50		19.41v 1901	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (E.b(t = {{{{{b}}}}} /\ <<t, <<{{{c}}}, <<{a}, n>>>>>> e. (( Ins2k Ins2k Sk i^i (_V X.k Ins2k Sk )) i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))) <-> (E.b t = {{{{{b}}}}} /\ <<t, <<{{{c}}}, <<{a}, n>>>>>> e. (( Ins2k Ins2k Sk i^i (_V X.k Ins2k Sk )) i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))))
51	49, 50	bitr4i 243	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((t e. ~P1 ~P1 ~P1 ~P1 1c /\ <<t, <<{{{c}}}, <<{a}, n>>>>>> e. (( Ins2k Ins2k Sk i^i (_V X.k Ins2k Sk )) i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))) <-> E.b(t = {{{{{b}}}}} /\ <<t, <<{{{c}}}, <<{a}, n>>>>>> e. (( Ins2k Ins2k Sk i^i (_V X.k Ins2k Sk )) i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))))
52	51	exbii 1582	. . . . . . . . . . . . . . . . . . . . . 22 |- (E.t(t e. ~P1 ~P1 ~P1 ~P1 1c /\ <<t, <<{{{c}}}, <<{a}, n>>>>>> e. (( Ins2k Ins2k Sk i^i (_V X.k Ins2k Sk )) i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))) <-> E.tE.b(t = {{{{{b}}}}} /\ <<t, <<{{{c}}}, <<{a}, n>>>>>> e. (( Ins2k Ins2k Sk i^i (_V X.k Ins2k Sk )) i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))))
53		excom 1741	. . . . . . . . . . . . . . . . . . . . . 22 |- (E.bE.t(t = {{{{{b}}}}} /\ <<t, <<{{{c}}}, <<{a}, n>>>>>> e. (( Ins2k Ins2k Sk i^i (_V X.k Ins2k Sk )) i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))) <-> E.tE.b(t = {{{{{b}}}}} /\ <<t, <<{{{c}}}, <<{a}, n>>>>>> e. (( Ins2k Ins2k Sk i^i (_V X.k Ins2k Sk )) i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))))
54	52, 53	bitr4i 243	. . . . . . . . . . . . . . . . . . . . 21 |- (E.t(t e. ~P1 ~P1 ~P1 ~P1 1c /\ <<t, <<{{{c}}}, <<{a}, n>>>>>> e. (( Ins2k Ins2k Sk i^i (_V X.k Ins2k Sk )) i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))) <-> E.bE.t(t = {{{{{b}}}}} /\ <<t, <<{{{c}}}, <<{a}, n>>>>>> e. (( Ins2k Ins2k Sk i^i (_V X.k Ins2k Sk )) i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))))
55	46, 47, 54	3bitri 262	. . . . . . . . . . . . . . . . . . . 20 |- (<<{{{c}}}, <<{a}, n>>>> e. ((( Ins2k Ins2k Sk i^i (_V X.k Ins2k Sk )) i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))"k~P1 ~P1 ~P1 ~P1 1c) <-> E.bE.t(t = {{{{{b}}}}} /\ <<t, <<{{{c}}}, <<{a}, n>>>>>> e. (( Ins2k Ins2k Sk i^i (_V X.k Ins2k Sk )) i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))))
56		snex 4111	. . . . . . . . . . . . . . . . . . . . . . 23 |- {{{{{b}}}}} e. _V
57		opkeq1 4059	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (t = {{{{{b}}}}} -> <<t, <<{{{c}}}, <<{a}, n>>>>>> = <<{{{{{b}}}}}, <<{{{c}}}, <<{a}, n>>>>>>)
58	57	eleq1d 2419	. . . . . . . . . . . . . . . . . . . . . . 23 |- (t = {{{{{b}}}}} -> (<<t, <<{{{c}}}, <<{a}, n>>>>>> e. (( Ins2k Ins2k Sk i^i (_V X.k Ins2k Sk )) i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c))) <-> <<{{{{{b}}}}}, <<{{{c}}}, <<{a}, n>>>>>> e. (( Ins2k Ins2k Sk i^i (_V X.k Ins2k Sk )) i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))))
59	56, 58	ceqsexv 2894	. . . . . . . . . . . . . . . . . . . . . 22 |- (E.t(t = {{{{{b}}}}} /\ <<t, <<{{{c}}}, <<{a}, n>>>>>> e. (( Ins2k Ins2k Sk i^i (_V X.k Ins2k Sk )) i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))) <-> <<{{{{{b}}}}}, <<{{{c}}}, <<{a}, n>>>>>> e. (( Ins2k Ins2k Sk i^i (_V X.k Ins2k Sk )) i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c))))
60		elin 3219	. . . . . . . . . . . . . . . . . . . . . 22 |- (<<{{{{{b}}}}}, <<{{{c}}}, <<{a}, n>>>>>> e. (( Ins2k Ins2k Sk i^i (_V X.k Ins2k Sk )) i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c))) <-> (<<{{{{{b}}}}}, <<{{{c}}}, <<{a}, n>>>>>> e. ( Ins2k Ins2k Sk i^i (_V X.k Ins2k Sk )) /\ <<{{{{{b}}}}}, <<{{{c}}}, <<{a}, n>>>>>> e. ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c))))
61		elin 3219	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (<<{{{{{b}}}}}, <<{{{c}}}, <<{a}, n>>>>>> e. ( Ins2k Ins2k Sk i^i (_V X.k Ins2k Sk )) <-> (<<{{{{{b}}}}}, <<{{{c}}}, <<{a}, n>>>>>> e. Ins2k Ins2k Sk /\ <<{{{{{b}}}}}, <<{{{c}}}, <<{a}, n>>>>>> e. (_V X.k Ins2k Sk )))
62		snex 4111	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- {{{b}}} e. _V
63	62, 41, 26	otkelins2k 4255	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (<<{{{{{b}}}}}, <<{{{c}}}, <<{a}, n>>>>>> e. Ins2k Ins2k Sk <-> <<{{{b}}}, <<{a}, n>>>> e. Ins2k Sk )
64		snex 4111	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- {b} e. _V
65	64, 20, 21	otkelins2k 4255	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (<<{{{b}}}, <<{a}, n>>>> e. Ins2k Sk <-> <<{b}, n>> e. Sk )
66		vex 2862	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- b e. _V
67	66, 21	elssetk 4270	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (<<{b}, n>> e. Sk <-> b e. n)
68	63, 65, 67	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (<<{{{{{b}}}}}, <<{{{c}}}, <<{a}, n>>>>>> e. Ins2k Ins2k Sk <-> b e. n)
69	56, 45	opkelxpk 4248	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (<<{{{{{b}}}}}, <<{{{c}}}, <<{a}, n>>>>>> e. (_V X.k Ins2k Sk ) <-> ({{{{{b}}}}} e. _V /\ <<{{{c}}}, <<{a}, n>>>> e. Ins2k Sk ))
70	56, 69	mpbiran 884	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (<<{{{{{b}}}}}, <<{{{c}}}, <<{a}, n>>>>>> e. (_V X.k Ins2k Sk ) <-> <<{{{c}}}, <<{a}, n>>>> e. Ins2k Sk )
71		snex 4111	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- {c} e. _V
72	71, 20, 21	otkelins2k 4255	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (<<{{{c}}}, <<{a}, n>>>> e. Ins2k Sk <-> <<{c}, n>> e. Sk )
73		vex 2862	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- c e. _V
74	73, 21	elssetk 4270	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (<<{c}, n>> e. Sk <-> c e. n)
75	70, 72, 74	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (<<{{{{{b}}}}}, <<{{{c}}}, <<{a}, n>>>>>> e. (_V X.k Ins2k Sk ) <-> c e. n)
76	68, 75	anbi12i 678	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((<<{{{{{b}}}}}, <<{{{c}}}, <<{a}, n>>>>>> e. Ins2k Ins2k Sk /\ <<{{{{{b}}}}}, <<{{{c}}}, <<{a}, n>>>>>> e. (_V X.k Ins2k Sk )) <-> (b e. n /\ c e. n))
77	61, 76	bitri 240	. . . . . . . . . . . . . . . . . . . . . . 23 |- (<<{{{{{b}}}}}, <<{{{c}}}, <<{a}, n>>>>>> e. ( Ins2k Ins2k Sk i^i (_V X.k Ins2k Sk )) <-> (b e. n /\ c e. n))
78		elin 3219	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (<<{{{{{b}}}}}, <<{{{c}}}, <<{a}, n>>>>>> e. ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)) <-> (<<{{{{{b}}}}}, <<{{{c}}}, <<{a}, n>>>>>> e. Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) /\ <<{{{{{b}}}}}, <<{{{c}}}, <<{a}, n>>>>>> e. ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))
79	62, 41, 26	otkelins3k 4256	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (<<{{{{{b}}}}}, <<{{{c}}}, <<{a}, n>>>>>> e. Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) <-> <<{{{b}}}, {{{c}}}>> e. SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c))
80		snex 4111	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- {{b}} e. _V
81		snex 4111	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- {{c}} e. _V
82	80, 81	opksnelsik 4265	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (<<{{{b}}}, {{{c}}}>> e. SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) <-> <<{{b}}, {{c}}>> e. SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c))
83	64, 71	opksnelsik 4265	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (<<{{b}}, {{c}}>> e. SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) <-> <<{b}, {c}>> e. SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c))
84	66, 73	opksnelsik 4265	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (<<{b}, {c}>> e. SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) <-> <<b, c>> e. ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c))
85	66, 73	ndisjrelk 4323	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (<<b, c>> e. (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) <-> (b i^i c) =/= (/))
86	85	notbii 287	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (-. <<b, c>> e. (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) <-> -. (b i^i c) =/= (/))
87		opkex 4113	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- <<b, c>> e. _V
88	87	elcompl 3225	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (<<b, c>> e. ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) <-> -. <<b, c>> e. (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c))
89		df-ne 2518	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((b i^i c) =/= (/) <-> -. (b i^i c) = (/))
90	89	con2bii 322	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((b i^i c) = (/) <-> -. (b i^i c) =/= (/))
91	86, 88, 90	3bitr4i 268	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (<<b, c>> e. ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) <-> (b i^i c) = (/))
92	83, 84, 91	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (<<{{b}}, {{c}}>> e. SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) <-> (b i^i c) = (/))
93	79, 82, 92	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (<<{{{{{b}}}}}, <<{{{c}}}, <<{a}, n>>>>>> e. Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) <-> (b i^i c) = (/))
94		opkex 4113	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- <<{{{{{b}}}}}, <<{{{c}}}, <<{a}, n>>>>>> e. _V
95	94	elimak 4259	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (<<{{{{{b}}}}}, <<{{{c}}}, <<{a}, n>>>>>> e. (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c) <-> E.t e. ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c<<t, <<{{{{{b}}}}}, <<{{{c}}}, <<{a}, n>>>>>>>> e. ( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk )))
96		elpw171c 4153	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (t e. ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c <-> E.x t = {{{{{{{{x}}}}}}}})
97	96	anbi1i 676	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ((t e. ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c /\ <<t, <<{{{{{b}}}}}, <<{{{c}}}, <<{a}, n>>>>>>>> e. ( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))) <-> (E.x t = {{{{{{{{x}}}}}}}} /\ <<t, <<{{{{{b}}}}}, <<{{{c}}}, <<{a}, n>>>>>>>> e. ( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))))
98		19.41v 1901	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (E.x(t = {{{{{{{{x}}}}}}}} /\ <<t, <<{{{{{b}}}}}, <<{{{c}}}, <<{a}, n>>>>>>>> e. ( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))) <-> (E.x t = {{{{{{{{x}}}}}}}} /\ <<t, <<{{{{{b}}}}}, <<{{{c}}}, <<{a}, n>>>>>>>> e. ( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))))
99	97, 98	bitr4i 243	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((t e. ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c /\ <<t, <<{{{{{b}}}}}, <<{{{c}}}, <<{a}, n>>>>>>>> e. ( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))) <-> E.x(t = {{{{{{{{x}}}}}}}} /\ <<t, <<{{{{{b}}}}}, <<{{{c}}}, <<{a}, n>>>>>>>> e. ( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))))
100	99	exbii 1582	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (E.t(t e. ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c /\ <<t, <<{{{{{b}}}}}, <<{{{c}}}, <<{a}, n>>>>>>>> e. ( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))) <-> E.tE.x(t = {{{{{{{{x}}}}}}}} /\ <<t, <<{{{{{b}}}}}, <<{{{c}}}, <<{a}, n>>>>>>>> e. ( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))))
101		df-rex 2620	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (E.t e. ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c<<t, <<{{{{{b}}}}}, <<{{{c}}}, <<{a}, n>>>>>>>> e. ( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk )) <-> E.t(t e. ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c /\ <<t, <<{{{{{b}}}}}, <<{{{c}}}, <<{a}, n>>>>>>>> e. ( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))))
102		excom 1741	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (E.xE.t(t = {{{{{{{{x}}}}}}}} /\ <<t, <<{{{{{b}}}}}, <<{{{c}}}, <<{a}, n>>>>>>>> e. ( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))) <-> E.tE.x(t = {{{{{{{{x}}}}}}}} /\ <<t, <<{{{{{b}}}}}, <<{{{c}}}, <<{a}, n>>>>>>>> e. ( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))))
103	100, 101, 102	3bitr4i 268	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (E.t e. ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c<<t, <<{{{{{b}}}}}, <<{{{c}}}, <<{a}, n>>>>>>>> e. ( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk )) <-> E.xE.t(t = {{{{{{{{x}}}}}}}} /\ <<t, <<{{{{{b}}}}}, <<{{{c}}}, <<{a}, n>>>>>>>> e. ( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))))
104		snex 4111	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- {{{{{{{{x}}}}}}}} e. _V
105		opkeq1 4059	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (t = {{{{{{{{x}}}}}}}} -> <<t, <<{{{{{b}}}}}, <<{{{c}}}, <<{a}, n>>>>>>>> = <<{{{{{{{{x}}}}}}}}, <<{{{{{b}}}}}, <<{{{c}}}, <<{a}, n>>>>>>>>)
106	105	eleq1d 2419	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (t = {{{{{{{{x}}}}}}}} -> (<<t, <<{{{{{b}}}}}, <<{{{c}}}, <<{a}, n>>>>>>>> e. ( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk )) <-> <<{{{{{{{{x}}}}}}}}, <<{{{{{b}}}}}, <<{{{c}}}, <<{a}, n>>>>>>>> e. ( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))))
107	104, 106	ceqsexv 2894	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (E.t(t = {{{{{{{{x}}}}}}}} /\ <<t, <<{{{{{b}}}}}, <<{{{c}}}, <<{a}, n>>>>>>>> e. ( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))) <-> <<{{{{{{{{x}}}}}}}}, <<{{{{{b}}}}}, <<{{{c}}}, <<{a}, n>>>>>>>> e. ( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk )))
108		elsymdif 3223	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (<<{{{{{{{{x}}}}}}}}, <<{{{{{b}}}}}, <<{{{c}}}, <<{a}, n>>>>>>>> e. ( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk )) <-> -. (<<{{{{{{{{x}}}}}}}}, <<{{{{{b}}}}}, <<{{{c}}}, <<{a}, n>>>>>>>> e. Ins2k Ins2k Ins3k SIk Sk <-> <<{{{{{{{{x}}}}}}}}, <<{{{{{b}}}}}, <<{{{c}}}, <<{a}, n>>>>>>>> e. ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk )))
109		snex 4111	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- {{{{{{x}}}}}} e. _V
110	109, 56, 45	otkelins2k 4255	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (<<{{{{{{{{x}}}}}}}}, <<{{{{{b}}}}}, <<{{{c}}}, <<{a}, n>>>>>>>> e. Ins2k Ins2k Ins3k SIk Sk <-> <<{{{{{{x}}}}}}, <<{{{c}}}, <<{a}, n>>>>>> e. Ins2k Ins3k SIk Sk )
111		snex 4111	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- {{{{x}}}} e. _V
112	111, 41, 26	otkelins2k 4255	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (<<{{{{{{x}}}}}}, <<{{{c}}}, <<{a}, n>>>>>> e. Ins2k Ins3k SIk Sk <-> <<{{{{x}}}}, <<{a}, n>>>> e. Ins3k SIk Sk )
113		snex 4111	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- {{x}} e. _V
114	113, 20, 21	otkelins3k 4256	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (<<{{{{x}}}}, <<{a}, n>>>> e. Ins3k SIk Sk <-> <<{{x}}, {a}>> e. SIk Sk )
115		snex 4111	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- {x} e. _V
116	115, 23	opksnelsik 4265	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (<<{{x}}, {a}>> e. SIk Sk <-> <<{x}, a>> e. Sk )
117	3, 23	elssetk 4270	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (<<{x}, a>> e. Sk <-> x e. a)
118	114, 116, 117	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (<<{{{{x}}}}, <<{a}, n>>>> e. Ins3k SIk Sk <-> x e. a)
119	110, 112, 118	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (<<{{{{{{{{x}}}}}}}}, <<{{{{{b}}}}}, <<{{{c}}}, <<{a}, n>>>>>>>> e. Ins2k Ins2k Ins3k SIk Sk <-> x e. a)
120	109, 56, 45	otkelins3k 4256	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (<<{{{{{{{{x}}}}}}}}, <<{{{{{b}}}}}, <<{{{c}}}, <<{a}, n>>>>>>>> e. Ins3k SIk SIk SIk SIk SIk Sk <-> <<{{{{{{x}}}}}}, {{{{{b}}}}}>> e. SIk SIk SIk SIk SIk Sk )
121		snex 4111	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- {{{{{x}}}}} e. _V
122		snex 4111	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- {{{{b}}}} e. _V
123	121, 122	opksnelsik 4265	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (<<{{{{{{x}}}}}}, {{{{{b}}}}}>> e. SIk SIk SIk SIk SIk Sk <-> <<{{{{{x}}}}}, {{{{b}}}}>> e. SIk SIk SIk SIk Sk )
124	111, 62	opksnelsik 4265	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- (<<{{{{{x}}}}}, {{{{b}}}}>> e. SIk SIk SIk SIk Sk <-> <<{{{{x}}}}, {{{b}}}>> e. SIk SIk SIk Sk )
125		snex 4111	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- {{{x}}} e. _V
126	125, 80	opksnelsik 4265	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- (<<{{{{x}}}}, {{{b}}}>> e. SIk SIk SIk Sk <-> <<{{{x}}}, {{b}}>> e. SIk SIk Sk )
127	113, 64	opksnelsik 4265	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- (<<{{{x}}}, {{b}}>> e. SIk SIk Sk <-> <<{{x}}, {b}>> e. SIk Sk )
128	115, 66	opksnelsik 4265	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- (<<{{x}}, {b}>> e. SIk Sk <-> <<{x}, b>> e. Sk )
129	3, 66	elssetk 4270	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- (<<{x}, b>> e. Sk <-> x e. b)
130	127, 128, 129	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- (<<{{{x}}}, {{b}}>> e. SIk SIk Sk <-> x e. b)
131	124, 126, 130	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (<<{{{{{x}}}}}, {{{{b}}}}>> e. SIk SIk SIk SIk Sk <-> x e. b)
132	120, 123, 131	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (<<{{{{{{{{x}}}}}}}}, <<{{{{{b}}}}}, <<{{{c}}}, <<{a}, n>>>>>>>> e. Ins3k SIk SIk SIk SIk SIk Sk <-> x e. b)
133	109, 56, 45	otkelins2k 4255	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (<<{{{{{{{{x}}}}}}}}, <<{{{{{b}}}}}, <<{{{c}}}, <<{a}, n>>>>>>>> e. Ins2k Ins3k SIk SIk SIk Sk <-> <<{{{{{{x}}}}}}, <<{{{c}}}, <<{a}, n>>>>>> e. Ins3k SIk SIk SIk Sk )
134	111, 41, 26	otkelins3k 4256	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (<<{{{{{{x}}}}}}, <<{{{c}}}, <<{a}, n>>>>>> e. Ins3k SIk SIk SIk Sk <-> <<{{{{x}}}}, {{{c}}}>> e. SIk SIk SIk Sk )
135	125, 81	opksnelsik 4265	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- (<<{{{{x}}}}, {{{c}}}>> e. SIk SIk SIk Sk <-> <<{{{x}}}, {{c}}>> e. SIk SIk Sk )
136	113, 71	opksnelsik 4265	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- (<<{{{x}}}, {{c}}>> e. SIk SIk Sk <-> <<{{x}}, {c}>> e. SIk Sk )
137	115, 73	opksnelsik 4265	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- (<<{{x}}, {c}>> e. SIk Sk <-> <<{x}, c>> e. Sk )
138	3, 73	elssetk 4270	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- (<<{x}, c>> e. Sk <-> x e. c)
139	137, 138	bitri 240	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- (<<{{x}}, {c}>> e. SIk Sk <-> x e. c)
140	135, 136, 139	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (<<{{{{x}}}}, {{{c}}}>> e. SIk SIk SIk Sk <-> x e. c)
141	133, 134, 140	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (<<{{{{{{{{x}}}}}}}}, <<{{{{{b}}}}}, <<{{{c}}}, <<{a}, n>>>>>>>> e. Ins2k Ins3k SIk SIk SIk Sk <-> x e. c)
142	132, 141	orbi12i 507	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ((<<{{{{{{{{x}}}}}}}}, <<{{{{{b}}}}}, <<{{{c}}}, <<{a}, n>>>>>>>> e. Ins3k SIk SIk SIk SIk SIk Sk \/ <<{{{{{{{{x}}}}}}}}, <<{{{{{b}}}}}, <<{{{c}}}, <<{a}, n>>>>>>>> e. Ins2k Ins3k SIk SIk SIk Sk ) <-> (x e. b \/ x e. c))
143		elun 3220	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (<<{{{{{{{{x}}}}}}}}, <<{{{{{b}}}}}, <<{{{c}}}, <<{a}, n>>>>>>>> e. ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ) <-> (<<{{{{{{{{x}}}}}}}}, <<{{{{{b}}}}}, <<{{{c}}}, <<{a}, n>>>>>>>> e. Ins3k SIk SIk SIk SIk SIk Sk \/ <<{{{{{{{{x}}}}}}}}, <<{{{{{b}}}}}, <<{{{c}}}, <<{a}, n>>>>>>>> e. Ins2k Ins3k SIk SIk SIk Sk ))
144		elun 3220	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (x e. (b u. c) <-> (x e. b \/ x e. c))
145	142, 143, 144	3bitr4i 268	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (<<{{{{{{{{x}}}}}}}}, <<{{{{{b}}}}}, <<{{{c}}}, <<{a}, n>>>>>>>> e. ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ) <-> x e. (b u. c))
146	119, 145	bibi12i 306	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ((<<{{{{{{{{x}}}}}}}}, <<{{{{{b}}}}}, <<{{{c}}}, <<{a}, n>>>>>>>> e. Ins2k Ins2k Ins3k SIk Sk <-> <<{{{{{{{{x}}}}}}}}, <<{{{{{b}}}}}, <<{{{c}}}, <<{a}, n>>>>>>>> e. ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk )) <-> (x e. a <-> x e. (b u. c)))
147	146	notbii 287	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (-. (<<{{{{{{{{x}}}}}}}}, <<{{{{{b}}}}}, <<{{{c}}}, <<{a}, n>>>>>>>> e. Ins2k Ins2k Ins3k SIk Sk <-> <<{{{{{{{{x}}}}}}}}, <<{{{{{b}}}}}, <<{{{c}}}, <<{a}, n>>>>>>>> e. ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk )) <-> -. (x e. a <-> x e. (b u. c)))
148	107, 108, 147	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (E.t(t = {{{{{{{{x}}}}}}}} /\ <<t, <<{{{{{b}}}}}, <<{{{c}}}, <<{a}, n>>>>>>>> e. ( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))) <-> -. (x e. a <-> x e. (b u. c)))
149	148	exbii 1582	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (E.xE.t(t = {{{{{{{{x}}}}}}}} /\ <<t, <<{{{{{b}}}}}, <<{{{c}}}, <<{a}, n>>>>>>>> e. ( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))) <-> E.x -. (x e. a <-> x e. (b u. c)))
150	95, 103, 149	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (<<{{{{{b}}}}}, <<{{{c}}}, <<{a}, n>>>>>> e. (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c) <-> E.x -. (x e. a <-> x e. (b u. c)))
151	150	notbii 287	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (-. <<{{{{{b}}}}}, <<{{{c}}}, <<{a}, n>>>>>> e. (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c) <-> -. E.x -. (x e. a <-> x e. (b u. c)))
152	94	elcompl 3225	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (<<{{{{{b}}}}}, <<{{{c}}}, <<{a}, n>>>>>> e. ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c) <-> -. <<{{{{{b}}}}}, <<{{{c}}}, <<{a}, n>>>>>> e. (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c))
153		dfcleq 2347	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (a = (b u. c) <-> A.x(x e. a <-> x e. (b u. c)))
154		alex 1572	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (A.x(x e. a <-> x e. (b u. c)) <-> -. E.x -. (x e. a <-> x e. (b u. c)))
155	153, 154	bitri 240	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (a = (b u. c) <-> -. E.x -. (x e. a <-> x e. (b u. c)))
156	151, 152, 155	3bitr4i 268	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (<<{{{{{b}}}}}, <<{{{c}}}, <<{a}, n>>>>>> e. ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c) <-> a = (b u. c))
157	93, 156	anbi12i 678	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((<<{{{{{b}}}}}, <<{{{c}}}, <<{a}, n>>>>>> e. Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) /\ <<{{{{{b}}}}}, <<{{{c}}}, <<{a}, n>>>>>> e. ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)) <-> ((b i^i c) = (/) /\ a = (b u. c)))
158	78, 157	bitri 240	. . . . . . . . . . . . . . . . . . . . . . 23 |- (<<{{{{{b}}}}}, <<{{{c}}}, <<{a}, n>>>>>> e. ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)) <-> ((b i^i c) = (/) /\ a = (b u. c)))
159	77, 158	anbi12i 678	. . . . . . . . . . . . . . . . . . . . . 22 |- ((<<{{{{{b}}}}}, <<{{{c}}}, <<{a}, n>>>>>> e. ( Ins2k Ins2k Sk i^i (_V X.k Ins2k Sk )) /\ <<{{{{{b}}}}}, <<{{{c}}}, <<{a}, n>>>>>> e. ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c))) <-> ((b e. n /\ c e. n) /\ ((b i^i c) = (/) /\ a = (b u. c))))
160	59, 60, 159	3bitri 262	. . . . . . . . . . . . . . . . . . . . 21 |- (E.t(t = {{{{{b}}}}} /\ <<t, <<{{{c}}}, <<{a}, n>>>>>> e. (( Ins2k Ins2k Sk i^i (_V X.k Ins2k Sk )) i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))) <-> ((b e. n /\ c e. n) /\ ((b i^i c) = (/) /\ a = (b u. c))))
161	160	exbii 1582	. . . . . . . . . . . . . . . . . . . 20 |- (E.bE.t(t = {{{{{b}}}}} /\ <<t, <<{{{c}}}, <<{a}, n>>>>>> e. (( Ins2k Ins2k Sk i^i (_V X.k Ins2k Sk )) i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))) <-> E.b((b e. n /\ c e. n) /\ ((b i^i c) = (/) /\ a = (b u. c))))
162	44, 55, 161	3bitri 262	. . . . . . . . . . . . . . . . . . 19 |- (E.t(t = {{{c}}} /\ <<t, <<{a}, n>>>> e. ((( Ins2k Ins2k Sk i^i (_V X.k Ins2k Sk )) i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))"k~P1 ~P1 ~P1 ~P1 1c)) <-> E.b((b e. n /\ c e. n) /\ ((b i^i c) = (/) /\ a = (b u. c))))
163	162	exbii 1582	. . . . . . . . . . . . . . . . . 18 |- (E.cE.t(t = {{{c}}} /\ <<t, <<{a}, n>>>> e. ((( Ins2k Ins2k Sk i^i (_V X.k Ins2k Sk )) i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))"k~P1 ~P1 ~P1 ~P1 1c)) <-> E.cE.b((b e. n /\ c e. n) /\ ((b i^i c) = (/) /\ a = (b u. c))))
164	40, 163	bitr4i 243	. . . . . . . . . . . . . . . . 17 |- (E.bE.c((b e. n /\ c e. n) /\ ((b i^i c) = (/) /\ a = (b u. c))) <-> E.cE.t(t = {{{c}}} /\ <<t, <<{a}, n>>>> e. ((( Ins2k Ins2k Sk i^i (_V X.k Ins2k Sk )) i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))"k~P1 ~P1 ~P1 ~P1 1c)))
165	38, 39, 164	3bitri 262	. . . . . . . . . . . . . . . 16 |- (a e. (n +o n) <-> E.cE.t(t = {{{c}}} /\ <<t, <<{a}, n>>>> e. ((( Ins2k Ins2k Sk i^i (_V X.k Ins2k Sk )) i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))"k~P1 ~P1 ~P1 ~P1 1c)))
166	36, 37, 165	3bitr4i 268	. . . . . . . . . . . . . . 15 |- (<<{{{a}}}, <<n, x>>>> e. Ins3k (((( Ins2k Ins2k Sk i^i (_V X.k Ins2k Sk )) i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))"k~P1 ~P1 ~P1 ~P1 1c)"k~P1 ~P1 1c) <-> a e. (n +o n))
167	25, 166	bibi12i 306	. . . . . . . . . . . . . 14 |- ((<<{{{a}}}, <<n, x>>>> e. Ins2k Sk <-> <<{{{a}}}, <<n, x>>>> e. Ins3k (((( Ins2k Ins2k Sk i^i (_V X.k Ins2k Sk )) i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))"k~P1 ~P1 ~P1 ~P1 1c)"k~P1 ~P1 1c)) <-> (a e. x <-> a e. (n +o n)))
168	167	notbii 287	. . . . . . . . . . . . 13 |- (-. (<<{{{a}}}, <<n, x>>>> e. Ins2k Sk <-> <<{{{a}}}, <<n, x>>>> e. Ins3k (((( Ins2k Ins2k Sk i^i (_V X.k Ins2k Sk )) i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))"k~P1 ~P1 ~P1 ~P1 1c)"k~P1 ~P1 1c)) <-> -. (a e. x <-> a e. (n +o n)))
169	18, 19, 168	3bitri 262	. . . . . . . . . . . 12 |- (E.t(t = {{{a}}} /\ <<t, <<n, x>>>> e. ( Ins2k Sk (+) Ins3k (((( Ins2k Ins2k Sk i^i (_V X.k Ins2k Sk )) i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))"k~P1 ~P1 ~P1 ~P1 1c)"k~P1 ~P1 1c))) <-> -. (a e. x <-> a e. (n +o n)))
170	169	exbii 1582	. . . . . . . . . . 11 |- (E.aE.t(t = {{{a}}} /\ <<t, <<n, x>>>> e. ( Ins2k Sk (+) Ins3k (((( Ins2k Ins2k Sk i^i (_V X.k Ins2k Sk )) i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))"k~P1 ~P1 ~P1 ~P1 1c)"k~P1 ~P1 1c))) <-> E.a -. (a e. x <-> a e. (n +o n)))
171	6, 14, 170	3bitri 262	. . . . . . . . . 10 |- (<<n, x>> e. (( Ins2k Sk (+) Ins3k (((( Ins2k Ins2k Sk i^i (_V X.k Ins2k Sk )) i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))"k~P1 ~P1 ~P1 ~P1 1c)"k~P1 ~P1 1c))"k~P1 ~P1 1c) <-> E.a -. (a e. x <-> a e. (n +o n)))
172	171	notbii 287	. . . . . . . . 9 |- (-. <<n, x>> e. (( Ins2k Sk (+) Ins3k (((( Ins2k Ins2k Sk i^i (_V X.k Ins2k Sk )) i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))"k~P1 ~P1 ~P1 ~P1 1c)"k~P1 ~P1 1c))"k~P1 ~P1 1c) <-> -. E.a -. (a e. x <-> a e. (n +o n)))
173	5	elcompl 3225	. . . . . . . . 9 |- (<<n, x>> e. ∼ (( Ins2k Sk (+) Ins3k (((( Ins2k Ins2k Sk i^i (_V X.k Ins2k Sk )) i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))"k~P1 ~P1 ~P1 ~P1 1c)"k~P1 ~P1 1c))"k~P1 ~P1 1c) <-> -. <<n, x>> e. (( Ins2k Sk (+) Ins3k (((( Ins2k Ins2k Sk i^i (_V X.k Ins2k Sk )) i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))"k~P1 ~P1 ~P1 ~P1 1c)"k~P1 ~P1 1c))"k~P1 ~P1 1c))
174		dfcleq 2347	. . . . . . . . . 10 |- (x = (n +o n) <-> A.a(a e. x <-> a e. (n +o n)))
175		alex 1572	. . . . . . . . . 10 |- (A.a(a e. x <-> a e. (n +o n)) <-> -. E.a -. (a e. x <-> a e. (n +o n)))
176	174, 175	bitri 240	. . . . . . . . 9 |- (x = (n +o n) <-> -. E.a -. (a e. x <-> a e. (n +o n)))
177	172, 173, 176	3bitr4i 268	. . . . . . . 8 |- (<<n, x>> e. ∼ (( Ins2k Sk (+) Ins3k (((( Ins2k Ins2k Sk i^i (_V X.k Ins2k Sk )) i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))"k~P1 ~P1 ~P1 ~P1 1c)"k~P1 ~P1 1c))"k~P1 ~P1 1c) <-> x = (n +o n))
178	177	rexbii 2639	. . . . . . 7 |- (E.n e. Nn <<n, x>> e. ∼ (( Ins2k Sk (+) Ins3k (((( Ins2k Ins2k Sk i^i (_V X.k Ins2k Sk )) i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))"k~P1 ~P1 ~P1 ~P1 1c)"k~P1 ~P1 1c))"k~P1 ~P1 1c) <-> E.n e. Nn x = (n +o n))
179	4, 178	bitri 240	. . . . . 6 |- (x e. ( ∼ (( Ins2k Sk (+) Ins3k (((( Ins2k Ins2k Sk i^i (_V X.k Ins2k Sk )) i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))"k~P1 ~P1 ~P1 ~P1 1c)"k~P1 ~P1 1c))"k~P1 ~P1 1c)"k Nn ) <-> E.n e. Nn x = (n +o n))
180	179	anbi1i 676	. . . . 5 |- ((x e. ( ∼ (( Ins2k Sk (+) Ins3k (((( Ins2k Ins2k Sk i^i (_V X.k Ins2k Sk )) i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))"k~P1 ~P1 ~P1 ~P1 1c)"k~P1 ~P1 1c))"k~P1 ~P1 1c)"k Nn ) /\ x =/= (/)) <-> (E.n e. Nn x = (n +o n) /\ x =/= (/)))
181	2, 180	bitri 240	. . . 4 |- (x e. (( ∼ (( Ins2k Sk (+) Ins3k (((( Ins2k Ins2k Sk i^i (_V X.k Ins2k Sk )) i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))"k~P1 ~P1 ~P1 ~P1 1c)"k~P1 ~P1 1c))"k~P1 ~P1 1c)"k Nn ) \ {(/)}) <-> (E.n e. Nn x = (n +o n) /\ x =/= (/)))
182	181	abbi2i 2464	. . 3 |- (( ∼ (( Ins2k Sk (+) Ins3k (((( Ins2k Ins2k Sk i^i (_V X.k Ins2k Sk )) i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))"k~P1 ~P1 ~P1 ~P1 1c)"k~P1 ~P1 1c))"k~P1 ~P1 1c)"k Nn ) \ {(/)}) = {x | (E.n e. Nn x = (n +o n) /\ x =/= (/))}
183	1, 182	eqtr4i 2376	. 2 |- Evenfin = (( ∼ (( Ins2k Sk (+) Ins3k (((( Ins2k Ins2k Sk i^i (_V X.k Ins2k Sk )) i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))"k~P1 ~P1 ~P1 ~P1 1c)"k~P1 ~P1 1c))"k~P1 ~P1 1c)"k Nn ) \ {(/)})
184		ssetkex 4294	. . . . . . . 8 |- Sk e. _V
185	184	ins2kex 4307	. . . . . . 7 |- Ins2k Sk e. _V
186	185	ins2kex 4307	. . . . . . . . . . . 12 |- Ins2k Ins2k Sk e. _V
187		vvex 4109	. . . . . . . . . . . . 13 |- _V e. _V
188	187, 185	xpkex 4289	. . . . . . . . . . . 12 |- (_V X.k Ins2k Sk ) e. _V
189	186, 188	inex 4105	. . . . . . . . . . 11 |- ( Ins2k Ins2k Sk i^i (_V X.k Ins2k Sk )) e. _V
190	184	ins3kex 4308	. . . . . . . . . . . . . . . . . . 19 |- Ins3k Sk e. _V
191	190, 185	inex 4105	. . . . . . . . . . . . . . . . . 18 |- ( Ins3k Sk i^i Ins2k Sk ) e. _V
192		1cex 4142	. . . . . . . . . . . . . . . . . . . 20 |- 1c e. _V
193	192	pw1ex 4303	. . . . . . . . . . . . . . . . . . 19 |- ~P1 1c e. _V
194	193	pw1ex 4303	. . . . . . . . . . . . . . . . . 18 |- ~P1 ~P1 1c e. _V
195	191, 194	imakex 4300	. . . . . . . . . . . . . . . . 17 |- (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) e. _V
196	195	complex 4104	. . . . . . . . . . . . . . . 16 |- ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) e. _V
197	196	sikex 4297	. . . . . . . . . . . . . . 15 |- SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) e. _V
198	197	sikex 4297	. . . . . . . . . . . . . 14 |- SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) e. _V
199	198	sikex 4297	. . . . . . . . . . . . 13 |- SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) e. _V
200	199	ins3kex 4308	. . . . . . . . . . . 12 |- Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) e. _V
201	184	sikex 4297	. . . . . . . . . . . . . . . . . 18 |- SIk Sk e. _V
202	201	ins3kex 4308	. . . . . . . . . . . . . . . . 17 |- Ins3k SIk Sk e. _V
203	202	ins2kex 4307	. . . . . . . . . . . . . . . 16 |- Ins2k Ins3k SIk Sk e. _V
204	203	ins2kex 4307	. . . . . . . . . . . . . . 15 |- Ins2k Ins2k Ins3k SIk Sk e. _V
205	201	sikex 4297	. . . . . . . . . . . . . . . . . . . 20 |- SIk SIk Sk e. _V
206	205	sikex 4297	. . . . . . . . . . . . . . . . . . 19 |- SIk SIk SIk Sk e. _V
207	206	sikex 4297	. . . . . . . . . . . . . . . . . 18 |- SIk SIk SIk SIk Sk e. _V
208	207	sikex 4297	. . . . . . . . . . . . . . . . 17 |- SIk SIk SIk SIk SIk Sk e. _V
209	208	ins3kex 4308	. . . . . . . . . . . . . . . 16 |- Ins3k SIk SIk SIk SIk SIk Sk e. _V
210	206	ins3kex 4308	. . . . . . . . . . . . . . . . 17 |- Ins3k SIk SIk SIk Sk e. _V
211	210	ins2kex 4307	. . . . . . . . . . . . . . . 16 |- Ins2k Ins3k SIk SIk SIk Sk e. _V
212	209, 211	unex 4106	. . . . . . . . . . . . . . 15 |- ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ) e. _V
213	204, 212	symdifex 4108	. . . . . . . . . . . . . 14 |- ( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk )) e. _V
214	194	pw1ex 4303	. . . . . . . . . . . . . . . . . 18 |- ~P1 ~P1 ~P1 1c e. _V
215	214	pw1ex 4303	. . . . . . . . . . . . . . . . 17 |- ~P1 ~P1 ~P1 ~P1 1c e. _V
216	215	pw1ex 4303	. . . . . . . . . . . . . . . 16 |- ~P1 ~P1 ~P1 ~P1 ~P1 1c e. _V
217	216	pw1ex 4303	. . . . . . . . . . . . . . 15 |- ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c e. _V
218	217	pw1ex 4303	. . . . . . . . . . . . . 14 |- ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c e. _V
219	213, 218	imakex 4300	. . . . . . . . . . . . 13 |- (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c) e. _V
220	219	complex 4104	. . . . . . . . . . . 12 |- ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c) e. _V
221	200, 220	inex 4105	. . . . . . . . . . 11 |- ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)) e. _V
222	189, 221	inex 4105	. . . . . . . . . 10 |- (( Ins2k Ins2k Sk i^i (_V X.k Ins2k Sk )) i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c))) e. _V
223	222, 215	imakex 4300	. . . . . . . . 9 |- ((( Ins2k Ins2k Sk i^i (_V X.k Ins2k Sk )) i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))"k~P1 ~P1 ~P1 ~P1 1c) e. _V
224	223, 194	imakex 4300	. . . . . . . 8 |- (((( Ins2k Ins2k Sk i^i (_V X.k Ins2k Sk )) i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))"k~P1 ~P1 ~P1 ~P1 1c)"k~P1 ~P1 1c) e. _V
225	224	ins3kex 4308	. . . . . . 7 |- Ins3k (((( Ins2k Ins2k Sk i^i (_V X.k Ins2k Sk )) i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))"k~P1 ~P1 ~P1 ~P1 1c)"k~P1 ~P1 1c) e. _V
226	185, 225	symdifex 4108	. . . . . 6 |- ( Ins2k Sk (+) Ins3k (((( Ins2k Ins2k Sk i^i (_V X.k Ins2k Sk )) i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))"k~P1 ~P1 ~P1 ~P1 1c)"k~P1 ~P1 1c)) e. _V
227	226, 194	imakex 4300	. . . . 5 |- (( Ins2k Sk (+) Ins3k (((( Ins2k Ins2k Sk i^i (_V X.k Ins2k Sk )) i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))"k~P1 ~P1 ~P1 ~P1 1c)"k~P1 ~P1 1c))"k~P1 ~P1 1c) e. _V
228	227	complex 4104	. . . 4 |- ∼ (( Ins2k Sk (+) Ins3k (((( Ins2k Ins2k Sk i^i (_V X.k Ins2k Sk )) i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))"k~P1 ~P1 ~P1 ~P1 1c)"k~P1 ~P1 1c))"k~P1 ~P1 1c) e. _V
229		nncex 4396	. . . 4 |- Nn e. _V
230	228, 229	imakex 4300	. . 3 |- ( ∼ (( Ins2k Sk (+) Ins3k (((( Ins2k Ins2k Sk i^i (_V X.k Ins2k Sk )) i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))"k~P1 ~P1 ~P1 ~P1 1c)"k~P1 ~P1 1c))"k~P1 ~P1 1c)"k Nn ) e. _V
231		snex 4111	. . 3 |- {(/)} e. _V
232	230, 231	difex 4107	. 2 |- (( ∼ (( Ins2k Sk (+) Ins3k (((( Ins2k Ins2k Sk i^i (_V X.k Ins2k Sk )) i^i ( Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))"k~P1 ~P1 ~P1 ~P1 1c)"k~P1 ~P1 1c))"k~P1 ~P1 1c)"k Nn ) \ {(/)}) e. _V
233	183, 232	eqeltri 2423	1 |- Evenfin e. _V

Syntax hints:  -. wn 3   <-> wb 176   \/ wo 357   /\ wa 358  A.wal 1540  E.wex 1541   = wceq 1642   e. wcel 1710  {cab 2339   =/= wne 2516  E.wrex 2615  _Vcvv 2859   ∼ ccompl 3205   \ cdif 3206   u. cun 3207   i^i cin 3208   (+) csymdif 3209  (/)c0 3550  {csn 3737  <<copk 4057  1_cc1c 4134  ~P₁ cpw1 4135   X._k cxpk 4174   Ins2_k cins2k 4176   Ins3_k cins3k 4177  "_kcimak 4179   SI_k csik 4181   S_k cssetk 4183   Nn cnnc 4373   +o cplc 4375   Even_fin 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