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

Theorem f1ompt 6003
Description: Express bijection for a mapping operation. (Contributed by Mario Carneiro, 30-May-2015.) (Revised by Mario Carneiro, 4-Dec-2016.)
Hypothesis
Ref Expression
fmpt.1  |-  F  =  ( x  e.  A  |->  C )
Assertion
Ref Expression
f1ompt  |-  ( F : A -1-1-onto-> B  <->  ( A. x  e.  A  C  e.  B  /\  A. y  e.  B  E! x  e.  A  y  =  C ) )
Distinct variable groups:    x, y, A    x, B, y    y, C    y, F
Allowed substitution hints:    C( x)    F( x)

Proof of Theorem f1ompt
Dummy variable  z is distinct from all other variables.
StepHypRef Expression
1 ffn 5689 . . . . 5  |-  ( F : A --> B  ->  F  Fn  A )
2 dff1o4 5782 . . . . . 6  |-  ( F : A -1-1-onto-> B  <->  ( F  Fn  A  /\  `' F  Fn  B ) )
32baib 911 . . . . 5  |-  ( F  Fn  A  ->  ( F : A -1-1-onto-> B  <->  `' F  Fn  B
) )
41, 3syl 17 . . . 4  |-  ( F : A --> B  -> 
( F : A -1-1-onto-> B  <->  `' F  Fn  B ) )
5 fnres 5653 . . . . . 6  |-  ( ( `' F  |`  B )  Fn  B  <->  A. y  e.  B  E! z 
y `' F z )
6 nfcv 2569 . . . . . . . . . 10  |-  F/_ x
z
7 fmpt.1 . . . . . . . . . . 11  |-  F  =  ( x  e.  A  |->  C )
8 nfmpt1 4456 . . . . . . . . . . 11  |-  F/_ x
( x  e.  A  |->  C )
97, 8nfcxfr 2567 . . . . . . . . . 10  |-  F/_ x F
10 nfcv 2569 . . . . . . . . . 10  |-  F/_ x
y
116, 9, 10nfbr 4411 . . . . . . . . 9  |-  F/ x  z F y
12 nfv 1755 . . . . . . . . 9  |-  F/ z ( x  e.  A  /\  y  =  C
)
13 breq1 4369 . . . . . . . . . 10  |-  ( z  =  x  ->  (
z F y  <->  x F
y ) )
14 df-mpt 4427 . . . . . . . . . . . . 13  |-  ( x  e.  A  |->  C )  =  { <. x ,  y >.  |  ( x  e.  A  /\  y  =  C ) }
157, 14eqtri 2450 . . . . . . . . . . . 12  |-  F  =  { <. x ,  y
>.  |  ( x  e.  A  /\  y  =  C ) }
1615breqi 4372 . . . . . . . . . . 11  |-  ( x F y  <->  x { <. x ,  y >.  |  ( x  e.  A  /\  y  =  C ) } y )
17 df-br 4367 . . . . . . . . . . . 12  |-  ( x { <. x ,  y
>.  |  ( x  e.  A  /\  y  =  C ) } y  <->  <. x ,  y >.  e.  { <. x ,  y
>.  |  ( x  e.  A  /\  y  =  C ) } )
18 opabid 4670 . . . . . . . . . . . 12  |-  ( <.
x ,  y >.  e.  { <. x ,  y
>.  |  ( x  e.  A  /\  y  =  C ) }  <->  ( x  e.  A  /\  y  =  C ) )
1917, 18bitri 252 . . . . . . . . . . 11  |-  ( x { <. x ,  y
>.  |  ( x  e.  A  /\  y  =  C ) } y  <-> 
( x  e.  A  /\  y  =  C
) )
2016, 19bitri 252 . . . . . . . . . 10  |-  ( x F y  <->  ( x  e.  A  /\  y  =  C ) )
2113, 20syl6bb 264 . . . . . . . . 9  |-  ( z  =  x  ->  (
z F y  <->  ( x  e.  A  /\  y  =  C ) ) )
2211, 12, 21cbveu 2311 . . . . . . . 8  |-  ( E! z  z F y  <-> 
E! x ( x  e.  A  /\  y  =  C ) )
23 vex 3025 . . . . . . . . . 10  |-  y  e. 
_V
24 vex 3025 . . . . . . . . . 10  |-  z  e. 
_V
2523, 24brcnv 4979 . . . . . . . . 9  |-  ( y `' F z  <->  z F
y )
2625eubii 2298 . . . . . . . 8  |-  ( E! z  y `' F
z  <->  E! z  z F y )
27 df-reu 2721 . . . . . . . 8  |-  ( E! x  e.  A  y  =  C  <->  E! x
( x  e.  A  /\  y  =  C
) )
2822, 26, 273bitr4i 280 . . . . . . 7  |-  ( E! z  y `' F
z  <->  E! x  e.  A  y  =  C )
2928ralbii 2796 . . . . . 6  |-  ( A. y  e.  B  E! z  y `' F
z  <->  A. y  e.  B  E! x  e.  A  y  =  C )
305, 29bitri 252 . . . . 5  |-  ( ( `' F  |`  B )  Fn  B  <->  A. y  e.  B  E! x  e.  A  y  =  C )
31 relcnv 5169 . . . . . . 7  |-  Rel  `' F
32 df-rn 4807 . . . . . . . 8  |-  ran  F  =  dom  `' F
33 frn 5695 . . . . . . . 8  |-  ( F : A --> B  ->  ran  F  C_  B )
3432, 33syl5eqssr 3452 . . . . . . 7  |-  ( F : A --> B  ->  dom  `' F  C_  B )
35 relssres 5104 . . . . . . 7  |-  ( ( Rel  `' F  /\  dom  `' F  C_  B )  ->  ( `' F  |`  B )  =  `' F )
3631, 34, 35sylancr 667 . . . . . 6  |-  ( F : A --> B  -> 
( `' F  |`  B )  =  `' F )
3736fneq1d 5627 . . . . 5  |-  ( F : A --> B  -> 
( ( `' F  |`  B )  Fn  B  <->  `' F  Fn  B ) )
3830, 37syl5bbr 262 . . . 4  |-  ( F : A --> B  -> 
( A. y  e.  B  E! x  e.  A  y  =  C  <->  `' F  Fn  B
) )
394, 38bitr4d 259 . . 3  |-  ( F : A --> B  -> 
( F : A -1-1-onto-> B  <->  A. y  e.  B  E! x  e.  A  y  =  C ) )
4039pm5.32i 641 . 2  |-  ( ( F : A --> B  /\  F : A -1-1-onto-> B )  <->  ( F : A --> B  /\  A. y  e.  B  E! x  e.  A  y  =  C ) )
41 f1of 5774 . . 3  |-  ( F : A -1-1-onto-> B  ->  F : A
--> B )
4241pm4.71ri 637 . 2  |-  ( F : A -1-1-onto-> B  <->  ( F : A
--> B  /\  F : A
-1-1-onto-> B ) )
437fmpt 6002 . . 3  |-  ( A. x  e.  A  C  e.  B  <->  F : A --> B )
4443anbi1i 699 . 2  |-  ( ( A. x  e.  A  C  e.  B  /\  A. y  e.  B  E! x  e.  A  y  =  C )  <->  ( F : A --> B  /\  A. y  e.  B  E! x  e.  A  y  =  C ) )
4540, 42, 443bitr4i 280 1  |-  ( F : A -1-1-onto-> B  <->  ( A. x  e.  A  C  e.  B  /\  A. y  e.  B  E! x  e.  A  y  =  C ) )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 187    /\ wa 370    = wceq 1437    e. wcel 1872   E!weu 2276   A.wral 2714   E!wreu 2716    C_ wss 3379   <.cop 3947   class class class wbr 4366   {copab 4424    |-> cmpt 4425   `'ccnv 4795   dom cdm 4796   ran crn 4797    |` cres 4798   Rel wrel 4801    Fn wfn 5539   -->wf 5540   -1-1-onto->wf1o 5543
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2063  ax-ext 2408  ax-sep 4489  ax-nul 4498  ax-pr 4603
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2280  df-mo 2281  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2558  df-ne 2601  df-ral 2719  df-rex 2720  df-reu 2721  df-rab 2723  df-v 3024  df-sbc 3243  df-dif 3382  df-un 3384  df-in 3386  df-ss 3393  df-nul 3705  df-if 3855  df-sn 3942  df-pr 3944  df-op 3948  df-uni 4163  df-br 4367  df-opab 4426  df-mpt 4427  df-id 4711  df-xp 4802  df-rel 4803  df-cnv 4804  df-co 4805  df-dm 4806  df-rn 4807  df-res 4808  df-ima 4809  df-iota 5508  df-fun 5546  df-fn 5547  df-f 5548  df-f1 5549  df-fo 5550  df-f1o 5551  df-fv 5552
This theorem is referenced by:  oaf1o  7219  xpf1o  7687  icoshftf1o  11706  fprodser  13946  dfod2  17158  gsummptf1o  17538  cusgrafilem2  25150  numclwlk2lem2f1o  25775  f1mptrn  28178  xrmulc1cn  28688  poimirlem4  31851  poimirlem16  31863  poimirlem17  31864  poimirlem19  31866  poimirlem20  31867  nbusgrf1o0  39179  cusgrfilem2  39245
  Copyright terms: Public domain W3C validator