Theorem smupp1

Description: The initial element of the partial sum sequence. (Contributed by Mario Carneiro, 9-Sep-2016)

	Ref	Expression
Hypotheses	smuval.a	⊢ ( 𝜑 → 𝐴 ⊆ ℕ0 )
	smuval.b	⊢ ( 𝜑 → 𝐵 ⊆ ℕ0 )
	smuval.p	⊢ 𝑃 = seq 0 ( ( 𝑝 ∈ 𝒫 ℕ0 , 𝑚 ∈ ℕ0 ↦ ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ 𝐴 ∧ ( 𝑛 − 𝑚 ) ∈ 𝐵 ) } ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) )
	smuval.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
Assertion	smupp1	⊢ ( 𝜑 → ( 𝑃 ‘ ( 𝑁 + 1 ) ) = ( ( 𝑃 ‘ 𝑁 ) sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑁 ∈ 𝐴 ∧ ( 𝑛 − 𝑁 ) ∈ 𝐵 ) } ) )

Proof

Step	Hyp	Ref	Expression
1		smuval.a	⊢ ( 𝜑 → 𝐴 ⊆ ℕ0 )
2		smuval.b	⊢ ( 𝜑 → 𝐵 ⊆ ℕ0 )
3		smuval.p	⊢ 𝑃 = seq 0 ( ( 𝑝 ∈ 𝒫 ℕ0 , 𝑚 ∈ ℕ0 ↦ ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ 𝐴 ∧ ( 𝑛 − 𝑚 ) ∈ 𝐵 ) } ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) )
4		smuval.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
5		nn0uz	⊢ ℕ0 = ( ℤ≥ ‘ 0 )
6	4 5	eleqtrdi	⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 0 ) )
7		seqp1	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 0 ) → ( seq 0 ( ( 𝑝 ∈ 𝒫 ℕ0 , 𝑚 ∈ ℕ0 ↦ ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ 𝐴 ∧ ( 𝑛 − 𝑚 ) ∈ 𝐵 ) } ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) ‘ ( 𝑁 + 1 ) ) = ( ( seq 0 ( ( 𝑝 ∈ 𝒫 ℕ0 , 𝑚 ∈ ℕ0 ↦ ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ 𝐴 ∧ ( 𝑛 − 𝑚 ) ∈ 𝐵 ) } ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) ‘ 𝑁 ) ( 𝑝 ∈ 𝒫 ℕ0 , 𝑚 ∈ ℕ0 ↦ ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ 𝐴 ∧ ( 𝑛 − 𝑚 ) ∈ 𝐵 ) } ) ) ( ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ‘ ( 𝑁 + 1 ) ) ) )
8	6 7	syl	⊢ ( 𝜑 → ( seq 0 ( ( 𝑝 ∈ 𝒫 ℕ0 , 𝑚 ∈ ℕ0 ↦ ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ 𝐴 ∧ ( 𝑛 − 𝑚 ) ∈ 𝐵 ) } ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) ‘ ( 𝑁 + 1 ) ) = ( ( seq 0 ( ( 𝑝 ∈ 𝒫 ℕ0 , 𝑚 ∈ ℕ0 ↦ ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ 𝐴 ∧ ( 𝑛 − 𝑚 ) ∈ 𝐵 ) } ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) ‘ 𝑁 ) ( 𝑝 ∈ 𝒫 ℕ0 , 𝑚 ∈ ℕ0 ↦ ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ 𝐴 ∧ ( 𝑛 − 𝑚 ) ∈ 𝐵 ) } ) ) ( ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ‘ ( 𝑁 + 1 ) ) ) )
9	3	fveq1i	⊢ ( 𝑃 ‘ ( 𝑁 + 1 ) ) = ( seq 0 ( ( 𝑝 ∈ 𝒫 ℕ0 , 𝑚 ∈ ℕ0 ↦ ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ 𝐴 ∧ ( 𝑛 − 𝑚 ) ∈ 𝐵 ) } ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) ‘ ( 𝑁 + 1 ) )
10	3	fveq1i	⊢ ( 𝑃 ‘ 𝑁 ) = ( seq 0 ( ( 𝑝 ∈ 𝒫 ℕ0 , 𝑚 ∈ ℕ0 ↦ ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ 𝐴 ∧ ( 𝑛 − 𝑚 ) ∈ 𝐵 ) } ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) ‘ 𝑁 )
11	10	oveq1i	⊢ ( ( 𝑃 ‘ 𝑁 ) ( 𝑝 ∈ 𝒫 ℕ0 , 𝑚 ∈ ℕ0 ↦ ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ 𝐴 ∧ ( 𝑛 − 𝑚 ) ∈ 𝐵 ) } ) ) ( ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ‘ ( 𝑁 + 1 ) ) ) = ( ( seq 0 ( ( 𝑝 ∈ 𝒫 ℕ0 , 𝑚 ∈ ℕ0 ↦ ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ 𝐴 ∧ ( 𝑛 − 𝑚 ) ∈ 𝐵 ) } ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) ‘ 𝑁 ) ( 𝑝 ∈ 𝒫 ℕ0 , 𝑚 ∈ ℕ0 ↦ ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ 𝐴 ∧ ( 𝑛 − 𝑚 ) ∈ 𝐵 ) } ) ) ( ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ‘ ( 𝑁 + 1 ) ) )
12	8 9 11	3eqtr4g	⊢ ( 𝜑 → ( 𝑃 ‘ ( 𝑁 + 1 ) ) = ( ( 𝑃 ‘ 𝑁 ) ( 𝑝 ∈ 𝒫 ℕ0 , 𝑚 ∈ ℕ0 ↦ ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ 𝐴 ∧ ( 𝑛 − 𝑚 ) ∈ 𝐵 ) } ) ) ( ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ‘ ( 𝑁 + 1 ) ) ) )
13		1nn0	⊢ 1 ∈ ℕ0
14	13	a1i	⊢ ( 𝜑 → 1 ∈ ℕ0 )
15	4 14	nn0addcld	⊢ ( 𝜑 → ( 𝑁 + 1 ) ∈ ℕ0 )
16		eqeq1	⊢ ( 𝑛 = ( 𝑁 + 1 ) → ( 𝑛 = 0 ↔ ( 𝑁 + 1 ) = 0 ) )
17		oveq1	⊢ ( 𝑛 = ( 𝑁 + 1 ) → ( 𝑛 − 1 ) = ( ( 𝑁 + 1 ) − 1 ) )
18	16 17	ifbieq2d	⊢ ( 𝑛 = ( 𝑁 + 1 ) → if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) = if ( ( 𝑁 + 1 ) = 0 , ∅ , ( ( 𝑁 + 1 ) − 1 ) ) )
19		eqid	⊢ ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) = ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) )
20		0ex	⊢ ∅ ∈ V
21		ovex	⊢ ( ( 𝑁 + 1 ) − 1 ) ∈ V
22	20 21	ifex	⊢ if ( ( 𝑁 + 1 ) = 0 , ∅ , ( ( 𝑁 + 1 ) − 1 ) ) ∈ V
23	18 19 22	fvmpt	⊢ ( ( 𝑁 + 1 ) ∈ ℕ0 → ( ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ‘ ( 𝑁 + 1 ) ) = if ( ( 𝑁 + 1 ) = 0 , ∅ , ( ( 𝑁 + 1 ) − 1 ) ) )
24	15 23	syl	⊢ ( 𝜑 → ( ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ‘ ( 𝑁 + 1 ) ) = if ( ( 𝑁 + 1 ) = 0 , ∅ , ( ( 𝑁 + 1 ) − 1 ) ) )
25		nn0p1nn	⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 + 1 ) ∈ ℕ )
26	4 25	syl	⊢ ( 𝜑 → ( 𝑁 + 1 ) ∈ ℕ )
27	26	nnne0d	⊢ ( 𝜑 → ( 𝑁 + 1 ) ≠ 0 )
28		ifnefalse	⊢ ( ( 𝑁 + 1 ) ≠ 0 → if ( ( 𝑁 + 1 ) = 0 , ∅ , ( ( 𝑁 + 1 ) − 1 ) ) = ( ( 𝑁 + 1 ) − 1 ) )
29	27 28	syl	⊢ ( 𝜑 → if ( ( 𝑁 + 1 ) = 0 , ∅ , ( ( 𝑁 + 1 ) − 1 ) ) = ( ( 𝑁 + 1 ) − 1 ) )
30	4	nn0cnd	⊢ ( 𝜑 → 𝑁 ∈ ℂ )
31	14	nn0cnd	⊢ ( 𝜑 → 1 ∈ ℂ )
32	30 31	pncand	⊢ ( 𝜑 → ( ( 𝑁 + 1 ) − 1 ) = 𝑁 )
33	24 29 32	3eqtrd	⊢ ( 𝜑 → ( ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ‘ ( 𝑁 + 1 ) ) = 𝑁 )
34	33	oveq2d	⊢ ( 𝜑 → ( ( 𝑃 ‘ 𝑁 ) ( 𝑝 ∈ 𝒫 ℕ0 , 𝑚 ∈ ℕ0 ↦ ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ 𝐴 ∧ ( 𝑛 − 𝑚 ) ∈ 𝐵 ) } ) ) ( ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ‘ ( 𝑁 + 1 ) ) ) = ( ( 𝑃 ‘ 𝑁 ) ( 𝑝 ∈ 𝒫 ℕ0 , 𝑚 ∈ ℕ0 ↦ ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ 𝐴 ∧ ( 𝑛 − 𝑚 ) ∈ 𝐵 ) } ) ) 𝑁 ) )
35	1 2 3	smupf	⊢ ( 𝜑 → 𝑃 : ℕ0 ⟶ 𝒫 ℕ0 )
36	35 4	ffvelrnd	⊢ ( 𝜑 → ( 𝑃 ‘ 𝑁 ) ∈ 𝒫 ℕ0 )
37		simpl	⊢ ( ( 𝑥 = ( 𝑃 ‘ 𝑁 ) ∧ 𝑦 = 𝑁 ) → 𝑥 = ( 𝑃 ‘ 𝑁 ) )
38		simpr	⊢ ( ( 𝑥 = ( 𝑃 ‘ 𝑁 ) ∧ 𝑦 = 𝑁 ) → 𝑦 = 𝑁 )
39	38	eleq1d	⊢ ( ( 𝑥 = ( 𝑃 ‘ 𝑁 ) ∧ 𝑦 = 𝑁 ) → ( 𝑦 ∈ 𝐴 ↔ 𝑁 ∈ 𝐴 ) )
40	38	oveq2d	⊢ ( ( 𝑥 = ( 𝑃 ‘ 𝑁 ) ∧ 𝑦 = 𝑁 ) → ( 𝑘 − 𝑦 ) = ( 𝑘 − 𝑁 ) )
41	40	eleq1d	⊢ ( ( 𝑥 = ( 𝑃 ‘ 𝑁 ) ∧ 𝑦 = 𝑁 ) → ( ( 𝑘 − 𝑦 ) ∈ 𝐵 ↔ ( 𝑘 − 𝑁 ) ∈ 𝐵 ) )
42	39 41	anbi12d	⊢ ( ( 𝑥 = ( 𝑃 ‘ 𝑁 ) ∧ 𝑦 = 𝑁 ) → ( ( 𝑦 ∈ 𝐴 ∧ ( 𝑘 − 𝑦 ) ∈ 𝐵 ) ↔ ( 𝑁 ∈ 𝐴 ∧ ( 𝑘 − 𝑁 ) ∈ 𝐵 ) ) )
43	42	rabbidv	⊢ ( ( 𝑥 = ( 𝑃 ‘ 𝑁 ) ∧ 𝑦 = 𝑁 ) → { 𝑘 ∈ ℕ0 ∣ ( 𝑦 ∈ 𝐴 ∧ ( 𝑘 − 𝑦 ) ∈ 𝐵 ) } = { 𝑘 ∈ ℕ0 ∣ ( 𝑁 ∈ 𝐴 ∧ ( 𝑘 − 𝑁 ) ∈ 𝐵 ) } )
44		oveq1	⊢ ( 𝑘 = 𝑛 → ( 𝑘 − 𝑁 ) = ( 𝑛 − 𝑁 ) )
45	44	eleq1d	⊢ ( 𝑘 = 𝑛 → ( ( 𝑘 − 𝑁 ) ∈ 𝐵 ↔ ( 𝑛 − 𝑁 ) ∈ 𝐵 ) )
46	45	anbi2d	⊢ ( 𝑘 = 𝑛 → ( ( 𝑁 ∈ 𝐴 ∧ ( 𝑘 − 𝑁 ) ∈ 𝐵 ) ↔ ( 𝑁 ∈ 𝐴 ∧ ( 𝑛 − 𝑁 ) ∈ 𝐵 ) ) )
47	46	cbvrabv	⊢ { 𝑘 ∈ ℕ0 ∣ ( 𝑁 ∈ 𝐴 ∧ ( 𝑘 − 𝑁 ) ∈ 𝐵 ) } = { 𝑛 ∈ ℕ0 ∣ ( 𝑁 ∈ 𝐴 ∧ ( 𝑛 − 𝑁 ) ∈ 𝐵 ) }
48	43 47	eqtrdi	⊢ ( ( 𝑥 = ( 𝑃 ‘ 𝑁 ) ∧ 𝑦 = 𝑁 ) → { 𝑘 ∈ ℕ0 ∣ ( 𝑦 ∈ 𝐴 ∧ ( 𝑘 − 𝑦 ) ∈ 𝐵 ) } = { 𝑛 ∈ ℕ0 ∣ ( 𝑁 ∈ 𝐴 ∧ ( 𝑛 − 𝑁 ) ∈ 𝐵 ) } )
49	37 48	oveq12d	⊢ ( ( 𝑥 = ( 𝑃 ‘ 𝑁 ) ∧ 𝑦 = 𝑁 ) → ( 𝑥 sadd { 𝑘 ∈ ℕ0 ∣ ( 𝑦 ∈ 𝐴 ∧ ( 𝑘 − 𝑦 ) ∈ 𝐵 ) } ) = ( ( 𝑃 ‘ 𝑁 ) sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑁 ∈ 𝐴 ∧ ( 𝑛 − 𝑁 ) ∈ 𝐵 ) } ) )
50		oveq1	⊢ ( 𝑝 = 𝑥 → ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ 𝐴 ∧ ( 𝑛 − 𝑚 ) ∈ 𝐵 ) } ) = ( 𝑥 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ 𝐴 ∧ ( 𝑛 − 𝑚 ) ∈ 𝐵 ) } ) )
51		eleq1w	⊢ ( 𝑚 = 𝑦 → ( 𝑚 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴 ) )
52		oveq2	⊢ ( 𝑚 = 𝑦 → ( 𝑛 − 𝑚 ) = ( 𝑛 − 𝑦 ) )
53	52	eleq1d	⊢ ( 𝑚 = 𝑦 → ( ( 𝑛 − 𝑚 ) ∈ 𝐵 ↔ ( 𝑛 − 𝑦 ) ∈ 𝐵 ) )
54	51 53	anbi12d	⊢ ( 𝑚 = 𝑦 → ( ( 𝑚 ∈ 𝐴 ∧ ( 𝑛 − 𝑚 ) ∈ 𝐵 ) ↔ ( 𝑦 ∈ 𝐴 ∧ ( 𝑛 − 𝑦 ) ∈ 𝐵 ) ) )
55	54	rabbidv	⊢ ( 𝑚 = 𝑦 → { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ 𝐴 ∧ ( 𝑛 − 𝑚 ) ∈ 𝐵 ) } = { 𝑛 ∈ ℕ0 ∣ ( 𝑦 ∈ 𝐴 ∧ ( 𝑛 − 𝑦 ) ∈ 𝐵 ) } )
56		oveq1	⊢ ( 𝑘 = 𝑛 → ( 𝑘 − 𝑦 ) = ( 𝑛 − 𝑦 ) )
57	56	eleq1d	⊢ ( 𝑘 = 𝑛 → ( ( 𝑘 − 𝑦 ) ∈ 𝐵 ↔ ( 𝑛 − 𝑦 ) ∈ 𝐵 ) )
58	57	anbi2d	⊢ ( 𝑘 = 𝑛 → ( ( 𝑦 ∈ 𝐴 ∧ ( 𝑘 − 𝑦 ) ∈ 𝐵 ) ↔ ( 𝑦 ∈ 𝐴 ∧ ( 𝑛 − 𝑦 ) ∈ 𝐵 ) ) )
59	58	cbvrabv	⊢ { 𝑘 ∈ ℕ0 ∣ ( 𝑦 ∈ 𝐴 ∧ ( 𝑘 − 𝑦 ) ∈ 𝐵 ) } = { 𝑛 ∈ ℕ0 ∣ ( 𝑦 ∈ 𝐴 ∧ ( 𝑛 − 𝑦 ) ∈ 𝐵 ) }
60	55 59	eqtr4di	⊢ ( 𝑚 = 𝑦 → { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ 𝐴 ∧ ( 𝑛 − 𝑚 ) ∈ 𝐵 ) } = { 𝑘 ∈ ℕ0 ∣ ( 𝑦 ∈ 𝐴 ∧ ( 𝑘 − 𝑦 ) ∈ 𝐵 ) } )
61	60	oveq2d	⊢ ( 𝑚 = 𝑦 → ( 𝑥 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ 𝐴 ∧ ( 𝑛 − 𝑚 ) ∈ 𝐵 ) } ) = ( 𝑥 sadd { 𝑘 ∈ ℕ0 ∣ ( 𝑦 ∈ 𝐴 ∧ ( 𝑘 − 𝑦 ) ∈ 𝐵 ) } ) )
62	50 61	cbvmpov	⊢ ( 𝑝 ∈ 𝒫 ℕ0 , 𝑚 ∈ ℕ0 ↦ ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ 𝐴 ∧ ( 𝑛 − 𝑚 ) ∈ 𝐵 ) } ) ) = ( 𝑥 ∈ 𝒫 ℕ0 , 𝑦 ∈ ℕ0 ↦ ( 𝑥 sadd { 𝑘 ∈ ℕ0 ∣ ( 𝑦 ∈ 𝐴 ∧ ( 𝑘 − 𝑦 ) ∈ 𝐵 ) } ) )
63		ovex	⊢ ( ( 𝑃 ‘ 𝑁 ) sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑁 ∈ 𝐴 ∧ ( 𝑛 − 𝑁 ) ∈ 𝐵 ) } ) ∈ V
64	49 62 63	ovmpoa	⊢ ( ( ( 𝑃 ‘ 𝑁 ) ∈ 𝒫 ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝑃 ‘ 𝑁 ) ( 𝑝 ∈ 𝒫 ℕ0 , 𝑚 ∈ ℕ0 ↦ ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ 𝐴 ∧ ( 𝑛 − 𝑚 ) ∈ 𝐵 ) } ) ) 𝑁 ) = ( ( 𝑃 ‘ 𝑁 ) sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑁 ∈ 𝐴 ∧ ( 𝑛 − 𝑁 ) ∈ 𝐵 ) } ) )
65	36 4 64	syl2anc	⊢ ( 𝜑 → ( ( 𝑃 ‘ 𝑁 ) ( 𝑝 ∈ 𝒫 ℕ0 , 𝑚 ∈ ℕ0 ↦ ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ 𝐴 ∧ ( 𝑛 − 𝑚 ) ∈ 𝐵 ) } ) ) 𝑁 ) = ( ( 𝑃 ‘ 𝑁 ) sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑁 ∈ 𝐴 ∧ ( 𝑛 − 𝑁 ) ∈ 𝐵 ) } ) )
66	12 34 65	3eqtrd	⊢ ( 𝜑 → ( 𝑃 ‘ ( 𝑁 + 1 ) ) = ( ( 𝑃 ‘ 𝑁 ) sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑁 ∈ 𝐴 ∧ ( 𝑛 − 𝑁 ) ∈ 𝐵 ) } ) )