Theorem ncfinlowerlem1 4483

Description: Lemma for ncfinlower 4484. Set up stratification for induction. (Contributed by SF, 22-Jan-2015.)

Assertion

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

Distinct variable group:   m,n,a,b

Proof of Theorem ncfinlowerlem1

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

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

Syntax hints:  -. wn 3   -> wi 4   /\ wa 358  A.wal 1540  E.wex 1541   = wceq 1642   e. wcel 1710  {cab 2339  E.wrex 2616  _Vcvv 2860   ∼ ccompl 3206   \ cdif 3207   i^i cin 3209   (+) csymdif 3210  ~Pcpw 3723  {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   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:  ncfinlower  4484