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

Theorem mpt2fun 6408
Description: The maps-to notation for an operation is always a function. (Contributed by Scott Fenton, 21-Mar-2012.)
Hypothesis
Ref Expression
mpt2fun.1  |-  F  =  ( x  e.  A ,  y  e.  B  |->  C )
Assertion
Ref Expression
mpt2fun  |-  Fun  F
Distinct variable group:    x, y
Allowed substitution hints:    A( x, y)    B( x, y)    C( x, y)    F( x, y)

Proof of Theorem mpt2fun
Dummy variables  w  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eqtr3 2450 . . . . . 6  |-  ( ( z  =  C  /\  w  =  C )  ->  z  =  w )
21ad2ant2l 750 . . . . 5  |-  ( ( ( ( x  e.  A  /\  y  e.  B )  /\  z  =  C )  /\  (
( x  e.  A  /\  y  e.  B
)  /\  w  =  C ) )  -> 
z  =  w )
32gen2 1666 . . . 4  |-  A. z A. w ( ( ( ( x  e.  A  /\  y  e.  B
)  /\  z  =  C )  /\  (
( x  e.  A  /\  y  e.  B
)  /\  w  =  C ) )  -> 
z  =  w )
4 eqeq1 2426 . . . . . 6  |-  ( z  =  w  ->  (
z  =  C  <->  w  =  C ) )
54anbi2d 708 . . . . 5  |-  ( z  =  w  ->  (
( ( x  e.  A  /\  y  e.  B )  /\  z  =  C )  <->  ( (
x  e.  A  /\  y  e.  B )  /\  w  =  C
) ) )
65mo4 2313 . . . 4  |-  ( E* z ( ( x  e.  A  /\  y  e.  B )  /\  z  =  C )  <->  A. z A. w ( ( ( ( x  e.  A  /\  y  e.  B
)  /\  z  =  C )  /\  (
( x  e.  A  /\  y  e.  B
)  /\  w  =  C ) )  -> 
z  =  w ) )
73, 6mpbir 212 . . 3  |-  E* z
( ( x  e.  A  /\  y  e.  B )  /\  z  =  C )
87funoprab 6406 . 2  |-  Fun  { <. <. x ,  y
>. ,  z >.  |  ( ( x  e.  A  /\  y  e.  B )  /\  z  =  C ) }
9 mpt2fun.1 . . . 4  |-  F  =  ( x  e.  A ,  y  e.  B  |->  C )
10 df-mpt2 6306 . . . 4  |-  ( x  e.  A ,  y  e.  B  |->  C )  =  { <. <. x ,  y >. ,  z
>.  |  ( (
x  e.  A  /\  y  e.  B )  /\  z  =  C
) }
119, 10eqtri 2451 . . 3  |-  F  =  { <. <. x ,  y
>. ,  z >.  |  ( ( x  e.  A  /\  y  e.  B )  /\  z  =  C ) }
1211funeqi 5617 . 2  |-  ( Fun 
F  <->  Fun  { <. <. x ,  y >. ,  z
>.  |  ( (
x  e.  A  /\  y  e.  B )  /\  z  =  C
) } )
138, 12mpbir 212 1  |-  Fun  F
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370   A.wal 1435    = wceq 1437    e. wcel 1868   E*wmo 2266   Fun wfun 5591   {coprab 6302    |-> cmpt2 6303
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-9 1872  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400  ax-sep 4543  ax-nul 4551  ax-pr 4656
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2269  df-mo 2270  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-ne 2620  df-ral 2780  df-rex 2781  df-rab 2784  df-v 3083  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762  df-if 3910  df-sn 3997  df-pr 3999  df-op 4003  df-br 4421  df-opab 4480  df-id 4764  df-xp 4855  df-rel 4856  df-cnv 4857  df-co 4858  df-fun 5599  df-oprab 6305  df-mpt2 6306
This theorem is referenced by:  ofexg  6545  mpt2exxg  6877  mpt2curryd  7020  imasvscafn  15430  coapm  15953  oppglsm  17281  gsum2d2lem  17592  evlslem2  18722  xkococnlem  20660  ucnima  21282  ucnprima  21283  fmucnd  21293  smatrcl  28617  smatlem  28618  txomap  28656  tpr2rico  28713  elunirnmbfm  29070  relowlpssretop  31707  aovmpt4g  38414  mpt2exxg2  39392
  Copyright terms: Public domain W3C validator