Theorem reprfz1

Description: Corollary of reprinfz1 . (Contributed by Thierry Arnoux, 14-Dec-2021)

	Ref	Expression
Hypotheses	reprfz1.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
	reprfz1.s	⊢ ( 𝜑 → 𝑆 ∈ ℕ0 )
Assertion	reprfz1	⊢ ( 𝜑 → ( ℕ ( repr ‘ 𝑆 ) 𝑁 ) = ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		reprfz1.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
2		reprfz1.s	⊢ ( 𝜑 → 𝑆 ∈ ℕ0 )
3		ssidd	⊢ ( 𝜑 → ℕ ⊆ ℕ )
4	1 2 3	reprinfz1	⊢ ( 𝜑 → ( ℕ ( repr ‘ 𝑆 ) 𝑁 ) = ( ( ℕ ∩ ( 1 ... 𝑁 ) ) ( repr ‘ 𝑆 ) 𝑁 ) )
5		fz1ssnn	⊢ ( 1 ... 𝑁 ) ⊆ ℕ
6		dfss	⊢ ( ( 1 ... 𝑁 ) ⊆ ℕ ↔ ( 1 ... 𝑁 ) = ( ( 1 ... 𝑁 ) ∩ ℕ ) )
7	5 6	mpbi	⊢ ( 1 ... 𝑁 ) = ( ( 1 ... 𝑁 ) ∩ ℕ )
8		incom	⊢ ( ( 1 ... 𝑁 ) ∩ ℕ ) = ( ℕ ∩ ( 1 ... 𝑁 ) )
9	7 8	eqtri	⊢ ( 1 ... 𝑁 ) = ( ℕ ∩ ( 1 ... 𝑁 ) )
10	9	oveq1i	⊢ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑁 ) = ( ( ℕ ∩ ( 1 ... 𝑁 ) ) ( repr ‘ 𝑆 ) 𝑁 )
11	4 10	eqtr4di	⊢ ( 𝜑 → ( ℕ ( repr ‘ 𝑆 ) 𝑁 ) = ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑁 ) )