Metamath Proof Explorer

Theorem fvineqsneu

Description: A theorem about functions where the image of every point intersects the domain only at that point. (Contributed by ML, 27-Mar-2021)

Ref Expression
Assertion fvineqsneu 
|- ( ( F Fn A /\ A. p e. A ( ( F ` p ) i^i A ) = { p } ) -> A. q e. A E! x e. ran F q e. x )

Proof

Step Hyp Ref Expression
1 fnfvelrn 
 |-  ( ( F Fn A /\ o e. A ) -> ( F ` o ) e. ran F )
2 1 ex 
 |-  ( F Fn A -> ( o e. A -> ( F ` o ) e. ran F ) )
3 2 adantr 
 |-  ( ( F Fn A /\ A. p e. A ( ( F ` p ) i^i A ) = { p } ) -> ( o e. A -> ( F ` o ) e. ran F ) )
4 fnrnfv 
 |-  ( F Fn A -> ran F = { y | E. p e. A y = ( F ` p ) } )
5 4 abeq2d 
 |-  ( F Fn A -> ( y e. ran F <-> E. p e. A y = ( F ` p ) ) )
6 5 adantr 
 |-  ( ( F Fn A /\ A. p e. A ( ( F ` p ) i^i A ) = { p } ) -> ( y e. ran F <-> E. p e. A y = ( F ` p ) ) )
7 nfv 
 |-  F/ p F Fn A
8 nfra1 
 |-  F/ p A. p e. A ( ( F ` p ) i^i A ) = { p }
9 7 8 nfan 
 |-  F/ p ( F Fn A /\ A. p e. A ( ( F ` p ) i^i A ) = { p } )
10 nfv 
 |-  F/ p A. o e. A ( o e. y <-> y = ( F ` o ) )
11 eleq2 
 |-  ( y = ( F ` p ) -> ( o e. y <-> o e. ( F ` p ) ) )
12 elin 
 |-  ( o e. ( ( F ` p ) i^i A ) <-> ( o e. ( F ` p ) /\ o e. A ) )
13 12 rbaib 
 |-  ( o e. A -> ( o e. ( ( F ` p ) i^i A ) <-> o e. ( F ` p ) ) )
14 13 ad2antll 
 |-  ( ( ( F Fn A /\ A. p e. A ( ( F ` p ) i^i A ) = { p } ) /\ ( p e. A /\ o e. A ) ) -> ( o e. ( ( F ` p ) i^i A ) <-> o e. ( F ` p ) ) )
15 rsp 
 |-  ( A. p e. A ( ( F ` p ) i^i A ) = { p } -> ( p e. A -> ( ( F ` p ) i^i A ) = { p } ) )
16 eleq2 
 |-  ( ( ( F ` p ) i^i A ) = { p } -> ( o e. ( ( F ` p ) i^i A ) <-> o e. { p } ) )
17 velsn 
 |-  ( o e. { p } <-> o = p )
18 equcom 
 |-  ( o = p <-> p = o )
19 17 18 bitri 
 |-  ( o e. { p } <-> p = o )
20 16 19 bitrdi 
 |-  ( ( ( F ` p ) i^i A ) = { p } -> ( o e. ( ( F ` p ) i^i A ) <-> p = o ) )
21 15 20 syl6 
 |-  ( A. p e. A ( ( F ` p ) i^i A ) = { p } -> ( p e. A -> ( o e. ( ( F ` p ) i^i A ) <-> p = o ) ) )
22 21 adantl 
 |-  ( ( F Fn A /\ A. p e. A ( ( F ` p ) i^i A ) = { p } ) -> ( p e. A -> ( o e. ( ( F ` p ) i^i A ) <-> p = o ) ) )
23 22 adantrd 
 |-  ( ( F Fn A /\ A. p e. A ( ( F ` p ) i^i A ) = { p } ) -> ( ( p e. A /\ o e. A ) -> ( o e. ( ( F ` p ) i^i A ) <-> p = o ) ) )
24 23 imp 
 |-  ( ( ( F Fn A /\ A. p e. A ( ( F ` p ) i^i A ) = { p } ) /\ ( p e. A /\ o e. A ) ) -> ( o e. ( ( F ` p ) i^i A ) <-> p = o ) )
25 14 24 bitr3d 
 |-  ( ( ( F Fn A /\ A. p e. A ( ( F ` p ) i^i A ) = { p } ) /\ ( p e. A /\ o e. A ) ) -> ( o e. ( F ` p ) <-> p = o ) )
26 11 25 sylan9bbr 
 |-  ( ( ( ( F Fn A /\ A. p e. A ( ( F ` p ) i^i A ) = { p } ) /\ ( p e. A /\ o e. A ) ) /\ y = ( F ` p ) ) -> ( o e. y <-> p = o ) )
27 26 ex 
 |-  ( ( ( F Fn A /\ A. p e. A ( ( F ` p ) i^i A ) = { p } ) /\ ( p e. A /\ o e. A ) ) -> ( y = ( F ` p ) -> ( o e. y <-> p = o ) ) )
28 27 anass1rs 
 |-  ( ( ( ( F Fn A /\ A. p e. A ( ( F ` p ) i^i A ) = { p } ) /\ o e. A ) /\ p e. A ) -> ( y = ( F ` p ) -> ( o e. y <-> p = o ) ) )
29 28 impr 
 |-  ( ( ( ( F Fn A /\ A. p e. A ( ( F ` p ) i^i A ) = { p } ) /\ o e. A ) /\ ( p e. A /\ y = ( F ` p ) ) ) -> ( o e. y <-> p = o ) )
30 29 an32s 
 |-  ( ( ( ( F Fn A /\ A. p e. A ( ( F ` p ) i^i A ) = { p } ) /\ ( p e. A /\ y = ( F ` p ) ) ) /\ o e. A ) -> ( o e. y <-> p = o ) )
31 eqeq1 
 |-  ( y = ( F ` p ) -> ( y = ( F ` o ) <-> ( F ` p ) = ( F ` o ) ) )
32 dffn3 
 |-  ( F Fn A <-> F : A --> ran F )
33 fvineqsnf1 
 |-  ( ( F : A --> ran F /\ A. p e. A ( ( F ` p ) i^i A ) = { p } ) -> F : A -1-1-> ran F )
34 32 33 sylanb 
 |-  ( ( F Fn A /\ A. p e. A ( ( F ` p ) i^i A ) = { p } ) -> F : A -1-1-> ran F )
35 dff13 
 |-  ( F : A -1-1-> ran F <-> ( F : A --> ran F /\ A. p e. A A. o e. A ( ( F ` p ) = ( F ` o ) -> p = o ) ) )
36 34 35 sylib 
 |-  ( ( F Fn A /\ A. p e. A ( ( F ` p ) i^i A ) = { p } ) -> ( F : A --> ran F /\ A. p e. A A. o e. A ( ( F ` p ) = ( F ` o ) -> p = o ) ) )
37 36 simprd 
 |-  ( ( F Fn A /\ A. p e. A ( ( F ` p ) i^i A ) = { p } ) -> A. p e. A A. o e. A ( ( F ` p ) = ( F ` o ) -> p = o ) )
38 rsp 
 |-  ( A. p e. A A. o e. A ( ( F ` p ) = ( F ` o ) -> p = o ) -> ( p e. A -> A. o e. A ( ( F ` p ) = ( F ` o ) -> p = o ) ) )
39 37 38 syl 
 |-  ( ( F Fn A /\ A. p e. A ( ( F ` p ) i^i A ) = { p } ) -> ( p e. A -> A. o e. A ( ( F ` p ) = ( F ` o ) -> p = o ) ) )
40 rsp 
 |-  ( A. o e. A ( ( F ` p ) = ( F ` o ) -> p = o ) -> ( o e. A -> ( ( F ` p ) = ( F ` o ) -> p = o ) ) )
41 39 40 syl6 
 |-  ( ( F Fn A /\ A. p e. A ( ( F ` p ) i^i A ) = { p } ) -> ( p e. A -> ( o e. A -> ( ( F ` p ) = ( F ` o ) -> p = o ) ) ) )
42 41 imp32 
 |-  ( ( ( F Fn A /\ A. p e. A ( ( F ` p ) i^i A ) = { p } ) /\ ( p e. A /\ o e. A ) ) -> ( ( F ` p ) = ( F ` o ) -> p = o ) )
43 fveq2 
 |-  ( p = o -> ( F ` p ) = ( F ` o ) )
44 42 43 impbid1 
 |-  ( ( ( F Fn A /\ A. p e. A ( ( F ` p ) i^i A ) = { p } ) /\ ( p e. A /\ o e. A ) ) -> ( ( F ` p ) = ( F ` o ) <-> p = o ) )
45 31 44 sylan9bbr 
 |-  ( ( ( ( F Fn A /\ A. p e. A ( ( F ` p ) i^i A ) = { p } ) /\ ( p e. A /\ o e. A ) ) /\ y = ( F ` p ) ) -> ( y = ( F ` o ) <-> p = o ) )
46 45 ex 
 |-  ( ( ( F Fn A /\ A. p e. A ( ( F ` p ) i^i A ) = { p } ) /\ ( p e. A /\ o e. A ) ) -> ( y = ( F ` p ) -> ( y = ( F ` o ) <-> p = o ) ) )
47 46 anass1rs 
 |-  ( ( ( ( F Fn A /\ A. p e. A ( ( F ` p ) i^i A ) = { p } ) /\ o e. A ) /\ p e. A ) -> ( y = ( F ` p ) -> ( y = ( F ` o ) <-> p = o ) ) )
48 47 impr 
 |-  ( ( ( ( F Fn A /\ A. p e. A ( ( F ` p ) i^i A ) = { p } ) /\ o e. A ) /\ ( p e. A /\ y = ( F ` p ) ) ) -> ( y = ( F ` o ) <-> p = o ) )
49 48 an32s 
 |-  ( ( ( ( F Fn A /\ A. p e. A ( ( F ` p ) i^i A ) = { p } ) /\ ( p e. A /\ y = ( F ` p ) ) ) /\ o e. A ) -> ( y = ( F ` o ) <-> p = o ) )
50 30 49 bitr4d 
 |-  ( ( ( ( F Fn A /\ A. p e. A ( ( F ` p ) i^i A ) = { p } ) /\ ( p e. A /\ y = ( F ` p ) ) ) /\ o e. A ) -> ( o e. y <-> y = ( F ` o ) ) )
51 50 ex 
 |-  ( ( ( F Fn A /\ A. p e. A ( ( F ` p ) i^i A ) = { p } ) /\ ( p e. A /\ y = ( F ` p ) ) ) -> ( o e. A -> ( o e. y <-> y = ( F ` o ) ) ) )
52 51 ralrimiv 
 |-  ( ( ( F Fn A /\ A. p e. A ( ( F ` p ) i^i A ) = { p } ) /\ ( p e. A /\ y = ( F ` p ) ) ) -> A. o e. A ( o e. y <-> y = ( F ` o ) ) )
53 52 exp32 
 |-  ( ( F Fn A /\ A. p e. A ( ( F ` p ) i^i A ) = { p } ) -> ( p e. A -> ( y = ( F ` p ) -> A. o e. A ( o e. y <-> y = ( F ` o ) ) ) ) )
54 9 10 53 rexlimd 
 |-  ( ( F Fn A /\ A. p e. A ( ( F ` p ) i^i A ) = { p } ) -> ( E. p e. A y = ( F ` p ) -> A. o e. A ( o e. y <-> y = ( F ` o ) ) ) )
55 6 54 sylbid 
 |-  ( ( F Fn A /\ A. p e. A ( ( F ` p ) i^i A ) = { p } ) -> ( y e. ran F -> A. o e. A ( o e. y <-> y = ( F ` o ) ) ) )
56 rsp 
 |-  ( A. o e. A ( o e. y <-> y = ( F ` o ) ) -> ( o e. A -> ( o e. y <-> y = ( F ` o ) ) ) )
57 55 56 syl6 
 |-  ( ( F Fn A /\ A. p e. A ( ( F ` p ) i^i A ) = { p } ) -> ( y e. ran F -> ( o e. A -> ( o e. y <-> y = ( F ` o ) ) ) ) )
58 57 com23 
 |-  ( ( F Fn A /\ A. p e. A ( ( F ` p ) i^i A ) = { p } ) -> ( o e. A -> ( y e. ran F -> ( o e. y <-> y = ( F ` o ) ) ) ) )
59 58 ralrimdv 
 |-  ( ( F Fn A /\ A. p e. A ( ( F ` p ) i^i A ) = { p } ) -> ( o e. A -> A. y e. ran F ( o e. y <-> y = ( F ` o ) ) ) )
60 reu6i 
 |-  ( ( ( F ` o ) e. ran F /\ A. y e. ran F ( o e. y <-> y = ( F ` o ) ) ) -> E! y e. ran F o e. y )
61 60 ex 
 |-  ( ( F ` o ) e. ran F -> ( A. y e. ran F ( o e. y <-> y = ( F ` o ) ) -> E! y e. ran F o e. y ) )
62 3 59 61 syl6c 
 |-  ( ( F Fn A /\ A. p e. A ( ( F ` p ) i^i A ) = { p } ) -> ( o e. A -> E! y e. ran F o e. y ) )
63 62 ralrimiv 
 |-  ( ( F Fn A /\ A. p e. A ( ( F ` p ) i^i A ) = { p } ) -> A. o e. A E! y e. ran F o e. y )
64 nfv 
 |-  F/ x q = o
65 nfv 
 |-  F/ y q = o
66 nfvd 
 |-  ( q = o -> F/ y q e. x )
67 nfvd 
 |-  ( q = o -> F/ x o e. y )
68 eleq12 
 |-  ( ( q = o /\ x = y ) -> ( q e. x <-> o e. y ) )
69 68 ex 
 |-  ( q = o -> ( x = y -> ( q e. x <-> o e. y ) ) )
70 64 65 66 67 69 cbvreud 
 |-  ( q = o -> ( E! x e. ran F q e. x <-> E! y e. ran F o e. y ) )
71 70 cbvralvw 
 |-  ( A. q e. A E! x e. ran F q e. x <-> A. o e. A E! y e. ran F o e. y )
72 63 71 sylibr 
 |-  ( ( F Fn A /\ A. p e. A ( ( F ` p ) i^i A ) = { p } ) -> A. q e. A E! x e. ran F q e. x )