Metamath Proof Explorer


Theorem fsneqrn

Description: Equality condition for two functions defined on a singleton. (Contributed by Glauco Siliprandi, 3-Mar-2021)

Ref Expression
Hypotheses fsneqrn.a
|- ( ph -> A e. V )
fsneqrn.b
|- B = { A }
fsneqrn.f
|- ( ph -> F Fn B )
fsneqrn.g
|- ( ph -> G Fn B )
Assertion fsneqrn
|- ( ph -> ( F = G <-> ( F ` A ) e. ran G ) )

Proof

Step Hyp Ref Expression
1 fsneqrn.a
 |-  ( ph -> A e. V )
2 fsneqrn.b
 |-  B = { A }
3 fsneqrn.f
 |-  ( ph -> F Fn B )
4 fsneqrn.g
 |-  ( ph -> G Fn B )
5 dffn3
 |-  ( F Fn B <-> F : B --> ran F )
6 3 5 sylib
 |-  ( ph -> F : B --> ran F )
7 snidg
 |-  ( A e. V -> A e. { A } )
8 1 7 syl
 |-  ( ph -> A e. { A } )
9 2 a1i
 |-  ( ph -> B = { A } )
10 9 eqcomd
 |-  ( ph -> { A } = B )
11 8 10 eleqtrd
 |-  ( ph -> A e. B )
12 6 11 ffvelrnd
 |-  ( ph -> ( F ` A ) e. ran F )
13 12 adantr
 |-  ( ( ph /\ F = G ) -> ( F ` A ) e. ran F )
14 simpr
 |-  ( ( ph /\ F = G ) -> F = G )
15 14 rneqd
 |-  ( ( ph /\ F = G ) -> ran F = ran G )
16 13 15 eleqtrd
 |-  ( ( ph /\ F = G ) -> ( F ` A ) e. ran G )
17 16 ex
 |-  ( ph -> ( F = G -> ( F ` A ) e. ran G ) )
18 simpr
 |-  ( ( ph /\ ( F ` A ) e. ran G ) -> ( F ` A ) e. ran G )
19 dffn2
 |-  ( G Fn B <-> G : B --> _V )
20 4 19 sylib
 |-  ( ph -> G : B --> _V )
21 9 feq2d
 |-  ( ph -> ( G : B --> _V <-> G : { A } --> _V ) )
22 20 21 mpbid
 |-  ( ph -> G : { A } --> _V )
23 1 22 rnsnf
 |-  ( ph -> ran G = { ( G ` A ) } )
24 23 adantr
 |-  ( ( ph /\ ( F ` A ) e. ran G ) -> ran G = { ( G ` A ) } )
25 18 24 eleqtrd
 |-  ( ( ph /\ ( F ` A ) e. ran G ) -> ( F ` A ) e. { ( G ` A ) } )
26 elsni
 |-  ( ( F ` A ) e. { ( G ` A ) } -> ( F ` A ) = ( G ` A ) )
27 25 26 syl
 |-  ( ( ph /\ ( F ` A ) e. ran G ) -> ( F ` A ) = ( G ` A ) )
28 1 adantr
 |-  ( ( ph /\ ( F ` A ) e. ran G ) -> A e. V )
29 3 adantr
 |-  ( ( ph /\ ( F ` A ) e. ran G ) -> F Fn B )
30 4 adantr
 |-  ( ( ph /\ ( F ` A ) e. ran G ) -> G Fn B )
31 28 2 29 30 fsneq
 |-  ( ( ph /\ ( F ` A ) e. ran G ) -> ( F = G <-> ( F ` A ) = ( G ` A ) ) )
32 27 31 mpbird
 |-  ( ( ph /\ ( F ` A ) e. ran G ) -> F = G )
33 32 ex
 |-  ( ph -> ( ( F ` A ) e. ran G -> F = G ) )
34 17 33 impbid
 |-  ( ph -> ( F = G <-> ( F ` A ) e. ran G ) )