Metamath Proof Explorer

Theorem fvineqsnf1

Description: A theorem about functions where the image of every point intersects the domain only at that point. If J is a topology and A is a set with no limit points, then there exists an F such that this antecedent is true. See nlpfvineqsn for a proof of this fact. (Contributed by ML, 23-Mar-2021)

Ref Expression
Assertion fvineqsnf1 
|- ( ( F : A --> J /\ A. p e. A ( ( F ` p ) i^i A ) = { p } ) -> F : A -1-1-> J )

Proof

Step Hyp Ref Expression
1 fveq2 
 |-  ( p = q -> ( F ` p ) = ( F ` q ) )
2 1 ineq1d 
 |-  ( p = q -> ( ( F ` p ) i^i A ) = ( ( F ` q ) i^i A ) )
3 sneq 
 |-  ( p = q -> { p } = { q } )
4 2 3 eqeq12d 
 |-  ( p = q -> ( ( ( F ` p ) i^i A ) = { p } <-> ( ( F ` q ) i^i A ) = { q } ) )
5 4 cbvralvw 
 |-  ( A. p e. A ( ( F ` p ) i^i A ) = { p } <-> A. q e. A ( ( F ` q ) i^i A ) = { q } )
6 5 biimpi 
 |-  ( A. p e. A ( ( F ` p ) i^i A ) = { p } -> A. q e. A ( ( F ` q ) i^i A ) = { q } )
7 ax-5 
 |-  ( A. p e. A ( ( F ` p ) i^i A ) = { p } -> A. q A. p e. A ( ( F ` p ) i^i A ) = { p } )
8 alral 
 |-  ( A. q A. p e. A ( ( F ` p ) i^i A ) = { p } -> A. q e. A A. p e. A ( ( F ` p ) i^i A ) = { p } )
9 ralcom 
 |-  ( A. q e. A A. p e. A ( ( F ` p ) i^i A ) = { p } <-> A. p e. A A. q e. A ( ( F ` p ) i^i A ) = { p } )
10 9 biimpi 
 |-  ( A. q e. A A. p e. A ( ( F ` p ) i^i A ) = { p } -> A. p e. A A. q e. A ( ( F ` p ) i^i A ) = { p } )
11 7 8 10 3syl 
 |-  ( A. p e. A ( ( F ` p ) i^i A ) = { p } -> A. p e. A A. q e. A ( ( F ` p ) i^i A ) = { p } )
12 ax-5 
 |-  ( A. q e. A ( ( F ` q ) i^i A ) = { q } -> A. p A. q e. A ( ( F ` q ) i^i A ) = { q } )
13 alral 
 |-  ( A. p A. q e. A ( ( F ` q ) i^i A ) = { q } -> A. p e. A A. q e. A ( ( F ` q ) i^i A ) = { q } )
14 12 13 syl 
 |-  ( A. q e. A ( ( F ` q ) i^i A ) = { q } -> A. p e. A A. q e. A ( ( F ` q ) i^i A ) = { q } )
15 11 14 anim12i 
 |-  ( ( A. p e. A ( ( F ` p ) i^i A ) = { p } /\ A. q e. A ( ( F ` q ) i^i A ) = { q } ) -> ( A. p e. A A. q e. A ( ( F ` p ) i^i A ) = { p } /\ A. p e. A A. q e. A ( ( F ` q ) i^i A ) = { q } ) )
16 6 15 mpdan 
 |-  ( A. p e. A ( ( F ` p ) i^i A ) = { p } -> ( A. p e. A A. q e. A ( ( F ` p ) i^i A ) = { p } /\ A. p e. A A. q e. A ( ( F ` q ) i^i A ) = { q } ) )
17 r19.26-2 
 |-  ( A. p e. A A. q e. A ( ( ( F ` p ) i^i A ) = { p } /\ ( ( F ` q ) i^i A ) = { q } ) <-> ( A. p e. A A. q e. A ( ( F ` p ) i^i A ) = { p } /\ A. p e. A A. q e. A ( ( F ` q ) i^i A ) = { q } ) )
18 16 17 sylibr 
 |-  ( A. p e. A ( ( F ` p ) i^i A ) = { p } -> A. p e. A A. q e. A ( ( ( F ` p ) i^i A ) = { p } /\ ( ( F ` q ) i^i A ) = { q } ) )
19 ineq1 
 |-  ( ( F ` p ) = ( F ` q ) -> ( ( F ` p ) i^i A ) = ( ( F ` q ) i^i A ) )
20 eqeq1 
 |-  ( ( ( F ` p ) i^i A ) = { p } -> ( ( ( F ` p ) i^i A ) = ( ( F ` q ) i^i A ) <-> { p } = ( ( F ` q ) i^i A ) ) )
21 eqcom 
 |-  ( { p } = ( ( F ` q ) i^i A ) <-> ( ( F ` q ) i^i A ) = { p } )
22 20 21 bitrdi 
 |-  ( ( ( F ` p ) i^i A ) = { p } -> ( ( ( F ` p ) i^i A ) = ( ( F ` q ) i^i A ) <-> ( ( F ` q ) i^i A ) = { p } ) )
23 eqeq1 
 |-  ( ( ( F ` q ) i^i A ) = { q } -> ( ( ( F ` q ) i^i A ) = { p } <-> { q } = { p } ) )
24 eqcom 
 |-  ( { q } = { p } <-> { p } = { q } )
25 vex 
 |-  p e. _V
26 sneqbg 
 |-  ( p e. _V -> ( { p } = { q } <-> p = q ) )
27 25 26 ax-mp 
 |-  ( { p } = { q } <-> p = q )
28 24 27 bitri 
 |-  ( { q } = { p } <-> p = q )
29 23 28 bitrdi 
 |-  ( ( ( F ` q ) i^i A ) = { q } -> ( ( ( F ` q ) i^i A ) = { p } <-> p = q ) )
30 22 29 sylan9bb 
 |-  ( ( ( ( F ` p ) i^i A ) = { p } /\ ( ( F ` q ) i^i A ) = { q } ) -> ( ( ( F ` p ) i^i A ) = ( ( F ` q ) i^i A ) <-> p = q ) )
31 19 30 imbitrid 
 |-  ( ( ( ( F ` p ) i^i A ) = { p } /\ ( ( F ` q ) i^i A ) = { q } ) -> ( ( F ` p ) = ( F ` q ) -> p = q ) )
32 31 ralimi 
 |-  ( A. q e. A ( ( ( F ` p ) i^i A ) = { p } /\ ( ( F ` q ) i^i A ) = { q } ) -> A. q e. A ( ( F ` p ) = ( F ` q ) -> p = q ) )
33 32 ralimi 
 |-  ( A. p e. A A. q e. A ( ( ( F ` p ) i^i A ) = { p } /\ ( ( F ` q ) i^i A ) = { q } ) -> A. p e. A A. q e. A ( ( F ` p ) = ( F ` q ) -> p = q ) )
34 18 33 syl 
 |-  ( A. p e. A ( ( F ` p ) i^i A ) = { p } -> A. p e. A A. q e. A ( ( F ` p ) = ( F ` q ) -> p = q ) )
35 34 anim2i 
 |-  ( ( F : A --> J /\ A. p e. A ( ( F ` p ) i^i A ) = { p } ) -> ( F : A --> J /\ A. p e. A A. q e. A ( ( F ` p ) = ( F ` q ) -> p = q ) ) )
36 dff13 
 |-  ( F : A -1-1-> J <-> ( F : A --> J /\ A. p e. A A. q e. A ( ( F ` p ) = ( F ` q ) -> p = q ) ) )
37 35 36 sylibr 
 |-  ( ( F : A --> J /\ A. p e. A ( ( F ` p ) i^i A ) = { p } ) -> F : A -1-1-> J )