Theorem nnsucelrlem1 4424

Description: Lemma for nnsucelr 4428. Establish stratification for the inductive hypothesis. (Contributed by SF, 15-Jan-2015.)

Assertion

Ref	Expression
nnsucelrlem1	|- {m | A.aA.x((-. x e. a /\ (a u. {x}) e. (m +o 1c)) -> a e. m)} e. _V

Distinct variable group:   m,a,x

Proof of Theorem nnsucelrlem1

Dummy variables e t w are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		vex 2862	. . . . . . . 8 |- m e. _V
2	1	elimak 4259	. . . . . . 7 |- (m e. (((((( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk (+) Ins2k ( Ins2k Ins3k SIk Sk u. Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c) i^i Ins2k Ins2k (`'kImagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 1c) o.k Sk ))"k~P1 ~P1 ~P1 ~P1 1c) \ Ins3k SIk Sk ) \ (_V X.k Sk ))"k~P1 ~P1 ~P1 1c)"k1c) <-> E.t e. 1c <<t, m>> e. ((((( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk (+) Ins2k ( Ins2k Ins3k SIk Sk u. Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c) i^i Ins2k Ins2k (`'kImagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 1c) o.k Sk ))"k~P1 ~P1 ~P1 ~P1 1c) \ Ins3k SIk Sk ) \ (_V X.k Sk ))"k~P1 ~P1 ~P1 1c))
3		df-rex 2620	. . . . . . . 8 |- (E.t e. 1c <<t, m>> e. ((((( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk (+) Ins2k ( Ins2k Ins3k SIk Sk u. Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c) i^i Ins2k Ins2k (`'kImagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 1c) o.k Sk ))"k~P1 ~P1 ~P1 ~P1 1c) \ Ins3k SIk Sk ) \ (_V X.k Sk ))"k~P1 ~P1 ~P1 1c) <-> E.t(t e. 1c /\ <<t, m>> e. ((((( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk (+) Ins2k ( Ins2k Ins3k SIk Sk u. Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c) i^i Ins2k Ins2k (`'kImagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 1c) o.k Sk ))"k~P1 ~P1 ~P1 ~P1 1c) \ Ins3k SIk Sk ) \ (_V X.k Sk ))"k~P1 ~P1 ~P1 1c)))
4		el1c 4139	. . . . . . . . . . . 12 |- (t e. 1c <-> E.a t = {a})
5	4	anbi1i 676	. . . . . . . . . . 11 |- ((t e. 1c /\ <<t, m>> e. ((((( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk (+) Ins2k ( Ins2k Ins3k SIk Sk u. Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c) i^i Ins2k Ins2k (`'kImagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 1c) o.k Sk ))"k~P1 ~P1 ~P1 ~P1 1c) \ Ins3k SIk Sk ) \ (_V X.k Sk ))"k~P1 ~P1 ~P1 1c)) <-> (E.a t = {a} /\ <<t, m>> e. ((((( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk (+) Ins2k ( Ins2k Ins3k SIk Sk u. Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c) i^i Ins2k Ins2k (`'kImagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 1c) o.k Sk ))"k~P1 ~P1 ~P1 ~P1 1c) \ Ins3k SIk Sk ) \ (_V X.k Sk ))"k~P1 ~P1 ~P1 1c)))
6		19.41v 1901	. . . . . . . . . . 11 |- (E.a(t = {a} /\ <<t, m>> e. ((((( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk (+) Ins2k ( Ins2k Ins3k SIk Sk u. Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c) i^i Ins2k Ins2k (`'kImagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 1c) o.k Sk ))"k~P1 ~P1 ~P1 ~P1 1c) \ Ins3k SIk Sk ) \ (_V X.k Sk ))"k~P1 ~P1 ~P1 1c)) <-> (E.a t = {a} /\ <<t, m>> e. ((((( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk (+) Ins2k ( Ins2k Ins3k SIk Sk u. Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c) i^i Ins2k Ins2k (`'kImagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 1c) o.k Sk ))"k~P1 ~P1 ~P1 ~P1 1c) \ Ins3k SIk Sk ) \ (_V X.k Sk ))"k~P1 ~P1 ~P1 1c)))
7	5, 6	bitr4i 243	. . . . . . . . . 10 |- ((t e. 1c /\ <<t, m>> e. ((((( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk (+) Ins2k ( Ins2k Ins3k SIk Sk u. Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c) i^i Ins2k Ins2k (`'kImagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 1c) o.k Sk ))"k~P1 ~P1 ~P1 ~P1 1c) \ Ins3k SIk Sk ) \ (_V X.k Sk ))"k~P1 ~P1 ~P1 1c)) <-> E.a(t = {a} /\ <<t, m>> e. ((((( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk (+) Ins2k ( Ins2k Ins3k SIk Sk u. Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c) i^i Ins2k Ins2k (`'kImagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 1c) o.k Sk ))"k~P1 ~P1 ~P1 ~P1 1c) \ Ins3k SIk Sk ) \ (_V X.k Sk ))"k~P1 ~P1 ~P1 1c)))
8	7	exbii 1582	. . . . . . . . 9 |- (E.t(t e. 1c /\ <<t, m>> e. ((((( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk (+) Ins2k ( Ins2k Ins3k SIk Sk u. Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c) i^i Ins2k Ins2k (`'kImagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 1c) o.k Sk ))"k~P1 ~P1 ~P1 ~P1 1c) \ Ins3k SIk Sk ) \ (_V X.k Sk ))"k~P1 ~P1 ~P1 1c)) <-> E.tE.a(t = {a} /\ <<t, m>> e. ((((( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk (+) Ins2k ( Ins2k Ins3k SIk Sk u. Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c) i^i Ins2k Ins2k (`'kImagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 1c) o.k Sk ))"k~P1 ~P1 ~P1 ~P1 1c) \ Ins3k SIk Sk ) \ (_V X.k Sk ))"k~P1 ~P1 ~P1 1c)))
9		excom 1741	. . . . . . . . 9 |- (E.aE.t(t = {a} /\ <<t, m>> e. ((((( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk (+) Ins2k ( Ins2k Ins3k SIk Sk u. Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c) i^i Ins2k Ins2k (`'kImagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 1c) o.k Sk ))"k~P1 ~P1 ~P1 ~P1 1c) \ Ins3k SIk Sk ) \ (_V X.k Sk ))"k~P1 ~P1 ~P1 1c)) <-> E.tE.a(t = {a} /\ <<t, m>> e. ((((( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk (+) Ins2k ( Ins2k Ins3k SIk Sk u. Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c) i^i Ins2k Ins2k (`'kImagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 1c) o.k Sk ))"k~P1 ~P1 ~P1 ~P1 1c) \ Ins3k SIk Sk ) \ (_V X.k Sk ))"k~P1 ~P1 ~P1 1c)))
10	8, 9	bitr4i 243	. . . . . . . 8 |- (E.t(t e. 1c /\ <<t, m>> e. ((((( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk (+) Ins2k ( Ins2k Ins3k SIk Sk u. Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c) i^i Ins2k Ins2k (`'kImagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 1c) o.k Sk ))"k~P1 ~P1 ~P1 ~P1 1c) \ Ins3k SIk Sk ) \ (_V X.k Sk ))"k~P1 ~P1 ~P1 1c)) <-> E.aE.t(t = {a} /\ <<t, m>> e. ((((( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk (+) Ins2k ( Ins2k Ins3k SIk Sk u. Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c) i^i Ins2k Ins2k (`'kImagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 1c) o.k Sk ))"k~P1 ~P1 ~P1 ~P1 1c) \ Ins3k SIk Sk ) \ (_V X.k Sk ))"k~P1 ~P1 ~P1 1c)))
11	3, 10	bitri 240	. . . . . . 7 |- (E.t e. 1c <<t, m>> e. ((((( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk (+) Ins2k ( Ins2k Ins3k SIk Sk u. Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c) i^i Ins2k Ins2k (`'kImagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 1c) o.k Sk ))"k~P1 ~P1 ~P1 ~P1 1c) \ Ins3k SIk Sk ) \ (_V X.k Sk ))"k~P1 ~P1 ~P1 1c) <-> E.aE.t(t = {a} /\ <<t, m>> e. ((((( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk (+) Ins2k ( Ins2k Ins3k SIk Sk u. Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c) i^i Ins2k Ins2k (`'kImagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 1c) o.k Sk ))"k~P1 ~P1 ~P1 ~P1 1c) \ Ins3k SIk Sk ) \ (_V X.k Sk ))"k~P1 ~P1 ~P1 1c)))
12	2, 11	bitri 240	. . . . . 6 |- (m e. (((((( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk (+) Ins2k ( Ins2k Ins3k SIk Sk u. Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c) i^i Ins2k Ins2k (`'kImagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 1c) o.k Sk ))"k~P1 ~P1 ~P1 ~P1 1c) \ Ins3k SIk Sk ) \ (_V X.k Sk ))"k~P1 ~P1 ~P1 1c)"k1c) <-> E.aE.t(t = {a} /\ <<t, m>> e. ((((( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk (+) Ins2k ( Ins2k Ins3k SIk Sk u. Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c) i^i Ins2k Ins2k (`'kImagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 1c) o.k Sk ))"k~P1 ~P1 ~P1 ~P1 1c) \ Ins3k SIk Sk ) \ (_V X.k Sk ))"k~P1 ~P1 ~P1 1c)))
13		snex 4111	. . . . . . . . 9 |- {a} e. _V
14		opkeq1 4059	. . . . . . . . . 10 |- (t = {a} -> <<t, m>> = <<{a}, m>>)
15	14	eleq1d 2419	. . . . . . . . 9 |- (t = {a} -> (<<t, m>> e. ((((( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk (+) Ins2k ( Ins2k Ins3k SIk Sk u. Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c) i^i Ins2k Ins2k (`'kImagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 1c) o.k Sk ))"k~P1 ~P1 ~P1 ~P1 1c) \ Ins3k SIk Sk ) \ (_V X.k Sk ))"k~P1 ~P1 ~P1 1c) <-> <<{a}, m>> e. ((((( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk (+) Ins2k ( Ins2k Ins3k SIk Sk u. Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c) i^i Ins2k Ins2k (`'kImagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 1c) o.k Sk ))"k~P1 ~P1 ~P1 ~P1 1c) \ Ins3k SIk Sk ) \ (_V X.k Sk ))"k~P1 ~P1 ~P1 1c)))
16	13, 15	ceqsexv 2894	. . . . . . . 8 |- (E.t(t = {a} /\ <<t, m>> e. ((((( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk (+) Ins2k ( Ins2k Ins3k SIk Sk u. Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c) i^i Ins2k Ins2k (`'kImagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 1c) o.k Sk ))"k~P1 ~P1 ~P1 ~P1 1c) \ Ins3k SIk Sk ) \ (_V X.k Sk ))"k~P1 ~P1 ~P1 1c)) <-> <<{a}, m>> e. ((((( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk (+) Ins2k ( Ins2k Ins3k SIk Sk u. Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c) i^i Ins2k Ins2k (`'kImagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 1c) o.k Sk ))"k~P1 ~P1 ~P1 ~P1 1c) \ Ins3k SIk Sk ) \ (_V X.k Sk ))"k~P1 ~P1 ~P1 1c))
17		opkex 4113	. . . . . . . . . . . 12 |- <<{a}, m>> e. _V
18	17	elimak 4259	. . . . . . . . . . 11 |- (<<{a}, m>> e. ((((( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk (+) Ins2k ( Ins2k Ins3k SIk Sk u. Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c) i^i Ins2k Ins2k (`'kImagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 1c) o.k Sk ))"k~P1 ~P1 ~P1 ~P1 1c) \ Ins3k SIk Sk ) \ (_V X.k Sk ))"k~P1 ~P1 ~P1 1c) <-> E.t e. ~P1 ~P1 ~P1 1c<<t, <<{a}, m>>>> e. (((( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk (+) Ins2k ( Ins2k Ins3k SIk Sk u. Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c) i^i Ins2k Ins2k (`'kImagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 1c) o.k Sk ))"k~P1 ~P1 ~P1 ~P1 1c) \ Ins3k SIk Sk ) \ (_V X.k Sk )))
19		df-rex 2620	. . . . . . . . . . . 12 |- (E.t e. ~P1 ~P1 ~P1 1c<<t, <<{a}, m>>>> e. (((( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk (+) Ins2k ( Ins2k Ins3k SIk Sk u. Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c) i^i Ins2k Ins2k (`'kImagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 1c) o.k Sk ))"k~P1 ~P1 ~P1 ~P1 1c) \ Ins3k SIk Sk ) \ (_V X.k Sk )) <-> E.t(t e. ~P1 ~P1 ~P1 1c /\ <<t, <<{a}, m>>>> e. (((( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk (+) Ins2k ( Ins2k Ins3k SIk Sk u. Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c) i^i Ins2k Ins2k (`'kImagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 1c) o.k Sk ))"k~P1 ~P1 ~P1 ~P1 1c) \ Ins3k SIk Sk ) \ (_V X.k Sk ))))
20		elpw131c 4149	. . . . . . . . . . . . . . . 16 |- (t e. ~P1 ~P1 ~P1 1c <-> E.x t = {{{{x}}}})
21	20	anbi1i 676	. . . . . . . . . . . . . . 15 |- ((t e. ~P1 ~P1 ~P1 1c /\ <<t, <<{a}, m>>>> e. (((( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk (+) Ins2k ( Ins2k Ins3k SIk Sk u. Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c) i^i Ins2k Ins2k (`'kImagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 1c) o.k Sk ))"k~P1 ~P1 ~P1 ~P1 1c) \ Ins3k SIk Sk ) \ (_V X.k Sk ))) <-> (E.x t = {{{{x}}}} /\ <<t, <<{a}, m>>>> e. (((( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk (+) Ins2k ( Ins2k Ins3k SIk Sk u. Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c) i^i Ins2k Ins2k (`'kImagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 1c) o.k Sk ))"k~P1 ~P1 ~P1 ~P1 1c) \ Ins3k SIk Sk ) \ (_V X.k Sk ))))
22		19.41v 1901	. . . . . . . . . . . . . . 15 |- (E.x(t = {{{{x}}}} /\ <<t, <<{a}, m>>>> e. (((( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk (+) Ins2k ( Ins2k Ins3k SIk Sk u. Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c) i^i Ins2k Ins2k (`'kImagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 1c) o.k Sk ))"k~P1 ~P1 ~P1 ~P1 1c) \ Ins3k SIk Sk ) \ (_V X.k Sk ))) <-> (E.x t = {{{{x}}}} /\ <<t, <<{a}, m>>>> e. (((( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk (+) Ins2k ( Ins2k Ins3k SIk Sk u. Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c) i^i Ins2k Ins2k (`'kImagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 1c) o.k Sk ))"k~P1 ~P1 ~P1 ~P1 1c) \ Ins3k SIk Sk ) \ (_V X.k Sk ))))
23	21, 22	bitr4i 243	. . . . . . . . . . . . . 14 |- ((t e. ~P1 ~P1 ~P1 1c /\ <<t, <<{a}, m>>>> e. (((( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk (+) Ins2k ( Ins2k Ins3k SIk Sk u. Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c) i^i Ins2k Ins2k (`'kImagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 1c) o.k Sk ))"k~P1 ~P1 ~P1 ~P1 1c) \ Ins3k SIk Sk ) \ (_V X.k Sk ))) <-> E.x(t = {{{{x}}}} /\ <<t, <<{a}, m>>>> e. (((( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk (+) Ins2k ( Ins2k Ins3k SIk Sk u. Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c) i^i Ins2k Ins2k (`'kImagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 1c) o.k Sk ))"k~P1 ~P1 ~P1 ~P1 1c) \ Ins3k SIk Sk ) \ (_V X.k Sk ))))
24	23	exbii 1582	. . . . . . . . . . . . 13 |- (E.t(t e. ~P1 ~P1 ~P1 1c /\ <<t, <<{a}, m>>>> e. (((( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk (+) Ins2k ( Ins2k Ins3k SIk Sk u. Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c) i^i Ins2k Ins2k (`'kImagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 1c) o.k Sk ))"k~P1 ~P1 ~P1 ~P1 1c) \ Ins3k SIk Sk ) \ (_V X.k Sk ))) <-> E.tE.x(t = {{{{x}}}} /\ <<t, <<{a}, m>>>> e. (((( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk (+) Ins2k ( Ins2k Ins3k SIk Sk u. Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c) i^i Ins2k Ins2k (`'kImagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 1c) o.k Sk ))"k~P1 ~P1 ~P1 ~P1 1c) \ Ins3k SIk Sk ) \ (_V X.k Sk ))))
25		excom 1741	. . . . . . . . . . . . 13 |- (E.xE.t(t = {{{{x}}}} /\ <<t, <<{a}, m>>>> e. (((( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk (+) Ins2k ( Ins2k Ins3k SIk Sk u. Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c) i^i Ins2k Ins2k (`'kImagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 1c) o.k Sk ))"k~P1 ~P1 ~P1 ~P1 1c) \ Ins3k SIk Sk ) \ (_V X.k Sk ))) <-> E.tE.x(t = {{{{x}}}} /\ <<t, <<{a}, m>>>> e. (((( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk (+) Ins2k ( Ins2k Ins3k SIk Sk u. Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c) i^i Ins2k Ins2k (`'kImagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 1c) o.k Sk ))"k~P1 ~P1 ~P1 ~P1 1c) \ Ins3k SIk Sk ) \ (_V X.k Sk ))))
26	24, 25	bitr4i 243	. . . . . . . . . . . 12 |- (E.t(t e. ~P1 ~P1 ~P1 1c /\ <<t, <<{a}, m>>>> e. (((( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk (+) Ins2k ( Ins2k Ins3k SIk Sk u. Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c) i^i Ins2k Ins2k (`'kImagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 1c) o.k Sk ))"k~P1 ~P1 ~P1 ~P1 1c) \ Ins3k SIk Sk ) \ (_V X.k Sk ))) <-> E.xE.t(t = {{{{x}}}} /\ <<t, <<{a}, m>>>> e. (((( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk (+) Ins2k ( Ins2k Ins3k SIk Sk u. Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c) i^i Ins2k Ins2k (`'kImagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 1c) o.k Sk ))"k~P1 ~P1 ~P1 ~P1 1c) \ Ins3k SIk Sk ) \ (_V X.k Sk ))))
27	19, 26	bitri 240	. . . . . . . . . . 11 |- (E.t e. ~P1 ~P1 ~P1 1c<<t, <<{a}, m>>>> e. (((( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk (+) Ins2k ( Ins2k Ins3k SIk Sk u. Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c) i^i Ins2k Ins2k (`'kImagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 1c) o.k Sk ))"k~P1 ~P1 ~P1 ~P1 1c) \ Ins3k SIk Sk ) \ (_V X.k Sk )) <-> E.xE.t(t = {{{{x}}}} /\ <<t, <<{a}, m>>>> e. (((( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk (+) Ins2k ( Ins2k Ins3k SIk Sk u. Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c) i^i Ins2k Ins2k (`'kImagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 1c) o.k Sk ))"k~P1 ~P1 ~P1 ~P1 1c) \ Ins3k SIk Sk ) \ (_V X.k Sk ))))
28	18, 27	bitri 240	. . . . . . . . . 10 |- (<<{a}, m>> e. ((((( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk (+) Ins2k ( Ins2k Ins3k SIk Sk u. Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c) i^i Ins2k Ins2k (`'kImagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 1c) o.k Sk ))"k~P1 ~P1 ~P1 ~P1 1c) \ Ins3k SIk Sk ) \ (_V X.k Sk ))"k~P1 ~P1 ~P1 1c) <-> E.xE.t(t = {{{{x}}}} /\ <<t, <<{a}, m>>>> e. (((( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk (+) Ins2k ( Ins2k Ins3k SIk Sk u. Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c) i^i Ins2k Ins2k (`'kImagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 1c) o.k Sk ))"k~P1 ~P1 ~P1 ~P1 1c) \ Ins3k SIk Sk ) \ (_V X.k Sk ))))
29		snex 4111	. . . . . . . . . . . . 13 |- {{{{x}}}} e. _V
30		opkeq1 4059	. . . . . . . . . . . . . 14 |- (t = {{{{x}}}} -> <<t, <<{a}, m>>>> = <<{{{{x}}}}, <<{a}, m>>>>)
31	30	eleq1d 2419	. . . . . . . . . . . . 13 |- (t = {{{{x}}}} -> (<<t, <<{a}, m>>>> e. (((( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk (+) Ins2k ( Ins2k Ins3k SIk Sk u. Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c) i^i Ins2k Ins2k (`'kImagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 1c) o.k Sk ))"k~P1 ~P1 ~P1 ~P1 1c) \ Ins3k SIk Sk ) \ (_V X.k Sk )) <-> <<{{{{x}}}}, <<{a}, m>>>> e. (((( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk (+) Ins2k ( Ins2k Ins3k SIk Sk u. Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c) i^i Ins2k Ins2k (`'kImagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 1c) o.k Sk ))"k~P1 ~P1 ~P1 ~P1 1c) \ Ins3k SIk Sk ) \ (_V X.k Sk ))))
32	29, 31	ceqsexv 2894	. . . . . . . . . . . 12 |- (E.t(t = {{{{x}}}} /\ <<t, <<{a}, m>>>> e. (((( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk (+) Ins2k ( Ins2k Ins3k SIk Sk u. Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c) i^i Ins2k Ins2k (`'kImagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 1c) o.k Sk ))"k~P1 ~P1 ~P1 ~P1 1c) \ Ins3k SIk Sk ) \ (_V X.k Sk ))) <-> <<{{{{x}}}}, <<{a}, m>>>> e. (((( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk (+) Ins2k ( Ins2k Ins3k SIk Sk u. Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c) i^i Ins2k Ins2k (`'kImagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 1c) o.k Sk ))"k~P1 ~P1 ~P1 ~P1 1c) \ Ins3k SIk Sk ) \ (_V X.k Sk )))
33		eldif 3221	. . . . . . . . . . . . . 14 |- (<<{{{{x}}}}, <<{a}, m>>>> e. (((( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk (+) Ins2k ( Ins2k Ins3k SIk Sk u. Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c) i^i Ins2k Ins2k (`'kImagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 1c) o.k Sk ))"k~P1 ~P1 ~P1 ~P1 1c) \ Ins3k SIk Sk ) \ (_V X.k Sk )) <-> (<<{{{{x}}}}, <<{a}, m>>>> e. ((( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk (+) Ins2k ( Ins2k Ins3k SIk Sk u. Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c) i^i Ins2k Ins2k (`'kImagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 1c) o.k Sk ))"k~P1 ~P1 ~P1 ~P1 1c) \ Ins3k SIk Sk ) /\ -. <<{{{{x}}}}, <<{a}, m>>>> e. (_V X.k Sk )))
34		eldif 3221	. . . . . . . . . . . . . . . . 17 |- (<<{{{{x}}}}, <<{a}, m>>>> e. ((( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk (+) Ins2k ( Ins2k Ins3k SIk Sk u. Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c) i^i Ins2k Ins2k (`'kImagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 1c) o.k Sk ))"k~P1 ~P1 ~P1 ~P1 1c) \ Ins3k SIk Sk ) <-> (<<{{{{x}}}}, <<{a}, m>>>> e. (( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk (+) Ins2k ( Ins2k Ins3k SIk Sk u. Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c) i^i Ins2k Ins2k (`'kImagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 1c) o.k Sk ))"k~P1 ~P1 ~P1 ~P1 1c) /\ -. <<{{{{x}}}}, <<{a}, m>>>> e. Ins3k SIk Sk ))
35		opkex 4113	. . . . . . . . . . . . . . . . . . . . 21 |- <<{{{{x}}}}, <<{a}, m>>>> e. _V
36	35	elimak 4259	. . . . . . . . . . . . . . . . . . . 20 |- (<<{{{{x}}}}, <<{a}, m>>>> e. (( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk (+) Ins2k ( Ins2k Ins3k SIk Sk u. Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c) i^i Ins2k Ins2k (`'kImagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 1c) o.k Sk ))"k~P1 ~P1 ~P1 ~P1 1c) <-> E.t e. ~P1 ~P1 ~P1 ~P1 1c<<t, <<{{{{x}}}}, <<{a}, m>>>>>> e. ( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk (+) Ins2k ( Ins2k Ins3k SIk Sk u. Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c) i^i Ins2k Ins2k (`'kImagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 1c) o.k Sk )))
37		df-rex 2620	. . . . . . . . . . . . . . . . . . . . . 22 |- (E.t e. ~P1 ~P1 ~P1 ~P1 1c<<t, <<{{{{x}}}}, <<{a}, m>>>>>> e. ( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk (+) Ins2k ( Ins2k Ins3k SIk Sk u. Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c) i^i Ins2k Ins2k (`'kImagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 1c) o.k Sk )) <-> E.t(t e. ~P1 ~P1 ~P1 ~P1 1c /\ <<t, <<{{{{x}}}}, <<{a}, m>>>>>> e. ( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk (+) Ins2k ( Ins2k Ins3k SIk Sk u. Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c) i^i Ins2k Ins2k (`'kImagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 1c) o.k Sk ))))
38		elpw141c 4150	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (t e. ~P1 ~P1 ~P1 ~P1 1c <-> E.w t = {{{{{w}}}}})
39	38	anbi1i 676	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((t e. ~P1 ~P1 ~P1 ~P1 1c /\ <<t, <<{{{{x}}}}, <<{a}, m>>>>>> e. ( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk (+) Ins2k ( Ins2k Ins3k SIk Sk u. Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c) i^i Ins2k Ins2k (`'kImagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 1c) o.k Sk ))) <-> (E.w t = {{{{{w}}}}} /\ <<t, <<{{{{x}}}}, <<{a}, m>>>>>> e. ( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk (+) Ins2k ( Ins2k Ins3k SIk Sk u. Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c) i^i Ins2k Ins2k (`'kImagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 1c) o.k Sk ))))
40		19.41v 1901	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (E.w(t = {{{{{w}}}}} /\ <<t, <<{{{{x}}}}, <<{a}, m>>>>>> e. ( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk (+) Ins2k ( Ins2k Ins3k SIk Sk u. Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c) i^i Ins2k Ins2k (`'kImagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 1c) o.k Sk ))) <-> (E.w t = {{{{{w}}}}} /\ <<t, <<{{{{x}}}}, <<{a}, m>>>>>> e. ( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk (+) Ins2k ( Ins2k Ins3k SIk Sk u. Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c) i^i Ins2k Ins2k (`'kImagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 1c) o.k Sk ))))
41	39, 40	bitr4i 243	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((t e. ~P1 ~P1 ~P1 ~P1 1c /\ <<t, <<{{{{x}}}}, <<{a}, m>>>>>> e. ( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk (+) Ins2k ( Ins2k Ins3k SIk Sk u. Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c) i^i Ins2k Ins2k (`'kImagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 1c) o.k Sk ))) <-> E.w(t = {{{{{w}}}}} /\ <<t, <<{{{{x}}}}, <<{a}, m>>>>>> e. ( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk (+) Ins2k ( Ins2k Ins3k SIk Sk u. Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c) i^i Ins2k Ins2k (`'kImagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 1c) o.k Sk ))))
42	41	exbii 1582	. . . . . . . . . . . . . . . . . . . . . . 23 |- (E.t(t e. ~P1 ~P1 ~P1 ~P1 1c /\ <<t, <<{{{{x}}}}, <<{a}, m>>>>>> e. ( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk (+) Ins2k ( Ins2k Ins3k SIk Sk u. Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c) i^i Ins2k Ins2k (`'kImagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 1c) o.k Sk ))) <-> E.tE.w(t = {{{{{w}}}}} /\ <<t, <<{{{{x}}}}, <<{a}, m>>>>>> e. ( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk (+) Ins2k ( Ins2k Ins3k SIk Sk u. Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c) i^i Ins2k Ins2k (`'kImagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 1c) o.k Sk ))))
43		excom 1741	. . . . . . . . . . . . . . . . . . . . . . 23 |- (E.wE.t(t = {{{{{w}}}}} /\ <<t, <<{{{{x}}}}, <<{a}, m>>>>>> e. ( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk (+) Ins2k ( Ins2k Ins3k SIk Sk u. Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c) i^i Ins2k Ins2k (`'kImagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 1c) o.k Sk ))) <-> E.tE.w(t = {{{{{w}}}}} /\ <<t, <<{{{{x}}}}, <<{a}, m>>>>>> e. ( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk (+) Ins2k ( Ins2k Ins3k SIk Sk u. Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c) i^i Ins2k Ins2k (`'kImagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 1c) o.k Sk ))))
44	42, 43	bitr4i 243	. . . . . . . . . . . . . . . . . . . . . 22 |- (E.t(t e. ~P1 ~P1 ~P1 ~P1 1c /\ <<t, <<{{{{x}}}}, <<{a}, m>>>>>> e. ( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk (+) Ins2k ( Ins2k Ins3k SIk Sk u. Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c) i^i Ins2k Ins2k (`'kImagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 1c) o.k Sk ))) <-> E.wE.t(t = {{{{{w}}}}} /\ <<t, <<{{{{x}}}}, <<{a}, m>>>>>> e. ( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk (+) Ins2k ( Ins2k Ins3k SIk Sk u. Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c) i^i Ins2k Ins2k (`'kImagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 1c) o.k Sk ))))
45	37, 44	bitri 240	. . . . . . . . . . . . . . . . . . . . 21 |- (E.t e. ~P1 ~P1 ~P1 ~P1 1c<<t, <<{{{{x}}}}, <<{a}, m>>>>>> e. ( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk (+) Ins2k ( Ins2k Ins3k SIk Sk u. Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c) i^i Ins2k Ins2k (`'kImagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 1c) o.k Sk )) <-> E.wE.t(t = {{{{{w}}}}} /\ <<t, <<{{{{x}}}}, <<{a}, m>>>>>> e. ( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk (+) Ins2k ( Ins2k Ins3k SIk Sk u. Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c) i^i Ins2k Ins2k (`'kImagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 1c) o.k Sk ))))
46		snex 4111	. . . . . . . . . . . . . . . . . . . . . . . 24 |- {{{{{w}}}}} e. _V
47		opkeq1 4059	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (t = {{{{{w}}}}} -> <<t, <<{{{{x}}}}, <<{a}, m>>>>>> = <<{{{{{w}}}}}, <<{{{{x}}}}, <<{a}, m>>>>>>)
48	47	eleq1d 2419	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (t = {{{{{w}}}}} -> (<<t, <<{{{{x}}}}, <<{a}, m>>>>>> e. ( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk (+) Ins2k ( Ins2k Ins3k SIk Sk u. Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c) i^i Ins2k Ins2k (`'kImagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 1c) o.k Sk )) <-> <<{{{{{w}}}}}, <<{{{{x}}}}, <<{a}, m>>>>>> e. ( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk (+) Ins2k ( Ins2k Ins3k SIk Sk u. Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c) i^i Ins2k Ins2k (`'kImagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 1c) o.k Sk ))))
49	46, 48	ceqsexv 2894	. . . . . . . . . . . . . . . . . . . . . . 23 |- (E.t(t = {{{{{w}}}}} /\ <<t, <<{{{{x}}}}, <<{a}, m>>>>>> e. ( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk (+) Ins2k ( Ins2k Ins3k SIk Sk u. Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c) i^i Ins2k Ins2k (`'kImagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 1c) o.k Sk ))) <-> <<{{{{{w}}}}}, <<{{{{x}}}}, <<{a}, m>>>>>> e. ( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk (+) Ins2k ( Ins2k Ins3k SIk Sk u. Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c) i^i Ins2k Ins2k (`'kImagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 1c) o.k Sk )))
50		elin 3219	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (<<{{{{{w}}}}}, <<{{{{x}}}}, <<{a}, m>>>>>> e. ( ∼ (( Ins3k SIk SIk SIk SIk SIk Sk (+) Ins2k ( Ins2k Ins3k SIk Sk u. Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c) i^i Ins2k Ins2k (`'kImagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 1c) o.k Sk )) <-> (<<{{{{{w}}}}}, <<{{{{x}}}}, <<{a}, m>>>>>> e. ∼ (( Ins3k SIk SIk SIk SIk SIk Sk (+) Ins2k ( Ins2k Ins3k SIk Sk u. Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c) /\ <<{{{{{w}}}}}, <<{{{{x}}}}, <<{a}, m>>>>>> e. Ins2k Ins2k (`'kImagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 1c) o.k Sk )))
51		opkex 4113	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- <<{{{{{w}}}}}, <<{{{{x}}}}, <<{a}, m>>>>>> e. _V
52	51	elimak 4259	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (<<{{{{{w}}}}}, <<{{{{x}}}}, <<{a}, m>>>>>> e. (( Ins3k SIk SIk SIk SIk SIk Sk (+) Ins2k ( Ins2k Ins3k SIk Sk u. Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c) <-> E.t e. ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c<<t, <<{{{{{w}}}}}, <<{{{{x}}}}, <<{a}, m>>>>>>>> e. ( Ins3k SIk SIk SIk SIk SIk Sk (+) Ins2k ( Ins2k Ins3k SIk Sk u. Ins3k _I_kk )))
53		df-rex 2620	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (E.t e. ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c<<t, <<{{{{{w}}}}}, <<{{{{x}}}}, <<{a}, m>>>>>>>> e. ( Ins3k SIk SIk SIk SIk SIk Sk (+) Ins2k ( Ins2k Ins3k SIk Sk u. Ins3k _I_kk )) <-> E.t(t e. ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c /\ <<t, <<{{{{{w}}}}}, <<{{{{x}}}}, <<{a}, m>>>>>>>> e. ( Ins3k SIk SIk SIk SIk SIk Sk (+) Ins2k ( Ins2k Ins3k SIk Sk u. Ins3k _I_kk ))))
54		elpw171c 4153	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (t e. ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c <-> E.e t = {{{{{{{{e}}}}}}}})
55	54	anbi1i 676	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ((t e. ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c /\ <<t, <<{{{{{w}}}}}, <<{{{{x}}}}, <<{a}, m>>>>>>>> e. ( Ins3k SIk SIk SIk SIk SIk Sk (+) Ins2k ( Ins2k Ins3k SIk Sk u. Ins3k _I_kk ))) <-> (E.e t = {{{{{{{{e}}}}}}}} /\ <<t, <<{{{{{w}}}}}, <<{{{{x}}}}, <<{a}, m>>>>>>>> e. ( Ins3k SIk SIk SIk SIk SIk Sk (+) Ins2k ( Ins2k Ins3k SIk Sk u. Ins3k _I_kk ))))
56		19.41v 1901	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (E.e(t = {{{{{{{{e}}}}}}}} /\ <<t, <<{{{{{w}}}}}, <<{{{{x}}}}, <<{a}, m>>>>>>>> e. ( Ins3k SIk SIk SIk SIk SIk Sk (+) Ins2k ( Ins2k Ins3k SIk Sk u. Ins3k _I_kk ))) <-> (E.e t = {{{{{{{{e}}}}}}}} /\ <<t, <<{{{{{w}}}}}, <<{{{{x}}}}, <<{a}, m>>>>>>>> e. ( Ins3k SIk SIk SIk SIk SIk Sk (+) Ins2k ( Ins2k Ins3k SIk Sk u. Ins3k _I_kk ))))
57	55, 56	bitr4i 243	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ((t e. ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c /\ <<t, <<{{{{{w}}}}}, <<{{{{x}}}}, <<{a}, m>>>>>>>> e. ( Ins3k SIk SIk SIk SIk SIk Sk (+) Ins2k ( Ins2k Ins3k SIk Sk u. Ins3k _I_kk ))) <-> E.e(t = {{{{{{{{e}}}}}}}} /\ <<t, <<{{{{{w}}}}}, <<{{{{x}}}}, <<{a}, m>>>>>>>> e. ( Ins3k SIk SIk SIk SIk SIk Sk (+) Ins2k ( Ins2k Ins3k SIk Sk u. Ins3k _I_kk ))))
58	57	exbii 1582	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (E.t(t e. ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c /\ <<t, <<{{{{{w}}}}}, <<{{{{x}}}}, <<{a}, m>>>>>>>> e. ( Ins3k SIk SIk SIk SIk SIk Sk (+) Ins2k ( Ins2k Ins3k SIk Sk u. Ins3k _I_kk ))) <-> E.tE.e(t = {{{{{{{{e}}}}}}}} /\ <<t, <<{{{{{w}}}}}, <<{{{{x}}}}, <<{a}, m>>>>>>>> e. ( Ins3k SIk SIk SIk SIk SIk Sk (+) Ins2k ( Ins2k Ins3k SIk Sk u. Ins3k _I_kk ))))
59		excom 1741	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (E.eE.t(t = {{{{{{{{e}}}}}}}} /\ <<t, <<{{{{{w}}}}}, <<{{{{x}}}}, <<{a}, m>>>>>>>> e. ( Ins3k SIk SIk SIk SIk SIk Sk (+) Ins2k ( Ins2k Ins3k SIk Sk u. Ins3k _I_kk ))) <-> E.tE.e(t = {{{{{{{{e}}}}}}}} /\ <<t, <<{{{{{w}}}}}, <<{{{{x}}}}, <<{a}, m>>>>>>>> e. ( Ins3k SIk SIk SIk SIk SIk Sk (+) Ins2k ( Ins2k Ins3k SIk Sk u. Ins3k _I_kk ))))
60	58, 59	bitr4i 243	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (E.t(t e. ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c /\ <<t, <<{{{{{w}}}}}, <<{{{{x}}}}, <<{a}, m>>>>>>>> e. ( Ins3k SIk SIk SIk SIk SIk Sk (+) Ins2k ( Ins2k Ins3k SIk Sk u. Ins3k _I_kk ))) <-> E.eE.t(t = {{{{{{{{e}}}}}}}} /\ <<t, <<{{{{{w}}}}}, <<{{{{x}}}}, <<{a}, m>>>>>>>> e. ( Ins3k SIk SIk SIk SIk SIk Sk (+) Ins2k ( Ins2k Ins3k SIk Sk u. Ins3k _I_kk ))))
61	53, 60	bitri 240	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (E.t e. ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c<<t, <<{{{{{w}}}}}, <<{{{{x}}}}, <<{a}, m>>>>>>>> e. ( Ins3k SIk SIk SIk SIk SIk Sk (+) Ins2k ( Ins2k Ins3k SIk Sk u. Ins3k _I_kk )) <-> E.eE.t(t = {{{{{{{{e}}}}}}}} /\ <<t, <<{{{{{w}}}}}, <<{{{{x}}}}, <<{a}, m>>>>>>>> e. ( Ins3k SIk SIk SIk SIk SIk Sk (+) Ins2k ( Ins2k Ins3k SIk Sk u. Ins3k _I_kk ))))
62	52, 61	bitri 240	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (<<{{{{{w}}}}}, <<{{{{x}}}}, <<{a}, m>>>>>> e. (( Ins3k SIk SIk SIk SIk SIk Sk (+) Ins2k ( Ins2k Ins3k SIk Sk u. Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c) <-> E.eE.t(t = {{{{{{{{e}}}}}}}} /\ <<t, <<{{{{{w}}}}}, <<{{{{x}}}}, <<{a}, m>>>>>>>> e. ( Ins3k SIk SIk SIk SIk SIk Sk (+) Ins2k ( Ins2k Ins3k SIk Sk u. Ins3k _I_kk ))))
63		snex 4111	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- {{{{{{{{e}}}}}}}} e. _V
64		opkeq1 4059	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (t = {{{{{{{{e}}}}}}}} -> <<t, <<{{{{{w}}}}}, <<{{{{x}}}}, <<{a}, m>>>>>>>> = <<{{{{{{{{e}}}}}}}}, <<{{{{{w}}}}}, <<{{{{x}}}}, <<{a}, m>>>>>>>>)
65	64	eleq1d 2419	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (t = {{{{{{{{e}}}}}}}} -> (<<t, <<{{{{{w}}}}}, <<{{{{x}}}}, <<{a}, m>>>>>>>> e. ( Ins3k SIk SIk SIk SIk SIk Sk (+) Ins2k ( Ins2k Ins3k SIk Sk u. Ins3k _I_kk )) <-> <<{{{{{{{{e}}}}}}}}, <<{{{{{w}}}}}, <<{{{{x}}}}, <<{a}, m>>>>>>>> e. ( Ins3k SIk SIk SIk SIk SIk Sk (+) Ins2k ( Ins2k Ins3k SIk Sk u. Ins3k _I_kk ))))
66	63, 65	ceqsexv 2894	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (E.t(t = {{{{{{{{e}}}}}}}} /\ <<t, <<{{{{{w}}}}}, <<{{{{x}}}}, <<{a}, m>>>>>>>> e. ( Ins3k SIk SIk SIk SIk SIk Sk (+) Ins2k ( Ins2k Ins3k SIk Sk u. Ins3k _I_kk ))) <-> <<{{{{{{{{e}}}}}}}}, <<{{{{{w}}}}}, <<{{{{x}}}}, <<{a}, m>>>>>>>> e. ( Ins3k SIk SIk SIk SIk SIk Sk (+) Ins2k ( Ins2k Ins3k SIk Sk u. Ins3k _I_kk )))
67		elsymdif 3223	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (<<{{{{{{{{e}}}}}}}}, <<{{{{{w}}}}}, <<{{{{x}}}}, <<{a}, m>>>>>>>> e. ( Ins3k SIk SIk SIk SIk SIk Sk (+) Ins2k ( Ins2k Ins3k SIk Sk u. Ins3k _I_kk )) <-> -. (<<{{{{{{{{e}}}}}}}}, <<{{{{{w}}}}}, <<{{{{x}}}}, <<{a}, m>>>>>>>> e. Ins3k SIk SIk SIk SIk SIk Sk <-> <<{{{{{{{{e}}}}}}}}, <<{{{{{w}}}}}, <<{{{{x}}}}, <<{a}, m>>>>>>>> e. Ins2k ( Ins2k Ins3k SIk Sk u. Ins3k _I_kk )))
68		snex 4111	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- {{{{{{e}}}}}} e. _V
69	68, 46, 35	otkelins3k 4256	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (<<{{{{{{{{e}}}}}}}}, <<{{{{{w}}}}}, <<{{{{x}}}}, <<{a}, m>>>>>>>> e. Ins3k SIk SIk SIk SIk SIk Sk <-> <<{{{{{{e}}}}}}, {{{{{w}}}}}>> e. SIk SIk SIk SIk SIk Sk )
70		snex 4111	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- {{{{{e}}}}} e. _V
71		snex 4111	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- {{{{w}}}} e. _V
72	70, 71	opksnelsik 4265	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (<<{{{{{{e}}}}}}, {{{{{w}}}}}>> e. SIk SIk SIk SIk SIk Sk <-> <<{{{{{e}}}}}, {{{{w}}}}>> e. SIk SIk SIk SIk Sk )
73		snex 4111	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- {{{{e}}}} e. _V
74		snex 4111	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- {{{w}}} e. _V
75	73, 74	opksnelsik 4265	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- (<<{{{{{e}}}}}, {{{{w}}}}>> e. SIk SIk SIk SIk Sk <-> <<{{{{e}}}}, {{{w}}}>> e. SIk SIk SIk Sk )
76		snex 4111	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- {{{e}}} e. _V
77		snex 4111	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- {{w}} e. _V
78	76, 77	opksnelsik 4265	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- (<<{{{{e}}}}, {{{w}}}>> e. SIk SIk SIk Sk <-> <<{{{e}}}, {{w}}>> e. SIk SIk Sk )
79		snex 4111	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- {{e}} e. _V
80		snex 4111	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- {w} e. _V
81	79, 80	opksnelsik 4265	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- (<<{{{e}}}, {{w}}>> e. SIk SIk Sk <-> <<{{e}}, {w}>> e. SIk Sk )
82		snex 4111	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- {e} e. _V
83		vex 2862	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- w e. _V
84	82, 83	opksnelsik 4265	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- (<<{{e}}, {w}>> e. SIk Sk <-> <<{e}, w>> e. Sk )
85		vex 2862	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- e e. _V
86	85, 83	elssetk 4270	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- (<<{e}, w>> e. Sk <-> e e. w)
87	84, 86	bitri 240	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- (<<{{e}}, {w}>> e. SIk Sk <-> e e. w)
88	81, 87	bitri 240	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- (<<{{{e}}}, {{w}}>> e. SIk SIk Sk <-> e e. w)
89	78, 88	bitri 240	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- (<<{{{{e}}}}, {{{w}}}>> e. SIk SIk SIk Sk <-> e e. w)
90	75, 89	bitri 240	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (<<{{{{{e}}}}}, {{{{w}}}}>> e. SIk SIk SIk SIk Sk <-> e e. w)
91	72, 90	bitri 240	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (<<{{{{{{e}}}}}}, {{{{{w}}}}}>> e. SIk SIk SIk SIk SIk Sk <-> e e. w)
92	69, 91	bitri 240	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (<<{{{{{{{{e}}}}}}}}, <<{{{{{w}}}}}, <<{{{{x}}}}, <<{a}, m>>>>>>>> e. Ins3k SIk SIk SIk SIk SIk Sk <-> e e. w)
93	68, 46, 35	otkelins2k 4255	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (<<{{{{{{{{e}}}}}}}}, <<{{{{{w}}}}}, <<{{{{x}}}}, <<{a}, m>>>>>>>> e. Ins2k ( Ins2k Ins3k SIk Sk u. Ins3k _I_kk ) <-> <<{{{{{{e}}}}}}, <<{{{{x}}}}, <<{a}, m>>>>>> e. ( Ins2k Ins3k SIk Sk u. Ins3k _I_kk ))
94	73, 29, 17	otkelins2k 4255	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- (<<{{{{{{e}}}}}}, <<{{{{x}}}}, <<{a}, m>>>>>> e. Ins2k Ins3k SIk Sk <-> <<{{{{e}}}}, <<{a}, m>>>> e. Ins3k SIk Sk )
95	79, 13, 1	otkelins3k 4256	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- (<<{{{{e}}}}, <<{a}, m>>>> e. Ins3k SIk Sk <-> <<{{e}}, {a}>> e. SIk Sk )
96		vex 2862	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- a e. _V
97	82, 96	opksnelsik 4265	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- (<<{{e}}, {a}>> e. SIk Sk <-> <<{e}, a>> e. Sk )
98	85, 96	elssetk 4270	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- (<<{e}, a>> e. Sk <-> e e. a)
99	97, 98	bitri 240	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- (<<{{e}}, {a}>> e. SIk Sk <-> e e. a)
100	95, 99	bitri 240	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- (<<{{{{e}}}}, <<{a}, m>>>> e. Ins3k SIk Sk <-> e e. a)
101	94, 100	bitri 240	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- (<<{{{{{{e}}}}}}, <<{{{{x}}}}, <<{a}, m>>>>>> e. Ins2k Ins3k SIk Sk <-> e e. a)
102	73, 29, 17	otkelins3k 4256	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- (<<{{{{{{e}}}}}}, <<{{{{x}}}}, <<{a}, m>>>>>> e. Ins3k _I_kk <-> <<{{{{e}}}}, {{{{x}}}}>> e. _I_kk )
103	76	sneqb 3876	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ({{{{e}}}} = {{{{x}}}} <-> {{{e}}} = {{{x}}})
104	79	sneqb 3876	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- ({{{e}}} = {{{x}}} <-> {{e}} = {{x}})
105	82	sneqb 3876	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- ({{e}} = {{x}} <-> {e} = {x})
106	85	sneqb 3876	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- ({e} = {x} <-> e = x)
107	105, 106	bitri 240	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- ({{e}} = {{x}} <-> e = x)
108	104, 107	bitri 240	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ({{{e}}} = {{{x}}} <-> e = x)
109	103, 108	bitri 240	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ({{{{e}}}} = {{{{x}}}} <-> e = x)
110		opkelidkg 4274	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- (({{{{e}}}} e. _V /\ {{{{x}}}} e. _V) -> (<<{{{{e}}}}, {{{{x}}}}>> e. _I_kk <-> {{{{e}}}} = {{{{x}}}}))
111	73, 29, 110	mp2an 653	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- (<<{{{{e}}}}, {{{{x}}}}>> e. _I_kk <-> {{{{e}}}} = {{{{x}}}})
112	85	elsnc 3756	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- (e e. {x} <-> e = x)
113	109, 111, 112	3bitr4i 268	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- (<<{{{{e}}}}, {{{{x}}}}>> e. _I_kk <-> e e. {x})
114	102, 113	bitri 240	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- (<<{{{{{{e}}}}}}, <<{{{{x}}}}, <<{a}, m>>>>>> e. Ins3k _I_kk <-> e e. {x})
115	101, 114	orbi12i 507	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ((<<{{{{{{e}}}}}}, <<{{{{x}}}}, <<{a}, m>>>>>> e. Ins2k Ins3k SIk Sk \/ <<{{{{{{e}}}}}}, <<{{{{x}}}}, <<{a}, m>>>>>> e. Ins3k _I_kk ) <-> (e e. a \/ e e. {x}))
116		elun 3220	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (<<{{{{{{e}}}}}}, <<{{{{x}}}}, <<{a}, m>>>>>> e. ( Ins2k Ins3k SIk Sk u. Ins3k _I_kk ) <-> (<<{{{{{{e}}}}}}, <<{{{{x}}}}, <<{a}, m>>>>>> e. Ins2k Ins3k SIk Sk \/ <<{{{{{{e}}}}}}, <<{{{{x}}}}, <<{a}, m>>>>>> e. Ins3k _I_kk ))
117		elun 3220	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (e e. (a u. {x}) <-> (e e. a \/ e e. {x}))
118	115, 116, 117	3bitr4i 268	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (<<{{{{{{e}}}}}}, <<{{{{x}}}}, <<{a}, m>>>>>> e. ( Ins2k Ins3k SIk Sk u. Ins3k _I_kk ) <-> e e. (a u. {x}))
119	93, 118	bitri 240	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (<<{{{{{{{{e}}}}}}}}, <<{{{{{w}}}}}, <<{{{{x}}}}, <<{a}, m>>>>>>>> e. Ins2k ( Ins2k Ins3k SIk Sk u. Ins3k _I_kk ) <-> e e. (a u. {x}))
120	92, 119	bibi12i 306	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ((<<{{{{{{{{e}}}}}}}}, <<{{{{{w}}}}}, <<{{{{x}}}}, <<{a}, m>>>>>>>> e. Ins3k SIk SIk SIk SIk SIk Sk <-> <<{{{{{{{{e}}}}}}}}, <<{{{{{w}}}}}, <<{{{{x}}}}, <<{a}, m>>>>>>>> e. Ins2k ( Ins2k Ins3k SIk Sk u. Ins3k _I_kk )) <-> (e e. w <-> e e. (a u. {x})))
121	120	notbii 287	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (-. (<<{{{{{{{{e}}}}}}}}, <<{{{{{w}}}}}, <<{{{{x}}}}, <<{a}, m>>>>>>>> e. Ins3k SIk SIk SIk SIk SIk Sk <-> <<{{{{{{{{e}}}}}}}}, <<{{{{{w}}}}}, <<{{{{x}}}}, <<{a}, m>>>>>>>> e. Ins2k ( Ins2k Ins3k SIk Sk u. Ins3k _I_kk )) <-> -. (e e. w <-> e e. (a u. {x})))
122	67, 121	bitri 240	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (<<{{{{{{{{e}}}}}}}}, <<{{{{{w}}}}}, <<{{{{x}}}}, <<{a}, m>>>>>>>> e. ( Ins3k SIk SIk SIk SIk SIk Sk (+) Ins2k ( Ins2k Ins3k SIk Sk u. Ins3k _I_kk )) <-> -. (e e. w <-> e e. (a u. {x})))
123	66, 122	bitri 240	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (E.t(t = {{{{{{{{e}}}}}}}} /\ <<t, <<{{{{{w}}}}}, <<{{{{x}}}}, <<{a}, m>>>>>>>> e. ( Ins3k SIk SIk SIk SIk SIk Sk (+) Ins2k ( Ins2k Ins3k SIk Sk u. Ins3k _I_kk ))) <-> -. (e e. w <-> e e. (a u. {x})))
124	123	exbii 1582	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (E.eE.t(t = {{{{{{{{e}}}}}}}} /\ <<t, <<{{{{{w}}}}}, <<{{{{x}}}}, <<{a}, m>>>>>>>> e. ( Ins3k SIk SIk SIk SIk SIk Sk (+) Ins2k ( Ins2k Ins3k SIk Sk u. Ins3k _I_kk ))) <-> E.e -. (e e. w <-> e e. (a u. {x})))
125	62, 124	bitri 240	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (<<{{{{{w}}}}}, <<{{{{x}}}}, <<{a}, m>>>>>> e. (( Ins3k SIk SIk SIk SIk SIk Sk (+) Ins2k ( Ins2k Ins3k SIk Sk u. Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c) <-> E.e -. (e e. w <-> e e. (a u. {x})))
126	125	notbii 287	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (-. <<{{{{{w}}}}}, <<{{{{x}}}}, <<{a}, m>>>>>> e. (( Ins3k SIk SIk SIk SIk SIk Sk (+) Ins2k ( Ins2k Ins3k SIk Sk u. Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c) <-> -. E.e -. (e e. w <-> e e. (a u. {x})))
127	51	elcompl 3225	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (<<{{{{{w}}}}}, <<{{{{x}}}}, <<{a}, m>>>>>> e. ∼ (( Ins3k SIk SIk SIk SIk SIk Sk (+) Ins2k ( Ins2k Ins3k SIk Sk u. Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c) <-> -. <<{{{{{w}}}}}, <<{{{{x}}}}, <<{a}, m>>>>>> e. (( Ins3k SIk SIk SIk SIk SIk Sk (+) Ins2k ( Ins2k Ins3k SIk Sk u. Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c))
128		dfcleq 2347	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (w = (a u. {x}) <-> A.e(e e. w <-> e e. (a u. {x})))
129		alex 1572	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (A.e(e e. w <-> e e. (a u. {x})) <-> -. E.e -. (e e. w <-> e e. (a u. {x})))
130	128, 129	bitri 240	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (w = (a u. {x}) <-> -. E.e -. (e e. w <-> e e. (a u. {x})))
131	126, 127, 130	3bitr4i 268	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (<<{{{{{w}}}}}, <<{{{{x}}}}, <<{a}, m>>>>>> e. ∼ (( Ins3k SIk SIk SIk SIk SIk Sk (+) Ins2k ( Ins2k Ins3k SIk Sk u. Ins3k _I_kk ))"k~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c) <-> w = (a u. {x}))
132	74, 29, 17	otkelins2k 4255	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (<<{{{{{w}}}}}, <<{{{{x}}}}, <<{a}, m>>>>>> e. Ins2k Ins2k (`'kImagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 1c) o.k Sk ) <-> <<{{{w}}}, <<{a}, m>>>> e. Ins2k (`'kImagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 1c) o.k Sk ))
133	80, 13, 1	otkelins2k 4255	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (<<{{{w}}}, <<{a}, m>>>> e. Ins2k (`'kImagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 1c) o.k Sk ) <-> <<{w}, m>> e. (`'kImagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 1c) o.k Sk ))
134		ancom 437	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((<<{w}, t>> e. Sk /\ <<t, m>> e. `'kImagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 1c)) <-> (<<t, m>> e. `'kImagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 1c) /\ <<{w}, t>> e. Sk ))
135		vex 2862	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- t e. _V
136	135, 1	opkelcnvk 4250	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (<<t, m>> e. `'kImagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 1c) <-> <<m, t>> e. Imagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 1c))
137		opkelimagekg 4271	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ((m e. _V /\ t e. _V) -> (<<m, t>> e. Imagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 1c) <-> t = ((( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 1c)"km)))
138	1, 135, 137	mp2an 653	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (<<m, t>> e. Imagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 1c) <-> t = ((( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 1c)"km))
139		dfaddc2 4381	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (m +o 1c) = ((( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 1c)"km)
140	139	eqeq2i 2363	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (t = (m +o 1c) <-> t = ((( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 1c)"km))
141	140	bicomi 193	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (t = ((( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 1c)"km) <-> t = (m +o 1c))
142	138, 141	bitri 240	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (<<m, t>> e. Imagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 1c) <-> t = (m +o 1c))
143	136, 142	bitri 240	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (<<t, m>> e. `'kImagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \