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 eqabrd 
 |-  ( 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 eleq2w2 
 |-  ( 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 eleq2w2 
 |-  ( ( ( 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 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 ) ) )
38 36 37 simpl2im 
 |-  ( ( 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 ) ) )
39 rsp 
 |-  ( A. o e. A ( ( F ` p ) = ( F ` o ) -> p = o ) -> ( o e. A -> ( ( F ` p ) = ( F ` o ) -> p = o ) ) )
40 38 39 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 ) ) ) )
41 40 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 ) )
42 fveq2 
 |-  ( p = o -> ( F ` p ) = ( F ` o ) )
43 41 42 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 ) )
44 31 43 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 ) )
45 44 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 ) ) )
46 45 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 ) ) )
47 46 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 ) )
48 47 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 ) )
49 30 48 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 ) ) )
50 49 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 ) ) ) )
51 50 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 ) ) )
52 51 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 ) ) ) ) )
53 9 10 52 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 ) ) ) )
54 6 53 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 ) ) ) )
55 rsp 
 |-  ( A. o e. A ( o e. y <-> y = ( F ` o ) ) -> ( o e. A -> ( o e. y <-> y = ( F ` o ) ) ) )
56 54 55 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 ) ) ) ) )
57 56 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 ) ) ) ) )
58 57 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 ) ) ) )
59 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 )
60 59 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 ) )
61 3 58 60 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 ) )
62 61 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 )
63 nfv 
 |-  F/ x q = o
64 nfv 
 |-  F/ y q = o
65 nfvd 
 |-  ( q = o -> F/ y q e. x )
66 nfvd 
 |-  ( q = o -> F/ x o e. y )
67 elequ12 
 |-  ( ( q = o /\ x = y ) -> ( q e. x <-> o e. y ) )
68 67 ex 
 |-  ( q = o -> ( x = y -> ( q e. x <-> o e. y ) ) )
69 63 64 65 66 68 cbvreud 
 |-  ( q = o -> ( E! x e. ran F q e. x <-> E! y e. ran F o e. y ) )
70 69 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 )
71 62 70 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 )