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

Syntax hints:  ¬ wn 3   → wi 4   ∨ wo 357   ∧ wa 358  ∃wex 1541   = wceq 1642   ∈ wcel 1710  {cab 2339   ≠ wne 2516  ∃wrex 2615  Vcvv 2859   ∼ ccompl 3205   ∖ cdif 3206   ∪ cun 3207   ∩ cin 3208   ⊕ csymdif 3209  ∅c0 3550  {csn 3737  ⟪copk 4057  1_cc1c 4134  ℘₁cpw1 4135  ^◡_kccnvk 4175   Ins2_k cins2k 4176   Ins3_k cins3k 4177   “_k cimak 4179   SI_k csik 4181  Image_kcimagek 4182   S_k cssetk 4183   Nn cnnc 4373   +_c 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