Metamath Proof Explorer

Theorem foresf1o

Description: From a surjective function, *choose* a subset of the domain, such that the restricted function is bijective. (Contributed by Thierry Arnoux, 27-Jan-2020)

Ref Expression
Assertion foresf1o 
|- ( ( A e. V /\ F : A -onto-> B ) -> E. x e. ~P A ( F |` x ) : x -1-1-onto-> B )

Proof

Step Hyp Ref Expression
1 focdmex 
 |-  ( A e. V -> ( F : A -onto-> B -> B e. _V ) )
2 1 imp 
 |-  ( ( A e. V /\ F : A -onto-> B ) -> B e. _V )
3 foelrn 
 |-  ( ( F : A -onto-> B /\ y e. B ) -> E. z e. A y = ( F ` z ) )
4 fofn 
 |-  ( F : A -onto-> B -> F Fn A )
5 eqcom 
 |-  ( ( F ` z ) = y <-> y = ( F ` z ) )
6 fniniseg 
 |-  ( F Fn A -> ( z e. ( `' F " { y } ) <-> ( z e. A /\ ( F ` z ) = y ) ) )
7 6 biimpar 
 |-  ( ( F Fn A /\ ( z e. A /\ ( F ` z ) = y ) ) -> z e. ( `' F " { y } ) )
8 7 anassrs 
 |-  ( ( ( F Fn A /\ z e. A ) /\ ( F ` z ) = y ) -> z e. ( `' F " { y } ) )
9 5 8 sylan2br 
 |-  ( ( ( F Fn A /\ z e. A ) /\ y = ( F ` z ) ) -> z e. ( `' F " { y } ) )
10 4 9 sylanl1 
 |-  ( ( ( F : A -onto-> B /\ z e. A ) /\ y = ( F ` z ) ) -> z e. ( `' F " { y } ) )
11 10 ex 
 |-  ( ( F : A -onto-> B /\ z e. A ) -> ( y = ( F ` z ) -> z e. ( `' F " { y } ) ) )
12 11 reximdva 
 |-  ( F : A -onto-> B -> ( E. z e. A y = ( F ` z ) -> E. z e. A z e. ( `' F " { y } ) ) )
13 12 adantr 
 |-  ( ( F : A -onto-> B /\ y e. B ) -> ( E. z e. A y = ( F ` z ) -> E. z e. A z e. ( `' F " { y } ) ) )
14 3 13 mpd 
 |-  ( ( F : A -onto-> B /\ y e. B ) -> E. z e. A z e. ( `' F " { y } ) )
15 14 adantll 
 |-  ( ( ( A e. V /\ F : A -onto-> B ) /\ y e. B ) -> E. z e. A z e. ( `' F " { y } ) )
16 15 ralrimiva 
 |-  ( ( A e. V /\ F : A -onto-> B ) -> A. y e. B E. z e. A z e. ( `' F " { y } ) )
17 eleq1 
 |-  ( z = ( g ` y ) -> ( z e. ( `' F " { y } ) <-> ( g ` y ) e. ( `' F " { y } ) ) )
18 17 ac6sg 
 |-  ( B e. _V -> ( A. y e. B E. z e. A z e. ( `' F " { y } ) -> E. g ( g : B --> A /\ A. y e. B ( g ` y ) e. ( `' F " { y } ) ) ) )
19 2 16 18 sylc 
 |-  ( ( A e. V /\ F : A -onto-> B ) -> E. g ( g : B --> A /\ A. y e. B ( g ` y ) e. ( `' F " { y } ) ) )
20 frn 
 |-  ( g : B --> A -> ran g C_ A )
21 20 ad2antrl 
 |-  ( ( ( A e. V /\ F : A -onto-> B ) /\ ( g : B --> A /\ A. y e. B ( g ` y ) e. ( `' F " { y } ) ) ) -> ran g C_ A )
22 vex 
 |-  g e. _V
23 22 rnex 
 |-  ran g e. _V
24 23 elpw 
 |-  ( ran g e. ~P A <-> ran g C_ A )
25 21 24 sylibr 
 |-  ( ( ( A e. V /\ F : A -onto-> B ) /\ ( g : B --> A /\ A. y e. B ( g ` y ) e. ( `' F " { y } ) ) ) -> ran g e. ~P A )
26 fof 
 |-  ( F : A -onto-> B -> F : A --> B )
27 26 ad2antlr 
 |-  ( ( ( A e. V /\ F : A -onto-> B ) /\ ( g : B --> A /\ A. y e. B ( g ` y ) e. ( `' F " { y } ) ) ) -> F : A --> B )
28 27 21 fssresd 
 |-  ( ( ( A e. V /\ F : A -onto-> B ) /\ ( g : B --> A /\ A. y e. B ( g ` y ) e. ( `' F " { y } ) ) ) -> ( F |` ran g ) : ran g --> B )
29 ffn 
 |-  ( g : B --> A -> g Fn B )
30 29 ad2antrl 
 |-  ( ( ( A e. V /\ F : A -onto-> B ) /\ ( g : B --> A /\ A. y e. B ( g ` y ) e. ( `' F " { y } ) ) ) -> g Fn B )
31 dffn3 
 |-  ( g Fn B <-> g : B --> ran g )
32 30 31 sylib 
 |-  ( ( ( A e. V /\ F : A -onto-> B ) /\ ( g : B --> A /\ A. y e. B ( g ` y ) e. ( `' F " { y } ) ) ) -> g : B --> ran g )
33 fvres 
 |-  ( z e. ran g -> ( ( F |` ran g ) ` z ) = ( F ` z ) )
34 33 adantl 
 |-  ( ( ( ( A e. V /\ F : A -onto-> B ) /\ ( g : B --> A /\ A. y e. B ( g ` y ) e. ( `' F " { y } ) ) ) /\ z e. ran g ) -> ( ( F |` ran g ) ` z ) = ( F ` z ) )
35 34 fveq2d 
 |-  ( ( ( ( A e. V /\ F : A -onto-> B ) /\ ( g : B --> A /\ A. y e. B ( g ` y ) e. ( `' F " { y } ) ) ) /\ z e. ran g ) -> ( g ` ( ( F |` ran g ) ` z ) ) = ( g ` ( F ` z ) ) )
36 nfv 
 |-  F/ y ( A e. V /\ F : A -onto-> B )
37 nfv 
 |-  F/ y g : B --> A
38 nfra1 
 |-  F/ y A. y e. B ( g ` y ) e. ( `' F " { y } )
39 37 38 nfan 
 |-  F/ y ( g : B --> A /\ A. y e. B ( g ` y ) e. ( `' F " { y } ) )
40 36 39 nfan 
 |-  F/ y ( ( A e. V /\ F : A -onto-> B ) /\ ( g : B --> A /\ A. y e. B ( g ` y ) e. ( `' F " { y } ) ) )
41 nfv 
 |-  F/ y z e. ran g
42 40 41 nfan 
 |-  F/ y ( ( ( A e. V /\ F : A -onto-> B ) /\ ( g : B --> A /\ A. y e. B ( g ` y ) e. ( `' F " { y } ) ) ) /\ z e. ran g )
43 simpr 
 |-  ( ( ( ( ( ( A e. V /\ F : A -onto-> B ) /\ ( g : B --> A /\ A. y e. B ( g ` y ) e. ( `' F " { y } ) ) ) /\ z e. ran g ) /\ y e. B ) /\ ( g ` y ) = z ) -> ( g ` y ) = z )
44 43 fveq2d 
 |-  ( ( ( ( ( ( A e. V /\ F : A -onto-> B ) /\ ( g : B --> A /\ A. y e. B ( g ` y ) e. ( `' F " { y } ) ) ) /\ z e. ran g ) /\ y e. B ) /\ ( g ` y ) = z ) -> ( F ` ( g ` y ) ) = ( F ` z ) )
45 4 ad5antlr 
 |-  ( ( ( ( ( ( A e. V /\ F : A -onto-> B ) /\ ( g : B --> A /\ A. y e. B ( g ` y ) e. ( `' F " { y } ) ) ) /\ z e. ran g ) /\ y e. B ) /\ ( g ` y ) = z ) -> F Fn A )
46 simplrr 
 |-  ( ( ( ( A e. V /\ F : A -onto-> B ) /\ ( g : B --> A /\ A. y e. B ( g ` y ) e. ( `' F " { y } ) ) ) /\ z e. ran g ) -> A. y e. B ( g ` y ) e. ( `' F " { y } ) )
47 46 ad2antrr 
 |-  ( ( ( ( ( ( A e. V /\ F : A -onto-> B ) /\ ( g : B --> A /\ A. y e. B ( g ` y ) e. ( `' F " { y } ) ) ) /\ z e. ran g ) /\ y e. B ) /\ ( g ` y ) = z ) -> A. y e. B ( g ` y ) e. ( `' F " { y } ) )
48 simplr 
 |-  ( ( ( ( ( ( A e. V /\ F : A -onto-> B ) /\ ( g : B --> A /\ A. y e. B ( g ` y ) e. ( `' F " { y } ) ) ) /\ z e. ran g ) /\ y e. B ) /\ ( g ` y ) = z ) -> y e. B )
49 rspa 
 |-  ( ( A. y e. B ( g ` y ) e. ( `' F " { y } ) /\ y e. B ) -> ( g ` y ) e. ( `' F " { y } ) )
50 47 48 49 syl2anc 
 |-  ( ( ( ( ( ( A e. V /\ F : A -onto-> B ) /\ ( g : B --> A /\ A. y e. B ( g ` y ) e. ( `' F " { y } ) ) ) /\ z e. ran g ) /\ y e. B ) /\ ( g ` y ) = z ) -> ( g ` y ) e. ( `' F " { y } ) )
51 fniniseg 
 |-  ( F Fn A -> ( ( g ` y ) e. ( `' F " { y } ) <-> ( ( g ` y ) e. A /\ ( F ` ( g ` y ) ) = y ) ) )
52 51 simplbda 
 |-  ( ( F Fn A /\ ( g ` y ) e. ( `' F " { y } ) ) -> ( F ` ( g ` y ) ) = y )
53 45 50 52 syl2anc 
 |-  ( ( ( ( ( ( A e. V /\ F : A -onto-> B ) /\ ( g : B --> A /\ A. y e. B ( g ` y ) e. ( `' F " { y } ) ) ) /\ z e. ran g ) /\ y e. B ) /\ ( g ` y ) = z ) -> ( F ` ( g ` y ) ) = y )
54 44 53 eqtr3d 
 |-  ( ( ( ( ( ( A e. V /\ F : A -onto-> B ) /\ ( g : B --> A /\ A. y e. B ( g ` y ) e. ( `' F " { y } ) ) ) /\ z e. ran g ) /\ y e. B ) /\ ( g ` y ) = z ) -> ( F ` z ) = y )
55 54 fveq2d 
 |-  ( ( ( ( ( ( A e. V /\ F : A -onto-> B ) /\ ( g : B --> A /\ A. y e. B ( g ` y ) e. ( `' F " { y } ) ) ) /\ z e. ran g ) /\ y e. B ) /\ ( g ` y ) = z ) -> ( g ` ( F ` z ) ) = ( g ` y ) )
56 55 43 eqtrd 
 |-  ( ( ( ( ( ( A e. V /\ F : A -onto-> B ) /\ ( g : B --> A /\ A. y e. B ( g ` y ) e. ( `' F " { y } ) ) ) /\ z e. ran g ) /\ y e. B ) /\ ( g ` y ) = z ) -> ( g ` ( F ` z ) ) = z )
57 fvelrnb 
 |-  ( g Fn B -> ( z e. ran g <-> E. y e. B ( g ` y ) = z ) )
58 57 biimpa 
 |-  ( ( g Fn B /\ z e. ran g ) -> E. y e. B ( g ` y ) = z )
59 30 58 sylan 
 |-  ( ( ( ( A e. V /\ F : A -onto-> B ) /\ ( g : B --> A /\ A. y e. B ( g ` y ) e. ( `' F " { y } ) ) ) /\ z e. ran g ) -> E. y e. B ( g ` y ) = z )
60 42 56 59 r19.29af 
 |-  ( ( ( ( A e. V /\ F : A -onto-> B ) /\ ( g : B --> A /\ A. y e. B ( g ` y ) e. ( `' F " { y } ) ) ) /\ z e. ran g ) -> ( g ` ( F ` z ) ) = z )
61 35 60 eqtrd 
 |-  ( ( ( ( A e. V /\ F : A -onto-> B ) /\ ( g : B --> A /\ A. y e. B ( g ` y ) e. ( `' F " { y } ) ) ) /\ z e. ran g ) -> ( g ` ( ( F |` ran g ) ` z ) ) = z )
62 61 ralrimiva 
 |-  ( ( ( A e. V /\ F : A -onto-> B ) /\ ( g : B --> A /\ A. y e. B ( g ` y ) e. ( `' F " { y } ) ) ) -> A. z e. ran g ( g ` ( ( F |` ran g ) ` z ) ) = z )
63 32 ffvelcdmda 
 |-  ( ( ( ( A e. V /\ F : A -onto-> B ) /\ ( g : B --> A /\ A. y e. B ( g ` y ) e. ( `' F " { y } ) ) ) /\ y e. B ) -> ( g ` y ) e. ran g )
64 fvres 
 |-  ( ( g ` y ) e. ran g -> ( ( F |` ran g ) ` ( g ` y ) ) = ( F ` ( g ` y ) ) )
65 63 64 syl 
 |-  ( ( ( ( A e. V /\ F : A -onto-> B ) /\ ( g : B --> A /\ A. y e. B ( g ` y ) e. ( `' F " { y } ) ) ) /\ y e. B ) -> ( ( F |` ran g ) ` ( g ` y ) ) = ( F ` ( g ` y ) ) )
66 4 ad3antlr 
 |-  ( ( ( ( A e. V /\ F : A -onto-> B ) /\ ( g : B --> A /\ A. y e. B ( g ` y ) e. ( `' F " { y } ) ) ) /\ y e. B ) -> F Fn A )
67 simplrr 
 |-  ( ( ( ( A e. V /\ F : A -onto-> B ) /\ ( g : B --> A /\ A. y e. B ( g ` y ) e. ( `' F " { y } ) ) ) /\ y e. B ) -> A. y e. B ( g ` y ) e. ( `' F " { y } ) )
68 simpr 
 |-  ( ( ( ( A e. V /\ F : A -onto-> B ) /\ ( g : B --> A /\ A. y e. B ( g ` y ) e. ( `' F " { y } ) ) ) /\ y e. B ) -> y e. B )
69 67 68 49 syl2anc 
 |-  ( ( ( ( A e. V /\ F : A -onto-> B ) /\ ( g : B --> A /\ A. y e. B ( g ` y ) e. ( `' F " { y } ) ) ) /\ y e. B ) -> ( g ` y ) e. ( `' F " { y } ) )
70 66 69 52 syl2anc 
 |-  ( ( ( ( A e. V /\ F : A -onto-> B ) /\ ( g : B --> A /\ A. y e. B ( g ` y ) e. ( `' F " { y } ) ) ) /\ y e. B ) -> ( F ` ( g ` y ) ) = y )
71 65 70 eqtrd 
 |-  ( ( ( ( A e. V /\ F : A -onto-> B ) /\ ( g : B --> A /\ A. y e. B ( g ` y ) e. ( `' F " { y } ) ) ) /\ y e. B ) -> ( ( F |` ran g ) ` ( g ` y ) ) = y )
72 71 ex 
 |-  ( ( ( A e. V /\ F : A -onto-> B ) /\ ( g : B --> A /\ A. y e. B ( g ` y ) e. ( `' F " { y } ) ) ) -> ( y e. B -> ( ( F |` ran g ) ` ( g ` y ) ) = y ) )
73 40 72 ralrimi 
 |-  ( ( ( A e. V /\ F : A -onto-> B ) /\ ( g : B --> A /\ A. y e. B ( g ` y ) e. ( `' F " { y } ) ) ) -> A. y e. B ( ( F |` ran g ) ` ( g ` y ) ) = y )
74 28 32 62 73 2fvidf1od 
 |-  ( ( ( A e. V /\ F : A -onto-> B ) /\ ( g : B --> A /\ A. y e. B ( g ` y ) e. ( `' F " { y } ) ) ) -> ( F |` ran g ) : ran g -1-1-onto-> B )
75 reseq2 
 |-  ( x = ran g -> ( F |` x ) = ( F |` ran g ) )
76 id 
 |-  ( x = ran g -> x = ran g )
77 eqidd 
 |-  ( x = ran g -> B = B )
78 75 76 77 f1oeq123d 
 |-  ( x = ran g -> ( ( F |` x ) : x -1-1-onto-> B <-> ( F |` ran g ) : ran g -1-1-onto-> B ) )
79 78 rspcev 
 |-  ( ( ran g e. ~P A /\ ( F |` ran g ) : ran g -1-1-onto-> B ) -> E. x e. ~P A ( F |` x ) : x -1-1-onto-> B )
80 25 74 79 syl2anc 
 |-  ( ( ( A e. V /\ F : A -onto-> B ) /\ ( g : B --> A /\ A. y e. B ( g ` y ) e. ( `' F " { y } ) ) ) -> E. x e. ~P A ( F |` x ) : x -1-1-onto-> B )
81 19 80 exlimddv 
 |-  ( ( A e. V /\ F : A -onto-> B ) -> E. x e. ~P A ( F |` x ) : x -1-1-onto-> B )