This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ‘ 𝑆 ) 𝑁 ) )