Theorem breprexplemb

Description: Lemma for breprexp (closure). (Contributed by Thierry Arnoux, 7-Dec-2021)

	Ref	Expression
Hypotheses	breprexp.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
	breprexp.s	⊢ ( 𝜑 → 𝑆 ∈ ℕ0 )
	breprexp.z	⊢ ( 𝜑 → 𝑍 ∈ ℂ )
	breprexp.h	⊢ ( 𝜑 → 𝐿 : ( 0 ..^ 𝑆 ) ⟶ ( ℂ ↑m ℕ ) )
	breprexplemb.x	⊢ ( 𝜑 → 𝑋 ∈ ( 0 ..^ 𝑆 ) )
	breprexplemb.y	⊢ ( 𝜑 → 𝑌 ∈ ℕ )
Assertion	breprexplemb	⊢ ( 𝜑 → ( ( 𝐿 ‘ 𝑋 ) ‘ 𝑌 ) ∈ ℂ )

Proof

Step	Hyp	Ref	Expression
1		breprexp.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
2		breprexp.s	⊢ ( 𝜑 → 𝑆 ∈ ℕ0 )
3		breprexp.z	⊢ ( 𝜑 → 𝑍 ∈ ℂ )
4		breprexp.h	⊢ ( 𝜑 → 𝐿 : ( 0 ..^ 𝑆 ) ⟶ ( ℂ ↑m ℕ ) )
5		breprexplemb.x	⊢ ( 𝜑 → 𝑋 ∈ ( 0 ..^ 𝑆 ) )
6		breprexplemb.y	⊢ ( 𝜑 → 𝑌 ∈ ℕ )
7	4 5	ffvelrnd	⊢ ( 𝜑 → ( 𝐿 ‘ 𝑋 ) ∈ ( ℂ ↑m ℕ ) )
8		cnex	⊢ ℂ ∈ V
9		nnex	⊢ ℕ ∈ V
10	8 9	elmap	⊢ ( ( 𝐿 ‘ 𝑋 ) ∈ ( ℂ ↑m ℕ ) ↔ ( 𝐿 ‘ 𝑋 ) : ℕ ⟶ ℂ )
11	7 10	sylib	⊢ ( 𝜑 → ( 𝐿 ‘ 𝑋 ) : ℕ ⟶ ℂ )
12	11 6	ffvelrnd	⊢ ( 𝜑 → ( ( 𝐿 ‘ 𝑋 ) ‘ 𝑌 ) ∈ ℂ )