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 p A F p 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 A = F q A
3 sneq p = q p = q
4 2 3 eqeq12d p = q F p A = p F q A = q
5 4 cbvralvw p A F p A = p q A F q A = q
6 5 biimpi p A F p A = p q A F q A = q
7 ax-5 p A F p A = p q p A F p A = p
8 alral q p A F p A = p q A p A F p A = p
9 ralcom q A p A F p A = p p A q A F p A = p
10 9 biimpi q A p A F p A = p p A q A F p A = p
11 7 8 10 3syl p A F p A = p p A q A F p A = p
12 ax-5 q A F q A = q p q A F q A = q
13 alral p q A F q A = q p A q A F q A = q
14 12 13 syl q A F q A = q p A q A F q A = q
15 11 14 anim12i p A F p A = p q A F q A = q p A q A F p A = p p A q A F q A = q
16 6 15 mpdan p A F p A = p p A q A F p A = p p A q A F q A = q
17 r19.26-2 p A q A F p A = p F q A = q p A q A F p A = p p A q A F q A = q
18 16 17 sylibr p A F p A = p p A q A F p A = p F q A = q
19 ineq1 F p = F q F p A = F q A
20 eqeq1 F p A = p F p A = F q A p = F q A
21 eqcom p = F q A F q A = p
22 20 21 bitrdi F p A = p F p A = F q A F q A = p
23 eqeq1 F q A = q F q A = p q = p
24 eqcom q = p p = q
25 vex p V
26 sneqbg p 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 A = q F q A = p p = q
30 22 29 sylan9bb F p A = p F q A = q F p A = F q A p = q
31 19 30 syl5ib F p A = p F q A = q F p = F q p = q
32 31 ralimi q A F p A = p F q A = q q A F p = F q p = q
33 32 ralimi p A q A F p A = p F q A = q p A q A F p = F q p = q
34 18 33 syl p A F p A = p p A q A F p = F q p = q
35 34 anim2i F : A J p A F p A = p F : A J p A q A F p = F q p = q
36 dff13 F : A 1-1 J F : A J p A q A F p = F q p = q
37 35 36 sylibr F : A J p A F p A = p F : A 1-1 J