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) Remove dependency on ax-reg and ax-inf2 . (Revised by Timothy J. O'Malley, 15-Oct-2026)

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 simpl 
 |-  ( ( A e. V /\ F : A -onto-> B ) -> A e. V )
4 foelrn 
 |-  ( ( F : A -onto-> B /\ y e. B ) -> E. z e. A y = ( F ` z ) )
5 fofn 
 |-  ( F : A -onto-> B -> F Fn A )
6 eqcom 
 |-  ( ( F ` z ) = y <-> y = ( F ` z ) )
7 fniniseg 
 |-  ( F Fn A -> ( z e. ( `' F " { y } ) <-> ( z e. A /\ ( F ` z ) = y ) ) )
8 7 biimpar 
 |-  ( ( F Fn A /\ ( z e. A /\ ( F ` z ) = y ) ) -> z e. ( `' F " { y } ) )
9 8 anassrs 
 |-  ( ( ( F Fn A /\ z e. A ) /\ ( F ` z ) = y ) -> z e. ( `' F " { y } ) )
10 6 9 sylan2br 
 |-  ( ( ( F Fn A /\ z e. A ) /\ y = ( F ` z ) ) -> z e. ( `' F " { y } ) )
11 5 10 sylanl1 
 |-  ( ( ( F : A -onto-> B /\ z e. A ) /\ y = ( F ` z ) ) -> z e. ( `' F " { y } ) )
12 11 ex 
 |-  ( ( F : A -onto-> B /\ z e. A ) -> ( y = ( F ` z ) -> z e. ( `' F " { y } ) ) )
13 12 reximdva 
 |-  ( F : A -onto-> B -> ( E. z e. A y = ( F ` z ) -> E. z e. A z e. ( `' F " { y } ) ) )
14 13 adantr 
 |-  ( ( F : A -onto-> B /\ y e. B ) -> ( E. z e. A y = ( F ` z ) -> E. z e. A z e. ( `' F " { y } ) ) )
15 4 14 mpd 
 |-  ( ( F : A -onto-> B /\ y e. B ) -> E. z e. A z e. ( `' F " { y } ) )
16 15 adantll 
 |-  ( ( ( A e. V /\ F : A -onto-> B ) /\ y e. B ) -> E. z e. A z e. ( `' F " { y } ) )
17 16 ralrimiva 
 |-  ( ( A e. V /\ F : A -onto-> B ) -> A. y e. B E. z e. A z e. ( `' F " { y } ) )
18 eleq1 
 |-  ( z = ( g ` y ) -> ( z e. ( `' F " { y } ) <-> ( g ` y ) e. ( `' F " { y } ) ) )
19 18 ac6 
 |-  ( ( B e. _V /\ A 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 } ) ) )
20 2 3 17 19 syl3anc 
 |-  ( ( A e. V /\ F : A -onto-> B ) -> E. g ( g : B --> A /\ A. y e. B ( g ` y ) e. ( `' F " { y } ) ) )
21 reseq2 
 |-  ( x = ran g -> ( F |` x ) = ( F |` ran g ) )
22 id 
 |-  ( x = ran g -> x = ran g )
23 eqidd 
 |-  ( x = ran g -> B = B )
24 21 22 23 f1oeq123d 
 |-  ( x = ran g -> ( ( F |` x ) : x -1-1-onto-> B <-> ( F |` ran g ) : ran g -1-1-onto-> B ) )
25 frn 
 |-  ( g : B --> A -> ran g C_ A )
26 25 ad2antrl 
 |-  ( ( ( A e. V /\ F : A -onto-> B ) /\ ( g : B --> A /\ A. y e. B ( g ` y ) e. ( `' F " { y } ) ) ) -> ran g C_ A )
27 vex 
 |-  g e. _V
28 27 rnex 
 |-  ran g e. _V
29 28 elpw 
 |-  ( ran g e. ~P A <-> ran g C_ A )
30 26 29 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 )
31 fof 
 |-  ( F : A -onto-> B -> F : A --> B )
32 31 ad2antlr 
 |-  ( ( ( A e. V /\ F : A -onto-> B ) /\ ( g : B --> A /\ A. y e. B ( g ` y ) e. ( `' F " { y } ) ) ) -> F : A --> B )
33 32 26 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 )
34 ffn 
 |-  ( g : B --> A -> g Fn B )
35 34 ad2antrl 
 |-  ( ( ( A e. V /\ F : A -onto-> B ) /\ ( g : B --> A /\ A. y e. B ( g ` y ) e. ( `' F " { y } ) ) ) -> g Fn B )
36 dffn3 
 |-  ( g Fn B <-> g : B --> ran g )
37 35 36 sylib 
 |-  ( ( ( A e. V /\ F : A -onto-> B ) /\ ( g : B --> A /\ A. y e. B ( g ` y ) e. ( `' F " { y } ) ) ) -> g : B --> ran g )
38 fvres 
 |-  ( z e. ran g -> ( ( F |` ran g ) ` z ) = ( F ` z ) )
39 38 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 ) )
40 39 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 ) ) )
41 nfv 
 |-  F/ y ( A e. V /\ F : A -onto-> B )
42 nfv 
 |-  F/ y g : B --> A
43 nfra1 
 |-  F/ y A. y e. B ( g ` y ) e. ( `' F " { y } )
44 42 43 nfan 
 |-  F/ y ( g : B --> A /\ A. y e. B ( g ` y ) e. ( `' F " { y } ) )
45 41 44 nfan 
 |-  F/ y ( ( A e. V /\ F : A -onto-> B ) /\ ( g : B --> A /\ A. y e. B ( g ` y ) e. ( `' F " { y } ) ) )
46 nfv 
 |-  F/ y z e. ran g
47 45 46 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 )
48 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 )
49 48 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 ) )
50 5 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 )
51 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 } ) )
52 51 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 } ) )
53 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 )
54 rspa 
 |-  ( ( A. y e. B ( g ` y ) e. ( `' F " { y } ) /\ y e. B ) -> ( g ` y ) e. ( `' F " { y } ) )
55 52 53 54 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 } ) )
56 fniniseg 
 |-  ( F Fn A -> ( ( g ` y ) e. ( `' F " { y } ) <-> ( ( g ` y ) e. A /\ ( F ` ( g ` y ) ) = y ) ) )
57 56 simplbda 
 |-  ( ( F Fn A /\ ( g ` y ) e. ( `' F " { y } ) ) -> ( F ` ( g ` y ) ) = y )
58 50 55 57 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 )
59 49 58 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 )
60 59 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 ) )
61 60 48 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 )
62 fvelrnb 
 |-  ( g Fn B -> ( z e. ran g <-> E. y e. B ( g ` y ) = z ) )
63 62 biimpa 
 |-  ( ( g Fn B /\ z e. ran g ) -> E. y e. B ( g ` y ) = z )
64 35 63 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 )
65 47 61 64 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 )
66 40 65 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 )
67 66 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 )
68 37 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 )
69 68 fvresd 
 |-  ( ( ( ( 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 ) ) )
70 5 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 )
71 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 } ) )
72 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 )
73 71 72 54 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 } ) )
74 70 73 57 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 )
75 69 74 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 )
76 45 75 ralrimia 
 |-  ( ( ( 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 )
77 33 37 67 76 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 )
78 24 30 77 rspcedvdw 
 |-  ( ( ( 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 )
79 20 78 exlimddv 
 |-  ( ( A e. V /\ F : A -onto-> B ) -> E. x e. ~P A ( F |` x ) : x -1-1-onto-> B )