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 ) )