Metamath Proof Explorer

Theorem ulmdvlem2

Description: Lemma for ulmdv . (Contributed by Mario Carneiro, 8-May-2015)

Ref Expression
Hypotheses ulmdv.z ⊢ Z = ℤ ≥ M
ulmdv.s ⊢ φ → S ∈ ℝ ℂ
ulmdv.m ⊢ φ → M ∈ ℤ
ulmdv.f ⊢ φ → F : Z ⟶ ℂ X
ulmdv.g ⊢ φ → G : X ⟶ ℂ
ulmdv.l ⊢ φ ∧ z ∈ X → k ∈ Z ⟼ F ⁡ k ⁡ z ⇝ G ⁡ z
ulmdv.u ⊢ φ → k ∈ Z ⟼ S D F ⁡ k ⇝u ⁡ X H
Assertion ulmdvlem2 ⊢ φ ∧ k ∈ Z → dom ⁡ F ⁡ k S ′ = X

Proof

Step Hyp Ref Expression
1 ulmdv.z ⊢ Z = ℤ ≥ M
2 ulmdv.s ⊢ φ → S ∈ ℝ ℂ
3 ulmdv.m ⊢ φ → M ∈ ℤ
4 ulmdv.f ⊢ φ → F : Z ⟶ ℂ X
5 ulmdv.g ⊢ φ → G : X ⟶ ℂ
6 ulmdv.l ⊢ φ ∧ z ∈ X → k ∈ Z ⟼ F ⁡ k ⁡ z ⇝ G ⁡ z
7 ulmdv.u ⊢ φ → k ∈ Z ⟼ S D F ⁡ k ⇝u ⁡ X H
8 ovex ⊢ S D F ⁡ k ∈ V
9 8 rgenw ⊢ ∀ k ∈ Z S D F ⁡ k ∈ V
10 eqid ⊢ k ∈ Z ⟼ S D F ⁡ k = k ∈ Z ⟼ S D F ⁡ k
11 10 fnmpt ⊢ ∀ k ∈ Z S D F ⁡ k ∈ V → k ∈ Z ⟼ S D F ⁡ k Fn Z
12 9 11 mp1i ⊢ φ → k ∈ Z ⟼ S D F ⁡ k Fn Z
13 ulmf2 ⊢ k ∈ Z ⟼ S D F ⁡ k Fn Z ∧ k ∈ Z ⟼ S D F ⁡ k ⇝u ⁡ X H → k ∈ Z ⟼ S D F ⁡ k : Z ⟶ ℂ X
14 12 7 13 syl2anc ⊢ φ → k ∈ Z ⟼ S D F ⁡ k : Z ⟶ ℂ X
15 14 fvmptelcdm ⊢ φ ∧ k ∈ Z → S D F ⁡ k ∈ ℂ X
16 elmapi ⊢ S D F ⁡ k ∈ ℂ X → F ⁡ k S ′ : X ⟶ ℂ
17 fdm ⊢ F ⁡ k S ′ : X ⟶ ℂ → dom ⁡ F ⁡ k S ′ = X
18 15 16 17 3syl ⊢ φ ∧ k ∈ Z → dom ⁡ F ⁡ k S ′ = X