Theorem smup0

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 ) ) ) )
Assertion	smup0	⊢ ( 𝜑 → ( 𝑃 ‘ 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		0z	⊢ 0 ∈ ℤ
5	3	fveq1i	⊢ ( 𝑃 ‘ 0 ) = ( seq 0 ( ( 𝑝 ∈ 𝒫 ℕ0 , 𝑚 ∈ ℕ0 ↦ ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ 𝐴 ∧ ( 𝑛 − 𝑚 ) ∈ 𝐵 ) } ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) ‘ 0 )
6		seq1	⊢ ( 0 ∈ ℤ → ( seq 0 ( ( 𝑝 ∈ 𝒫 ℕ0 , 𝑚 ∈ ℕ0 ↦ ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ 𝐴 ∧ ( 𝑛 − 𝑚 ) ∈ 𝐵 ) } ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) ‘ 0 ) = ( ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ‘ 0 ) )
7	5 6	eqtrid	⊢ ( 0 ∈ ℤ → ( 𝑃 ‘ 0 ) = ( ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ‘ 0 ) )
8	4 7	mp1i	⊢ ( 𝜑 → ( 𝑃 ‘ 0 ) = ( ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ‘ 0 ) )
9		0nn0	⊢ 0 ∈ ℕ0
10		iftrue	⊢ ( 𝑛 = 0 → if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) = ∅ )
11		eqid	⊢ ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) = ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) )
12		0ex	⊢ ∅ ∈ V
13	10 11 12	fvmpt	⊢ ( 0 ∈ ℕ0 → ( ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ‘ 0 ) = ∅ )
14	9 13	mp1i	⊢ ( 𝜑 → ( ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ‘ 0 ) = ∅ )
15	8 14	eqtrd	⊢ ( 𝜑 → ( 𝑃 ‘ 0 ) = ∅ )