Theorem preaddccan2lem1 4455

Description: Lemma for preaddccan2 4456. 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 4385	. . . . . . 7 ⊢ (n = N → (m +c n) = (m +c N))
2	1	neeq1d 2530	. . . . . 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 2468	. . 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 4385	. . . . . . 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 2468	. . 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 2466	. . . 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 3522	. . . 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 2863	. . . . . . . 8 ⊢ m ∈ V
19	18	elcompl 3226	. . . . . . 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 3220	. . . . . . . . 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 4111	. . . . . . . . . . . . . 14 ⊢ ∅ ∈ V
22	21, 18	opkelcnvk 4251	. . . . . . . . . . . . 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 4284	. . . . . . . . . . . . 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 4382	. . . . . . . . . . . . . . 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 4273	. . . . . . . . . . . . . 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 3226	. . . . . . . . . . 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 2519	. . . . . . . . . . 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 2874	. . . . . . . . . . . 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 2863	. . . . . . . . . . . . . . 15 ⊢ t ∈ V
36	35, 18	opkelcnvk 4251	. . . . . . . . . . . . . 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 3220	. . . . . . . . . . . . . . 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 4273	. . . . . . . . . . . . . . . . 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 4273	. . . . . . . . . . . . . . . . 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 4382	. . . . . . . . . . . . . . . . . 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 4260	. . . . . . . . . . 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 2863	. . . . . . . . . . . . 13 ⊢ n ∈ V
52	18, 51	addcex 4395	. . . . . . . . . . . 12 ⊢ (m +c n) ∈ V
53	52	eqvinc 2967	. . . . . . . . . . 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 2465	. . . . 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 4383	. . . . . . . . . . . 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 4304	. . . . . . . . . . . . 13 ⊢ ℘1n ∈ V
62	61	pw1ex 4304	. . . . . . . . . . . 12 ⊢ ℘1℘1n ∈ V
63	60, 62	imakex 4301	. . . . . . . . . . 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 4313	. . . . . . . . . 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 4288	. . . . . . . . 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 4112	. . . . . . . . 9 ⊢ {∅} ∈ V
67	65, 66	imakex 4301	. . . . . . . 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 4105	. . . . . . 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 2863	. . . . . . . . . . . . . 14 ⊢ p ∈ V
70	69	pw1ex 4304	. . . . . . . . . . . . 13 ⊢ ℘1p ∈ V
71	70	pw1ex 4304	. . . . . . . . . . . 12 ⊢ ℘1℘1p ∈ V
72	60, 71	imakex 4301	. . . . . . . . . . 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 4313	. . . . . . . . . 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 4106	. . . . . . . . 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 4288	. . . . . . . 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 4110	. . . . . . . 8 ⊢ V ∈ V
77	75, 76	imakex 4301	. . . . . . 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 4106	. . . . . 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 4105	. . . . 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 4325	. . . 4 ⊢ {m ∣ N = P} ∈ V
82	80, 81	unex 4107	. . 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 2919	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 2517  ∃wrex 2616  Vcvv 2860   ∼ ccompl 3206   ∖ cdif 3207   ∪ cun 3208   ∩ cin 3209   ⊕ csymdif 3210  ∅c0 3551  {csn 3738  ⟪copk 4058  1_cc1c 4135  ℘₁cpw1 4136  ^◡_kccnvk 4176   Ins2_k cins2k 4177   Ins3_k cins3k 4178   “_k cimak 4180   SI_k csik 4182  Image_kcimagek 4183   S_k cssetk 4184   Nn cnnc 4374   +_c cplc 4376

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

This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-nan 1288  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2340  df-cleq 2346  df-clel 2349  df-nfc 2479  df-ne 2519  df-ral 2620  df-rex 2621  df-v 2862  df-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-pw 3725  df-sn 3742  df-pr 3743  df-opk 4059  df-1c 4137  df-pw1 4138  df-xpk 4186  df-cnvk 4187  df-ins2k 4188  df-ins3k 4189  df-imak 4190  df-cok 4191  df-p6 4192  df-sik 4193  df-ssetk 4194  df-imagek 4195  df-addc 4379

This theorem is referenced by:  preaddccan2  4456