Metamath Proof Explorer

Theorem f1ompt

Description: Express bijection for a mapping operation. (Contributed by Mario Carneiro, 30-May-2015) (Revised by Mario Carneiro, 4-Dec-2016)

Ref Expression
Hypothesis fmpt.1 
|- F = ( x e. A |-> C )
Assertion f1ompt 
|- ( F : A -1-1-onto-> B <-> ( A. x e. A C e. B /\ A. y e. B E! x e. A y = C ) )

Proof

Step Hyp Ref Expression
1 fmpt.1 
 |-  F = ( x e. A |-> C )
2 ffn 
 |-  ( F : A --> B -> F Fn A )
3 dff1o4 
 |-  ( F : A -1-1-onto-> B <-> ( F Fn A /\ `' F Fn B ) )
4 3 baib 
 |-  ( F Fn A -> ( F : A -1-1-onto-> B <-> `' F Fn B ) )
5 2 4 syl 
 |-  ( F : A --> B -> ( F : A -1-1-onto-> B <-> `' F Fn B ) )
6 fnres 
 |-  ( ( `' F |` B ) Fn B <-> A. y e. B E! z y `' F z )
7 nfcv 
 |-  F/_ x z
8 nfmpt1 
 |-  F/_ x ( x e. A |-> C )
9 1 8 nfcxfr 
 |-  F/_ x F
10 nfcv 
 |-  F/_ x y
11 7 9 10 nfbr 
 |-  F/ x z F y
12 nfv 
 |-  F/ z ( x e. A /\ y = C )
13 breq1 
 |-  ( z = x -> ( z F y <-> x F y ) )
14 df-mpt 
 |-  ( x e. A |-> C ) = { <. x , y >. | ( x e. A /\ y = C ) }
15 1 14 eqtri 
 |-  F = { <. x , y >. | ( x e. A /\ y = C ) }
16 15 breqi 
 |-  ( x F y <-> x { <. x , y >. | ( x e. A /\ y = C ) } y )
17 df-br 
 |-  ( x { <. x , y >. | ( x e. A /\ y = C ) } y <-> <. x , y >. e. { <. x , y >. | ( x e. A /\ y = C ) } )
18 opabidw 
 |-  ( <. x , y >. e. { <. x , y >. | ( x e. A /\ y = C ) } <-> ( x e. A /\ y = C ) )
19 17 18 bitri 
 |-  ( x { <. x , y >. | ( x e. A /\ y = C ) } y <-> ( x e. A /\ y = C ) )
20 16 19 bitri 
 |-  ( x F y <-> ( x e. A /\ y = C ) )
21 13 20 bitrdi 
 |-  ( z = x -> ( z F y <-> ( x e. A /\ y = C ) ) )
22 11 12 21 cbveuw 
 |-  ( E! z z F y <-> E! x ( x e. A /\ y = C ) )
23 vex 
 |-  y e. _V
24 vex 
 |-  z e. _V
25 23 24 brcnv 
 |-  ( y `' F z <-> z F y )
26 25 eubii 
 |-  ( E! z y `' F z <-> E! z z F y )
27 df-reu 
 |-  ( E! x e. A y = C <-> E! x ( x e. A /\ y = C ) )
28 22 26 27 3bitr4i 
 |-  ( E! z y `' F z <-> E! x e. A y = C )
29 28 ralbii 
 |-  ( A. y e. B E! z y `' F z <-> A. y e. B E! x e. A y = C )
30 6 29 bitri 
 |-  ( ( `' F |` B ) Fn B <-> A. y e. B E! x e. A y = C )
31 relcnv 
 |-  Rel `' F
32 df-rn 
 |-  ran F = dom `' F
33 frn 
 |-  ( F : A --> B -> ran F C_ B )
34 32 33 eqsstrrid 
 |-  ( F : A --> B -> dom `' F C_ B )
35 relssres 
 |-  ( ( Rel `' F /\ dom `' F C_ B ) -> ( `' F |` B ) = `' F )
36 31 34 35 sylancr 
 |-  ( F : A --> B -> ( `' F |` B ) = `' F )
37 36 fneq1d 
 |-  ( F : A --> B -> ( ( `' F |` B ) Fn B <-> `' F Fn B ) )
38 30 37 bitr3id 
 |-  ( F : A --> B -> ( A. y e. B E! x e. A y = C <-> `' F Fn B ) )
39 5 38 bitr4d 
 |-  ( F : A --> B -> ( F : A -1-1-onto-> B <-> A. y e. B E! x e. A y = C ) )
40 39 pm5.32i 
 |-  ( ( F : A --> B /\ F : A -1-1-onto-> B ) <-> ( F : A --> B /\ A. y e. B E! x e. A y = C ) )
41 f1of 
 |-  ( F : A -1-1-onto-> B -> F : A --> B )
42 41 pm4.71ri 
 |-  ( F : A -1-1-onto-> B <-> ( F : A --> B /\ F : A -1-1-onto-> B ) )
43 1 fmpt 
 |-  ( A. x e. A C e. B <-> F : A --> B )
44 43 anbi1i 
 |-  ( ( 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 ) )
45 40 42 44 3bitr4i 
 |-  ( F : A -1-1-onto-> B <-> ( A. x e. A C e. B /\ A. y e. B E! x e. A y = C ) )