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 )