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

Metamath Proof Explorer

Theorem mbfmptcl

Description: Lemma for the MblFn predicate applied to a mapping operation. (Contributed by Mario Carneiro, 11-Aug-2014)

Ref Expression
Hypotheses mbfmptcl.1 ⊢ φ → x ∈ A ⟼ B ∈ MblFn
mbfmptcl.2 ⊢ φ ∧ x ∈ A → B ∈ V
Assertion mbfmptcl ⊢ φ ∧ x ∈ A → B ∈ ℂ

Proof

Step Hyp Ref Expression
1 mbfmptcl.1 ⊢ φ → x ∈ A ⟼ B ∈ MblFn
2 mbfmptcl.2 ⊢ φ ∧ x ∈ A → B ∈ V
3 mbff ⊢ x ∈ A ⟼ B ∈ MblFn → x ∈ A ⟼ B : dom ⁡ x ∈ A ⟼ B ⟶ ℂ
4 1 3 syl ⊢ φ → x ∈ A ⟼ B : dom ⁡ x ∈ A ⟼ B ⟶ ℂ
5 2 ralrimiva ⊢ φ → ∀ x ∈ A B ∈ V
6 dmmptg ⊢ ∀ x ∈ A B ∈ V → dom ⁡ x ∈ A ⟼ B = A
7 5 6 syl ⊢ φ → dom ⁡ x ∈ A ⟼ B = A
8 7 feq2d ⊢ φ → x ∈ A ⟼ B : dom ⁡ x ∈ A ⟼ B ⟶ ℂ ↔ x ∈ A ⟼ B : A ⟶ ℂ
9 4 8 mpbid ⊢ φ → x ∈ A ⟼ B : A ⟶ ℂ
10 9 fvmptelcdm ⊢ φ ∧ x ∈ A → B ∈ ℂ