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 ( ( 𝐹 : 𝐴 ⟶ 𝐽 ∧ ∀ 𝑝 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } ) → 𝐹 : 𝐴 –1-1→ 𝐽 )

Proof

Step Hyp Ref Expression
1 fveq2 ⊢ ( 𝑝 = 𝑞 → ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ 𝑞 ) )
2 1 ineq1d ⊢ ( 𝑝 = 𝑞 → ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = ( ( 𝐹 ‘ 𝑞 ) ∩ 𝐴 ) )
3 sneq ⊢ ( 𝑝 = 𝑞 → { 𝑝 } = { 𝑞 } )
4 2 3 eqeq12d ⊢ ( 𝑝 = 𝑞 → ( ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } ↔ ( ( 𝐹 ‘ 𝑞 ) ∩ 𝐴 ) = { 𝑞 } ) )
5 4 cbvralvw ⊢ ( ∀ 𝑝 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } ↔ ∀ 𝑞 ∈ 𝐴 ( ( 𝐹 ‘ 𝑞 ) ∩ 𝐴 ) = { 𝑞 } )
6 5 biimpi ⊢ ( ∀ 𝑝 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } → ∀ 𝑞 ∈ 𝐴 ( ( 𝐹 ‘ 𝑞 ) ∩ 𝐴 ) = { 𝑞 } )
7 ax-5 ⊢ ( ∀ 𝑝 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } → ∀ 𝑞 ∀ 𝑝 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } )
8 alral ⊢ ( ∀ 𝑞 ∀ 𝑝 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } → ∀ 𝑞 ∈ 𝐴 ∀ 𝑝 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } )
9 ralcom ⊢ ( ∀ 𝑞 ∈ 𝐴 ∀ 𝑝 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } ↔ ∀ 𝑝 ∈ 𝐴 ∀ 𝑞 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } )
10 9 biimpi ⊢ ( ∀ 𝑞 ∈ 𝐴 ∀ 𝑝 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } → ∀ 𝑝 ∈ 𝐴 ∀ 𝑞 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } )
11 7 8 10 3syl ⊢ ( ∀ 𝑝 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } → ∀ 𝑝 ∈ 𝐴 ∀ 𝑞 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } )
12 ax-5 ⊢ ( ∀ 𝑞 ∈ 𝐴 ( ( 𝐹 ‘ 𝑞 ) ∩ 𝐴 ) = { 𝑞 } → ∀ 𝑝 ∀ 𝑞 ∈ 𝐴 ( ( 𝐹 ‘ 𝑞 ) ∩ 𝐴 ) = { 𝑞 } )
13 alral ⊢ ( ∀ 𝑝 ∀ 𝑞 ∈ 𝐴 ( ( 𝐹 ‘ 𝑞 ) ∩ 𝐴 ) = { 𝑞 } → ∀ 𝑝 ∈ 𝐴 ∀ 𝑞 ∈ 𝐴 ( ( 𝐹 ‘ 𝑞 ) ∩ 𝐴 ) = { 𝑞 } )
14 12 13 syl ⊢ ( ∀ 𝑞 ∈ 𝐴 ( ( 𝐹 ‘ 𝑞 ) ∩ 𝐴 ) = { 𝑞 } → ∀ 𝑝 ∈ 𝐴 ∀ 𝑞 ∈ 𝐴 ( ( 𝐹 ‘ 𝑞 ) ∩ 𝐴 ) = { 𝑞 } )
15 11 14 anim12i ⊢ ( ( ∀ 𝑝 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } ∧ ∀ 𝑞 ∈ 𝐴 ( ( 𝐹 ‘ 𝑞 ) ∩ 𝐴 ) = { 𝑞 } ) → ( ∀ 𝑝 ∈ 𝐴 ∀ 𝑞 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } ∧ ∀ 𝑝 ∈ 𝐴 ∀ 𝑞 ∈ 𝐴 ( ( 𝐹 ‘ 𝑞 ) ∩ 𝐴 ) = { 𝑞 } ) )
16 6 15 mpdan ⊢ ( ∀ 𝑝 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } → ( ∀ 𝑝 ∈ 𝐴 ∀ 𝑞 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } ∧ ∀ 𝑝 ∈ 𝐴 ∀ 𝑞 ∈ 𝐴 ( ( 𝐹 ‘ 𝑞 ) ∩ 𝐴 ) = { 𝑞 } ) )
17 r19.26-2 ⊢ ( ∀ 𝑝 ∈ 𝐴 ∀ 𝑞 ∈ 𝐴 ( ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } ∧ ( ( 𝐹 ‘ 𝑞 ) ∩ 𝐴 ) = { 𝑞 } ) ↔ ( ∀ 𝑝 ∈ 𝐴 ∀ 𝑞 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } ∧ ∀ 𝑝 ∈ 𝐴 ∀ 𝑞 ∈ 𝐴 ( ( 𝐹 ‘ 𝑞 ) ∩ 𝐴 ) = { 𝑞 } ) )
18 16 17 sylibr ⊢ ( ∀ 𝑝 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } → ∀ 𝑝 ∈ 𝐴 ∀ 𝑞 ∈ 𝐴 ( ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } ∧ ( ( 𝐹 ‘ 𝑞 ) ∩ 𝐴 ) = { 𝑞 } ) )
19 ineq1 ⊢ ( ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ 𝑞 ) → ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = ( ( 𝐹 ‘ 𝑞 ) ∩ 𝐴 ) )
20 eqeq1 ⊢ ( ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } → ( ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = ( ( 𝐹 ‘ 𝑞 ) ∩ 𝐴 ) ↔ { 𝑝 } = ( ( 𝐹 ‘ 𝑞 ) ∩ 𝐴 ) ) )
21 eqcom ⊢ ( { 𝑝 } = ( ( 𝐹 ‘ 𝑞 ) ∩ 𝐴 ) ↔ ( ( 𝐹 ‘ 𝑞 ) ∩ 𝐴 ) = { 𝑝 } )
22 20 21 bitrdi ⊢ ( ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } → ( ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = ( ( 𝐹 ‘ 𝑞 ) ∩ 𝐴 ) ↔ ( ( 𝐹 ‘ 𝑞 ) ∩ 𝐴 ) = { 𝑝 } ) )
23 eqeq1 ⊢ ( ( ( 𝐹 ‘ 𝑞 ) ∩ 𝐴 ) = { 𝑞 } → ( ( ( 𝐹 ‘ 𝑞 ) ∩ 𝐴 ) = { 𝑝 } ↔ { 𝑞 } = { 𝑝 } ) )
24 eqcom ⊢ ( { 𝑞 } = { 𝑝 } ↔ { 𝑝 } = { 𝑞 } )
25 vex ⊢ 𝑝 ∈ V
26 sneqbg ⊢ ( 𝑝 ∈ V → ( { 𝑝 } = { 𝑞 } ↔ 𝑝 = 𝑞 ) )
27 25 26 ax-mp ⊢ ( { 𝑝 } = { 𝑞 } ↔ 𝑝 = 𝑞 )
28 24 27 bitri ⊢ ( { 𝑞 } = { 𝑝 } ↔ 𝑝 = 𝑞 )
29 23 28 bitrdi ⊢ ( ( ( 𝐹 ‘ 𝑞 ) ∩ 𝐴 ) = { 𝑞 } → ( ( ( 𝐹 ‘ 𝑞 ) ∩ 𝐴 ) = { 𝑝 } ↔ 𝑝 = 𝑞 ) )
30 22 29 sylan9bb ⊢ ( ( ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } ∧ ( ( 𝐹 ‘ 𝑞 ) ∩ 𝐴 ) = { 𝑞 } ) → ( ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = ( ( 𝐹 ‘ 𝑞 ) ∩ 𝐴 ) ↔ 𝑝 = 𝑞 ) )
31 19 30 syl5ib ⊢ ( ( ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } ∧ ( ( 𝐹 ‘ 𝑞 ) ∩ 𝐴 ) = { 𝑞 } ) → ( ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ 𝑞 ) → 𝑝 = 𝑞 ) )
32 31 ralimi ⊢ ( ∀ 𝑞 ∈ 𝐴 ( ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } ∧ ( ( 𝐹 ‘ 𝑞 ) ∩ 𝐴 ) = { 𝑞 } ) → ∀ 𝑞 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ 𝑞 ) → 𝑝 = 𝑞 ) )
33 32 ralimi ⊢ ( ∀ 𝑝 ∈ 𝐴 ∀ 𝑞 ∈ 𝐴 ( ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } ∧ ( ( 𝐹 ‘ 𝑞 ) ∩ 𝐴 ) = { 𝑞 } ) → ∀ 𝑝 ∈ 𝐴 ∀ 𝑞 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ 𝑞 ) → 𝑝 = 𝑞 ) )
34 18 33 syl ⊢ ( ∀ 𝑝 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } → ∀ 𝑝 ∈ 𝐴 ∀ 𝑞 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ 𝑞 ) → 𝑝 = 𝑞 ) )
35 34 anim2i ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐽 ∧ ∀ 𝑝 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } ) → ( 𝐹 : 𝐴 ⟶ 𝐽 ∧ ∀ 𝑝 ∈ 𝐴 ∀ 𝑞 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ 𝑞 ) → 𝑝 = 𝑞 ) ) )
36 dff13 ⊢ ( 𝐹 : 𝐴 –1-1→ 𝐽 ↔ ( 𝐹 : 𝐴 ⟶ 𝐽 ∧ ∀ 𝑝 ∈ 𝐴 ∀ 𝑞 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ 𝑞 ) → 𝑝 = 𝑞 ) ) )
37 35 36 sylibr ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐽 ∧ ∀ 𝑝 ∈ 𝐴 ( ( 𝐹 ‘ 𝑝 ) ∩ 𝐴 ) = { 𝑝 } ) → 𝐹 : 𝐴 –1-1→ 𝐽 )