MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mbfmptcl Structured version   Unicode version

Theorem mbfmptcl 22226
Description: Lemma for the MblFn predicate applied to a mapping operation. (Contributed by Mario Carneiro, 11-Aug-2014.)
Hypotheses
Ref Expression
mbfmptcl.1  |-  ( ph  ->  ( x  e.  A  |->  B )  e. MblFn )
mbfmptcl.2  |-  ( (
ph  /\  x  e.  A )  ->  B  e.  V )
Assertion
Ref Expression
mbfmptcl  |-  ( (
ph  /\  x  e.  A )  ->  B  e.  CC )
Distinct variable groups:    x, A    ph, x
Allowed substitution hints:    B( x)    V( x)

Proof of Theorem mbfmptcl
StepHypRef Expression
1 mbfmptcl.1 . . . . 5  |-  ( ph  ->  ( x  e.  A  |->  B )  e. MblFn )
2 mbff 22216 . . . . 5  |-  ( ( x  e.  A  |->  B )  e. MblFn  ->  ( x  e.  A  |->  B ) : dom  ( x  e.  A  |->  B ) --> CC )
31, 2syl 17 . . . 4  |-  ( ph  ->  ( x  e.  A  |->  B ) : dom  ( x  e.  A  |->  B ) --> CC )
4 mbfmptcl.2 . . . . . . 7  |-  ( (
ph  /\  x  e.  A )  ->  B  e.  V )
54ralrimiva 2815 . . . . . 6  |-  ( ph  ->  A. x  e.  A  B  e.  V )
6 dmmptg 5439 . . . . . 6  |-  ( A. x  e.  A  B  e.  V  ->  dom  (
x  e.  A  |->  B )  =  A )
75, 6syl 17 . . . . 5  |-  ( ph  ->  dom  ( x  e.  A  |->  B )  =  A )
87feq2d 5655 . . . 4  |-  ( ph  ->  ( ( x  e.  A  |->  B ) : dom  ( x  e.  A  |->  B ) --> CC  <->  ( x  e.  A  |->  B ) : A --> CC ) )
93, 8mpbid 210 . . 3  |-  ( ph  ->  ( x  e.  A  |->  B ) : A --> CC )
10 eqid 2400 . . . 4  |-  ( x  e.  A  |->  B )  =  ( x  e.  A  |->  B )
1110fmpt 5984 . . 3  |-  ( A. x  e.  A  B  e.  CC  <->  ( x  e.  A  |->  B ) : A --> CC )
129, 11sylibr 212 . 2  |-  ( ph  ->  A. x  e.  A  B  e.  CC )
1312r19.21bi 2770 1  |-  ( (
ph  /\  x  e.  A )  ->  B  e.  CC )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367    = wceq 1403    e. wcel 1840   A.wral 2751    |-> cmpt 4450   dom cdm 4940   -->wf 5519   CCcc 9438  MblFncmbf 22205
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1637  ax-4 1650  ax-5 1723  ax-6 1769  ax-7 1812  ax-8 1842  ax-9 1844  ax-10 1859  ax-11 1864  ax-12 1876  ax-13 2024  ax-ext 2378  ax-sep 4514  ax-nul 4522  ax-pow 4569  ax-pr 4627  ax-un 6528  ax-cnex 9496  ax-resscn 9497
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 974  df-tru 1406  df-ex 1632  df-nf 1636  df-sb 1762  df-eu 2240  df-mo 2241  df-clab 2386  df-cleq 2392  df-clel 2395  df-nfc 2550  df-ne 2598  df-ral 2756  df-rex 2757  df-rab 2760  df-v 3058  df-sbc 3275  df-dif 3414  df-un 3416  df-in 3418  df-ss 3425  df-nul 3736  df-if 3883  df-pw 3954  df-sn 3970  df-pr 3972  df-op 3976  df-uni 4189  df-br 4393  df-opab 4451  df-mpt 4452  df-id 4735  df-xp 4946  df-rel 4947  df-cnv 4948  df-co 4949  df-dm 4950  df-rn 4951  df-res 4952  df-ima 4953  df-iota 5487  df-fun 5525  df-fn 5526  df-f 5527  df-fv 5531  df-ov 6235  df-oprab 6236  df-mpt2 6237  df-pm 7378  df-mbf 22210
This theorem is referenced by:  mbfss  22235  mbfneg  22239  mbfmulc2  22252  mbflim  22257  itgcnlem  22378  itgcnval  22388  itgre  22389  itgim  22390  iblneg  22391  itgneg  22392  iblss  22393  iblss2  22394  ibladd  22409  iblsub  22410  itgadd  22413  itgsub  22414  itgfsum  22415  iblabs  22417  iblabsr  22418  iblmulc2  22419  itgmulc2  22422  itgabs  22423  itgsplit  22424  bddmulibl  22427  itgcn  22431  ditgswap  22445  ditgsplitlem  22446  ftc1a  22620  ibladdnc  31409  itgaddnc  31412  iblsubnc  31413  itgsubnc  31414  iblabsnc  31416  iblmulc2nc  31417  itgmulc2nc  31420  itgabsnc  31421
  Copyright terms: Public domain W3C validator