Theorem nnsucelrlem1 4425

Description: Lemma for nnsucelr 4429. 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 2863	. . . . . . . 8 |- m e. _V
2	1	elimak 4260	. . . . . . 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 2621	. . . . . . . 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 4140	. . . . . . . . . . . 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 4112	. . . . . . . . 9 |- {a} e. _V
14		opkeq1 4060	. . . . . . . . . 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 2895	. . . . . . . 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 4114	. . . . . . . . . . . 12 |- <<{a}, m>> e. _V
18	17	elimak 4260	. . . . . . . . . . 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 2621	. . . . . . . . . . . 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 4150	. . . . . . . . . . . . . . . 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 4112	. . . . . . . . . . . . 13 |- {{{{x}}}} e. _V
30		opkeq1 4060	. . . . . . . . . . . . . 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 2895	. . . . . . . . . . . 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 3222	. . . . . . . . . . . . . 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 3222	. . . . . . . . . . . . . . . . 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 4114	. . . . . . . . . . . . . . . . . . . . 21 |- <<{{{{x}}}}, <<{a}, m>>>> e. _V
36	35	elimak 4260	. . . . . . . . . . . . . . . . . . . 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 2621	. . . . . . . . . . . . . . . . . . . . . 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 4151	. . . . . . . . . . . . . . . . . . . . . . . . . 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 4112	. . . . . . . . . . . . . . . . . . . . . . . 24 |- {{{{{w}}}}} e. _V
47		opkeq1 4060	. . . . . . . . . . . . . . . . . . . . . . . . 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 2895	. . . . . . . . . . . . . . . . . . . . . . 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 3220	. . . . . . . . . . . . . . . . . . . . . . . 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 4114	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- <<{{{{{w}}}}}, <<{{{{x}}}}, <<{a}, m>>>>>> e. _V
52	51	elimak 4260	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2621	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4154	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4112	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- {{{{{{{{e}}}}}}}} e. _V
64		opkeq1 4060	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2895	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3224	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4112	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- {{{{{{e}}}}}} e. _V
69	68, 46, 35	otkelins3k 4257	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4112	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- {{{{{e}}}}} e. _V
71		snex 4112	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- {{{{w}}}} e. _V
72	70, 71	opksnelsik 4266	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (<<{{{{{{e}}}}}}, {{{{{w}}}}}>> e. SIk SIk SIk SIk SIk Sk <-> <<{{{{{e}}}}}, {{{{w}}}}>> e. SIk SIk SIk SIk Sk )
73		snex 4112	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- {{{{e}}}} e. _V
74		snex 4112	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- {{{w}}} e. _V
75	73, 74	opksnelsik 4266	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- (<<{{{{{e}}}}}, {{{{w}}}}>> e. SIk SIk SIk SIk Sk <-> <<{{{{e}}}}, {{{w}}}>> e. SIk SIk SIk Sk )
76		snex 4112	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- {{{e}}} e. _V
77		snex 4112	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- {{w}} e. _V
78	76, 77	opksnelsik 4266	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- (<<{{{{e}}}}, {{{w}}}>> e. SIk SIk SIk Sk <-> <<{{{e}}}, {{w}}>> e. SIk SIk Sk )
79		snex 4112	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- {{e}} e. _V
80		snex 4112	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- {w} e. _V
81	79, 80	opksnelsik 4266	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- (<<{{{e}}}, {{w}}>> e. SIk SIk Sk <-> <<{{e}}, {w}>> e. SIk Sk )
82		snex 4112	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- {e} e. _V
83		vex 2863	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- w e. _V
84	82, 83	opksnelsik 4266	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- (<<{{e}}, {w}>> e. SIk Sk <-> <<{e}, w>> e. Sk )
85		vex 2863	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- e e. _V
86	85, 83	elssetk 4271	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4256	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4256	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- (<<{{{{{{e}}}}}}, <<{{{{x}}}}, <<{a}, m>>>>>> e. Ins2k Ins3k SIk Sk <-> <<{{{{e}}}}, <<{a}, m>>>> e. Ins3k SIk Sk )
95	79, 13, 1	otkelins3k 4257	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- (<<{{{{e}}}}, <<{a}, m>>>> e. Ins3k SIk Sk <-> <<{{e}}, {a}>> e. SIk Sk )
96		vex 2863	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- a e. _V
97	82, 96	opksnelsik 4266	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- (<<{{e}}, {a}>> e. SIk Sk <-> <<{e}, a>> e. Sk )
98	85, 96	elssetk 4271	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4257	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- (<<{{{{{{e}}}}}}, <<{{{{x}}}}, <<{a}, m>>>>>> e. Ins3k _I_kk <-> <<{{{{e}}}}, {{{{x}}}}>> e. _I_kk )
103	76	sneqb 3877	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ({{{{e}}}} = {{{{x}}}} <-> {{{e}}} = {{{x}}})
104	79	sneqb 3877	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- ({{{e}}} = {{{x}}} <-> {{e}} = {{x}})
105	82	sneqb 3877	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- ({{e}} = {{x}} <-> {e} = {x})
106	85	sneqb 3877	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4275	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3757	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3221	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3221	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3226	. . . . . . . . . . . . . . . . . . . . . . . . . 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 4256	. . . . . . . . . . . . . . . . . . . . . . . . . 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 4256	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 2863	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- t e. _V
136	135, 1	opkelcnvk 4251	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4272	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4382	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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) \ (( 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))
144	83, 135	elssetk 4271	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (<<{w}, t>> e. Sk <-> w e. t)
145	143, 144	anbi12i 678	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((<<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 ) <-> (t = (m +o 1c) /\ w e. t))
146	134, 145	bitri 240	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((<<{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 +o 1c) /\ w e. t))
147	146	exbii 1582	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (E.t(<<{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)) <-> E.t(t = (m +o 1c) /\ w e. t))
148	80, 1	opkelcok 4263	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (<<{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 ) <-> E.t(<<{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)))
149		1cex 4143	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- 1c e. _V
150	1, 149	addcex 4395	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (m +o 1c) e. _V
151	150	clel3 2978	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (w e. (m +o 1c) <-> E.t(t = (m +o 1c) /\ w e. t))
152	147, 148, 151	3bitr4i 268	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (<<{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 ) <-> w e. (m +o 1c))
153	133, 152	bitri 240	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (<<{{{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 e. (m +o 1c))
154	132, 153	bitri 240	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (<<{{{{{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 e. (m +o 1c))
155	131, 154	anbi12i 678	. . . . . . . . . . . . . . . . . . . . . . . 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) /\ <<{{{{{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 u. {x}) /\ w e. (m +o 1c)))
156	50, 155	bitri 240	. . . . . . . . . . . . . . . . . . . . . . 23 |- (<<{{{{{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 = (a u. {x}) /\ w e. (m +o 1c)))
157	49, 156	bitri 240	. . . . . . . . . . . . . . . . . . . . . 22 |- (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 = (a u. {x}) /\ w e. (m +o 1c)))
158	157	exbii 1582	. . . . . . . . . . . . . . . . . . . . 21 |- (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.w(w = (a u. {x}) /\ w e. (m +o 1c)))
159	45, 158	bitri 240	. . . . . . . . . . . . . . . . . . . 20 |- (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.w(w = (a u. {x}) /\ w e. (m +o 1c)))
160	36, 159	bitri 240	. . . . . . . . . . . . . . . . . . 19 |- (<<{{{{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.w(w = (a u. {x}) /\ w e. (m +o 1c)))
161		df-clel 2349	. . . . . . . . . . . . . . . . . . 19 |- ((a u. {x}) e. (m +o 1c) <-> E.w(w = (a u. {x}) /\ w e. (m +o 1c)))
162	160, 161	bitr4i 243	. . . . . . . . . . . . . . . . . 18 |- (<<{{{{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) <-> (a u. {x}) e. (m +o 1c))
163		snex 4112	. . . . . . . . . . . . . . . . . . . . 21 |- {{x}} e. _V
164	163, 13, 1	otkelins3k 4257	. . . . . . . . . . . . . . . . . . . 20 |- (<<{{{{x}}}}, <<{a}, m>>>> e. Ins3k SIk Sk <-> <<{{x}}, {a}>> e. SIk Sk )
165		snex 4112	. . . . . . . . . . . . . . . . . . . . . 22 |- {x} e. _V
166	165, 96	opksnelsik 4266	. . . . . . . . . . . . . . . . . . . . 21 |- (<<{{x}}, {a}>> e. SIk Sk <-> <<{x}, a>> e. Sk )
167		vex 2863	. . . . . . . . . . . . . . . . . . . . . 22 |- x e. _V
168	167, 96	elssetk 4271	. . . . . . . . . . . . . . . . . . . . 21 |- (<<{x}, a>> e. Sk <-> x e. a)
169	166, 168	bitri 240	. . . . . . . . . . . . . . . . . . . 20 |- (<<{{x}}, {a}>> e. SIk Sk <-> x e. a)
170	164, 169	bitri 240	. . . . . . . . . . . . . . . . . . 19 |- (<<{{{{x}}}}, <<{a}, m>>>> e. Ins3k SIk Sk <-> x e. a)
171	170	notbii 287	. . . . . . . . . . . . . . . . . 18 |- (-. <<{{{{x}}}}, <<{a}, m>>>> e. Ins3k SIk Sk <-> -. x e. a)
172	162, 171	anbi12i 678	. . . . . . . . . . . . . . . . 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) /\ -. <<{{{{x}}}}, <<{a}, m>>>> e. Ins3k SIk Sk ) <-> ((a u. {x}) e. (m +o 1c) /\ -. x e. a))
173	34, 172	bitri 240	. . . . . . . . . . . . . . . 16 |- (<<{{{{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 ) <-> ((a u. {x}) e. (m +o 1c) /\ -. x e. a))
174		ancom 437	. . . . . . . . . . . . . . . 16 |- (((a u. {x}) e. (m +o 1c) /\ -. x e. a) <-> (-. x e. a /\ (a u. {x}) e. (m +o 1c)))
175	173, 174	bitri 240	. . . . . . . . . . . . . . 15 |- (<<{{{{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 e. a /\ (a u. {x}) e. (m +o 1c)))
176	29, 17	opkelxpk 4249	. . . . . . . . . . . . . . . . . 18 |- (<<{{{{x}}}}, <<{a}, m>>>> e. (_V X.k Sk ) <-> ({{{{x}}}} e. _V /\ <<{a}, m>> e. Sk ))
177	29, 176	mpbiran 884	. . . . . . . . . . . . . . . . 17 |- (<<{{{{x}}}}, <<{a}, m>>>> e. (_V X.k Sk ) <-> <<{a}, m>> e. Sk )
178	96, 1	elssetk 4271	. . . . . . . . . . . . . . . . 17 |- (<<{a}, m>> e. Sk <-> a e. m)
179	177, 178	bitri 240	. . . . . . . . . . . . . . . 16 |- (<<{{{{x}}}}, <<{a}, m>>>> e. (_V X.k Sk ) <-> a e. m)
180	179	notbii 287	. . . . . . . . . . . . . . 15 |- (-. <<{{{{x}}}}, <<{a}, m>>>> e. (_V X.k Sk ) <-> -. a e. m)
181	175, 180	anbi12i 678	. . . . . . . . . . . . . 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 ) /\ -. <<{{{{x}}}}, <<{a}, m>>>> e. (_V X.k Sk )) <-> ((-. x e. a /\ (a u. {x}) e. (m +o 1c)) /\ -. a e. m))
182	33, 181	bitri 240	. . . . . . . . . . . . 13 |- (<<{{{{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 e. a /\ (a u. {x}) e. (m +o 1c)) /\ -. a e. m))
183		annim 414	. . . . . . . . . . . . 13 |- (((-. x e. a /\ (a u. {x}) e. (m +o 1c)) /\ -. a e. m) <-> -. ((-. x e. a /\ (a u. {x}) e. (m +o 1c)) -> a e. m))
184	182, 183	bitri 240	. . . . . . . . . . . 12 |- (<<{{{{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 e. a /\ (a u. {x}) e. (m +o 1c)) -> a e. m))
185	32, 184	bitri 240	. . . . . . . . . . 11 |- (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 e. a /\ (a u. {x}) e. (m +o 1c)) -> a e. m))
186	185	exbii 1582	. . . . . . . . . 10 |- (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.x -. ((-. x e. a /\ (a u. {x}) e. (m +o 1c)) -> a e. m))
187	28, 186	bitri 240	. . . . . . . . 9 |- (<<{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.x -. ((-. x e. a /\ (a u. {x}) e. (m +o 1c)) -> a e. m))
188		exnal 1574	. . . . . . . . 9 |- (E.x -. ((-. x e. a /\ (a u. {x}) e. (m +o 1c)) -> a e. m) <-> -. A.x((-. x e. a /\ (a u. {x}) e. (m +o 1c)) -> a e. m))
189	187, 188	bitri 240	. . . . . . . 8 |- (<<{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) <-> -. A.x((-. x e. a /\ (a u. {x}) e. (m +o 1c)) -> a e. m))
190	16, 189	bitri 240	. . . . . . 7 |- (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.x((-. x e. a /\ (a u. {x}) e. (m +o 1c)) -> a e. m))
191	190	exbii 1582	. . . . . 6 |- (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.a -. A.x((-. x e. a /\ (a u. {x}) e. (m +o 1c)) -> a e. m))
192	12, 191	bitri 240	. . . . 5 |- (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.a -. A.x((-. x e. a /\ (a u. {x}) e. (m +o 1c)) -> a e. m))
193	192	notbii 287	. . . 4 |- (-. 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.a -. A.x((-. x e. a /\ (a u. {x}) e. (m +o 1c)) -> a e. m))
194	1	elcompl 3226	. . . 4 |- (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) <-> -. 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))
195		alex 1572	. . . 4 |- (A.aA.x((-. x e. a /\ (a u. {x}) e. (m +o 1c)) -> a e. m) <-> -. E.a -. A.x((-. x e. a /\ (a u. {x}) e. (m +o 1c)) -> a e. m))
196	193, 194, 195	3bitr4i 268	. . 3 |- (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) <-> A.aA.x((-. x e. a /\ (a u. {x}) e. (m +o 1c)) -> a e. m))
197	196	eqabi 2465	. 2 |- ∼ (((((( ∼ (( 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) = {m | A.aA.x((-. x e. a /\ (a u. {x}) e. (m +o 1c)) -> a e. m)}
198		ssetkex 4295	. . . . . . . . . . . . . . . . . 18 |- Sk e. _V
199	198	sikex 4298	. . . . . . . . . . . . . . . . 17 |- SIk Sk e. _V
200	199	sikex 4298	. . . . . . . . . . . . . . . 16 |- SIk SIk Sk e. _V
201	200	sikex 4298	. . . . . . . . . . . . . . 15 |- SIk SIk SIk Sk e. _V
202	201	sikex 4298	. . . . . . . . . . . . . 14 |- SIk SIk SIk SIk Sk e. _V
203	202	sikex 4298	. . . . . . . . . . . . 13 |- SIk SIk SIk SIk SIk Sk e. _V
204	203	ins3kex 4309	. . . . . . . . . . . 12 |- Ins3k SIk SIk SIk SIk SIk Sk e. _V
205	199	ins3kex 4309	. . . . . . . . . . . . . . 15 |- Ins3k SIk Sk e. _V
206	205	ins2kex 4308	. . . . . . . . . . . . . 14 |- Ins2k Ins3k SIk Sk e. _V
207		idkex 4315	. . . . . . . . . . . . . . 15 |- _I_kk e. _V
208	207	ins3kex 4309	. . . . . . . . . . . . . 14 |- Ins3k _I_kk e. _V
209	206, 208	unex 4107	. . . . . . . . . . . . 13 |- ( Ins2k Ins3k SIk Sk u. Ins3k _I_kk ) e. _V
210	209	ins2kex 4308	. . . . . . . . . . . 12 |- Ins2k ( Ins2k Ins3k SIk Sk u. Ins3k _I_kk ) e. _V
211	204, 210	symdifex 4109	. . . . . . . . . . 11 |- ( Ins3k SIk SIk SIk SIk SIk Sk (+) Ins2k ( Ins2k Ins3k SIk Sk u. Ins3k _I_kk )) e. _V
212	149	pw1ex 4304	. . . . . . . . . . . . . . . . 17 |- ~P1 1c e. _V
213	212	pw1ex 4304	. . . . . . . . . . . . . . . 16 |- ~P1 ~P1 1c e. _V
214	213	pw1ex 4304	. . . . . . . . . . . . . . 15 |- ~P1 ~P1 ~P1 1c e. _V
215	214	pw1ex 4304	. . . . . . . . . . . . . 14 |- ~P1 ~P1 ~P1 ~P1 1c e. _V
216	215	pw1ex 4304	. . . . . . . . . . . . 13 |- ~P1 ~P1 ~P1 ~P1 ~P1 1c e. _V
217	216	pw1ex 4304	. . . . . . . . . . . 12 |- ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c e. _V
218	217	pw1ex 4304	. . . . . . . . . . 11 |- ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c e. _V
219	211, 218	imakex 4301	. . . . . . . . . 10 |- (( 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. _V
220	219	complex 4105	. . . . . . . . 9 |- ∼ (( 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. _V
221		addcexlem 4383	. . . . . . . . . . . . . . 15 |- ( 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)) e. _V
222	221, 213	imakex 4301	. . . . . . . . . . . . . 14 |- (( 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) e. _V
223	222	imagekex 4313	. . . . . . . . . . . . 13 |- 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) e. _V
224	223	cnvkex 4288	. . . . . . . . . . . 12 |- `'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) e. _V
225	224, 198	cokex 4311	. . . . . . . . . . 11 |- (`'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. _V
226	225	ins2kex 4308	. . . . . . . . . 10 |- 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. _V
227	226	ins2kex 4308	. . . . . . . . 9 |- 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. _V
228	220, 227	inex 4106	. . . . . . . 8 |- ( ∼ (( 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. _V
229	228, 215	imakex 4301	. . . . . . 7 |- (( ∼ (( 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. _V
230	229, 205	difex 4108	. . . . . 6 |- ((( ∼ (( 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 ) e. _V
231		vvex 4110	. . . . . . 7 |- _V e. _V
232	231, 198	xpkex 4290	. . . . . 6 |- (_V X.k Sk ) e. _V
233	230, 232	difex 4108	. . . . 5 |- (((( ∼ (( 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. _V
234	233, 214	imakex 4301	. . . 4 |- ((((( ∼ (( 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. _V
235	234, 149	imakex 4301	. . 3 |- (((((( ∼ (( 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. _V
236	235	complex 4105	. 2 |- ∼ (((((( ∼ (( 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. _V
237	197, 236	eqeltrri 2424	1 |- {m | A.aA.x((-. x e. a /\ (a u. {x}) e. (m +o 1c)) -> a e. m)} e. _V

Syntax hints:  -. wn 3   -> wi 4   <-> wb 176   \/ wo 357   /\ wa 358  A.wal 1540  E.wex 1541   = wceq 1642   e. wcel 1710  {cab 2339  E.wrex 2616  _Vcvv 2860   ∼ ccompl 3206   \ cdif 3207   u. cun 3208   i^i cin 3209   (+) csymdif 3210  {csn 3738  <<copk 4058  1_cc1c 4135  ~P₁ cpw1 4136   X._k cxpk 4175  `'_kccnvk 4176   Ins2_k cins2k 4177   Ins3_k cins3k 4178  "_kcimak 4180   o._k ccomk 4181   SI_k csik 4182  Image_kcimagek 4183   S_k cssetk 4184   _I_k_k cidk 4185   +o cplc 4376

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

This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-nan 1288  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2340  df-cleq 2346  df-clel 2349  df-nfc 2479  df-ne 2519  df-ral 2620  df-rex 2621  df-v 2862  df-nin 3212  df-compl 3213  df-in 3214  df-un 3215  df-dif 3216  df-symdif 3217  df-ss 3260  df-nul 3552  df-pw 3725  df-sn 3742  df-pr 3743  df-opk 4059  df-1c 4137  df-pw1 4138  df-xpk 4186  df-cnvk 4187  df-ins2k 4188  df-ins3k 4189  df-imak 4190  df-cok 4191  df-p6 4192  df-sik 4193  df-ssetk 4194  df-imagek 4195  df-idk 4196  df-addc 4379

This theorem is referenced by:  nnsucelr  4429