Theorem oddfinex 4504

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

Assertion

Ref	Expression
oddfinex	|- Oddfin e. _V

Proof of Theorem oddfinex

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

Step	Hyp	Ref	Expression
1		df-oddfin 4445	. . 3 |- Oddfin = {x | (E.n e. Nn x = ((n +o n) +o 1c) /\ x =/= (/))}
2		eldifsn 3839	. . . . 5 |- (x e. (( ∼ (( Ins2k Sk (+) Ins3k (((( Ins2k Ins2k (((( 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) i^i Ins3k `'k SIk SIk SIk ∼ Sk ) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 ~P1 ~P1 1c)"k~P1 ~P1 ~P1 1c))"k~P1 ~P1 1c)"k Nn ) \ {(/)}) <-> (x e. ( ∼ (( Ins2k Sk (+) Ins3k (((( Ins2k Ins2k (((( 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) i^i Ins3k `'k SIk SIk SIk ∼ Sk ) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 ~P1 ~P1 1c)"k~P1 ~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 (((( 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) i^i Ins3k `'k SIk SIk SIk ∼ Sk ) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 ~P1 ~P1 1c)"k~P1 ~P1 ~P1 1c))"k~P1 ~P1 1c)"k Nn ) <-> E.n e. Nn <<n, x>> e. ∼ (( Ins2k Sk (+) Ins3k (((( Ins2k Ins2k (((( 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) i^i Ins3k `'k SIk SIk SIk ∼ Sk ) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 ~P1 ~P1 1c)"k~P1 ~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 (((( 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) i^i Ins3k `'k SIk SIk SIk ∼ Sk ) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 ~P1 ~P1 1c)"k~P1 ~P1 ~P1 1c))"k~P1 ~P1 1c) <-> E.t e. ~P1 ~P1 1c<<t, <<n, x>>>> e. ( Ins2k Sk (+) Ins3k (((( Ins2k Ins2k (((( 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) i^i Ins3k `'k SIk SIk SIk ∼ Sk ) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 ~P1 ~P1 1c)"k~P1 ~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 (((( 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) i^i Ins3k `'k SIk SIk SIk ∼ Sk ) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 ~P1 ~P1 1c)"k~P1 ~P1 ~P1 1c))) <-> (E.a t = {{{a}}} /\ <<t, <<n, x>>>> e. ( Ins2k Sk (+) Ins3k (((( Ins2k Ins2k (((( 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) i^i Ins3k `'k SIk SIk SIk ∼ Sk ) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 ~P1 ~P1 1c)"k~P1 ~P1 ~P1 1c))))
9		19.41v 1901	. . . . . . . . . . . . . 14 |- (E.a(t = {{{a}}} /\ <<t, <<n, x>>>> e. ( Ins2k Sk (+) Ins3k (((( Ins2k Ins2k (((( 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) i^i Ins3k `'k SIk SIk SIk ∼ Sk ) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 ~P1 ~P1 1c)"k~P1 ~P1 ~P1 1c))) <-> (E.a t = {{{a}}} /\ <<t, <<n, x>>>> e. ( Ins2k Sk (+) Ins3k (((( Ins2k Ins2k (((( 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) i^i Ins3k `'k SIk SIk SIk ∼ Sk ) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 ~P1 ~P1 1c)"k~P1 ~P1 ~P1 1c))))
10	8, 9	bitr4i 243	. . . . . . . . . . . . 13 |- ((t e. ~P1 ~P1 1c /\ <<t, <<n, x>>>> e. ( Ins2k Sk (+) Ins3k (((( Ins2k Ins2k (((( 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) i^i Ins3k `'k SIk SIk SIk ∼ Sk ) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 ~P1 ~P1 1c)"k~P1 ~P1 ~P1 1c))) <-> E.a(t = {{{a}}} /\ <<t, <<n, x>>>> e. ( Ins2k Sk (+) Ins3k (((( Ins2k Ins2k (((( 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) i^i Ins3k `'k SIk SIk SIk ∼ Sk ) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 ~P1 ~P1 1c)"k~P1 ~P1 ~P1 1c))))
11	10	exbii 1582	. . . . . . . . . . . 12 |- (E.t(t e. ~P1 ~P1 1c /\ <<t, <<n, x>>>> e. ( Ins2k Sk (+) Ins3k (((( Ins2k Ins2k (((( 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) i^i Ins3k `'k SIk SIk SIk ∼ Sk ) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 ~P1 ~P1 1c)"k~P1 ~P1 ~P1 1c))) <-> E.tE.a(t = {{{a}}} /\ <<t, <<n, x>>>> e. ( Ins2k Sk (+) Ins3k (((( Ins2k Ins2k (((( 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) i^i Ins3k `'k SIk SIk SIk ∼ Sk ) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 ~P1 ~P1 1c)"k~P1 ~P1 ~P1 1c))))
12		df-rex 2620	. . . . . . . . . . . 12 |- (E.t e. ~P1 ~P1 1c<<t, <<n, x>>>> e. ( Ins2k Sk (+) Ins3k (((( Ins2k Ins2k (((( 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) i^i Ins3k `'k SIk SIk SIk ∼ Sk ) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 ~P1 ~P1 1c)"k~P1 ~P1 ~P1 1c)) <-> E.t(t e. ~P1 ~P1 1c /\ <<t, <<n, x>>>> e. ( Ins2k Sk (+) Ins3k (((( Ins2k Ins2k (((( 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) i^i Ins3k `'k SIk SIk SIk ∼ Sk ) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 ~P1 ~P1 1c)"k~P1 ~P1 ~P1 1c))))
13		excom 1741	. . . . . . . . . . . 12 |- (E.aE.t(t = {{{a}}} /\ <<t, <<n, x>>>> e. ( Ins2k Sk (+) Ins3k (((( Ins2k Ins2k (((( 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) i^i Ins3k `'k SIk SIk SIk ∼ Sk ) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 ~P1 ~P1 1c)"k~P1 ~P1 ~P1 1c))) <-> E.tE.a(t = {{{a}}} /\ <<t, <<n, x>>>> e. ( Ins2k Sk (+) Ins3k (((( Ins2k Ins2k (((( 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) i^i Ins3k `'k SIk SIk SIk ∼ Sk ) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 ~P1 ~P1 1c)"k~P1 ~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 (((( 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) i^i Ins3k `'k SIk SIk SIk ∼ Sk ) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 ~P1 ~P1 1c)"k~P1 ~P1 ~P1 1c)) <-> E.aE.t(t = {{{a}}} /\ <<t, <<n, x>>>> e. ( Ins2k Sk (+) Ins3k (((( Ins2k Ins2k (((( 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) i^i Ins3k `'k SIk SIk SIk ∼ Sk ) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 ~P1 ~P1 1c)"k~P1 ~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 (((( 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) i^i Ins3k `'k SIk SIk SIk ∼ Sk ) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 ~P1 ~P1 1c)"k~P1 ~P1 ~P1 1c)) <-> <<{{{a}}}, <<n, x>>>> e. ( Ins2k Sk (+) Ins3k (((( Ins2k Ins2k (((( 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) i^i Ins3k `'k SIk SIk SIk ∼ Sk ) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 ~P1 ~P1 1c)"k~P1 ~P1 ~P1 1c))))
18	15, 17	ceqsexv 2894	. . . . . . . . . . . . 13 |- (E.t(t = {{{a}}} /\ <<t, <<n, x>>>> e. ( Ins2k Sk (+) Ins3k (((( Ins2k Ins2k (((( 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) i^i Ins3k `'k SIk SIk SIk ∼ Sk ) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 ~P1 ~P1 1c)"k~P1 ~P1 ~P1 1c))) <-> <<{{{a}}}, <<n, x>>>> e. ( Ins2k Sk (+) Ins3k (((( Ins2k Ins2k (((( 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) i^i Ins3k `'k SIk SIk SIk ∼ Sk ) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 ~P1 ~P1 1c)"k~P1 ~P1 ~P1 1c)))
19		elsymdif 3223	. . . . . . . . . . . . 13 |- (<<{{{a}}}, <<n, x>>>> e. ( Ins2k Sk (+) Ins3k (((( Ins2k Ins2k (((( 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) i^i Ins3k `'k SIk SIk SIk ∼ Sk ) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 ~P1 ~P1 1c)"k~P1 ~P1 ~P1 1c)) <-> -. (<<{{{a}}}, <<n, x>>>> e. Ins2k Sk <-> <<{{{a}}}, <<n, x>>>> e. Ins3k (((( Ins2k Ins2k (((( 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) i^i Ins3k `'k SIk SIk SIk ∼ Sk ) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 ~P1 ~P1 1c)"k~P1 ~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 (((( 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) i^i Ins3k `'k SIk SIk SIk ∼ Sk ) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 ~P1 ~P1 1c)"k~P1 ~P1 ~P1 1c) <-> E.t e. ~P1 ~P1 ~P1 1c<<t, <<{a}, n>>>> e. ((( Ins2k Ins2k (((( 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) i^i Ins3k `'k SIk SIk SIk ∼ Sk ) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 ~P1 ~P1 1c))
28		df-rex 2620	. . . . . . . . . . . . . . . . . 18 |- (E.t e. ~P1 ~P1 ~P1 1c<<t, <<{a}, n>>>> e. ((( Ins2k Ins2k (((( 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) i^i Ins3k `'k SIk SIk SIk ∼ Sk ) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 ~P1 ~P1 1c) <-> E.t(t e. ~P1 ~P1 ~P1 1c /\ <<t, <<{a}, n>>>> e. ((( Ins2k Ins2k (((( 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) i^i Ins3k `'k SIk SIk SIk ∼ Sk ) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 ~P1 ~P1 1c)))
29		elpw131c 4149	. . . . . . . . . . . . . . . . . . . . 21 |- (t e. ~P1 ~P1 ~P1 1c <-> E.x t = {{{{x}}}})
30	29	anbi1i 676	. . . . . . . . . . . . . . . . . . . 20 |- ((t e. ~P1 ~P1 ~P1 1c /\ <<t, <<{a}, n>>>> e. ((( Ins2k Ins2k (((( 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) i^i Ins3k `'k SIk SIk SIk ∼ Sk ) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 ~P1 ~P1 1c)) <-> (E.x t = {{{{x}}}} /\ <<t, <<{a}, n>>>> e. ((( Ins2k Ins2k (((( 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) i^i Ins3k `'k SIk SIk SIk ∼ Sk ) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 ~P1 ~P1 1c)))
31		19.41v 1901	. . . . . . . . . . . . . . . . . . . 20 |- (E.x(t = {{{{x}}}} /\ <<t, <<{a}, n>>>> e. ((( Ins2k Ins2k (((( 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) i^i Ins3k `'k SIk SIk SIk ∼ Sk ) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 ~P1 ~P1 1c)) <-> (E.x t = {{{{x}}}} /\ <<t, <<{a}, n>>>> e. ((( Ins2k Ins2k (((( 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) i^i Ins3k `'k SIk SIk SIk ∼ Sk ) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k _I_kk ))"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 ~P1 1c /\ <<t, <<{a}, n>>>> e. ((( Ins2k Ins2k (((( 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) i^i Ins3k `'k SIk SIk SIk ∼ Sk ) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 ~P1 ~P1 1c)) <-> E.x(t = {{{{x}}}} /\ <<t, <<{a}, n>>>> e. ((( Ins2k Ins2k (((( 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) i^i Ins3k `'k SIk SIk SIk ∼ Sk ) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k _I_kk ))"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 ~P1 1c /\ <<t, <<{a}, n>>>> e. ((( Ins2k Ins2k (((( 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) i^i Ins3k `'k SIk SIk SIk ∼ Sk ) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 ~P1 ~P1 1c)) <-> E.tE.x(t = {{{{x}}}} /\ <<t, <<{a}, n>>>> e. ((( Ins2k Ins2k (((( 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) i^i Ins3k `'k SIk SIk SIk ∼ Sk ) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 ~P1 ~P1 1c)))
34		excom 1741	. . . . . . . . . . . . . . . . . 18 |- (E.tE.x(t = {{{{x}}}} /\ <<t, <<{a}, n>>>> e. ((( Ins2k Ins2k (((( 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) i^i Ins3k `'k SIk SIk SIk ∼ Sk ) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 ~P1 ~P1 1c)) <-> E.xE.t(t = {{{{x}}}} /\ <<t, <<{a}, n>>>> e. ((( Ins2k Ins2k (((( 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) i^i Ins3k `'k SIk SIk SIk ∼ Sk ) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 ~P1 ~P1 1c)))
35	28, 33, 34	3bitri 262	. . . . . . . . . . . . . . . . 17 |- (E.t e. ~P1 ~P1 ~P1 1c<<t, <<{a}, n>>>> e. ((( Ins2k Ins2k (((( 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) i^i Ins3k `'k SIk SIk SIk ∼ Sk ) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 ~P1 ~P1 1c) <-> E.xE.t(t = {{{{x}}}} /\ <<t, <<{a}, n>>>> e. ((( Ins2k Ins2k (((( 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) i^i Ins3k `'k SIk SIk SIk ∼ Sk ) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 ~P1 ~P1 1c)))
36		snex 4111	. . . . . . . . . . . . . . . . . . . 20 |- {{{{x}}}} e. _V
37		opkeq1 4059	. . . . . . . . . . . . . . . . . . . . 21 |- (t = {{{{x}}}} -> <<t, <<{a}, n>>>> = <<{{{{x}}}}, <<{a}, n>>>>)
38	37	eleq1d 2419	. . . . . . . . . . . . . . . . . . . 20 |- (t = {{{{x}}}} -> (<<t, <<{a}, n>>>> e. ((( Ins2k Ins2k (((( 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) i^i Ins3k `'k SIk SIk SIk ∼ Sk ) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 ~P1 ~P1 1c) <-> <<{{{{x}}}}, <<{a}, n>>>> e. ((( Ins2k Ins2k (((( 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) i^i Ins3k `'k SIk SIk SIk ∼ Sk ) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 ~P1 ~P1 1c)))
39	36, 38	ceqsexv 2894	. . . . . . . . . . . . . . . . . . 19 |- (E.t(t = {{{{x}}}} /\ <<t, <<{a}, n>>>> e. ((( Ins2k Ins2k (((( 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) i^i Ins3k `'k SIk SIk SIk ∼ Sk ) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 ~P1 ~P1 1c)) <-> <<{{{{x}}}}, <<{a}, n>>>> e. ((( Ins2k Ins2k (((( 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) i^i Ins3k `'k SIk SIk SIk ∼ Sk ) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 ~P1 ~P1 1c))
40		opkex 4113	. . . . . . . . . . . . . . . . . . . . 21 |- <<{{{{x}}}}, <<{a}, n>>>> e. _V
41	40	elimak 4259	. . . . . . . . . . . . . . . . . . . 20 |- (<<{{{{x}}}}, <<{a}, n>>>> e. ((( Ins2k Ins2k (((( 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) i^i Ins3k `'k SIk SIk SIk ∼ Sk ) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 ~P1 ~P1 1c) <-> E.t e. ~P1 ~P1 ~P1 ~P1 1c<<t, <<{{{{x}}}}, <<{a}, n>>>>>> e. (( Ins2k Ins2k (((( 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) i^i Ins3k `'k SIk SIk SIk ∼ Sk ) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))
42		df-rex 2620	. . . . . . . . . . . . . . . . . . . 20 |- (E.t e. ~P1 ~P1 ~P1 ~P1 1c<<t, <<{{{{x}}}}, <<{a}, n>>>>>> e. (( Ins2k Ins2k (((( 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) i^i Ins3k `'k SIk SIk SIk ∼ Sk ) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)) <-> E.t(t e. ~P1 ~P1 ~P1 ~P1 1c /\ <<t, <<{{{{x}}}}, <<{a}, n>>>>>> e. (( Ins2k Ins2k (((( 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) i^i Ins3k `'k SIk SIk SIk ∼ Sk ) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c))))
43		elpw141c 4150	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (t e. ~P1 ~P1 ~P1 ~P1 1c <-> E.b t = {{{{{b}}}}})
44	43	anbi1i 676	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((t e. ~P1 ~P1 ~P1 ~P1 1c /\ <<t, <<{{{{x}}}}, <<{a}, n>>>>>> e. (( Ins2k Ins2k (((( 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) i^i Ins3k `'k SIk SIk SIk ∼ Sk ) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c))) <-> (E.b t = {{{{{b}}}}} /\ <<t, <<{{{{x}}}}, <<{a}, n>>>>>> e. (( Ins2k Ins2k (((( 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) i^i Ins3k `'k SIk SIk SIk ∼ Sk ) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c))))
45		19.41v 1901	. . . . . . . . . . . . . . . . . . . . . . 23 |- (E.b(t = {{{{{b}}}}} /\ <<t, <<{{{{x}}}}, <<{a}, n>>>>>> e. (( Ins2k Ins2k (((( 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) i^i Ins3k `'k SIk SIk SIk ∼ Sk ) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c))) <-> (E.b t = {{{{{b}}}}} /\ <<t, <<{{{{x}}}}, <<{a}, n>>>>>> e. (( Ins2k Ins2k (((( 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) i^i Ins3k `'k SIk SIk SIk ∼ Sk ) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c))))
46	44, 45	bitr4i 243	. . . . . . . . . . . . . . . . . . . . . 22 |- ((t e. ~P1 ~P1 ~P1 ~P1 1c /\ <<t, <<{{{{x}}}}, <<{a}, n>>>>>> e. (( Ins2k Ins2k (((( 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) i^i Ins3k `'k SIk SIk SIk ∼ Sk ) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c))) <-> E.b(t = {{{{{b}}}}} /\ <<t, <<{{{{x}}}}, <<{a}, n>>>>>> e. (( Ins2k Ins2k (((( 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) i^i Ins3k `'k SIk SIk SIk ∼ Sk ) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c))))
47	46	exbii 1582	. . . . . . . . . . . . . . . . . . . . 21 |- (E.t(t e. ~P1 ~P1 ~P1 ~P1 1c /\ <<t, <<{{{{x}}}}, <<{a}, n>>>>>> e. (( Ins2k Ins2k (((( 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) i^i Ins3k `'k SIk SIk SIk ∼ Sk ) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c))) <-> E.tE.b(t = {{{{{b}}}}} /\ <<t, <<{{{{x}}}}, <<{a}, n>>>>>> e. (( Ins2k Ins2k (((( 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) i^i Ins3k `'k SIk SIk SIk ∼ Sk ) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c))))
48		excom 1741	. . . . . . . . . . . . . . . . . . . . 21 |- (E.bE.t(t = {{{{{b}}}}} /\ <<t, <<{{{{x}}}}, <<{a}, n>>>>>> e. (( Ins2k Ins2k (((( 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) i^i Ins3k `'k SIk SIk SIk ∼ Sk ) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c))) <-> E.tE.b(t = {{{{{b}}}}} /\ <<t, <<{{{{x}}}}, <<{a}, n>>>>>> e. (( Ins2k Ins2k (((( 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) i^i Ins3k `'k SIk SIk SIk ∼ Sk ) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c))))
49	47, 48	bitr4i 243	. . . . . . . . . . . . . . . . . . . 20 |- (E.t(t e. ~P1 ~P1 ~P1 ~P1 1c /\ <<t, <<{{{{x}}}}, <<{a}, n>>>>>> e. (( Ins2k Ins2k (((( 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) i^i Ins3k `'k SIk SIk SIk ∼ Sk ) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c))) <-> E.bE.t(t = {{{{{b}}}}} /\ <<t, <<{{{{x}}}}, <<{a}, n>>>>>> e. (( Ins2k Ins2k (((( 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) i^i Ins3k `'k SIk SIk SIk ∼ Sk ) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c))))
50	41, 42, 49	3bitri 262	. . . . . . . . . . . . . . . . . . 19 |- (<<{{{{x}}}}, <<{a}, n>>>> e. ((( Ins2k Ins2k (((( 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) i^i Ins3k `'k SIk SIk SIk ∼ Sk ) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 ~P1 ~P1 1c) <-> E.bE.t(t = {{{{{b}}}}} /\ <<t, <<{{{{x}}}}, <<{a}, n>>>>>> e. (( Ins2k Ins2k (((( 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) i^i Ins3k `'k SIk SIk SIk ∼ Sk ) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c))))
51		snex 4111	. . . . . . . . . . . . . . . . . . . . . 22 |- {{{{{b}}}}} e. _V
52		opkeq1 4059	. . . . . . . . . . . . . . . . . . . . . . 23 |- (t = {{{{{b}}}}} -> <<t, <<{{{{x}}}}, <<{a}, n>>>>>> = <<{{{{{b}}}}}, <<{{{{x}}}}, <<{a}, n>>>>>>)
53	52	eleq1d 2419	. . . . . . . . . . . . . . . . . . . . . 22 |- (t = {{{{{b}}}}} -> (<<t, <<{{{{x}}}}, <<{a}, n>>>>>> e. (( Ins2k Ins2k (((( 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) i^i Ins3k `'k SIk SIk SIk ∼ Sk ) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)) <-> <<{{{{{b}}}}}, <<{{{{x}}}}, <<{a}, n>>>>>> e. (( Ins2k Ins2k (((( 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) i^i Ins3k `'k SIk SIk SIk ∼ Sk ) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c))))
54	51, 53	ceqsexv 2894	. . . . . . . . . . . . . . . . . . . . 21 |- (E.t(t = {{{{{b}}}}} /\ <<t, <<{{{{x}}}}, <<{a}, n>>>>>> e. (( Ins2k Ins2k (((( 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) i^i Ins3k `'k SIk SIk SIk ∼ Sk ) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c))) <-> <<{{{{{b}}}}}, <<{{{{x}}}}, <<{a}, n>>>>>> e. (( Ins2k Ins2k (((( 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) i^i Ins3k `'k SIk SIk SIk ∼ Sk ) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))
55		elin 3219	. . . . . . . . . . . . . . . . . . . . 21 |- (<<{{{{{b}}}}}, <<{{{{x}}}}, <<{a}, n>>>>>> e. (( Ins2k Ins2k (((( 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) i^i Ins3k `'k SIk SIk SIk ∼ Sk ) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)) <-> (<<{{{{{b}}}}}, <<{{{{x}}}}, <<{a}, n>>>>>> e. ( Ins2k Ins2k (((( 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) i^i Ins3k `'k SIk SIk SIk ∼ Sk ) /\ <<{{{{{b}}}}}, <<{{{{x}}}}, <<{a}, n>>>>>> e. ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)))
56		elin 3219	. . . . . . . . . . . . . . . . . . . . . . 23 |- (<<{{{{{b}}}}}, <<{{{{x}}}}, <<{a}, n>>>>>> e. ( Ins2k Ins2k (((( 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) i^i Ins3k `'k SIk SIk SIk ∼ Sk ) <-> (<<{{{{{b}}}}}, <<{{{{x}}}}, <<{a}, n>>>>>> e. Ins2k Ins2k (((( 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) /\ <<{{{{{b}}}}}, <<{{{{x}}}}, <<{a}, n>>>>>> e. Ins3k `'k SIk SIk SIk ∼ Sk ))
57		snex 4111	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- {{{b}}} e. _V
58	57, 36, 26	otkelins2k 4255	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (<<{{{{{b}}}}}, <<{{{{x}}}}, <<{a}, n>>>>>> e. Ins2k Ins2k (((( 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) <-> <<{{{b}}}, <<{a}, n>>>> e. Ins2k (((( 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))
59		snex 4111	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- {b} e. _V
60	59, 20, 21	otkelins2k 4255	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (<<{{{b}}}, <<{a}, n>>>> e. Ins2k (((( 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) <-> <<{b}, 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))
61		opkex 4113	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- <<{b}, n>> e. _V
62	61	elimak 4259	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (<<{b}, 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, <<{b}, 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))
63		elpw121c 4148	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (t e. ~P1 ~P1 1c <-> E.c t = {{{c}}})
64	63	anbi1i 676	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((t e. ~P1 ~P1 1c /\ <<t, <<{b}, 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, <<{b}, 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)))
65		19.41v 1901	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (E.c(t = {{{c}}} /\ <<t, <<{b}, 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, <<{b}, 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)))
66	64, 65	bitr4i 243	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((t e. ~P1 ~P1 1c /\ <<t, <<{b}, 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, <<{b}, 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)))
67	66	exbii 1582	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (E.t(t e. ~P1 ~P1 1c /\ <<t, <<{b}, 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, <<{b}, 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)))
68		df-rex 2620	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (E.t e. ~P1 ~P1 1c<<t, <<{b}, 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, <<{b}, 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)))
69		excom 1741	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (E.cE.t(t = {{{c}}} /\ <<t, <<{b}, 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, <<{b}, 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)))
70	67, 68, 69	3bitr4i 268	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (E.t e. ~P1 ~P1 1c<<t, <<{b}, 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, <<{b}, 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)))
71		snex 4111	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- {{{c}}} e. _V
72		opkeq1 4059	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (t = {{{c}}} -> <<t, <<{b}, n>>>> = <<{{{c}}}, <<{b}, n>>>>)
73	72	eleq1d 2419	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (t = {{{c}}} -> (<<t, <<{b}, 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}}}, <<{b}, 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)))
74	71, 73	ceqsexv 2894	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (E.t(t = {{{c}}} /\ <<t, <<{b}, 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}}}, <<{b}, 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))
75		opkex 4113	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- <<{{{c}}}, <<{b}, n>>>> e. _V
76	75	elimak 4259	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (<<{{{c}}}, <<{b}, 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}}}, <<{b}, 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))))
77		df-rex 2620	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (E.t e. ~P1 ~P1 ~P1 ~P1 1c<<t, <<{{{c}}}, <<{b}, 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}}}, <<{b}, 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)))))
78		elpw141c 4150	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (t e. ~P1 ~P1 ~P1 ~P1 1c <-> E.a t = {{{{{a}}}}})
79	78	anbi1i 676	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ((t e. ~P1 ~P1 ~P1 ~P1 1c /\ <<t, <<{{{c}}}, <<{b}, 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.a t = {{{{{a}}}}} /\ <<t, <<{{{c}}}, <<{b}, 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)))))
80		19.41v 1901	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (E.a(t = {{{{{a}}}}} /\ <<t, <<{{{c}}}, <<{b}, 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.a t = {{{{{a}}}}} /\ <<t, <<{{{c}}}, <<{b}, 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)))))
81	79, 80	bitr4i 243	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ((t e. ~P1 ~P1 ~P1 ~P1 1c /\ <<t, <<{{{c}}}, <<{b}, 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.a(t = {{{{{a}}}}} /\ <<t, <<{{{c}}}, <<{b}, 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)))))
82	81	exbii 1582	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (E.t(t e. ~P1 ~P1 ~P1 ~P1 1c /\ <<t, <<{{{c}}}, <<{b}, 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.a(t = {{{{{a}}}}} /\ <<t, <<{{{c}}}, <<{b}, 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)))))
83		excom 1741	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (E.aE.t(t = {{{{{a}}}}} /\ <<t, <<{{{c}}}, <<{b}, 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.a(t = {{{{{a}}}}} /\ <<t, <<{{{c}}}, <<{b}, 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)))))
84	82, 83	bitr4i 243	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (E.t(t e. ~P1 ~P1 ~P1 ~P1 1c /\ <<t, <<{{{c}}}, <<{b}, 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.aE.t(t = {{{{{a}}}}} /\ <<t, <<{{{c}}}, <<{b}, 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)))))
85	76, 77, 84	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (<<{{{c}}}, <<{b}, 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.aE.t(t = {{{{{a}}}}} /\ <<t, <<{{{c}}}, <<{b}, 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)))))
86		snex 4111	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- {{{{{a}}}}} e. _V
87		opkeq1 4059	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (t = {{{{{a}}}}} -> <<t, <<{{{c}}}, <<{b}, n>>>>>> = <<{{{{{a}}}}}, <<{{{c}}}, <<{b}, n>>>>>>)
88	87	eleq1d 2419	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (t = {{{{{a}}}}} -> (<<t, <<{{{c}}}, <<{b}, 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))) <-> <<{{{{{a}}}}}, <<{{{c}}}, <<{b}, 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)))))
89	86, 88	ceqsexv 2894	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (E.t(t = {{{{{a}}}}} /\ <<t, <<{{{c}}}, <<{b}, 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)))) <-> <<{{{{{a}}}}}, <<{{{c}}}, <<{b}, 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))))
90		elin 3219	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (<<{{{{{a}}}}}, <<{{{c}}}, <<{b}, 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))) <-> (<<{{{{{a}}}}}, <<{{{c}}}, <<{b}, n>>>>>> e. ( Ins2k Ins2k Sk i^i (_V X.k Ins2k Sk )) /\ <<{{{{{a}}}}}, <<{{{c}}}, <<{b}, 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))))
91		elin 3219	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (<<{{{{{a}}}}}, <<{{{c}}}, <<{b}, n>>>>>> e. ( Ins2k Ins2k Sk i^i (_V X.k Ins2k Sk )) <-> (<<{{{{{a}}}}}, <<{{{c}}}, <<{b}, n>>>>>> e. Ins2k Ins2k Sk /\ <<{{{{{a}}}}}, <<{{{c}}}, <<{b}, n>>>>>> e. (_V X.k Ins2k Sk )))
92	15, 71, 61	otkelins2k 4255	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (<<{{{{{a}}}}}, <<{{{c}}}, <<{b}, n>>>>>> e. Ins2k Ins2k Sk <-> <<{{{a}}}, <<{b}, n>>>> e. Ins2k Sk )
93	20, 59, 21	otkelins2k 4255	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (<<{{{a}}}, <<{b}, n>>>> e. Ins2k Sk <-> <<{a}, n>> e. Sk )
94	23, 21	elssetk 4270	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (<<{a}, n>> e. Sk <-> a e. n)
95	92, 93, 94	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (<<{{{{{a}}}}}, <<{{{c}}}, <<{b}, n>>>>>> e. Ins2k Ins2k Sk <-> a e. n)
96	86, 75	opkelxpk 4248	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- (<<{{{{{a}}}}}, <<{{{c}}}, <<{b}, n>>>>>> e. (_V X.k Ins2k Sk ) <-> ({{{{{a}}}}} e. _V /\ <<{{{c}}}, <<{b}, n>>>> e. Ins2k Sk ))
97	86, 96	mpbiran 884	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (<<{{{{{a}}}}}, <<{{{c}}}, <<{b}, n>>>>>> e. (_V X.k Ins2k Sk ) <-> <<{{{c}}}, <<{b}, n>>>> e. Ins2k Sk )
98		snex 4111	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- {c} e. _V
99	98, 59, 21	otkelins2k 4255	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (<<{{{c}}}, <<{b}, n>>>> e. Ins2k Sk <-> <<{c}, n>> e. Sk )
100		vex 2862	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- c e. _V
101	100, 21	elssetk 4270	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (<<{c}, n>> e. Sk <-> c e. n)
102	97, 99, 101	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (<<{{{{{a}}}}}, <<{{{c}}}, <<{b}, n>>>>>> e. (_V X.k Ins2k Sk ) <-> c e. n)
103	95, 102	anbi12i 678	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ((<<{{{{{a}}}}}, <<{{{c}}}, <<{b}, n>>>>>> e. Ins2k Ins2k Sk /\ <<{{{{{a}}}}}, <<{{{c}}}, <<{b}, n>>>>>> e. (_V X.k Ins2k Sk )) <-> (a e. n /\ c e. n))
104	91, 103	bitri 240	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (<<{{{{{a}}}}}, <<{{{c}}}, <<{b}, n>>>>>> e. ( Ins2k Ins2k Sk i^i (_V X.k Ins2k Sk )) <-> (a e. n /\ c e. n))
105		elin 3219	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (<<{{{{{a}}}}}, <<{{{c}}}, <<{b}, 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)) <-> (<<{{{{{a}}}}}, <<{{{c}}}, <<{b}, n>>>>>> e. Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) /\ <<{{{{{a}}}}}, <<{{{c}}}, <<{b}, 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)))
106	15, 71, 61	otkelins3k 4256	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (<<{{{{{a}}}}}, <<{{{c}}}, <<{b}, n>>>>>> e. Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) <-> <<{{{a}}}, {{{c}}}>> e. SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c))
107		snex 4111	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- {{a}} e. _V
108		snex 4111	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- {{c}} e. _V
109	107, 108	opksnelsik 4265	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (<<{{{a}}}, {{{c}}}>> e. SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) <-> <<{{a}}, {{c}}>> e. SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c))
110	20, 98	opksnelsik 4265	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- (<<{{a}}, {{c}}>> e. SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) <-> <<{a}, {c}>> e. SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c))
111	23, 100	opksnelsik 4265	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- (<<{a}, {c}>> e. SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) <-> <<a, c>> e. ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c))
112	23, 100	ndisjrelk 4323	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- (<<a, c>> e. (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) <-> (a i^i c) =/= (/))
113	112	notbii 287	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- (-. <<a, c>> e. (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) <-> -. (a i^i c) =/= (/))
114		opkex 4113	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- <<a, c>> e. _V
115	114	elcompl 3225	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- (<<a, c>> e. ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) <-> -. <<a, c>> e. (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c))
116		df-ne 2518	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ((a i^i c) =/= (/) <-> -. (a i^i c) = (/))
117	116	con2bii 322	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ((a i^i c) = (/) <-> -. (a i^i c) =/= (/))
118	113, 115, 117	3bitr4i 268	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- (<<a, c>> e. ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) <-> (a i^i c) = (/))
119	110, 111, 118	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (<<{{a}}, {{c}}>> e. SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) <-> (a i^i c) = (/))
120	106, 109, 119	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (<<{{{{{a}}}}}, <<{{{c}}}, <<{b}, n>>>>>> e. Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) <-> (a i^i c) = (/))
121		opkex 4113	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- <<{{{{{a}}}}}, <<{{{c}}}, <<{b}, n>>>>>> e. _V
122	121	elimak 4259	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- (<<{{{{{a}}}}}, <<{{{c}}}, <<{b}, 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, <<{{{{{a}}}}}, <<{{{c}}}, <<{b}, n>>>>>>>> e. ( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk )))
123		elpw171c 4153	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- (t e. ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c <-> E.x t = {{{{{{{{x}}}}}}}})
124	123	anbi1i 676	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- ((t e. ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c /\ <<t, <<{{{{{a}}}}}, <<{{{c}}}, <<{b}, 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, <<{{{{{a}}}}}, <<{{{c}}}, <<{b}, n>>>>>>>> e. ( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))))
125		19.41v 1901	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- (E.x(t = {{{{{{{{x}}}}}}}} /\ <<t, <<{{{{{a}}}}}, <<{{{c}}}, <<{b}, 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, <<{{{{{a}}}}}, <<{{{c}}}, <<{b}, n>>>>>>>> e. ( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))))
126	124, 125	bitr4i 243	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ((t e. ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c /\ <<t, <<{{{{{a}}}}}, <<{{{c}}}, <<{b}, 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, <<{{{{{a}}}}}, <<{{{c}}}, <<{b}, n>>>>>>>> e. ( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))))
127	126	exbii 1582	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- (E.t(t e. ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c /\ <<t, <<{{{{{a}}}}}, <<{{{c}}}, <<{b}, 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, <<{{{{{a}}}}}, <<{{{c}}}, <<{b}, n>>>>>>>> e. ( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))))
128		df-rex 2620	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- (E.t e. ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c<<t, <<{{{{{a}}}}}, <<{{{c}}}, <<{b}, 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, <<{{{{{a}}}}}, <<{{{c}}}, <<{b}, n>>>>>>>> e. ( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))))
129		excom 1741	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- (E.xE.t(t = {{{{{{{{x}}}}}}}} /\ <<t, <<{{{{{a}}}}}, <<{{{c}}}, <<{b}, 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, <<{{{{{a}}}}}, <<{{{c}}}, <<{b}, n>>>>>>>> e. ( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))))
130	127, 128, 129	3bitr4i 268	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- (E.t e. ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c<<t, <<{{{{{a}}}}}, <<{{{c}}}, <<{b}, 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, <<{{{{{a}}}}}, <<{{{c}}}, <<{b}, n>>>>>>>> e. ( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))))
131		snex 4111	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- {{{{{{{{x}}}}}}}} e. _V
132		opkeq1 4059	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- (t = {{{{{{{{x}}}}}}}} -> <<t, <<{{{{{a}}}}}, <<{{{c}}}, <<{b}, n>>>>>>>> = <<{{{{{{{{x}}}}}}}}, <<{{{{{a}}}}}, <<{{{c}}}, <<{b}, n>>>>>>>>)
133	132	eleq1d 2419	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- (t = {{{{{{{{x}}}}}}}} -> (<<t, <<{{{{{a}}}}}, <<{{{c}}}, <<{b}, n>>>>>>>> e. ( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk )) <-> <<{{{{{{{{x}}}}}}}}, <<{{{{{a}}}}}, <<{{{c}}}, <<{b}, n>>>>>>>> e. ( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))))
134	131, 133	ceqsexv 2894	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- (E.t(t = {{{{{{{{x}}}}}}}} /\ <<t, <<{{{{{a}}}}}, <<{{{c}}}, <<{b}, n>>>>>>>> e. ( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))) <-> <<{{{{{{{{x}}}}}}}}, <<{{{{{a}}}}}, <<{{{c}}}, <<{b}, n>>>>>>>> e. ( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk )))
135		elsymdif 3223	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- (<<{{{{{{{{x}}}}}}}}, <<{{{{{a}}}}}, <<{{{c}}}, <<{b}, n>>>>>>>> e. ( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk )) <-> -. (<<{{{{{{{{x}}}}}}}}, <<{{{{{a}}}}}, <<{{{c}}}, <<{b}, n>>>>>>>> e. Ins2k Ins2k Ins3k SIk Sk <-> <<{{{{{{{{x}}}}}}}}, <<{{{{{a}}}}}, <<{{{c}}}, <<{b}, n>>>>>>>> e. ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk )))
136		snex 4111	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 |- {{{{{{x}}}}}} e. _V
137	136, 86, 75	otkelins2k 4255	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 |- (<<{{{{{{{{x}}}}}}}}, <<{{{{{a}}}}}, <<{{{c}}}, <<{b}, n>>>>>>>> e. Ins2k Ins2k Ins3k SIk Sk <-> <<{{{{{{x}}}}}}, <<{{{c}}}, <<{b}, n>>>>>> e. Ins2k Ins3k SIk Sk )
138	36, 71, 61	otkelins2k 4255	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 |- (<<{{{{{{x}}}}}}, <<{{{c}}}, <<{b}, n>>>>>> e. Ins2k Ins3k SIk Sk <-> <<{{{{x}}}}, <<{b}, n>>>> e. Ins3k SIk Sk )
139		snex 4111	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 |- {{x}} e. _V
140	139, 59, 21	otkelins3k 4256	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 |- (<<{{{{x}}}}, <<{b}, n>>>> e. Ins3k SIk Sk <-> <<{{x}}, {b}>> e. SIk Sk )
141		snex 4111	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 |- {x} e. _V
142		vex 2862	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 |- b e. _V
143	141, 142	opksnelsik 4265	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 |- (<<{{x}}, {b}>> e. SIk Sk <-> <<{x}, b>> e. Sk )
144	3, 142	elssetk 4270	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 |- (<<{x}, b>> e. Sk <-> x e. b)
145	140, 143, 144	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 |- (<<{{{{x}}}}, <<{b}, n>>>> e. Ins3k SIk Sk <-> x e. b)
146	137, 138, 145	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- (<<{{{{{{{{x}}}}}}}}, <<{{{{{a}}}}}, <<{{{c}}}, <<{b}, n>>>>>>>> e. Ins2k Ins2k Ins3k SIk Sk <-> x e. b)
147	136, 86, 75	otkelins3k 4256	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 |- (<<{{{{{{{{x}}}}}}}}, <<{{{{{a}}}}}, <<{{{c}}}, <<{b}, n>>>>>>>> e. Ins3k SIk SIk SIk SIk SIk Sk <-> <<{{{{{{x}}}}}}, {{{{{a}}}}}>> e. SIk SIk SIk SIk SIk Sk )
148		snex 4111	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 |- {{{{{x}}}}} e. _V
149		snex 4111	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 |- {{{{a}}}} e. _V
150	148, 149	opksnelsik 4265	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 |- (<<{{{{{{x}}}}}}, {{{{{a}}}}}>> e. SIk SIk SIk SIk SIk Sk <-> <<{{{{{x}}}}}, {{{{a}}}}>> e. SIk SIk SIk SIk Sk )
151	36, 15	opksnelsik 4265	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 |- (<<{{{{{x}}}}}, {{{{a}}}}>> e. SIk SIk SIk SIk Sk <-> <<{{{{x}}}}, {{{a}}}>> e. SIk SIk SIk Sk )
152		snex 4111	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 |- {{{x}}} e. _V
153	152, 107	opksnelsik 4265	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 |- (<<{{{{x}}}}, {{{a}}}>> e. SIk SIk SIk Sk <-> <<{{{x}}}, {{a}}>> e. SIk SIk Sk )
154	139, 20	opksnelsik 4265	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 |- (<<{{{x}}}, {{a}}>> e. SIk SIk Sk <-> <<{{x}}, {a}>> e. SIk Sk )
155	141, 23	opksnelsik 4265	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 |- (<<{{x}}, {a}>> e. SIk Sk <-> <<{x}, a>> e. Sk )
156	3, 23	elssetk 4270	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 |- (<<{x}, a>> e. Sk <-> x e. a)
157	154, 155, 156	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 |- (<<{{{x}}}, {{a}}>> e. SIk SIk Sk <-> x e. a)
158	151, 153, 157	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 |- (<<{{{{{x}}}}}, {{{{a}}}}>> e. SIk SIk SIk SIk Sk <-> x e. a)
159	147, 150, 158	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 |- (<<{{{{{{{{x}}}}}}}}, <<{{{{{a}}}}}, <<{{{c}}}, <<{b}, n>>>>>>>> e. Ins3k SIk SIk SIk SIk SIk Sk <-> x e. a)
160	136, 86, 75	otkelins2k 4255	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 |- (<<{{{{{{{{x}}}}}}}}, <<{{{{{a}}}}}, <<{{{c}}}, <<{b}, n>>>>>>>> e. Ins2k Ins3k SIk SIk SIk Sk <-> <<{{{{{{x}}}}}}, <<{{{c}}}, <<{b}, n>>>>>> e. Ins3k SIk SIk SIk Sk )
161	36, 71, 61	otkelins3k 4256	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 |- (<<{{{{{{x}}}}}}, <<{{{c}}}, <<{b}, n>>>>>> e. Ins3k SIk SIk SIk Sk <-> <<{{{{x}}}}, {{{c}}}>> e. SIk SIk SIk Sk )
162	152, 108	opksnelsik 4265	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 |- (<<{{{{x}}}}, {{{c}}}>> e. SIk SIk SIk Sk <-> <<{{{x}}}, {{c}}>> e. SIk SIk Sk )
163	139, 98	opksnelsik 4265	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 |- (<<{{{x}}}, {{c}}>> e. SIk SIk Sk <-> <<{{x}}, {c}>> e. SIk Sk )
164	141, 100	opksnelsik 4265	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 |- (<<{{x}}, {c}>> e. SIk Sk <-> <<{x}, c>> e. Sk )
165	3, 100	elssetk 4270	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 |- (<<{x}, c>> e. Sk <-> x e. c)
166	164, 165	bitri 240	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 |- (<<{{x}}, {c}>> e. SIk Sk <-> x e. c)
167	162, 163, 166	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 |- (<<{{{{x}}}}, {{{c}}}>> e. SIk SIk SIk Sk <-> x e. c)
168	160, 161, 167	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 |- (<<{{{{{{{{x}}}}}}}}, <<{{{{{a}}}}}, <<{{{c}}}, <<{b}, n>>>>>>>> e. Ins2k Ins3k SIk SIk SIk Sk <-> x e. c)
169	159, 168	orbi12i 507	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 |- ((<<{{{{{{{{x}}}}}}}}, <<{{{{{a}}}}}, <<{{{c}}}, <<{b}, n>>>>>>>> e. Ins3k SIk SIk SIk SIk SIk Sk \/ <<{{{{{{{{x}}}}}}}}, <<{{{{{a}}}}}, <<{{{c}}}, <<{b}, n>>>>>>>> e. Ins2k Ins3k SIk SIk SIk Sk ) <-> (x e. a \/ x e. c))
170		elun 3220	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 |- (<<{{{{{{{{x}}}}}}}}, <<{{{{{a}}}}}, <<{{{c}}}, <<{b}, n>>>>>>>> e. ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ) <-> (<<{{{{{{{{x}}}}}}}}, <<{{{{{a}}}}}, <<{{{c}}}, <<{b}, n>>>>>>>> e. Ins3k SIk SIk SIk SIk SIk Sk \/ <<{{{{{{{{x}}}}}}}}, <<{{{{{a}}}}}, <<{{{c}}}, <<{b}, n>>>>>>>> e. Ins2k Ins3k SIk SIk SIk Sk ))
171		elun 3220	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 |- (x e. (a u. c) <-> (x e. a \/ x e. c))
172	169, 170, 171	3bitr4i 268	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- (<<{{{{{{{{x}}}}}}}}, <<{{{{{a}}}}}, <<{{{c}}}, <<{b}, n>>>>>>>> e. ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ) <-> x e. (a u. c))
173	146, 172	bibi12i 306	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- ((<<{{{{{{{{x}}}}}}}}, <<{{{{{a}}}}}, <<{{{c}}}, <<{b}, n>>>>>>>> e. Ins2k Ins2k Ins3k SIk Sk <-> <<{{{{{{{{x}}}}}}}}, <<{{{{{a}}}}}, <<{{{c}}}, <<{b}, n>>>>>>>> e. ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk )) <-> (x e. b <-> x e. (a u. c)))
174	173	notbii 287	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- (-. (<<{{{{{{{{x}}}}}}}}, <<{{{{{a}}}}}, <<{{{c}}}, <<{b}, n>>>>>>>> e. Ins2k Ins2k Ins3k SIk Sk <-> <<{{{{{{{{x}}}}}}}}, <<{{{{{a}}}}}, <<{{{c}}}, <<{b}, n>>>>>>>> e. ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk )) <-> -. (x e. b <-> x e. (a u. c)))
175	134, 135, 174	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- (E.t(t = {{{{{{{{x}}}}}}}} /\ <<t, <<{{{{{a}}}}}, <<{{{c}}}, <<{b}, n>>>>>>>> e. ( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ))) <-> -. (x e. b <-> x e. (a u. c)))
176	175	exbii 1582	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- (E.xE.t(t = {{{{{{{{x}}}}}}}} /\ <<t, <<{{{{{a}}}}}, <<{{{c}}}, <<{b}, 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. b <-> x e. (a u. c)))
177	122, 130, 176	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- (<<{{{{{a}}}}}, <<{{{c}}}, <<{b}, 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. b <-> x e. (a u. c)))
178	177	notbii 287	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (-. <<{{{{{a}}}}}, <<{{{c}}}, <<{b}, 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. b <-> x e. (a u. c)))
179	121	elcompl 3225	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (<<{{{{{a}}}}}, <<{{{c}}}, <<{b}, 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}}}}}, <<{{{c}}}, <<{b}, 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))
180		dfcleq 2347	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- (b = (a u. c) <-> A.x(x e. b <-> x e. (a u. c)))
181		alex 1572	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- (A.x(x e. b <-> x e. (a u. c)) <-> -. E.x -. (x e. b <-> x e. (a u. c)))
182	180, 181	bitri 240	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (b = (a u. c) <-> -. E.x -. (x e. b <-> x e. (a u. c)))
183	178, 179, 182	3bitr4i 268	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (<<{{{{{a}}}}}, <<{{{c}}}, <<{b}, 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 = (a u. c))
184	120, 183	anbi12i 678	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ((<<{{{{{a}}}}}, <<{{{c}}}, <<{b}, n>>>>>> e. Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) /\ <<{{{{{a}}}}}, <<{{{c}}}, <<{b}, 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 i^i c) = (/) /\ b = (a u. c)))
185	105, 184	bitri 240	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (<<{{{{{a}}}}}, <<{{{c}}}, <<{b}, 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)) <-> ((a i^i c) = (/) /\ b = (a u. c)))
186	104, 185	anbi12i 678	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ((<<{{{{{a}}}}}, <<{{{c}}}, <<{b}, n>>>>>> e. ( Ins2k Ins2k Sk i^i (_V X.k Ins2k Sk )) /\ <<{{{{{a}}}}}, <<{{{c}}}, <<{b}, 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))) <-> ((a e. n /\ c e. n) /\ ((a i^i c) = (/) /\ b = (a u. c))))
187	89, 90, 186	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (E.t(t = {{{{{a}}}}} /\ <<t, <<{{{c}}}, <<{b}, 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)))) <-> ((a e. n /\ c e. n) /\ ((a i^i c) = (/) /\ b = (a u. c))))
188	187	exbii 1582	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (E.aE.t(t = {{{{{a}}}}} /\ <<t, <<{{{c}}}, <<{b}, 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.a((a e. n /\ c e. n) /\ ((a i^i c) = (/) /\ b = (a u. c))))
189	74, 85, 188	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (E.t(t = {{{c}}} /\ <<t, <<{b}, 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.a((a e. n /\ c e. n) /\ ((a i^i c) = (/) /\ b = (a u. c))))
190	189	exbii 1582	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (E.cE.t(t = {{{c}}} /\ <<t, <<{b}, 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.a((a e. n /\ c e. n) /\ ((a i^i c) = (/) /\ b = (a u. c))))
191	62, 70, 190	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (<<{b}, 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.a((a e. n /\ c e. n) /\ ((a i^i c) = (/) /\ b = (a u. c))))
192		eladdc 4398	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (b e. (n +o n) <-> E.a e. n E.c e. n ((a i^i c) = (/) /\ b = (a u. c)))
193		r2ex 2652	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (E.a e. n E.c e. n ((a i^i c) = (/) /\ b = (a u. c)) <-> E.aE.c((a e. n /\ c e. n) /\ ((a i^i c) = (/) /\ b = (a u. c))))
194		excom 1741	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (E.aE.c((a e. n /\ c e. n) /\ ((a i^i c) = (/) /\ b = (a u. c))) <-> E.cE.a((a e. n /\ c e. n) /\ ((a i^i c) = (/) /\ b = (a u. c))))
195	192, 193, 194	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (b e. (n +o n) <-> E.cE.a((a e. n /\ c e. n) /\ ((a i^i c) = (/) /\ b = (a u. c))))
196	191, 195	bitr4i 243	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (<<{b}, 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) <-> b e. (n +o n))
197	58, 60, 196	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (<<{{{{{b}}}}}, <<{{{{x}}}}, <<{a}, n>>>>>> e. Ins2k Ins2k (((( 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) <-> b e. (n +o n))
198	57, 36, 26	otkelins3k 4256	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (<<{{{{{b}}}}}, <<{{{{x}}}}, <<{a}, n>>>>>> e. Ins3k `'k SIk SIk SIk ∼ Sk <-> <<{{{b}}}, {{{{x}}}}>> e. `'k SIk SIk SIk ∼ Sk )
199	57, 36	opkelcnvk 4250	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (<<{{{b}}}, {{{{x}}}}>> e. `'k SIk SIk SIk ∼ Sk <-> <<{{{{x}}}}, {{{b}}}>> e. SIk SIk SIk ∼ Sk )
200		snex 4111	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- {{b}} e. _V
201	152, 200	opksnelsik 4265	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (<<{{{{x}}}}, {{{b}}}>> e. SIk SIk SIk ∼ Sk <-> <<{{{x}}}, {{b}}>> e. SIk SIk ∼ Sk )
202	139, 59	opksnelsik 4265	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (<<{{{x}}}, {{b}}>> e. SIk SIk ∼ Sk <-> <<{{x}}, {b}>> e. SIk ∼ Sk )
203	141, 142	opksnelsik 4265	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (<<{{x}}, {b}>> e. SIk ∼ Sk <-> <<{x}, b>> e. ∼ Sk )
204	144	notbii 287	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (-. <<{x}, b>> e. Sk <-> -. x e. b)
205		opkex 4113	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- <<{x}, b>> e. _V
206	205	elcompl 3225	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (<<{x}, b>> e. ∼ Sk <-> -. <<{x}, b>> e. Sk )
207	3	elcompl 3225	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (x e. ∼ b <-> -. x e. b)
208	204, 206, 207	3bitr4i 268	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (<<{x}, b>> e. ∼ Sk <-> x e. ∼ b)
209	203, 208	bitri 240	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (<<{{x}}, {b}>> e. SIk ∼ Sk <-> x e. ∼ b)
210	201, 202, 209	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (<<{{{{x}}}}, {{{b}}}>> e. SIk SIk SIk ∼ Sk <-> x e. ∼ b)
211	198, 199, 210	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (<<{{{{{b}}}}}, <<{{{{x}}}}, <<{a}, n>>>>>> e. Ins3k `'k SIk SIk SIk ∼ Sk <-> x e. ∼ b)
212	197, 211	anbi12i 678	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((<<{{{{{b}}}}}, <<{{{{x}}}}, <<{a}, n>>>>>> e. Ins2k Ins2k (((( 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) /\ <<{{{{{b}}}}}, <<{{{{x}}}}, <<{a}, n>>>>>> e. Ins3k `'k SIk SIk SIk ∼ Sk ) <-> (b e. (n +o n) /\ x e. ∼ b))
213	56, 212	bitri 240	. . . . . . . . . . . . . . . . . . . . . 22 |- (<<{{{{{b}}}}}, <<{{{{x}}}}, <<{a}, n>>>>>> e. ( Ins2k Ins2k (((( 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) i^i Ins3k `'k SIk SIk SIk ∼ Sk ) <-> (b e. (n +o n) /\ x e. ∼ b))
214		opkex 4113	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- <<{{{{{b}}}}}, <<{{{{x}}}}, <<{a}, n>>>>>> e. _V
215	214	elimak 4259	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (<<{{{{{b}}}}}, <<{{{{x}}}}, <<{a}, n>>>>>> e. (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c) <-> E.t e. ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c<<t, <<{{{{{b}}}}}, <<{{{{x}}}}, <<{a}, n>>>>>>>> e. ( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k _I_kk )))
216		elpw171c 4153	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (t e. ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c <-> E.y t = {{{{{{{{y}}}}}}}})
217	216	anbi1i 676	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((t e. ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c /\ <<t, <<{{{{{b}}}}}, <<{{{{x}}}}, <<{a}, n>>>>>>>> e. ( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k _I_kk ))) <-> (E.y t = {{{{{{{{y}}}}}}}} /\ <<t, <<{{{{{b}}}}}, <<{{{{x}}}}, <<{a}, n>>>>>>>> e. ( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k _I_kk ))))
218		19.41v 1901	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (E.y(t = {{{{{{{{y}}}}}}}} /\ <<t, <<{{{{{b}}}}}, <<{{{{x}}}}, <<{a}, n>>>>>>>> e. ( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k _I_kk ))) <-> (E.y t = {{{{{{{{y}}}}}}}} /\ <<t, <<{{{{{b}}}}}, <<{{{{x}}}}, <<{a}, n>>>>>>>> e. ( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k _I_kk ))))
219	217, 218	bitr4i 243	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((t e. ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c /\ <<t, <<{{{{{b}}}}}, <<{{{{x}}}}, <<{a}, n>>>>>>>> e. ( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k _I_kk ))) <-> E.y(t = {{{{{{{{y}}}}}}}} /\ <<t, <<{{{{{b}}}}}, <<{{{{x}}}}, <<{a}, n>>>>>>>> e. ( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k _I_kk ))))
220	219	exbii 1582	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (E.t(t e. ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c /\ <<t, <<{{{{{b}}}}}, <<{{{{x}}}}, <<{a}, n>>>>>>>> e. ( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k _I_kk ))) <-> E.tE.y(t = {{{{{{{{y}}}}}}}} /\ <<t, <<{{{{{b}}}}}, <<{{{{x}}}}, <<{a}, n>>>>>>>> e. ( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k _I_kk ))))
221		df-rex 2620	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (E.t e. ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c<<t, <<{{{{{b}}}}}, <<{{{{x}}}}, <<{a}, n>>>>>>>> e. ( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k _I_kk )) <-> E.t(t e. ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c /\ <<t, <<{{{{{b}}}}}, <<{{{{x}}}}, <<{a}, n>>>>>>>> e. ( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k _I_kk ))))
222		excom 1741	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (E.yE.t(t = {{{{{{{{y}}}}}}}} /\ <<t, <<{{{{{b}}}}}, <<{{{{x}}}}, <<{a}, n>>>>>>>> e. ( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k _I_kk ))) <-> E.tE.y(t = {{{{{{{{y}}}}}}}} /\ <<t, <<{{{{{b}}}}}, <<{{{{x}}}}, <<{a}, n>>>>>>>> e. ( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k _I_kk ))))
223	220, 221, 222	3bitr4i 268	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (E.t e. ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c<<t, <<{{{{{b}}}}}, <<{{{{x}}}}, <<{a}, n>>>>>>>> e. ( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k _I_kk )) <-> E.yE.t(t = {{{{{{{{y}}}}}}}} /\ <<t, <<{{{{{b}}}}}, <<{{{{x}}}}, <<{a}, n>>>>>>>> e. ( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k _I_kk ))))
224		snex 4111	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- {{{{{{{{y}}}}}}}} e. _V
225		opkeq1 4059	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (t = {{{{{{{{y}}}}}}}} -> <<t, <<{{{{{b}}}}}, <<{{{{x}}}}, <<{a}, n>>>>>>>> = <<{{{{{{{{y}}}}}}}}, <<{{{{{b}}}}}, <<{{{{x}}}}, <<{a}, n>>>>>>>>)
226	225	eleq1d 2419	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (t = {{{{{{{{y}}}}}}}} -> (<<t, <<{{{{{b}}}}}, <<{{{{x}}}}, <<{a}, n>>>>>>>> e. ( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k _I_kk )) <-> <<{{{{{{{{y}}}}}}}}, <<{{{{{b}}}}}, <<{{{{x}}}}, <<{a}, n>>>>>>>> e. ( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k _I_kk ))))
227	224, 226	ceqsexv 2894	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (E.t(t = {{{{{{{{y}}}}}}}} /\ <<t, <<{{{{{b}}}}}, <<{{{{x}}}}, <<{a}, n>>>>>>>> e. ( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k _I_kk ))) <-> <<{{{{{{{{y}}}}}}}}, <<{{{{{b}}}}}, <<{{{{x}}}}, <<{a}, n>>>>>>>> e. ( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k _I_kk )))
228		elsymdif 3223	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (<<{{{{{{{{y}}}}}}}}, <<{{{{{b}}}}}, <<{{{{x}}}}, <<{a}, n>>>>>>>> e. ( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k _I_kk )) <-> -. (<<{{{{{{{{y}}}}}}}}, <<{{{{{b}}}}}, <<{{{{x}}}}, <<{a}, n>>>>>>>> e. Ins2k Ins2k Ins3k SIk Sk <-> <<{{{{{{{{y}}}}}}}}, <<{{{{{b}}}}}, <<{{{{x}}}}, <<{a}, n>>>>>>>> e. ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k _I_kk )))
229		snex 4111	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- {{{{{{y}}}}}} e. _V
230	229, 51, 40	otkelins2k 4255	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (<<{{{{{{{{y}}}}}}}}, <<{{{{{b}}}}}, <<{{{{x}}}}, <<{a}, n>>>>>>>> e. Ins2k Ins2k Ins3k SIk Sk <-> <<{{{{{{y}}}}}}, <<{{{{x}}}}, <<{a}, n>>>>>> e. Ins2k Ins3k SIk Sk )
231		snex 4111	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- {{{{y}}}} e. _V
232	231, 36, 26	otkelins2k 4255	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (<<{{{{{{y}}}}}}, <<{{{{x}}}}, <<{a}, n>>>>>> e. Ins2k Ins3k SIk Sk <-> <<{{{{y}}}}, <<{a}, n>>>> e. Ins3k SIk Sk )
233		snex 4111	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- {{y}} e. _V
234	233, 20, 21	otkelins3k 4256	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (<<{{{{y}}}}, <<{a}, n>>>> e. Ins3k SIk Sk <-> <<{{y}}, {a}>> e. SIk Sk )
235		snex 4111	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- {y} e. _V
236	235, 23	opksnelsik 4265	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (<<{{y}}, {a}>> e. SIk Sk <-> <<{y}, a>> e. Sk )
237		vex 2862	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- y e. _V
238	237, 23	elssetk 4270	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (<<{y}, a>> e. Sk <-> y e. a)
239	234, 236, 238	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (<<{{{{y}}}}, <<{a}, n>>>> e. Ins3k SIk Sk <-> y e. a)
240	230, 232, 239	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (<<{{{{{{{{y}}}}}}}}, <<{{{{{b}}}}}, <<{{{{x}}}}, <<{a}, n>>>>>>>> e. Ins2k Ins2k Ins3k SIk Sk <-> y e. a)
241	229, 51, 40	otkelins3k 4256	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (<<{{{{{{{{y}}}}}}}}, <<{{{{{b}}}}}, <<{{{{x}}}}, <<{a}, n>>>>>>>> e. Ins3k SIk SIk SIk SIk SIk Sk <-> <<{{{{{{y}}}}}}, {{{{{b}}}}}>> e. SIk SIk SIk SIk SIk Sk )
242		snex 4111	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- {{{{{y}}}}} e. _V
243		snex 4111	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- {{{{b}}}} e. _V
244	242, 243	opksnelsik 4265	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (<<{{{{{{y}}}}}}, {{{{{b}}}}}>> e. SIk SIk SIk SIk SIk Sk <-> <<{{{{{y}}}}}, {{{{b}}}}>> e. SIk SIk SIk SIk Sk )
245	231, 57	opksnelsik 4265	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (<<{{{{{y}}}}}, {{{{b}}}}>> e. SIk SIk SIk SIk Sk <-> <<{{{{y}}}}, {{{b}}}>> e. SIk SIk SIk Sk )
246		snex 4111	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- {{{y}}} e. _V
247	246, 200	opksnelsik 4265	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (<<{{{{y}}}}, {{{b}}}>> e. SIk SIk SIk Sk <-> <<{{{y}}}, {{b}}>> e. SIk SIk Sk )
248	233, 59	opksnelsik 4265	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (<<{{{y}}}, {{b}}>> e. SIk SIk Sk <-> <<{{y}}, {b}>> e. SIk Sk )
249	235, 142	opksnelsik 4265	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (<<{{y}}, {b}>> e. SIk Sk <-> <<{y}, b>> e. Sk )
250	237, 142	elssetk 4270	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (<<{y}, b>> e. Sk <-> y e. b)
251	248, 249, 250	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (<<{{{y}}}, {{b}}>> e. SIk SIk Sk <-> y e. b)
252	245, 247, 251	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (<<{{{{{y}}}}}, {{{{b}}}}>> e. SIk SIk SIk SIk Sk <-> y e. b)
253	241, 244, 252	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (<<{{{{{{{{y}}}}}}}}, <<{{{{{b}}}}}, <<{{{{x}}}}, <<{a}, n>>>>>>>> e. Ins3k SIk SIk SIk SIk SIk Sk <-> y e. b)
254	229, 51, 40	otkelins2k 4255	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (<<{{{{{{{{y}}}}}}}}, <<{{{{{b}}}}}, <<{{{{x}}}}, <<{a}, n>>>>>>>> e. Ins2k Ins3k _I_kk <-> <<{{{{{{y}}}}}}, <<{{{{x}}}}, <<{a}, n>>>>>> e. Ins3k _I_kk )
255	231, 36, 26	otkelins3k 4256	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (<<{{{{{{y}}}}}}, <<{{{{x}}}}, <<{a}, n>>>>>> e. Ins3k _I_kk <-> <<{{{{y}}}}, {{{{x}}}}>> e. _I_kk )
256	246	sneqb 3876	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ({{{{y}}}} = {{{{x}}}} <-> {{{y}}} = {{{x}}})
257	233	sneqb 3876	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ({{{y}}} = {{{x}}} <-> {{y}} = {{x}})
258	235	sneqb 3876	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ({{y}} = {{x}} <-> {y} = {x})
259	237	sneqb 3876	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ({y} = {x} <-> y = x)
260	258, 259	bitri 240	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ({{y}} = {{x}} <-> y = x)
261	256, 257, 260	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ({{{{y}}}} = {{{{x}}}} <-> y = x)
262		opkelidkg 4274	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (({{{{y}}}} e. _V /\ {{{{x}}}} e. _V) -> (<<{{{{y}}}}, {{{{x}}}}>> e. _I_kk <-> {{{{y}}}} = {{{{x}}}}))
263	231, 36, 262	mp2an 653	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (<<{{{{y}}}}, {{{{x}}}}>> e. _I_kk <-> {{{{y}}}} = {{{{x}}}})
264	237	elsnc 3756	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (y e. {x} <-> y = x)
265	261, 263, 264	3bitr4i 268	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (<<{{{{y}}}}, {{{{x}}}}>> e. _I_kk <-> y e. {x})
266	254, 255, 265	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (<<{{{{{{{{y}}}}}}}}, <<{{{{{b}}}}}, <<{{{{x}}}}, <<{a}, n>>>>>>>> e. Ins2k Ins3k _I_kk <-> y e. {x})
267	253, 266	orbi12i 507	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((<<{{{{{{{{y}}}}}}}}, <<{{{{{b}}}}}, <<{{{{x}}}}, <<{a}, n>>>>>>>> e. Ins3k SIk SIk SIk SIk SIk Sk \/ <<{{{{{{{{y}}}}}}}}, <<{{{{{b}}}}}, <<{{{{x}}}}, <<{a}, n>>>>>>>> e. Ins2k Ins3k _I_kk ) <-> (y e. b \/ y e. {x}))
268		elun 3220	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (<<{{{{{{{{y}}}}}}}}, <<{{{{{b}}}}}, <<{{{{x}}}}, <<{a}, n>>>>>>>> e. ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k _I_kk ) <-> (<<{{{{{{{{y}}}}}}}}, <<{{{{{b}}}}}, <<{{{{x}}}}, <<{a}, n>>>>>>>> e. Ins3k SIk SIk SIk SIk SIk Sk \/ <<{{{{{{{{y}}}}}}}}, <<{{{{{b}}}}}, <<{{{{x}}}}, <<{a}, n>>>>>>>> e. Ins2k Ins3k _I_kk ))
269		elun 3220	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (y e. (b u. {x}) <-> (y e. b \/ y e. {x}))
270	267, 268, 269	3bitr4i 268	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (<<{{{{{{{{y}}}}}}}}, <<{{{{{b}}}}}, <<{{{{x}}}}, <<{a}, n>>>>>>>> e. ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k _I_kk ) <-> y e. (b u. {x}))
271	240, 270	bibi12i 306	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((<<{{{{{{{{y}}}}}}}}, <<{{{{{b}}}}}, <<{{{{x}}}}, <<{a}, n>>>>>>>> e. Ins2k Ins2k Ins3k SIk Sk <-> <<{{{{{{{{y}}}}}}}}, <<{{{{{b}}}}}, <<{{{{x}}}}, <<{a}, n>>>>>>>> e. ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k _I_kk )) <-> (y e. a <-> y e. (b u. {x})))
272	271	notbii 287	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (-. (<<{{{{{{{{y}}}}}}}}, <<{{{{{b}}}}}, <<{{{{x}}}}, <<{a}, n>>>>>>>> e. Ins2k Ins2k Ins3k SIk Sk <-> <<{{{{{{{{y}}}}}}}}, <<{{{{{b}}}}}, <<{{{{x}}}}, <<{a}, n>>>>>>>> e. ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k _I_kk )) <-> -. (y e. a <-> y e. (b u. {x})))
273	227, 228, 272	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (E.t(t = {{{{{{{{y}}}}}}}} /\ <<t, <<{{{{{b}}}}}, <<{{{{x}}}}, <<{a}, n>>>>>>>> e. ( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k _I_kk ))) <-> -. (y e. a <-> y e. (b u. {x})))
274	273	exbii 1582	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (E.yE.t(t = {{{{{{{{y}}}}}}}} /\ <<t, <<{{{{{b}}}}}, <<{{{{x}}}}, <<{a}, n>>>>>>>> e. ( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k _I_kk ))) <-> E.y -. (y e. a <-> y e. (b u. {x})))
275	215, 223, 274	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (<<{{{{{b}}}}}, <<{{{{x}}}}, <<{a}, n>>>>>> e. (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c) <-> E.y -. (y e. a <-> y e. (b u. {x})))
276	275	notbii 287	. . . . . . . . . . . . . . . . . . . . . . 23 |- (-. <<{{{{{b}}}}}, <<{{{{x}}}}, <<{a}, n>>>>>> e. (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c) <-> -. E.y -. (y e. a <-> y e. (b u. {x})))
277	214	elcompl 3225	. . . . . . . . . . . . . . . . . . . . . . 23 |- (<<{{{{{b}}}}}, <<{{{{x}}}}, <<{a}, n>>>>>> e. ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c) <-> -. <<{{{{{b}}}}}, <<{{{{x}}}}, <<{a}, n>>>>>> e. (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c))
278		dfcleq 2347	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (a = (b u. {x}) <-> A.y(y e. a <-> y e. (b u. {x})))
279		alex 1572	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (A.y(y e. a <-> y e. (b u. {x})) <-> -. E.y -. (y e. a <-> y e. (b u. {x})))
280	278, 279	bitri 240	. . . . . . . . . . . . . . . . . . . . . . 23 |- (a = (b u. {x}) <-> -. E.y -. (y e. a <-> y e. (b u. {x})))
281	276, 277, 280	3bitr4i 268	. . . . . . . . . . . . . . . . . . . . . 22 |- (<<{{{{{b}}}}}, <<{{{{x}}}}, <<{a}, n>>>>>> e. ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c) <-> a = (b u. {x}))
282	213, 281	anbi12i 678	. . . . . . . . . . . . . . . . . . . . 21 |- ((<<{{{{{b}}}}}, <<{{{{x}}}}, <<{a}, n>>>>>> e. ( Ins2k Ins2k (((( 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) i^i Ins3k `'k SIk SIk SIk ∼ Sk ) /\ <<{{{{{b}}}}}, <<{{{{x}}}}, <<{a}, n>>>>>> e. ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)) <-> ((b e. (n +o n) /\ x e. ∼ b) /\ a = (b u. {x})))
283	54, 55, 282	3bitri 262	. . . . . . . . . . . . . . . . . . . 20 |- (E.t(t = {{{{{b}}}}} /\ <<t, <<{{{{x}}}}, <<{a}, n>>>>>> e. (( Ins2k Ins2k (((( 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) i^i Ins3k `'k SIk SIk SIk ∼ Sk ) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c))) <-> ((b e. (n +o n) /\ x e. ∼ b) /\ a = (b u. {x})))
284	283	exbii 1582	. . . . . . . . . . . . . . . . . . 19 |- (E.bE.t(t = {{{{{b}}}}} /\ <<t, <<{{{{x}}}}, <<{a}, n>>>>>> e. (( Ins2k Ins2k (((( 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) i^i Ins3k `'k SIk SIk SIk ∼ Sk ) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c))) <-> E.b((b e. (n +o n) /\ x e. ∼ b) /\ a = (b u. {x})))
285	39, 50, 284	3bitri 262	. . . . . . . . . . . . . . . . . 18 |- (E.t(t = {{{{x}}}} /\ <<t, <<{a}, n>>>> e. ((( Ins2k Ins2k (((( 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) i^i Ins3k `'k SIk SIk SIk ∼ Sk ) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 ~P1 ~P1 1c)) <-> E.b((b e. (n +o n) /\ x e. ∼ b) /\ a = (b u. {x})))
286	285	exbii 1582	. . . . . . . . . . . . . . . . 17 |- (E.xE.t(t = {{{{x}}}} /\ <<t, <<{a}, n>>>> e. ((( Ins2k Ins2k (((( 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) i^i Ins3k `'k SIk SIk SIk ∼ Sk ) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 ~P1 ~P1 1c)) <-> E.xE.b((b e. (n +o n) /\ x e. ∼ b) /\ a = (b u. {x})))
287	27, 35, 286	3bitri 262	. . . . . . . . . . . . . . . 16 |- (<<{a}, n>> e. (((( Ins2k Ins2k (((( 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) i^i Ins3k `'k SIk SIk SIk ∼ Sk ) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 ~P1 ~P1 1c)"k~P1 ~P1 ~P1 1c) <-> E.xE.b((b e. (n +o n) /\ x e. ∼ b) /\ a = (b u. {x})))
288	20, 21, 3	otkelins3k 4256	. . . . . . . . . . . . . . . 16 |- (<<{{{a}}}, <<n, x>>>> e. Ins3k (((( Ins2k Ins2k (((( 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) i^i Ins3k `'k SIk SIk SIk ∼ Sk ) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 ~P1 ~P1 1c)"k~P1 ~P1 ~P1 1c) <-> <<{a}, n>> e. (((( Ins2k Ins2k (((( 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) i^i Ins3k `'k SIk SIk SIk ∼ Sk ) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 ~P1 ~P1 1c)"k~P1 ~P1 ~P1 1c))
289		elsuc 4413	. . . . . . . . . . . . . . . . 17 |- (a e. ((n +o n) +o 1c) <-> E.b e. (n +o n)E.x e. ∼ ba = (b u. {x}))
290		r2ex 2652	. . . . . . . . . . . . . . . . 17 |- (E.b e. (n +o n)E.x e. ∼ ba = (b u. {x}) <-> E.bE.x((b e. (n +o n) /\ x e. ∼ b) /\ a = (b u. {x})))
291		excom 1741	. . . . . . . . . . . . . . . . 17 |- (E.bE.x((b e. (n +o n) /\ x e. ∼ b) /\ a = (b u. {x})) <-> E.xE.b((b e. (n +o n) /\ x e. ∼ b) /\ a = (b u. {x})))
292	289, 290, 291	3bitri 262	. . . . . . . . . . . . . . . 16 |- (a e. ((n +o n) +o 1c) <-> E.xE.b((b e. (n +o n) /\ x e. ∼ b) /\ a = (b u. {x})))
293	287, 288, 292	3bitr4i 268	. . . . . . . . . . . . . . 15 |- (<<{{{a}}}, <<n, x>>>> e. Ins3k (((( Ins2k Ins2k (((( 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) i^i Ins3k `'k SIk SIk SIk ∼ Sk ) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 ~P1 ~P1 1c)"k~P1 ~P1 ~P1 1c) <-> a e. ((n +o n) +o 1c))
294	25, 293	bibi12i 306	. . . . . . . . . . . . . 14 |- ((<<{{{a}}}, <<n, x>>>> e. Ins2k Sk <-> <<{{{a}}}, <<n, x>>>> e. Ins3k (((( Ins2k Ins2k (((( 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) i^i Ins3k `'k SIk SIk SIk ∼ Sk ) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 ~P1 ~P1 1c)"k~P1 ~P1 ~P1 1c)) <-> (a e. x <-> a e. ((n +o n) +o 1c)))
295	294	notbii 287	. . . . . . . . . . . . 13 |- (-. (<<{{{a}}}, <<n, x>>>> e. Ins2k Sk <-> <<{{{a}}}, <<n, x>>>> e. Ins3k (((( Ins2k Ins2k (((( 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) i^i Ins3k `'k SIk SIk SIk ∼ Sk ) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 ~P1 ~P1 1c)"k~P1 ~P1 ~P1 1c)) <-> -. (a e. x <-> a e. ((n +o n) +o 1c)))
296	18, 19, 295	3bitri 262	. . . . . . . . . . . 12 |- (E.t(t = {{{a}}} /\ <<t, <<n, x>>>> e. ( Ins2k Sk (+) Ins3k (((( Ins2k Ins2k (((( 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) i^i Ins3k `'k SIk SIk SIk ∼ Sk ) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 ~P1 ~P1 1c)"k~P1 ~P1 ~P1 1c))) <-> -. (a e. x <-> a e. ((n +o n) +o 1c)))
297	296	exbii 1582	. . . . . . . . . . 11 |- (E.aE.t(t = {{{a}}} /\ <<t, <<n, x>>>> e. ( Ins2k Sk (+) Ins3k (((( Ins2k Ins2k (((( 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) i^i Ins3k `'k SIk SIk SIk ∼ Sk ) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 ~P1 ~P1 1c)"k~P1 ~P1 ~P1 1c))) <-> E.a -. (a e. x <-> a e. ((n +o n) +o 1c)))
298	6, 14, 297	3bitri 262	. . . . . . . . . 10 |- (<<n, x>> e. (( Ins2k Sk (+) Ins3k (((( Ins2k Ins2k (((( 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) i^i Ins3k `'k SIk SIk SIk ∼ Sk ) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 ~P1 ~P1 1c)"k~P1 ~P1 ~P1 1c))"k~P1 ~P1 1c) <-> E.a -. (a e. x <-> a e. ((n +o n) +o 1c)))
299	298	notbii 287	. . . . . . . . 9 |- (-. <<n, x>> e. (( Ins2k Sk (+) Ins3k (((( Ins2k Ins2k (((( 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) i^i Ins3k `'k SIk SIk SIk ∼ Sk ) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 ~P1 ~P1 1c)"k~P1 ~P1 ~P1 1c))"k~P1 ~P1 1c) <-> -. E.a -. (a e. x <-> a e. ((n +o n) +o 1c)))
300	5	elcompl 3225	. . . . . . . . 9 |- (<<n, x>> e. ∼ (( Ins2k Sk (+) Ins3k (((( Ins2k Ins2k (((( 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) i^i Ins3k `'k SIk SIk SIk ∼ Sk ) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 ~P1 ~P1 1c)"k~P1 ~P1 ~P1 1c))"k~P1 ~P1 1c) <-> -. <<n, x>> e. (( Ins2k Sk (+) Ins3k (((( Ins2k Ins2k (((( 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) i^i Ins3k `'k SIk SIk SIk ∼ Sk ) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 ~P1 ~P1 1c)"k~P1 ~P1 ~P1 1c))"k~P1 ~P1 1c))
301		dfcleq 2347	. . . . . . . . . 10 |- (x = ((n +o n) +o 1c) <-> A.a(a e. x <-> a e. ((n +o n) +o 1c)))
302		alex 1572	. . . . . . . . . 10 |- (A.a(a e. x <-> a e. ((n +o n) +o 1c)) <-> -. E.a -. (a e. x <-> a e. ((n +o n) +o 1c)))
303	301, 302	bitri 240	. . . . . . . . 9 |- (x = ((n +o n) +o 1c) <-> -. E.a -. (a e. x <-> a e. ((n +o n) +o 1c)))
304	299, 300, 303	3bitr4i 268	. . . . . . . 8 |- (<<n, x>> e. ∼ (( Ins2k Sk (+) Ins3k (((( Ins2k Ins2k (((( 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) i^i Ins3k `'k SIk SIk SIk ∼ Sk ) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 ~P1 ~P1 1c)"k~P1 ~P1 ~P1 1c))"k~P1 ~P1 1c) <-> x = ((n +o n) +o 1c))
305	304	rexbii 2639	. . . . . . 7 |- (E.n e. Nn <<n, x>> e. ∼ (( Ins2k Sk (+) Ins3k (((( Ins2k Ins2k (((( 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) i^i Ins3k `'k SIk SIk SIk ∼ Sk ) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 ~P1 ~P1 1c)"k~P1 ~P1 ~P1 1c))"k~P1 ~P1 1c) <-> E.n e. Nn x = ((n +o n) +o 1c))
306	4, 305	bitri 240	. . . . . 6 |- (x e. ( ∼ (( Ins2k Sk (+) Ins3k (((( Ins2k Ins2k (((( 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) i^i Ins3k `'k SIk SIk SIk ∼ Sk ) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 ~P1 ~P1 1c)"k~P1 ~P1 ~P1 1c))"k~P1 ~P1 1c)"k Nn ) <-> E.n e. Nn x = ((n +o n) +o 1c))
307	306	anbi1i 676	. . . . 5 |- ((x e. ( ∼ (( Ins2k Sk (+) Ins3k (((( Ins2k Ins2k (((( 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) i^i Ins3k `'k SIk SIk SIk ∼ Sk ) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 ~P1 ~P1 1c)"k~P1 ~P1 ~P1 1c))"k~P1 ~P1 1c)"k Nn ) /\ x =/= (/)) <-> (E.n e. Nn x = ((n +o n) +o 1c) /\ x =/= (/)))
308	2, 307	bitri 240	. . . 4 |- (x e. (( ∼ (( Ins2k Sk (+) Ins3k (((( Ins2k Ins2k (((( 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) i^i Ins3k `'k SIk SIk SIk ∼ Sk ) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 ~P1 ~P1 1c)"k~P1 ~P1 ~P1 1c))"k~P1 ~P1 1c)"k Nn ) \ {(/)}) <-> (E.n e. Nn x = ((n +o n) +o 1c) /\ x =/= (/)))
309	308	abbi2i 2464	. . 3 |- (( ∼ (( Ins2k Sk (+) Ins3k (((( Ins2k Ins2k (((( 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) i^i Ins3k `'k SIk SIk SIk ∼ Sk ) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 ~P1 ~P1 1c)"k~P1 ~P1 ~P1 1c))"k~P1 ~P1 1c)"k Nn ) \ {(/)}) = {x | (E.n e. Nn x = ((n +o n) +o 1c) /\ x =/= (/))}
310	1, 309	eqtr4i 2376	. 2 |- Oddfin = (( ∼ (( Ins2k Sk (+) Ins3k (((( Ins2k Ins2k (((( 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) i^i Ins3k `'k SIk SIk SIk ∼ Sk ) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 ~P1 ~P1 1c)"k~P1 ~P1 ~P1 1c))"k~P1 ~P1 1c)"k Nn ) \ {(/)})
311		ssetkex 4294	. . . . . . . 8 |- Sk e. _V
312	311	ins2kex 4307	. . . . . . 7 |- Ins2k Sk e. _V
313	312	ins2kex 4307	. . . . . . . . . . . . . . . . . 18 |- Ins2k Ins2k Sk e. _V
314		vvex 4109	. . . . . . . . . . . . . . . . . . 19 |- _V e. _V
315	314, 312	xpkex 4289	. . . . . . . . . . . . . . . . . 18 |- (_V X.k Ins2k Sk ) e. _V
316	313, 315	inex 4105	. . . . . . . . . . . . . . . . 17 |- ( Ins2k Ins2k Sk i^i (_V X.k Ins2k Sk )) e. _V
317	311	ins3kex 4308	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- Ins3k Sk e. _V
318	317, 312	inex 4105	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( Ins3k Sk i^i Ins2k Sk ) e. _V
319		1cex 4142	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- 1c e. _V
320	319	pw1ex 4303	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ~P1 1c e. _V
321	320	pw1ex 4303	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ~P1 ~P1 1c e. _V
322	318, 321	imakex 4300	. . . . . . . . . . . . . . . . . . . . . . 23 |- (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) e. _V
323	322	complex 4104	. . . . . . . . . . . . . . . . . . . . . 22 |- ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) e. _V
324	323	sikex 4297	. . . . . . . . . . . . . . . . . . . . 21 |- SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) e. _V
325	324	sikex 4297	. . . . . . . . . . . . . . . . . . . 20 |- SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) e. _V
326	325	sikex 4297	. . . . . . . . . . . . . . . . . . 19 |- SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) e. _V
327	326	ins3kex 4308	. . . . . . . . . . . . . . . . . 18 |- Ins3k SIk SIk SIk ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) e. _V
328	311	sikex 4297	. . . . . . . . . . . . . . . . . . . . . . . 24 |- SIk Sk e. _V
329	328	ins3kex 4308	. . . . . . . . . . . . . . . . . . . . . . 23 |- Ins3k SIk Sk e. _V
330	329	ins2kex 4307	. . . . . . . . . . . . . . . . . . . . . 22 |- Ins2k Ins3k SIk Sk e. _V
331	330	ins2kex 4307	. . . . . . . . . . . . . . . . . . . . 21 |- Ins2k Ins2k Ins3k SIk Sk e. _V
332	328	sikex 4297	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- SIk SIk Sk e. _V
333	332	sikex 4297	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- SIk SIk SIk Sk e. _V
334	333	sikex 4297	. . . . . . . . . . . . . . . . . . . . . . . 24 |- SIk SIk SIk SIk Sk e. _V
335	334	sikex 4297	. . . . . . . . . . . . . . . . . . . . . . 23 |- SIk SIk SIk SIk SIk Sk e. _V
336	335	ins3kex 4308	. . . . . . . . . . . . . . . . . . . . . 22 |- Ins3k SIk SIk SIk SIk SIk Sk e. _V
337	333	ins3kex 4308	. . . . . . . . . . . . . . . . . . . . . . 23 |- Ins3k SIk SIk SIk Sk e. _V
338	337	ins2kex 4307	. . . . . . . . . . . . . . . . . . . . . 22 |- Ins2k Ins3k SIk SIk SIk Sk e. _V
339	336, 338	unex 4106	. . . . . . . . . . . . . . . . . . . . 21 |- ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk ) e. _V
340	331, 339	symdifex 4108	. . . . . . . . . . . . . . . . . . . 20 |- ( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k SIk SIk SIk Sk )) e. _V
341	321	pw1ex 4303	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ~P1 ~P1 ~P1 1c e. _V
342	341	pw1ex 4303	. . . . . . . . . . . . . . . . . . . . . . 23 |- ~P1 ~P1 ~P1 ~P1 1c e. _V
343	342	pw1ex 4303	. . . . . . . . . . . . . . . . . . . . . 22 |- ~P1 ~P1 ~P1 ~P1 ~P1 1c e. _V
344	343	pw1ex 4303	. . . . . . . . . . . . . . . . . . . . 21 |- ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c e. _V
345	344	pw1ex 4303	. . . . . . . . . . . . . . . . . . . 20 |- ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c e. _V
346	340, 345	imakex 4300	. . . . . . . . . . . . . . . . . . 19 |- (( 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
347	346	complex 4104	. . . . . . . . . . . . . . . . . 18 |- ∼ (( 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
348	327, 347	inex 4105	. . . . . . . . . . . . . . . . 17 |- ( 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
349	316, 348	inex 4105	. . . . . . . . . . . . . . . 16 |- (( 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
350	349, 342	imakex 4300	. . . . . . . . . . . . . . 15 |- ((( 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
351	350, 321	imakex 4300	. . . . . . . . . . . . . 14 |- (((( 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
352	351	ins2kex 4307	. . . . . . . . . . . . 13 |- Ins2k (((( 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
353	352	ins2kex 4307	. . . . . . . . . . . 12 |- Ins2k Ins2k (((( 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
354	311	complex 4104	. . . . . . . . . . . . . . . . 17 |- ∼ Sk e. _V
355	354	sikex 4297	. . . . . . . . . . . . . . . 16 |- SIk ∼ Sk e. _V
356	355	sikex 4297	. . . . . . . . . . . . . . 15 |- SIk SIk ∼ Sk e. _V
357	356	sikex 4297	. . . . . . . . . . . . . 14 |- SIk SIk SIk ∼ Sk e. _V
358	357	cnvkex 4287	. . . . . . . . . . . . 13 |- `'k SIk SIk SIk ∼ Sk e. _V
359	358	ins3kex 4308	. . . . . . . . . . . 12 |- Ins3k `'k SIk SIk SIk ∼ Sk e. _V
360	353, 359	inex 4105	. . . . . . . . . . 11 |- ( Ins2k Ins2k (((( 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) i^i Ins3k `'k SIk SIk SIk ∼ Sk ) e. _V
361		idkex 4314	. . . . . . . . . . . . . . . . 17 |- _I_kk e. _V
362	361	ins3kex 4308	. . . . . . . . . . . . . . . 16 |- Ins3k _I_kk e. _V
363	362	ins2kex 4307	. . . . . . . . . . . . . . 15 |- Ins2k Ins3k _I_kk e. _V
364	336, 363	unex 4106	. . . . . . . . . . . . . 14 |- ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k _I_kk ) e. _V
365	331, 364	symdifex 4108	. . . . . . . . . . . . 13 |- ( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k _I_kk )) e. _V
366	365, 345	imakex 4300	. . . . . . . . . . . 12 |- (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c) e. _V
367	366	complex 4104	. . . . . . . . . . 11 |- ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c) e. _V
368	360, 367	inex 4105	. . . . . . . . . 10 |- (( Ins2k Ins2k (((( 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) i^i Ins3k `'k SIk SIk SIk ∼ Sk ) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c)) e. _V
369	368, 342	imakex 4300	. . . . . . . . 9 |- ((( Ins2k Ins2k (((( 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) i^i Ins3k `'k SIk SIk SIk ∼ Sk ) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 ~P1 ~P1 1c) e. _V
370	369, 341	imakex 4300	. . . . . . . 8 |- (((( Ins2k Ins2k (((( 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) i^i Ins3k `'k SIk SIk SIk ∼ Sk ) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 ~P1 ~P1 1c)"k~P1 ~P1 ~P1 1c) e. _V
371	370	ins3kex 4308	. . . . . . 7 |- Ins3k (((( Ins2k Ins2k (((( 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) i^i Ins3k `'k SIk SIk SIk ∼ Sk ) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 ~P1 ~P1 1c)"k~P1 ~P1 ~P1 1c) e. _V
372	312, 371	symdifex 4108	. . . . . 6 |- ( Ins2k Sk (+) Ins3k (((( Ins2k Ins2k (((( 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) i^i Ins3k `'k SIk SIk SIk ∼ Sk ) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 ~P1 ~P1 1c)"k~P1 ~P1 ~P1 1c)) e. _V
373	372, 321	imakex 4300	. . . . 5 |- (( Ins2k Sk (+) Ins3k (((( Ins2k Ins2k (((( 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) i^i Ins3k `'k SIk SIk SIk ∼ Sk ) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 ~P1 ~P1 1c)"k~P1 ~P1 ~P1 1c))"k~P1 ~P1 1c) e. _V
374	373	complex 4104	. . . 4 |- ∼ (( Ins2k Sk (+) Ins3k (((( Ins2k Ins2k (((( 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) i^i Ins3k `'k SIk SIk SIk ∼ Sk ) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 ~P1 ~P1 1c)"k~P1 ~P1 ~P1 1c))"k~P1 ~P1 1c) e. _V
375		nncex 4396	. . . 4 |- Nn e. _V
376	374, 375	imakex 4300	. . 3 |- ( ∼ (( Ins2k Sk (+) Ins3k (((( Ins2k Ins2k (((( 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) i^i Ins3k `'k SIk SIk SIk ∼ Sk ) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 ~P1 ~P1 1c)"k~P1 ~P1 ~P1 1c))"k~P1 ~P1 1c)"k Nn ) e. _V
377		snex 4111	. . 3 |- {(/)} e. _V
378	376, 377	difex 4107	. 2 |- (( ∼ (( Ins2k Sk (+) Ins3k (((( Ins2k Ins2k (((( 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) i^i Ins3k `'k SIk SIk SIk ∼ Sk ) i^i ∼ (( Ins2k Ins2k Ins3k SIk Sk (+) ( Ins3k SIk SIk SIk SIk SIk Sk u. Ins2k Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 ~P1 ~P1 1c)"k~P1 ~P1 ~P1 1c))"k~P1 ~P1 1c)"k Nn ) \ {(/)}) e. _V
379	310, 378	eqeltri 2423	1 |- Oddfin 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  `'_kccnvk 4175   Ins2_k cins2k 4176   Ins3_k cins3k 4177  "_kcimak 4179   SI_k csik 4181   S_k cssetk 4183   _I_k_k cidk 4184   Nn cnnc 4373   +o cplc 4375   Odd_fin coddfin 4437

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-ext 2334  ax-nin 4078  ax-xp 4079  ax-cnv 4080  ax-1c 4081  ax-sset 4082  ax-si 4083  ax-ins2 4084  ax-ins3 4085  ax-typlower 4086  ax-sn 4087

This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-nan 1288  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2340  df-cleq 2346  df-clel 2349  df-nfc 2478  df-ne 2518  df-ral 2619  df-rex 2620  df-v 2861  df-sbc 3047  df-nin 3211  df-compl 3212  df-in 3213  df-un 3214  df-dif 3215  df-symdif 3216  df-ss 3259  df-nul 3551  df-if 3663  df-pw 3724  df-sn 3741  df-pr 3742  df-uni 3892  df-int 3927  df-opk 4058  df-1c 4136  df-pw1 4137  df-uni1 4138  df-xpk 4185  df-cnvk 4186  df-ins2k 4187  df-ins3k 4188  df-imak 4189  df-cok 4190  df-p6 4191  df-sik 4192  df-ssetk 4193  df-imagek 4194  df-idk 4195  df-addc 4378  df-nnc 4379  df-oddfin 4445

This theorem is referenced by:  evenoddnnnul  4514