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

Metamath Proof Explorer

Theorem reprfi2

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

Ref Expression
Hypotheses reprinfz1.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
reprinfz1.s ⊢ ( 𝜑 → 𝑆 ∈ ℕ0 )
reprinfz1.a ⊢ ( 𝜑 → 𝐴 ⊆ ℕ )
Assertion reprfi2 ( 𝜑 → ( 𝐴 ( repr ‘ 𝑆 ) 𝑁 ) ∈ Fin )

Proof

Step Hyp Ref Expression
1 reprinfz1.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
2 reprinfz1.s ⊢ ( 𝜑 → 𝑆 ∈ ℕ0 )
3 reprinfz1.a ⊢ ( 𝜑 → 𝐴 ⊆ ℕ )
4 1 2 3 reprinfz1 ⊢ ( 𝜑 → ( 𝐴 ( repr ‘ 𝑆 ) 𝑁 ) = ( ( 𝐴 ∩ ( 1 ... 𝑁 ) ) ( repr ‘ 𝑆 ) 𝑁 ) )
5 inss2 ⊢ ( 𝐴 ∩ ( 1 ... 𝑁 ) ) ⊆ ( 1 ... 𝑁 )
6 fz1ssnn ⊢ ( 1 ... 𝑁 ) ⊆ ℕ
7 5 6 sstri ⊢ ( 𝐴 ∩ ( 1 ... 𝑁 ) ) ⊆ ℕ
8 7 a1i ⊢ ( 𝜑 → ( 𝐴 ∩ ( 1 ... 𝑁 ) ) ⊆ ℕ )
9 1 nn0zd ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
10 fzfi ⊢ ( 1 ... 𝑁 ) ∈ Fin
11 10 a1i ⊢ ( 𝜑 → ( 1 ... 𝑁 ) ∈ Fin )
12 5 a1i ⊢ ( 𝜑 → ( 𝐴 ∩ ( 1 ... 𝑁 ) ) ⊆ ( 1 ... 𝑁 ) )
13 11 12 ssfid ⊢ ( 𝜑 → ( 𝐴 ∩ ( 1 ... 𝑁 ) ) ∈ Fin )
14 8 9 2 13 reprfi ⊢ ( 𝜑 → ( ( 𝐴 ∩ ( 1 ... 𝑁 ) ) ( repr ‘ 𝑆 ) 𝑁 ) ∈ Fin )
15 4 14 eqeltrd ⊢ ( 𝜑 → ( 𝐴 ( repr ‘ 𝑆 ) 𝑁 ) ∈ Fin )