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
|- ( ph -> ( x e. A |-> B ) e. MblFn )
mbfmptcl.2
|- ( ( ph /\ x e. A ) -> B e. V )
Assertion mbfmptcl
|- ( ( ph /\ x e. A ) -> B e. CC )

Proof

Step Hyp Ref Expression
1 mbfmptcl.1
 |-  ( ph -> ( x e. A |-> B ) e. MblFn )
2 mbfmptcl.2
 |-  ( ( ph /\ x e. A ) -> B e. V )
3 mbff
 |-  ( ( x e. A |-> B ) e. MblFn -> ( x e. A |-> B ) : dom ( x e. A |-> B ) --> CC )
4 1 3 syl
 |-  ( ph -> ( x e. A |-> B ) : dom ( x e. A |-> B ) --> CC )
5 2 ralrimiva
 |-  ( ph -> A. x e. A B e. V )
6 dmmptg
 |-  ( A. x e. A B e. V -> dom ( x e. A |-> B ) = A )
7 5 6 syl
 |-  ( ph -> dom ( x e. A |-> B ) = A )
8 7 feq2d
 |-  ( ph -> ( ( x e. A |-> B ) : dom ( x e. A |-> B ) --> CC <-> ( x e. A |-> B ) : A --> CC ) )
9 4 8 mpbid
 |-  ( ph -> ( x e. A |-> B ) : A --> CC )
10 9 fvmptelrn
 |-  ( ( ph /\ x e. A ) -> B e. CC )