Theorem preaddccan2lem1 4454

Description: Lemma for preaddccan2 4455. Establish stratification for the induction step. (Contributed by SF, 30-Mar-2021.)

Assertion

Ref	Expression
preaddccan2lem1	|- ((N e. Nn /\ P e. Nn ) -> {m | (((m +o N) =/= (/) /\ (m +o N) = (m +o P)) -> N = P)} e. _V)

Distinct variable groups:   m,N   P,m

Proof of Theorem preaddccan2lem1

Dummy variables n p t are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		addceq2 4384	. . . . . . 7 |- (n = N -> (m +o n) = (m +o N))
2	1	neeq1d 2529	. . . . . 6 |- (n = N -> ((m +o n) =/= (/) <-> (m +o N) =/= (/)))
3	1	eqeq1d 2361	. . . . . 6 |- (n = N -> ((m +o n) = (m +o p) <-> (m +o N) = (m +o p)))
4	2, 3	anbi12d 691	. . . . 5 |- (n = N -> (((m +o n) =/= (/) /\ (m +o n) = (m +o p)) <-> ((m +o N) =/= (/) /\ (m +o N) = (m +o p))))
5	4	imbi1d 308	. . . 4 |- (n = N -> ((((m +o n) =/= (/) /\ (m +o n) = (m +o p)) -> N = P) <-> (((m +o N) =/= (/) /\ (m +o N) = (m +o p)) -> N = P)))
6	5	abbidv 2467	. . 3 |- (n = N -> {m | (((m +o n) =/= (/) /\ (m +o n) = (m +o p)) -> N = P)} = {m | (((m +o N) =/= (/) /\ (m +o N) = (m +o p)) -> N = P)})
7	6	eleq1d 2419	. 2 |- (n = N -> ({m | (((m +o n) =/= (/) /\ (m +o n) = (m +o p)) -> N = P)} e. _V <-> {m | (((m +o N) =/= (/) /\ (m +o N) = (m +o p)) -> N = P)} e. _V))
8		addceq2 4384	. . . . . . 7 |- (p = P -> (m +o p) = (m +o P))
9	8	eqeq2d 2364	. . . . . 6 |- (p = P -> ((m +o N) = (m +o p) <-> (m +o N) = (m +o P)))
10	9	anbi2d 684	. . . . 5 |- (p = P -> (((m +o N) =/= (/) /\ (m +o N) = (m +o p)) <-> ((m +o N) =/= (/) /\ (m +o N) = (m +o P))))
11	10	imbi1d 308	. . . 4 |- (p = P -> ((((m +o N) =/= (/) /\ (m +o N) = (m +o p)) -> N = P) <-> (((m +o N) =/= (/) /\ (m +o N) = (m +o P)) -> N = P)))
12	11	abbidv 2467	. . 3 |- (p = P -> {m | (((m +o N) =/= (/) /\ (m +o N) = (m +o p)) -> N = P)} = {m | (((m +o N) =/= (/) /\ (m +o N) = (m +o P)) -> N = P)})
13	12	eleq1d 2419	. 2 |- (p = P -> ({m | (((m +o N) =/= (/) /\ (m +o N) = (m +o p)) -> N = P)} e. _V <-> {m | (((m +o N) =/= (/) /\ (m +o N) = (m +o P)) -> N = P)} e. _V))
14		imor 401	. . . . 5 |- ((((m +o n) =/= (/) /\ (m +o n) = (m +o p)) -> N = P) <-> (-. ((m +o n) =/= (/) /\ (m +o n) = (m +o p)) \/ N = P))
15	14	abbii 2465	. . . 4 |- {m | (((m +o n) =/= (/) /\ (m +o n) = (m +o p)) -> N = P)} = {m | (-. ((m +o n) =/= (/) /\ (m +o n) = (m +o p)) \/ N = P)}
16		unab 3521	. . . 4 |- ({m | -. ((m +o n) =/= (/) /\ (m +o n) = (m +o p))} u. {m | N = P}) = {m | (-. ((m +o n) =/= (/) /\ (m +o n) = (m +o p)) \/ N = P)}
17	15, 16	eqtr4i 2376	. . 3 |- {m | (((m +o n) =/= (/) /\ (m +o n) = (m +o p)) -> N = P)} = ({m | -. ((m +o n) =/= (/) /\ (m +o n) = (m +o p))} u. {m | N = P})
18		vex 2862	. . . . . . . 8 |- m e. _V
19	18	elcompl 3225	. . . . . . 7 |- (m e. ∼ ( ∼ (`'kImagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 n)"k{(/)}) i^i (`'k(Imagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 n) i^i Imagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 p))"k_V)) <-> -. m e. ( ∼ (`'kImagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 n)"k{(/)}) i^i (`'k(Imagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 n) i^i Imagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 p))"k_V)))
20		elin 3219	. . . . . . . . 9 |- (m e. ( ∼ (`'kImagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 n)"k{(/)}) i^i (`'k(Imagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 n) i^i Imagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 p))"k_V)) <-> (m e. ∼ (`'kImagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 n)"k{(/)}) /\ m e. (`'k(Imagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 n) i^i Imagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 p))"k_V)))
21		0ex 4110	. . . . . . . . . . . . . 14 |- (/) e. _V
22	21, 18	opkelcnvk 4250	. . . . . . . . . . . . 13 |- (<<(/), m>> e. `'kImagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 n) <-> <<m, (/)>> e. Imagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 n))
23	21, 18	elimaksn 4283	. . . . . . . . . . . . 13 |- (m e. (`'kImagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 n)"k{(/)}) <-> <<(/), m>> e. `'kImagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 n))
24		dfaddc2 4381	. . . . . . . . . . . . . . 15 |- (m +o n) = ((( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 n)"km)
25	24	eqeq2i 2363	. . . . . . . . . . . . . 14 |- ((/) = (m +o n) <-> (/) = ((( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 n)"km))
26		eqcom 2355	. . . . . . . . . . . . . 14 |- ((m +o n) = (/) <-> (/) = (m +o n))
27	18, 21	opkelimagek 4272	. . . . . . . . . . . . . 14 |- (<<m, (/)>> e. Imagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 n) <-> (/) = ((( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 n)"km))
28	25, 26, 27	3bitr4i 268	. . . . . . . . . . . . 13 |- ((m +o n) = (/) <-> <<m, (/)>> e. Imagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 n))
29	22, 23, 28	3bitr4i 268	. . . . . . . . . . . 12 |- (m e. (`'kImagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 n)"k{(/)}) <-> (m +o n) = (/))
30	29	notbii 287	. . . . . . . . . . 11 |- (-. m e. (`'kImagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 n)"k{(/)}) <-> -. (m +o n) = (/))
31	18	elcompl 3225	. . . . . . . . . . 11 |- (m e. ∼ (`'kImagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 n)"k{(/)}) <-> -. m e. (`'kImagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 n)"k{(/)}))
32		df-ne 2518	. . . . . . . . . . 11 |- ((m +o n) =/= (/) <-> -. (m +o n) = (/))
33	30, 31, 32	3bitr4i 268	. . . . . . . . . 10 |- (m e. ∼ (`'kImagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 n)"k{(/)}) <-> (m +o n) =/= (/))
34		rexv 2873	. . . . . . . . . . . 12 |- (E.t e. _V <<t, m>> e. `'k(Imagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 n) i^i Imagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 p)) <-> E.t<<t, m>> e. `'k(Imagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 n) i^i Imagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 p)))
35		vex 2862	. . . . . . . . . . . . . . 15 |- t e. _V
36	35, 18	opkelcnvk 4250	. . . . . . . . . . . . . 14 |- (<<t, m>> e. `'k(Imagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 n) i^i Imagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 p)) <-> <<m, t>> e. (Imagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 n) i^i Imagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 p)))
37		elin 3219	. . . . . . . . . . . . . . 15 |- (<<m, t>> e. (Imagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 n) i^i Imagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 p)) <-> (<<m, t>> e. Imagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 n) /\ <<m, t>> e. Imagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 p)))
38	18, 35	opkelimagek 4272	. . . . . . . . . . . . . . . . 17 |- (<<m, t>> e. Imagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 n) <-> t = ((( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 n)"km))
39	24	eqeq2i 2363	. . . . . . . . . . . . . . . . 17 |- (t = (m +o n) <-> t = ((( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 n)"km))
40	38, 39	bitr4i 243	. . . . . . . . . . . . . . . 16 |- (<<m, t>> e. Imagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 n) <-> t = (m +o n))
41	18, 35	opkelimagek 4272	. . . . . . . . . . . . . . . . 17 |- (<<m, t>> e. Imagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 p) <-> t = ((( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 p)"km))
42		dfaddc2 4381	. . . . . . . . . . . . . . . . . 18 |- (m +o p) = ((( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 p)"km)
43	42	eqeq2i 2363	. . . . . . . . . . . . . . . . 17 |- (t = (m +o p) <-> t = ((( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 p)"km))
44	41, 43	bitr4i 243	. . . . . . . . . . . . . . . 16 |- (<<m, t>> e. Imagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 p) <-> t = (m +o p))
45	40, 44	anbi12i 678	. . . . . . . . . . . . . . 15 |- ((<<m, t>> e. Imagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 n) /\ <<m, t>> e. Imagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 p)) <-> (t = (m +o n) /\ t = (m +o p)))
46	37, 45	bitri 240	. . . . . . . . . . . . . 14 |- (<<m, t>> e. (Imagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 n) i^i Imagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 p)) <-> (t = (m +o n) /\ t = (m +o p)))
47	36, 46	bitri 240	. . . . . . . . . . . . 13 |- (<<t, m>> e. `'k(Imagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 n) i^i Imagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 p)) <-> (t = (m +o n) /\ t = (m +o p)))
48	47	exbii 1582	. . . . . . . . . . . 12 |- (E.t<<t, m>> e. `'k(Imagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 n) i^i Imagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 p)) <-> E.t(t = (m +o n) /\ t = (m +o p)))
49	34, 48	bitri 240	. . . . . . . . . . 11 |- (E.t e. _V <<t, m>> e. `'k(Imagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 n) i^i Imagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 p)) <-> E.t(t = (m +o n) /\ t = (m +o p)))
50	18	elimak 4259	. . . . . . . . . . 11 |- (m e. (`'k(Imagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 n) i^i Imagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 p))"k_V) <-> E.t e. _V <<t, m>> e. `'k(Imagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 n) i^i Imagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 p)))
51		vex 2862	. . . . . . . . . . . . 13 |- n e. _V
52	18, 51	addcex 4394	. . . . . . . . . . . 12 |- (m +o n) e. _V
53	52	eqvinc 2966	. . . . . . . . . . 11 |- ((m +o n) = (m +o p) <-> E.t(t = (m +o n) /\ t = (m +o p)))
54	49, 50, 53	3bitr4i 268	. . . . . . . . . 10 |- (m e. (`'k(Imagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 n) i^i Imagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 p))"k_V) <-> (m +o n) = (m +o p))
55	33, 54	anbi12i 678	. . . . . . . . 9 |- ((m e. ∼ (`'kImagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 n)"k{(/)}) /\ m e. (`'k(Imagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 n) i^i Imagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 p))"k_V)) <-> ((m +o n) =/= (/) /\ (m +o n) = (m +o p)))
56	20, 55	bitri 240	. . . . . . . 8 |- (m e. ( ∼ (`'kImagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 n)"k{(/)}) i^i (`'k(Imagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 n) i^i Imagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 p))"k_V)) <-> ((m +o n) =/= (/) /\ (m +o n) = (m +o p)))
57	56	notbii 287	. . . . . . 7 |- (-. m e. ( ∼ (`'kImagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 n)"k{(/)}) i^i (`'k(Imagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 n) i^i Imagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 p))"k_V)) <-> -. ((m +o n) =/= (/) /\ (m +o n) = (m +o p)))
58	19, 57	bitri 240	. . . . . 6 |- (m e. ∼ ( ∼ (`'kImagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 n)"k{(/)}) i^i (`'k(Imagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 n) i^i Imagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 p))"k_V)) <-> -. ((m +o n) =/= (/) /\ (m +o n) = (m +o p)))
59	58	abbi2i 2464	. . . . 5 |- ∼ ( ∼ (`'kImagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 n)"k{(/)}) i^i (`'k(Imagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 n) i^i Imagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 p))"k_V)) = {m | -. ((m +o n) =/= (/) /\ (m +o n) = (m +o p))}
60		addcexlem 4382	. . . . . . . . . . . 12 |- ( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c)) e. _V
61	51	pw1ex 4303	. . . . . . . . . . . . 13 |- ~P1 n e. _V
62	61	pw1ex 4303	. . . . . . . . . . . 12 |- ~P1 ~P1 n e. _V
63	60, 62	imakex 4300	. . . . . . . . . . 11 |- (( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 n) e. _V
64	63	imagekex 4312	. . . . . . . . . 10 |- Imagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 n) e. _V
65	64	cnvkex 4287	. . . . . . . . 9 |- `'kImagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 n) e. _V
66		snex 4111	. . . . . . . . 9 |- {(/)} e. _V
67	65, 66	imakex 4300	. . . . . . . 8 |- (`'kImagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 n)"k{(/)}) e. _V
68	67	complex 4104	. . . . . . 7 |- ∼ (`'kImagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 n)"k{(/)}) e. _V
69		vex 2862	. . . . . . . . . . . . . 14 |- p e. _V
70	69	pw1ex 4303	. . . . . . . . . . . . 13 |- ~P1 p e. _V
71	70	pw1ex 4303	. . . . . . . . . . . 12 |- ~P1 ~P1 p e. _V
72	60, 71	imakex 4300	. . . . . . . . . . 11 |- (( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 p) e. _V
73	72	imagekex 4312	. . . . . . . . . 10 |- Imagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 p) e. _V
74	64, 73	inex 4105	. . . . . . . . 9 |- (Imagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 n) i^i Imagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 p)) e. _V
75	74	cnvkex 4287	. . . . . . . 8 |- `'k(Imagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 n) i^i Imagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 p)) e. _V
76		vvex 4109	. . . . . . . 8 |- _V e. _V
77	75, 76	imakex 4300	. . . . . . 7 |- (`'k(Imagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 n) i^i Imagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 p))"k_V) e. _V
78	68, 77	inex 4105	. . . . . 6 |- ( ∼ (`'kImagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 n)"k{(/)}) i^i (`'k(Imagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 n) i^i Imagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 p))"k_V)) e. _V
79	78	complex 4104	. . . . 5 |- ∼ ( ∼ (`'kImagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 n)"k{(/)}) i^i (`'k(Imagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 n) i^i Imagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 p))"k_V)) e. _V
80	59, 79	eqeltrri 2424	. . . 4 |- {m | -. ((m +o n) =/= (/) /\ (m +o n) = (m +o p))} e. _V
81		abexv 4324	. . . 4 |- {m | N = P} e. _V
82	80, 81	unex 4106	. . 3 |- ({m | -. ((m +o n) =/= (/) /\ (m +o n) = (m +o p))} u. {m | N = P}) e. _V
83	17, 82	eqeltri 2423	. 2 |- {m | (((m +o n) =/= (/) /\ (m +o n) = (m +o p)) -> N = P)} e. _V
84	7, 13, 83	vtocl2g 2918	1 |- ((N e. Nn /\ P e. Nn ) -> {m | (((m +o N) =/= (/) /\ (m +o N) = (m +o P)) -> N = P)} e. _V)

Syntax hints:  -. wn 3   -> wi 4   \/ wo 357   /\ wa 358  E.wex 1541   = wceq 1642   e. wcel 1710  {cab 2339   =/= wne 2516  E.wrex 2615  _Vcvv 2859   ∼ ccompl 3205   \ cdif 3206   u. cun 3207   i^i cin 3208   (+) csymdif 3209  (/)c0 3550  {csn 3737  <<copk 4057  1_cc1c 4134  ~P₁ cpw1 4135  `'_kccnvk 4175   Ins2_k cins2k 4176   Ins3_k cins3k 4177  "_kcimak 4179   SI_k csik 4181  Image_kcimagek 4182   S_k cssetk 4183   Nn cnnc 4373   +o cplc 4375

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 4078  ax-xp 4079  ax-cnv 4080  ax-1c 4081  ax-sset 4082  ax-si 4083  ax-ins2 4084  ax-ins3 4085  ax-typlower 4086  ax-sn 4087

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 2478  df-ne 2518  df-ral 2619  df-rex 2620  df-v 2861  df-sbc 3047  df-nin 3211  df-compl 3212  df-in 3213  df-un 3214  df-dif 3215  df-symdif 3216  df-ss 3259  df-nul 3551  df-pw 3724  df-sn 3741  df-pr 3742  df-opk 4058  df-1c 4136  df-pw1 4137  df-xpk 4185  df-cnvk 4186  df-ins2k 4187  df-ins3k 4188  df-imak 4189  df-cok 4190  df-p6 4191  df-sik 4192  df-ssetk 4193  df-imagek 4194  df-addc 4378

This theorem is referenced by:  preaddccan2  4455