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

Metamath Proof Explorer

Theorem breprexplemb

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

Ref Expression
Hypotheses breprexp.n ⊢ φ → N ∈ ℕ 0
breprexp.s ⊢ φ → S ∈ ℕ 0
breprexp.z ⊢ φ → Z ∈ ℂ
breprexp.h ⊢ φ → L : 0 ..^ S ⟶ ℂ ℕ
breprexplemb.x ⊢ φ → X ∈ 0 ..^ S
breprexplemb.y ⊢ φ → Y ∈ ℕ
Assertion breprexplemb ⊢ φ → L ⁡ X ⁡ Y ∈ ℂ

Proof

Step Hyp Ref Expression
1 breprexp.n ⊢ φ → N ∈ ℕ 0
2 breprexp.s ⊢ φ → S ∈ ℕ 0
3 breprexp.z ⊢ φ → Z ∈ ℂ
4 breprexp.h ⊢ φ → L : 0 ..^ S ⟶ ℂ ℕ
5 breprexplemb.x ⊢ φ → X ∈ 0 ..^ S
6 breprexplemb.y ⊢ φ → Y ∈ ℕ
7 4 5 ffvelcdmd ⊢ φ → L ⁡ X ∈ ℂ ℕ
8 cnex ⊢ ℂ ∈ V
9 nnex ⊢ ℕ ∈ V
10 8 9 elmap ⊢ L ⁡ X ∈ ℂ ℕ ↔ L ⁡ X : ℕ ⟶ ℂ
11 7 10 sylib ⊢ φ → L ⁡ X : ℕ ⟶ ℂ
12 11 6 ffvelcdmd ⊢ φ → L ⁡ X ⁡ Y ∈ ℂ