Theorem ncfinraiselem2 4481

Description: Lemma for ncfinraise 4482. Show stratification for induction. (Contributed by SF, 22-Jan-2015.)

Assertion

Ref	Expression
ncfinraiselem2	|- {m | A.a e. m A.b e. m E.n e. Nn (~P1 a e. n /\ ~P1 b e. n)} e. _V

Distinct variable groups:   a,b,m   n,a   m,b   n,b

Proof of Theorem ncfinraiselem2

Dummy variables t x are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		snex 4112	. . . . . 6 |- {m} e. _V
2	1	elcompl 3226	. . . . 5 |- ({m} e. ∼ (( SIk Sk i^i (( Ins2k SIk Sk \ Ins3k (((~P1 ~P1 Nn X.k _V) i^i ( Ins2k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c) i^i Ins3k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c)))"k~P1 1c))"k~P1 ~P1 ~P1 1c))"k~P1 1c) <-> -. {m} e. (( SIk Sk i^i (( Ins2k SIk Sk \ Ins3k (((~P1 ~P1 Nn X.k _V) i^i ( Ins2k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c) i^i Ins3k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c)))"k~P1 1c))"k~P1 ~P1 ~P1 1c))"k~P1 1c))
3	1	elimak 4260	. . . . . 6 |- ({m} e. (( SIk Sk i^i (( Ins2k SIk Sk \ Ins3k (((~P1 ~P1 Nn X.k _V) i^i ( Ins2k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c) i^i Ins3k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c)))"k~P1 1c))"k~P1 ~P1 ~P1 1c))"k~P1 1c) <-> E.t e. ~P1 1c<<t, {m}>> e. ( SIk Sk i^i (( Ins2k SIk Sk \ Ins3k (((~P1 ~P1 Nn X.k _V) i^i ( Ins2k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c) i^i Ins3k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c)))"k~P1 1c))"k~P1 ~P1 ~P1 1c)))
4		elpw11c 4148	. . . . . . . . . 10 |- (t e. ~P1 1c <-> E.a t = {{a}})
5	4	anbi1i 676	. . . . . . . . 9 |- ((t e. ~P1 1c /\ <<t, {m}>> e. ( SIk Sk i^i (( Ins2k SIk Sk \ Ins3k (((~P1 ~P1 Nn X.k _V) i^i ( Ins2k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c) i^i Ins3k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c)))"k~P1 1c))"k~P1 ~P1 ~P1 1c))) <-> (E.a t = {{a}} /\ <<t, {m}>> e. ( SIk Sk i^i (( Ins2k SIk Sk \ Ins3k (((~P1 ~P1 Nn X.k _V) i^i ( Ins2k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c) i^i Ins3k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c)))"k~P1 1c))"k~P1 ~P1 ~P1 1c))))
6		19.41v 1901	. . . . . . . . 9 |- (E.a(t = {{a}} /\ <<t, {m}>> e. ( SIk Sk i^i (( Ins2k SIk Sk \ Ins3k (((~P1 ~P1 Nn X.k _V) i^i ( Ins2k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c) i^i Ins3k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c)))"k~P1 1c))"k~P1 ~P1 ~P1 1c))) <-> (E.a t = {{a}} /\ <<t, {m}>> e. ( SIk Sk i^i (( Ins2k SIk Sk \ Ins3k (((~P1 ~P1 Nn X.k _V) i^i ( Ins2k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c) i^i Ins3k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c)))"k~P1 1c))"k~P1 ~P1 ~P1 1c))))
7	5, 6	bitr4i 243	. . . . . . . 8 |- ((t e. ~P1 1c /\ <<t, {m}>> e. ( SIk Sk i^i (( Ins2k SIk Sk \ Ins3k (((~P1 ~P1 Nn X.k _V) i^i ( Ins2k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c) i^i Ins3k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c)))"k~P1 1c))"k~P1 ~P1 ~P1 1c))) <-> E.a(t = {{a}} /\ <<t, {m}>> e. ( SIk Sk i^i (( Ins2k SIk Sk \ Ins3k (((~P1 ~P1 Nn X.k _V) i^i ( Ins2k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c) i^i Ins3k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c)))"k~P1 1c))"k~P1 ~P1 ~P1 1c))))
8	7	exbii 1582	. . . . . . 7 |- (E.t(t e. ~P1 1c /\ <<t, {m}>> e. ( SIk Sk i^i (( Ins2k SIk Sk \ Ins3k (((~P1 ~P1 Nn X.k _V) i^i ( Ins2k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c) i^i Ins3k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c)))"k~P1 1c))"k~P1 ~P1 ~P1 1c))) <-> E.tE.a(t = {{a}} /\ <<t, {m}>> e. ( SIk Sk i^i (( Ins2k SIk Sk \ Ins3k (((~P1 ~P1 Nn X.k _V) i^i ( Ins2k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c) i^i Ins3k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c)))"k~P1 1c))"k~P1 ~P1 ~P1 1c))))
9		df-rex 2621	. . . . . . 7 |- (E.t e. ~P1 1c<<t, {m}>> e. ( SIk Sk i^i (( Ins2k SIk Sk \ Ins3k (((~P1 ~P1 Nn X.k _V) i^i ( Ins2k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c) i^i Ins3k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c)))"k~P1 1c))"k~P1 ~P1 ~P1 1c)) <-> E.t(t e. ~P1 1c /\ <<t, {m}>> e. ( SIk Sk i^i (( Ins2k SIk Sk \ Ins3k (((~P1 ~P1 Nn X.k _V) i^i ( Ins2k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c) i^i Ins3k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c)))"k~P1 1c))"k~P1 ~P1 ~P1 1c))))
10		excom 1741	. . . . . . 7 |- (E.aE.t(t = {{a}} /\ <<t, {m}>> e. ( SIk Sk i^i (( Ins2k SIk Sk \ Ins3k (((~P1 ~P1 Nn X.k _V) i^i ( Ins2k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c) i^i Ins3k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c)))"k~P1 1c))"k~P1 ~P1 ~P1 1c))) <-> E.tE.a(t = {{a}} /\ <<t, {m}>> e. ( SIk Sk i^i (( Ins2k SIk Sk \ Ins3k (((~P1 ~P1 Nn X.k _V) i^i ( Ins2k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c) i^i Ins3k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c)))"k~P1 1c))"k~P1 ~P1 ~P1 1c))))
11	8, 9, 10	3bitr4i 268	. . . . . 6 |- (E.t e. ~P1 1c<<t, {m}>> e. ( SIk Sk i^i (( Ins2k SIk Sk \ Ins3k (((~P1 ~P1 Nn X.k _V) i^i ( Ins2k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c) i^i Ins3k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c)))"k~P1 1c))"k~P1 ~P1 ~P1 1c)) <-> E.aE.t(t = {{a}} /\ <<t, {m}>> e. ( SIk Sk i^i (( Ins2k SIk Sk \ Ins3k (((~P1 ~P1 Nn X.k _V) i^i ( Ins2k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c) i^i Ins3k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c)))"k~P1 1c))"k~P1 ~P1 ~P1 1c))))
12		snex 4112	. . . . . . . . . 10 |- {{a}} e. _V
13		opkeq1 4060	. . . . . . . . . . 11 |- (t = {{a}} -> <<t, {m}>> = <<{{a}}, {m}>>)
14	13	eleq1d 2419	. . . . . . . . . 10 |- (t = {{a}} -> (<<t, {m}>> e. ( SIk Sk i^i (( Ins2k SIk Sk \ Ins3k (((~P1 ~P1 Nn X.k _V) i^i ( Ins2k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c) i^i Ins3k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c)))"k~P1 1c))"k~P1 ~P1 ~P1 1c)) <-> <<{{a}}, {m}>> e. ( SIk Sk i^i (( Ins2k SIk Sk \ Ins3k (((~P1 ~P1 Nn X.k _V) i^i ( Ins2k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c) i^i Ins3k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c)))"k~P1 1c))"k~P1 ~P1 ~P1 1c))))
15	12, 14	ceqsexv 2895	. . . . . . . . 9 |- (E.t(t = {{a}} /\ <<t, {m}>> e. ( SIk Sk i^i (( Ins2k SIk Sk \ Ins3k (((~P1 ~P1 Nn X.k _V) i^i ( Ins2k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c) i^i Ins3k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c)))"k~P1 1c))"k~P1 ~P1 ~P1 1c))) <-> <<{{a}}, {m}>> e. ( SIk Sk i^i (( Ins2k SIk Sk \ Ins3k (((~P1 ~P1 Nn X.k _V) i^i ( Ins2k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c) i^i Ins3k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c)))"k~P1 1c))"k~P1 ~P1 ~P1 1c)))
16		elin 3220	. . . . . . . . 9 |- (<<{{a}}, {m}>> e. ( SIk Sk i^i (( Ins2k SIk Sk \ Ins3k (((~P1 ~P1 Nn X.k _V) i^i ( Ins2k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c) i^i Ins3k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c)))"k~P1 1c))"k~P1 ~P1 ~P1 1c)) <-> (<<{{a}}, {m}>> e. SIk Sk /\ <<{{a}}, {m}>> e. (( Ins2k SIk Sk \ Ins3k (((~P1 ~P1 Nn X.k _V) i^i ( Ins2k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c) i^i Ins3k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c)))"k~P1 1c))"k~P1 ~P1 ~P1 1c)))
17		snex 4112	. . . . . . . . . . . 12 |- {a} e. _V
18		vex 2863	. . . . . . . . . . . 12 |- m e. _V
19	17, 18	opksnelsik 4266	. . . . . . . . . . 11 |- (<<{{a}}, {m}>> e. SIk Sk <-> <<{a}, m>> e. Sk )
20		vex 2863	. . . . . . . . . . . 12 |- a e. _V
21	20, 18	elssetk 4271	. . . . . . . . . . 11 |- (<<{a}, m>> e. Sk <-> a e. m)
22	19, 21	bitri 240	. . . . . . . . . 10 |- (<<{{a}}, {m}>> e. SIk Sk <-> a e. m)
23		opkex 4114	. . . . . . . . . . . . 13 |- <<{{a}}, {m}>> e. _V
24	23	elimak 4260	. . . . . . . . . . . 12 |- (<<{{a}}, {m}>> e. (( Ins2k SIk Sk \ Ins3k (((~P1 ~P1 Nn X.k _V) i^i ( Ins2k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c) i^i Ins3k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c)))"k~P1 1c))"k~P1 ~P1 ~P1 1c) <-> E.t e. ~P1 ~P1 ~P1 1c<<t, <<{{a}}, {m}>>>> e. ( Ins2k SIk Sk \ Ins3k (((~P1 ~P1 Nn X.k _V) i^i ( Ins2k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c) i^i Ins3k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c)))"k~P1 1c)))
25		df-rex 2621	. . . . . . . . . . . 12 |- (E.t e. ~P1 ~P1 ~P1 1c<<t, <<{{a}}, {m}>>>> e. ( Ins2k SIk Sk \ Ins3k (((~P1 ~P1 Nn X.k _V) i^i ( Ins2k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c) i^i Ins3k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c)))"k~P1 1c)) <-> E.t(t e. ~P1 ~P1 ~P1 1c /\ <<t, <<{{a}}, {m}>>>> e. ( Ins2k SIk Sk \ Ins3k (((~P1 ~P1 Nn X.k _V) i^i ( Ins2k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c) i^i Ins3k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c)))"k~P1 1c))))
26		elpw131c 4150	. . . . . . . . . . . . . . . 16 |- (t e. ~P1 ~P1 ~P1 1c <-> E.b t = {{{{b}}}})
27	26	anbi1i 676	. . . . . . . . . . . . . . 15 |- ((t e. ~P1 ~P1 ~P1 1c /\ <<t, <<{{a}}, {m}>>>> e. ( Ins2k SIk Sk \ Ins3k (((~P1 ~P1 Nn X.k _V) i^i ( Ins2k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c) i^i Ins3k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c)))"k~P1 1c))) <-> (E.b t = {{{{b}}}} /\ <<t, <<{{a}}, {m}>>>> e. ( Ins2k SIk Sk \ Ins3k (((~P1 ~P1 Nn X.k _V) i^i ( Ins2k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c) i^i Ins3k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c)))"k~P1 1c))))
28		19.41v 1901	. . . . . . . . . . . . . . 15 |- (E.b(t = {{{{b}}}} /\ <<t, <<{{a}}, {m}>>>> e. ( Ins2k SIk Sk \ Ins3k (((~P1 ~P1 Nn X.k _V) i^i ( Ins2k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c) i^i Ins3k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c)))"k~P1 1c))) <-> (E.b t = {{{{b}}}} /\ <<t, <<{{a}}, {m}>>>> e. ( Ins2k SIk Sk \ Ins3k (((~P1 ~P1 Nn X.k _V) i^i ( Ins2k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c) i^i Ins3k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c)))"k~P1 1c))))
29	27, 28	bitr4i 243	. . . . . . . . . . . . . 14 |- ((t e. ~P1 ~P1 ~P1 1c /\ <<t, <<{{a}}, {m}>>>> e. ( Ins2k SIk Sk \ Ins3k (((~P1 ~P1 Nn X.k _V) i^i ( Ins2k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c) i^i Ins3k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c)))"k~P1 1c))) <-> E.b(t = {{{{b}}}} /\ <<t, <<{{a}}, {m}>>>> e. ( Ins2k SIk Sk \ Ins3k (((~P1 ~P1 Nn X.k _V) i^i ( Ins2k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c) i^i Ins3k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c)))"k~P1 1c))))
30	29	exbii 1582	. . . . . . . . . . . . 13 |- (E.t(t e. ~P1 ~P1 ~P1 1c /\ <<t, <<{{a}}, {m}>>>> e. ( Ins2k SIk Sk \ Ins3k (((~P1 ~P1 Nn X.k _V) i^i ( Ins2k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c) i^i Ins3k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c)))"k~P1 1c))) <-> E.tE.b(t = {{{{b}}}} /\ <<t, <<{{a}}, {m}>>>> e. ( Ins2k SIk Sk \ Ins3k (((~P1 ~P1 Nn X.k _V) i^i ( Ins2k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c) i^i Ins3k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c)))"k~P1 1c))))
31		excom 1741	. . . . . . . . . . . . 13 |- (E.bE.t(t = {{{{b}}}} /\ <<t, <<{{a}}, {m}>>>> e. ( Ins2k SIk Sk \ Ins3k (((~P1 ~P1 Nn X.k _V) i^i ( Ins2k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c) i^i Ins3k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c)))"k~P1 1c))) <-> E.tE.b(t = {{{{b}}}} /\ <<t, <<{{a}}, {m}>>>> e. ( Ins2k SIk Sk \ Ins3k (((~P1 ~P1 Nn X.k _V) i^i ( Ins2k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c) i^i Ins3k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c)))"k~P1 1c))))
32	30, 31	bitr4i 243	. . . . . . . . . . . 12 |- (E.t(t e. ~P1 ~P1 ~P1 1c /\ <<t, <<{{a}}, {m}>>>> e. ( Ins2k SIk Sk \ Ins3k (((~P1 ~P1 Nn X.k _V) i^i ( Ins2k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c) i^i Ins3k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c)))"k~P1 1c))) <-> E.bE.t(t = {{{{b}}}} /\ <<t, <<{{a}}, {m}>>>> e. ( Ins2k SIk Sk \ Ins3k (((~P1 ~P1 Nn X.k _V) i^i ( Ins2k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c) i^i Ins3k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c)))"k~P1 1c))))
33	24, 25, 32	3bitri 262	. . . . . . . . . . 11 |- (<<{{a}}, {m}>> e. (( Ins2k SIk Sk \ Ins3k (((~P1 ~P1 Nn X.k _V) i^i ( Ins2k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c) i^i Ins3k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c)))"k~P1 1c))"k~P1 ~P1 ~P1 1c) <-> E.bE.t(t = {{{{b}}}} /\ <<t, <<{{a}}, {m}>>>> e. ( Ins2k SIk Sk \ Ins3k (((~P1 ~P1 Nn X.k _V) i^i ( Ins2k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c) i^i Ins3k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c)))"k~P1 1c))))
34		snex 4112	. . . . . . . . . . . . . . 15 |- {{{{b}}}} e. _V
35		opkeq1 4060	. . . . . . . . . . . . . . . 16 |- (t = {{{{b}}}} -> <<t, <<{{a}}, {m}>>>> = <<{{{{b}}}}, <<{{a}}, {m}>>>>)
36	35	eleq1d 2419	. . . . . . . . . . . . . . 15 |- (t = {{{{b}}}} -> (<<t, <<{{a}}, {m}>>>> e. ( Ins2k SIk Sk \ Ins3k (((~P1 ~P1 Nn X.k _V) i^i ( Ins2k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c) i^i Ins3k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c)))"k~P1 1c)) <-> <<{{{{b}}}}, <<{{a}}, {m}>>>> e. ( Ins2k SIk Sk \ Ins3k (((~P1 ~P1 Nn X.k _V) i^i ( Ins2k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c) i^i Ins3k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c)))"k~P1 1c))))
37	34, 36	ceqsexv 2895	. . . . . . . . . . . . . 14 |- (E.t(t = {{{{b}}}} /\ <<t, <<{{a}}, {m}>>>> e. ( Ins2k SIk Sk \ Ins3k (((~P1 ~P1 Nn X.k _V) i^i ( Ins2k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c) i^i Ins3k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c)))"k~P1 1c))) <-> <<{{{{b}}}}, <<{{a}}, {m}>>>> e. ( Ins2k SIk Sk \ Ins3k (((~P1 ~P1 Nn X.k _V) i^i ( Ins2k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c) i^i Ins3k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c)))"k~P1 1c)))
38		eldif 3222	. . . . . . . . . . . . . 14 |- (<<{{{{b}}}}, <<{{a}}, {m}>>>> e. ( Ins2k SIk Sk \ Ins3k (((~P1 ~P1 Nn X.k _V) i^i ( Ins2k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c) i^i Ins3k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c)))"k~P1 1c)) <-> (<<{{{{b}}}}, <<{{a}}, {m}>>>> e. Ins2k SIk Sk /\ -. <<{{{{b}}}}, <<{{a}}, {m}>>>> e. Ins3k (((~P1 ~P1 Nn X.k _V) i^i ( Ins2k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c) i^i Ins3k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c)))"k~P1 1c)))
39		snex 4112	. . . . . . . . . . . . . . . . 17 |- {{b}} e. _V
40	39, 12, 1	otkelins2k 4256	. . . . . . . . . . . . . . . 16 |- (<<{{{{b}}}}, <<{{a}}, {m}>>>> e. Ins2k SIk Sk <-> <<{{b}}, {m}>> e. SIk Sk )
41		snex 4112	. . . . . . . . . . . . . . . . 17 |- {b} e. _V
42	41, 18	opksnelsik 4266	. . . . . . . . . . . . . . . 16 |- (<<{{b}}, {m}>> e. SIk Sk <-> <<{b}, m>> e. Sk )
43		vex 2863	. . . . . . . . . . . . . . . . 17 |- b e. _V
44	43, 18	elssetk 4271	. . . . . . . . . . . . . . . 16 |- (<<{b}, m>> e. Sk <-> b e. m)
45	40, 42, 44	3bitri 262	. . . . . . . . . . . . . . 15 |- (<<{{{{b}}}}, <<{{a}}, {m}>>>> e. Ins2k SIk Sk <-> b e. m)
46	39, 12, 1	otkelins3k 4257	. . . . . . . . . . . . . . . . 17 |- (<<{{{{b}}}}, <<{{a}}, {m}>>>> e. Ins3k (((~P1 ~P1 Nn X.k _V) i^i ( Ins2k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c) i^i Ins3k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c)))"k~P1 1c) <-> <<{{b}}, {{a}}>> e. (((~P1 ~P1 Nn X.k _V) i^i ( Ins2k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c) i^i Ins3k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c)))"k~P1 1c))
47		df-rex 2621	. . . . . . . . . . . . . . . . . . 19 |- (E.t e. ~P1 1c<<t, <<{{b}}, {{a}}>>>> e. ((~P1 ~P1 Nn X.k _V) i^i ( Ins2k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c) i^i Ins3k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c))) <-> E.t(t e. ~P1 1c /\ <<t, <<{{b}}, {{a}}>>>> e. ((~P1 ~P1 Nn X.k _V) i^i ( Ins2k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c) i^i Ins3k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c)))))
48		elpw11c 4148	. . . . . . . . . . . . . . . . . . . . . 22 |- (t e. ~P1 1c <-> E.n t = {{n}})
49	48	anbi1i 676	. . . . . . . . . . . . . . . . . . . . 21 |- ((t e. ~P1 1c /\ <<t, <<{{b}}, {{a}}>>>> e. ((~P1 ~P1 Nn X.k _V) i^i ( Ins2k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c) i^i Ins3k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c)))) <-> (E.n t = {{n}} /\ <<t, <<{{b}}, {{a}}>>>> e. ((~P1 ~P1 Nn X.k _V) i^i ( Ins2k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c) i^i Ins3k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c)))))
50		19.41v 1901	. . . . . . . . . . . . . . . . . . . . 21 |- (E.n(t = {{n}} /\ <<t, <<{{b}}, {{a}}>>>> e. ((~P1 ~P1 Nn X.k _V) i^i ( Ins2k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c) i^i Ins3k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c)))) <-> (E.n t = {{n}} /\ <<t, <<{{b}}, {{a}}>>>> e. ((~P1 ~P1 Nn X.k _V) i^i ( Ins2k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c) i^i Ins3k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c)))))
51	49, 50	bitr4i 243	. . . . . . . . . . . . . . . . . . . 20 |- ((t e. ~P1 1c /\ <<t, <<{{b}}, {{a}}>>>> e. ((~P1 ~P1 Nn X.k _V) i^i ( Ins2k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c) i^i Ins3k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c)))) <-> E.n(t = {{n}} /\ <<t, <<{{b}}, {{a}}>>>> e. ((~P1 ~P1 Nn X.k _V) i^i ( Ins2k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c) i^i Ins3k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c)))))
52	51	exbii 1582	. . . . . . . . . . . . . . . . . . 19 |- (E.t(t e. ~P1 1c /\ <<t, <<{{b}}, {{a}}>>>> e. ((~P1 ~P1 Nn X.k _V) i^i ( Ins2k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c) i^i Ins3k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c)))) <-> E.tE.n(t = {{n}} /\ <<t, <<{{b}}, {{a}}>>>> e. ((~P1 ~P1 Nn X.k _V) i^i ( Ins2k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c) i^i Ins3k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c)))))
53	47, 52	bitri 240	. . . . . . . . . . . . . . . . . 18 |- (E.t e. ~P1 1c<<t, <<{{b}}, {{a}}>>>> e. ((~P1 ~P1 Nn X.k _V) i^i ( Ins2k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c) i^i Ins3k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c))) <-> E.tE.n(t = {{n}} /\ <<t, <<{{b}}, {{a}}>>>> e. ((~P1 ~P1 Nn X.k _V) i^i ( Ins2k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c) i^i Ins3k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c)))))
54		opkex 4114	. . . . . . . . . . . . . . . . . . 19 |- <<{{b}}, {{a}}>> e. _V
55	54	elimak 4260	. . . . . . . . . . . . . . . . . 18 |- (<<{{b}}, {{a}}>> e. (((~P1 ~P1 Nn X.k _V) i^i ( Ins2k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c) i^i Ins3k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c)))"k~P1 1c) <-> E.t e. ~P1 1c<<t, <<{{b}}, {{a}}>>>> e. ((~P1 ~P1 Nn X.k _V) i^i ( Ins2k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c) i^i Ins3k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c))))
56		excom 1741	. . . . . . . . . . . . . . . . . 18 |- (E.nE.t(t = {{n}} /\ <<t, <<{{b}}, {{a}}>>>> e. ((~P1 ~P1 Nn X.k _V) i^i ( Ins2k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c) i^i Ins3k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c)))) <-> E.tE.n(t = {{n}} /\ <<t, <<{{b}}, {{a}}>>>> e. ((~P1 ~P1 Nn X.k _V) i^i ( Ins2k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c) i^i Ins3k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c)))))
57	53, 55, 56	3bitr4i 268	. . . . . . . . . . . . . . . . 17 |- (<<{{b}}, {{a}}>> e. (((~P1 ~P1 Nn X.k _V) i^i ( Ins2k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c) i^i Ins3k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c)))"k~P1 1c) <-> E.nE.t(t = {{n}} /\ <<t, <<{{b}}, {{a}}>>>> e. ((~P1 ~P1 Nn X.k _V) i^i ( Ins2k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c) i^i Ins3k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c)))))
58		snex 4112	. . . . . . . . . . . . . . . . . . . . 21 |- {{n}} e. _V
59		opkeq1 4060	. . . . . . . . . . . . . . . . . . . . . 22 |- (t = {{n}} -> <<t, <<{{b}}, {{a}}>>>> = <<{{n}}, <<{{b}}, {{a}}>>>>)
60	59	eleq1d 2419	. . . . . . . . . . . . . . . . . . . . 21 |- (t = {{n}} -> (<<t, <<{{b}}, {{a}}>>>> e. ((~P1 ~P1 Nn X.k _V) i^i ( Ins2k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c) i^i Ins3k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c))) <-> <<{{n}}, <<{{b}}, {{a}}>>>> e. ((~P1 ~P1 Nn X.k _V) i^i ( Ins2k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c) i^i Ins3k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c)))))
61	58, 60	ceqsexv 2895	. . . . . . . . . . . . . . . . . . . 20 |- (E.t(t = {{n}} /\ <<t, <<{{b}}, {{a}}>>>> e. ((~P1 ~P1 Nn X.k _V) i^i ( Ins2k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c) i^i Ins3k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c)))) <-> <<{{n}}, <<{{b}}, {{a}}>>>> e. ((~P1 ~P1 Nn X.k _V) i^i ( Ins2k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c) i^i Ins3k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c))))
62		elin 3220	. . . . . . . . . . . . . . . . . . . 20 |- (<<{{n}}, <<{{b}}, {{a}}>>>> e. ((~P1 ~P1 Nn X.k _V) i^i ( Ins2k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c) i^i Ins3k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c))) <-> (<<{{n}}, <<{{b}}, {{a}}>>>> e. (~P1 ~P1 Nn X.k _V) /\ <<{{n}}, <<{{b}}, {{a}}>>>> e. ( Ins2k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c) i^i Ins3k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c))))
63	58, 54	opkelxpk 4249	. . . . . . . . . . . . . . . . . . . . . . 23 |- (<<{{n}}, <<{{b}}, {{a}}>>>> e. (~P1 ~P1 Nn X.k _V) <-> ({{n}} e. ~P1 ~P1 Nn /\ <<{{b}}, {{a}}>> e. _V))
64	54, 63	mpbiran2 885	. . . . . . . . . . . . . . . . . . . . . 22 |- (<<{{n}}, <<{{b}}, {{a}}>>>> e. (~P1 ~P1 Nn X.k _V) <-> {{n}} e. ~P1 ~P1 Nn )
65		snelpw1 4147	. . . . . . . . . . . . . . . . . . . . . 22 |- ({{n}} e. ~P1 ~P1 Nn <-> {n} e. ~P1 Nn )
66		snelpw1 4147	. . . . . . . . . . . . . . . . . . . . . 22 |- ({n} e. ~P1 Nn <-> n e. Nn )
67	64, 65, 66	3bitri 262	. . . . . . . . . . . . . . . . . . . . 21 |- (<<{{n}}, <<{{b}}, {{a}}>>>> e. (~P1 ~P1 Nn X.k _V) <-> n e. Nn )
68		elin 3220	. . . . . . . . . . . . . . . . . . . . . 22 |- (<<{{n}}, <<{{b}}, {{a}}>>>> e. ( Ins2k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c) i^i Ins3k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c)) <-> (<<{{n}}, <<{{b}}, {{a}}>>>> e. Ins2k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c) /\ <<{{n}}, <<{{b}}, {{a}}>>>> e. Ins3k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c)))
69		vex 2863	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- n e. _V
70	69, 39, 12	otkelins2k 4256	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (<<{{n}}, <<{{b}}, {{a}}>>>> e. Ins2k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c) <-> <<n, {{a}}>> e. (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c))
71		opkex 4114	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- <<n, {{a}}>> e. _V
72	71	elimak 4260	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (<<n, {{a}}>> e. (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c) <-> E.t e. ~P1 ~P1 1c<<t, <<n, {{a}}>>>> e. ( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk ))
73		df-rex 2621	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (E.t e. ~P1 ~P1 1c<<t, <<n, {{a}}>>>> e. ( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk ) <-> E.t(t e. ~P1 ~P1 1c /\ <<t, <<n, {{a}}>>>> e. ( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )))
74		elpw121c 4149	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (t e. ~P1 ~P1 1c <-> E.x t = {{{x}}})
75	74	anbi1i 676	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((t e. ~P1 ~P1 1c /\ <<t, <<n, {{a}}>>>> e. ( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )) <-> (E.x t = {{{x}}} /\ <<t, <<n, {{a}}>>>> e. ( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )))
76		19.41v 1901	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (E.x(t = {{{x}}} /\ <<t, <<n, {{a}}>>>> e. ( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )) <-> (E.x t = {{{x}}} /\ <<t, <<n, {{a}}>>>> e. ( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )))
77	75, 76	bitr4i 243	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((t e. ~P1 ~P1 1c /\ <<t, <<n, {{a}}>>>> e. ( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )) <-> E.x(t = {{{x}}} /\ <<t, <<n, {{a}}>>>> e. ( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )))
78	77	exbii 1582	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (E.t(t e. ~P1 ~P1 1c /\ <<t, <<n, {{a}}>>>> e. ( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )) <-> E.tE.x(t = {{{x}}} /\ <<t, <<n, {{a}}>>>> e. ( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )))
79		excom 1741	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (E.xE.t(t = {{{x}}} /\ <<t, <<n, {{a}}>>>> e. ( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )) <-> E.tE.x(t = {{{x}}} /\ <<t, <<n, {{a}}>>>> e. ( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )))
80	78, 79	bitr4i 243	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (E.t(t e. ~P1 ~P1 1c /\ <<t, <<n, {{a}}>>>> e. ( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )) <-> E.xE.t(t = {{{x}}} /\ <<t, <<n, {{a}}>>>> e. ( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )))
81	72, 73, 80	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (<<n, {{a}}>> e. (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c) <-> E.xE.t(t = {{{x}}} /\ <<t, <<n, {{a}}>>>> e. ( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )))
82		snex 4112	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- {{{x}}} e. _V
83		opkeq1 4060	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (t = {{{x}}} -> <<t, <<n, {{a}}>>>> = <<{{{x}}}, <<n, {{a}}>>>>)
84	83	eleq1d 2419	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (t = {{{x}}} -> (<<t, <<n, {{a}}>>>> e. ( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk ) <-> <<{{{x}}}, <<n, {{a}}>>>> e. ( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )))
85	82, 84	ceqsexv 2895	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (E.t(t = {{{x}}} /\ <<t, <<n, {{a}}>>>> e. ( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )) <-> <<{{{x}}}, <<n, {{a}}>>>> e. ( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk ))
86		elin 3220	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (<<{{{x}}}, <<n, {{a}}>>>> e. ( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk ) <-> (<<{{{x}}}, <<n, {{a}}>>>> e. Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) /\ <<{{{x}}}, <<n, {{a}}>>>> e. Ins3k Sk ))
87		snex 4112	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- {x} e. _V
88	87, 69, 12	otkelins2k 4256	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (<<{{{x}}}, <<n, {{a}}>>>> e. Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) <-> <<{x}, {{a}}>> e. SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)))
89		vex 2863	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- x e. _V
90	89, 17	opksnelsik 4266	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (<<{x}, {{a}}>> e. SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) <-> <<x, {a}>> e. ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)))
91	89, 20	eqpw1relk 4480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (<<x, {a}>> e. ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) <-> x = ~P1 a)
92	88, 90, 91	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (<<{{{x}}}, <<n, {{a}}>>>> e. Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) <-> x = ~P1 a)
93	87, 69, 12	otkelins3k 4257	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (<<{{{x}}}, <<n, {{a}}>>>> e. Ins3k Sk <-> <<{x}, n>> e. Sk )
94	89, 69	elssetk 4271	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (<<{x}, n>> e. Sk <-> x e. n)
95	93, 94	bitri 240	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (<<{{{x}}}, <<n, {{a}}>>>> e. Ins3k Sk <-> x e. n)
96	92, 95	anbi12i 678	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((<<{{{x}}}, <<n, {{a}}>>>> e. Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) /\ <<{{{x}}}, <<n, {{a}}>>>> e. Ins3k Sk ) <-> (x = ~P1 a /\ x e. n))
97	85, 86, 96	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (E.t(t = {{{x}}} /\ <<t, <<n, {{a}}>>>> e. ( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )) <-> (x = ~P1 a /\ x e. n))
98	97	exbii 1582	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (E.xE.t(t = {{{x}}} /\ <<t, <<n, {{a}}>>>> e. ( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )) <-> E.x(x = ~P1 a /\ x e. n))
99		df-clel 2349	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (~P1 a e. n <-> E.x(x = ~P1 a /\ x e. n))
100	98, 99	bitr4i 243	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (E.xE.t(t = {{{x}}} /\ <<t, <<n, {{a}}>>>> e. ( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )) <-> ~P1 a e. n)
101	70, 81, 100	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . 23 |- (<<{{n}}, <<{{b}}, {{a}}>>>> e. Ins2k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c) <-> ~P1 a e. n)
102		opkex 4114	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- <<n, {{b}}>> e. _V
103	102	elimak 4260	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (<<n, {{b}}>> e. (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c) <-> E.t e. ~P1 ~P1 1c<<t, <<n, {{b}}>>>> e. ( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk ))
104	74	anbi1i 676	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((t e. ~P1 ~P1 1c /\ <<t, <<n, {{b}}>>>> e. ( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )) <-> (E.x t = {{{x}}} /\ <<t, <<n, {{b}}>>>> e. ( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )))
105		19.41v 1901	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (E.x(t = {{{x}}} /\ <<t, <<n, {{b}}>>>> e. ( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )) <-> (E.x t = {{{x}}} /\ <<t, <<n, {{b}}>>>> e. ( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )))
106	104, 105	bitr4i 243	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((t e. ~P1 ~P1 1c /\ <<t, <<n, {{b}}>>>> e. ( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )) <-> E.x(t = {{{x}}} /\ <<t, <<n, {{b}}>>>> e. ( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )))
107	106	exbii 1582	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (E.t(t e. ~P1 ~P1 1c /\ <<t, <<n, {{b}}>>>> e. ( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )) <-> E.tE.x(t = {{{x}}} /\ <<t, <<n, {{b}}>>>> e. ( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )))
108		df-rex 2621	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (E.t e. ~P1 ~P1 1c<<t, <<n, {{b}}>>>> e. ( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk ) <-> E.t(t e. ~P1 ~P1 1c /\ <<t, <<n, {{b}}>>>> e. ( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )))
109		excom 1741	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (E.xE.t(t = {{{x}}} /\ <<t, <<n, {{b}}>>>> e. ( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )) <-> E.tE.x(t = {{{x}}} /\ <<t, <<n, {{b}}>>>> e. ( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )))
110	107, 108, 109	3bitr4i 268	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (E.t e. ~P1 ~P1 1c<<t, <<n, {{b}}>>>> e. ( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk ) <-> E.xE.t(t = {{{x}}} /\ <<t, <<n, {{b}}>>>> e. ( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )))
111		opkeq1 4060	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (t = {{{x}}} -> <<t, <<n, {{b}}>>>> = <<{{{x}}}, <<n, {{b}}>>>>)
112	111	eleq1d 2419	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (t = {{{x}}} -> (<<t, <<n, {{b}}>>>> e. ( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk ) <-> <<{{{x}}}, <<n, {{b}}>>>> e. ( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )))
113	82, 112	ceqsexv 2895	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (E.t(t = {{{x}}} /\ <<t, <<n, {{b}}>>>> e. ( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )) <-> <<{{{x}}}, <<n, {{b}}>>>> e. ( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk ))
114		elin 3220	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (<<{{{x}}}, <<n, {{b}}>>>> e. ( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk ) <-> (<<{{{x}}}, <<n, {{b}}>>>> e. Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) /\ <<{{{x}}}, <<n, {{b}}>>>> e. Ins3k Sk ))
115	87, 69, 39	otkelins2k 4256	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (<<{{{x}}}, <<n, {{b}}>>>> e. Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) <-> <<{x}, {{b}}>> e. SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)))
116	89, 41	opksnelsik 4266	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (<<{x}, {{b}}>> e. SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) <-> <<x, {b}>> e. ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)))
117	89, 43	eqpw1relk 4480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (<<x, {b}>> e. ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) <-> x = ~P1 b)
118	115, 116, 117	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (<<{{{x}}}, <<n, {{b}}>>>> e. Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) <-> x = ~P1 b)
119	87, 69, 39	otkelins3k 4257	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (<<{{{x}}}, <<n, {{b}}>>>> e. Ins3k Sk <-> <<{x}, n>> e. Sk )
120	119, 94	bitri 240	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (<<{{{x}}}, <<n, {{b}}>>>> e. Ins3k Sk <-> x e. n)
121	118, 120	anbi12i 678	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((<<{{{x}}}, <<n, {{b}}>>>> e. Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) /\ <<{{{x}}}, <<n, {{b}}>>>> e. Ins3k Sk ) <-> (x = ~P1 b /\ x e. n))
122	113, 114, 121	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (E.t(t = {{{x}}} /\ <<t, <<n, {{b}}>>>> e. ( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )) <-> (x = ~P1 b /\ x e. n))
123	122	exbii 1582	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (E.xE.t(t = {{{x}}} /\ <<t, <<n, {{b}}>>>> e. ( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )) <-> E.x(x = ~P1 b /\ x e. n))
124	103, 110, 123	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (<<n, {{b}}>> e. (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c) <-> E.x(x = ~P1 b /\ x e. n))
125	69, 39, 12	otkelins3k 4257	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (<<{{n}}, <<{{b}}, {{a}}>>>> e. Ins3k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c) <-> <<n, {{b}}>> e. (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c))
126		df-clel 2349	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (~P1 b e. n <-> E.x(x = ~P1 b /\ x e. n))
127	124, 125, 126	3bitr4i 268	. . . . . . . . . . . . . . . . . . . . . . 23 |- (<<{{n}}, <<{{b}}, {{a}}>>>> e. Ins3k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c) <-> ~P1 b e. n)
128	101, 127	anbi12i 678	. . . . . . . . . . . . . . . . . . . . . 22 |- ((<<{{n}}, <<{{b}}, {{a}}>>>> e. Ins2k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c) /\ <<{{n}}, <<{{b}}, {{a}}>>>> e. Ins3k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c)) <-> (~P1 a e. n /\ ~P1 b e. n))
129	68, 128	bitri 240	. . . . . . . . . . . . . . . . . . . . 21 |- (<<{{n}}, <<{{b}}, {{a}}>>>> e. ( Ins2k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c) i^i Ins3k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c)) <-> (~P1 a e. n /\ ~P1 b e. n))
130	67, 129	anbi12i 678	. . . . . . . . . . . . . . . . . . . 20 |- ((<<{{n}}, <<{{b}}, {{a}}>>>> e. (~P1 ~P1 Nn X.k _V) /\ <<{{n}}, <<{{b}}, {{a}}>>>> e. ( Ins2k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c) i^i Ins3k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c))) <-> (n e. Nn /\ (~P1 a e. n /\ ~P1 b e. n)))
131	61, 62, 130	3bitri 262	. . . . . . . . . . . . . . . . . . 19 |- (E.t(t = {{n}} /\ <<t, <<{{b}}, {{a}}>>>> e. ((~P1 ~P1 Nn X.k _V) i^i ( Ins2k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c) i^i Ins3k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c)))) <-> (n e. Nn /\ (~P1 a e. n /\ ~P1 b e. n)))
132	131	exbii 1582	. . . . . . . . . . . . . . . . . 18 |- (E.nE.t(t = {{n}} /\ <<t, <<{{b}}, {{a}}>>>> e. ((~P1 ~P1 Nn X.k _V) i^i ( Ins2k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c) i^i Ins3k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c)))) <-> E.n(n e. Nn /\ (~P1 a e. n /\ ~P1 b e. n)))
133		df-rex 2621	. . . . . . . . . . . . . . . . . 18 |- (E.n e. Nn (~P1 a e. n /\ ~P1 b e. n) <-> E.n(n e. Nn /\ (~P1 a e. n /\ ~P1 b e. n)))
134	132, 133	bitr4i 243	. . . . . . . . . . . . . . . . 17 |- (E.nE.t(t = {{n}} /\ <<t, <<{{b}}, {{a}}>>>> e. ((~P1 ~P1 Nn X.k _V) i^i ( Ins2k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c) i^i Ins3k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c)))) <-> E.n e. Nn (~P1 a e. n /\ ~P1 b e. n))
135	46, 57, 134	3bitri 262	. . . . . . . . . . . . . . . 16 |- (<<{{{{b}}}}, <<{{a}}, {m}>>>> e. Ins3k (((~P1 ~P1 Nn X.k _V) i^i ( Ins2k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c) i^i Ins3k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c)))"k~P1 1c) <-> E.n e. Nn (~P1 a e. n /\ ~P1 b e. n))
136	135	notbii 287	. . . . . . . . . . . . . . 15 |- (-. <<{{{{b}}}}, <<{{a}}, {m}>>>> e. Ins3k (((~P1 ~P1 Nn X.k _V) i^i ( Ins2k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c) i^i Ins3k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c)))"k~P1 1c) <-> -. E.n e. Nn (~P1 a e. n /\ ~P1 b e. n))
137	45, 136	anbi12i 678	. . . . . . . . . . . . . 14 |- ((<<{{{{b}}}}, <<{{a}}, {m}>>>> e. Ins2k SIk Sk /\ -. <<{{{{b}}}}, <<{{a}}, {m}>>>> e. Ins3k (((~P1 ~P1 Nn X.k _V) i^i ( Ins2k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c) i^i Ins3k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c)))"k~P1 1c)) <-> (b e. m /\ -. E.n e. Nn (~P1 a e. n /\ ~P1 b e. n)))
138	37, 38, 137	3bitri 262	. . . . . . . . . . . . 13 |- (E.t(t = {{{{b}}}} /\ <<t, <<{{a}}, {m}>>>> e. ( Ins2k SIk Sk \ Ins3k (((~P1 ~P1 Nn X.k _V) i^i ( Ins2k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c) i^i Ins3k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c)))"k~P1 1c))) <-> (b e. m /\ -. E.n e. Nn (~P1 a e. n /\ ~P1 b e. n)))
139	138	exbii 1582	. . . . . . . . . . . 12 |- (E.bE.t(t = {{{{b}}}} /\ <<t, <<{{a}}, {m}>>>> e. ( Ins2k SIk Sk \ Ins3k (((~P1 ~P1 Nn X.k _V) i^i ( Ins2k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c) i^i Ins3k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c)))"k~P1 1c))) <-> E.b(b e. m /\ -. E.n e. Nn (~P1 a e. n /\ ~P1 b e. n)))
140		df-rex 2621	. . . . . . . . . . . 12 |- (E.b e. m -. E.n e. Nn (~P1 a e. n /\ ~P1 b e. n) <-> E.b(b e. m /\ -. E.n e. Nn (~P1 a e. n /\ ~P1 b e. n)))
141	139, 140	bitr4i 243	. . . . . . . . . . 11 |- (E.bE.t(t = {{{{b}}}} /\ <<t, <<{{a}}, {m}>>>> e. ( Ins2k SIk Sk \ Ins3k (((~P1 ~P1 Nn X.k _V) i^i ( Ins2k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c) i^i Ins3k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c)))"k~P1 1c))) <-> E.b e. m -. E.n e. Nn (~P1 a e. n /\ ~P1 b e. n))
142		rexnal 2626	. . . . . . . . . . 11 |- (E.b e. m -. E.n e. Nn (~P1 a e. n /\ ~P1 b e. n) <-> -. A.b e. m E.n e. Nn (~P1 a e. n /\ ~P1 b e. n))
143	33, 141, 142	3bitri 262	. . . . . . . . . 10 |- (<<{{a}}, {m}>> e. (( Ins2k SIk Sk \ Ins3k (((~P1 ~P1 Nn X.k _V) i^i ( Ins2k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c) i^i Ins3k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c)))"k~P1 1c))"k~P1 ~P1 ~P1 1c) <-> -. A.b e. m E.n e. Nn (~P1 a e. n /\ ~P1 b e. n))
144	22, 143	anbi12i 678	. . . . . . . . 9 |- ((<<{{a}}, {m}>> e. SIk Sk /\ <<{{a}}, {m}>> e. (( Ins2k SIk Sk \ Ins3k (((~P1 ~P1 Nn X.k _V) i^i ( Ins2k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c) i^i Ins3k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c)))"k~P1 1c))"k~P1 ~P1 ~P1 1c)) <-> (a e. m /\ -. A.b e. m E.n e. Nn (~P1 a e. n /\ ~P1 b e. n)))
145	15, 16, 144	3bitri 262	. . . . . . . 8 |- (E.t(t = {{a}} /\ <<t, {m}>> e. ( SIk Sk i^i (( Ins2k SIk Sk \ Ins3k (((~P1 ~P1 Nn X.k _V) i^i ( Ins2k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c) i^i Ins3k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c)))"k~P1 1c))"k~P1 ~P1 ~P1 1c))) <-> (a e. m /\ -. A.b e. m E.n e. Nn (~P1 a e. n /\ ~P1 b e. n)))
146	145	exbii 1582	. . . . . . 7 |- (E.aE.t(t = {{a}} /\ <<t, {m}>> e. ( SIk Sk i^i (( Ins2k SIk Sk \ Ins3k (((~P1 ~P1 Nn X.k _V) i^i ( Ins2k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c) i^i Ins3k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c)))"k~P1 1c))"k~P1 ~P1 ~P1 1c))) <-> E.a(a e. m /\ -. A.b e. m E.n e. Nn (~P1 a e. n /\ ~P1 b e. n)))
147		df-rex 2621	. . . . . . 7 |- (E.a e. m -. A.b e. m E.n e. Nn (~P1 a e. n /\ ~P1 b e. n) <-> E.a(a e. m /\ -. A.b e. m E.n e. Nn (~P1 a e. n /\ ~P1 b e. n)))
148	146, 147	bitr4i 243	. . . . . 6 |- (E.aE.t(t = {{a}} /\ <<t, {m}>> e. ( SIk Sk i^i (( Ins2k SIk Sk \ Ins3k (((~P1 ~P1 Nn X.k _V) i^i ( Ins2k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c) i^i Ins3k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c)))"k~P1 1c))"k~P1 ~P1 ~P1 1c))) <-> E.a e. m -. A.b e. m E.n e. Nn (~P1 a e. n /\ ~P1 b e. n))
149	3, 11, 148	3bitri 262	. . . . 5 |- ({m} e. (( SIk Sk i^i (( Ins2k SIk Sk \ Ins3k (((~P1 ~P1 Nn X.k _V) i^i ( Ins2k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c) i^i Ins3k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c)))"k~P1 1c))"k~P1 ~P1 ~P1 1c))"k~P1 1c) <-> E.a e. m -. A.b e. m E.n e. Nn (~P1 a e. n /\ ~P1 b e. n))
150	2, 149	xchbinx 301	. . . 4 |- ({m} e. ∼ (( SIk Sk i^i (( Ins2k SIk Sk \ Ins3k (((~P1 ~P1 Nn X.k _V) i^i ( Ins2k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c) i^i Ins3k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c)))"k~P1 1c))"k~P1 ~P1 ~P1 1c))"k~P1 1c) <-> -. E.a e. m -. A.b e. m E.n e. Nn (~P1 a e. n /\ ~P1 b e. n))
151	18	eluni1 4174	. . . 4 |- (m e. ⋃1 ∼ (( SIk Sk i^i (( Ins2k SIk Sk \ Ins3k (((~P1 ~P1 Nn X.k _V) i^i ( Ins2k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c) i^i Ins3k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c)))"k~P1 1c))"k~P1 ~P1 ~P1 1c))"k~P1 1c) <-> {m} e. ∼ (( SIk Sk i^i (( Ins2k SIk Sk \ Ins3k (((~P1 ~P1 Nn X.k _V) i^i ( Ins2k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c) i^i Ins3k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c)))"k~P1 1c))"k~P1 ~P1 ~P1 1c))"k~P1 1c))
152		dfral2 2627	. . . 4 |- (A.a e. m A.b e. m E.n e. Nn (~P1 a e. n /\ ~P1 b e. n) <-> -. E.a e. m -. A.b e. m E.n e. Nn (~P1 a e. n /\ ~P1 b e. n))
153	150, 151, 152	3bitr4i 268	. . 3 |- (m e. ⋃1 ∼ (( SIk Sk i^i (( Ins2k SIk Sk \ Ins3k (((~P1 ~P1 Nn X.k _V) i^i ( Ins2k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c) i^i Ins3k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c)))"k~P1 1c))"k~P1 ~P1 ~P1 1c))"k~P1 1c) <-> A.a e. m A.b e. m E.n e. Nn (~P1 a e. n /\ ~P1 b e. n))
154	153	eqabi 2465	. 2 |- ⋃1 ∼ (( SIk Sk i^i (( Ins2k SIk Sk \ Ins3k (((~P1 ~P1 Nn X.k _V) i^i ( Ins2k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c) i^i Ins3k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c)))"k~P1 1c))"k~P1 ~P1 ~P1 1c))"k~P1 1c) = {m | A.a e. m A.b e. m E.n e. Nn (~P1 a e. n /\ ~P1 b e. n)}
155		ssetkex 4295	. . . . . . 7 |- Sk e. _V
156	155	sikex 4298	. . . . . 6 |- SIk Sk e. _V
157	156	ins2kex 4308	. . . . . . . 8 |- Ins2k SIk Sk e. _V
158		nncex 4397	. . . . . . . . . . . . . 14 |- Nn e. _V
159	158	pw1ex 4304	. . . . . . . . . . . . 13 |- ~P1 Nn e. _V
160	159	pw1ex 4304	. . . . . . . . . . . 12 |- ~P1 ~P1 Nn e. _V
161		vvex 4110	. . . . . . . . . . . 12 |- _V e. _V
162	160, 161	xpkex 4290	. . . . . . . . . . 11 |- (~P1 ~P1 Nn X.k _V) e. _V
163		1cex 4143	. . . . . . . . . . . . . . . . . . . 20 |- 1c e. _V
164	163	pwex 4330	. . . . . . . . . . . . . . . . . . 19 |- ~P1c e. _V
165	164, 161	xpkex 4290	. . . . . . . . . . . . . . . . . 18 |- (~P1c X.k _V) e. _V
166	155	ins3kex 4309	. . . . . . . . . . . . . . . . . . . 20 |- Ins3k Sk e. _V
167	166, 157	symdifex 4109	. . . . . . . . . . . . . . . . . . 19 |- ( Ins3k Sk (+) Ins2k SIk Sk ) e. _V
168	163	pw1ex 4304	. . . . . . . . . . . . . . . . . . . . 21 |- ~P1 1c e. _V
169	168	pw1ex 4304	. . . . . . . . . . . . . . . . . . . 20 |- ~P1 ~P1 1c e. _V
170	169	pw1ex 4304	. . . . . . . . . . . . . . . . . . 19 |- ~P1 ~P1 ~P1 1c e. _V
171	167, 170	imakex 4301	. . . . . . . . . . . . . . . . . 18 |- (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c) e. _V
172	165, 171	difex 4108	. . . . . . . . . . . . . . . . 17 |- ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) e. _V
173	172	sikex 4298	. . . . . . . . . . . . . . . 16 |- SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) e. _V
174	173	ins2kex 4308	. . . . . . . . . . . . . . 15 |- Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) e. _V
175	174, 166	inex 4106	. . . . . . . . . . . . . 14 |- ( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk ) e. _V
176	175, 169	imakex 4301	. . . . . . . . . . . . 13 |- (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c) e. _V
177	176	ins2kex 4308	. . . . . . . . . . . 12 |- Ins2k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c) e. _V
178	176	ins3kex 4309	. . . . . . . . . . . 12 |- Ins3k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c) e. _V
179	177, 178	inex 4106	. . . . . . . . . . 11 |- ( Ins2k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c) i^i Ins3k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c)) e. _V
180	162, 179	inex 4106	. . . . . . . . . 10 |- ((~P1 ~P1 Nn X.k _V) i^i ( Ins2k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c) i^i Ins3k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c))) e. _V
181	180, 168	imakex 4301	. . . . . . . . 9 |- (((~P1 ~P1 Nn X.k _V) i^i ( Ins2k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c) i^i Ins3k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c)))"k~P1 1c) e. _V
182	181	ins3kex 4309	. . . . . . . 8 |- Ins3k (((~P1 ~P1 Nn X.k _V) i^i ( Ins2k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c) i^i Ins3k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c)))"k~P1 1c) e. _V
183	157, 182	difex 4108	. . . . . . 7 |- ( Ins2k SIk Sk \ Ins3k (((~P1 ~P1 Nn X.k _V) i^i ( Ins2k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c) i^i Ins3k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c)))"k~P1 1c)) e. _V
184	183, 170	imakex 4301	. . . . . 6 |- (( Ins2k SIk Sk \ Ins3k (((~P1 ~P1 Nn X.k _V) i^i ( Ins2k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c) i^i Ins3k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c)))"k~P1 1c))"k~P1 ~P1 ~P1 1c) e. _V
185	156, 184	inex 4106	. . . . 5 |- ( SIk Sk i^i (( Ins2k SIk Sk \ Ins3k (((~P1 ~P1 Nn X.k _V) i^i ( Ins2k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c) i^i Ins3k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c)))"k~P1 1c))"k~P1 ~P1 ~P1 1c)) e. _V
186	185, 168	imakex 4301	. . . 4 |- (( SIk Sk i^i (( Ins2k SIk Sk \ Ins3k (((~P1 ~P1 Nn X.k _V) i^i ( Ins2k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c) i^i Ins3k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c)))"k~P1 1c))"k~P1 ~P1 ~P1 1c))"k~P1 1c) e. _V
187	186	complex 4105	. . 3 |- ∼ (( SIk Sk i^i (( Ins2k SIk Sk \ Ins3k (((~P1 ~P1 Nn X.k _V) i^i ( Ins2k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c) i^i Ins3k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c)))"k~P1 1c))"k~P1 ~P1 ~P1 1c))"k~P1 1c) e. _V
188	187	uni1ex 4294	. 2 |- ⋃1 ∼ (( SIk Sk i^i (( Ins2k SIk Sk \ Ins3k (((~P1 ~P1 Nn X.k _V) i^i ( Ins2k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c) i^i Ins3k (( Ins2k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins3k Sk )"k~P1 ~P1 1c)))"k~P1 1c))"k~P1 ~P1 ~P1 1c))"k~P1 1c) e. _V
189	154, 188	eqeltrri 2424	1 |- {m | A.a e. m A.b e. m E.n e. Nn (~P1 a e. n /\ ~P1 b e. n)} e. _V

Syntax hints:  -. wn 3   /\ wa 358  E.wex 1541   = wceq 1642   e. wcel 1710  {cab 2339  A.wral 2615  E.wrex 2616  _Vcvv 2860   ∼ ccompl 3206   \ cdif 3207   i^i cin 3209   (+) csymdif 3210  ~Pcpw 3723  {csn 3738  <<copk 4058  ⋃₁cuni1 4134  1_cc1c 4135  ~P₁ cpw1 4136   X._k cxpk 4175   Ins2_k cins2k 4177   Ins3_k cins3k 4178  "_kcimak 4180   SI_k csik 4182   S_k cssetk 4184   Nn cnnc 4374

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-sbc 3048  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-if 3664  df-pw 3725  df-sn 3742  df-pr 3743  df-uni 3893  df-int 3928  df-opk 4059  df-1c 4137  df-pw1 4138  df-uni1 4139  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-addc 4379  df-nnc 4380

This theorem is referenced by:  ncfinraise  4482