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 ffvelcdmd 
 |-  ( 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 ) )