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 ( 𝜑𝐴𝑉 )
fsneqrn.b 𝐵 = { 𝐴 }
fsneqrn.f ( 𝜑𝐹 Fn 𝐵 )
fsneqrn.g ( 𝜑𝐺 Fn 𝐵 )
Assertion fsneqrn ( 𝜑 → ( 𝐹 = 𝐺 ↔ ( 𝐹𝐴 ) ∈ ran 𝐺 ) )

Proof

Step Hyp Ref Expression
1 fsneqrn.a ( 𝜑𝐴𝑉 )
2 fsneqrn.b 𝐵 = { 𝐴 }
3 fsneqrn.f ( 𝜑𝐹 Fn 𝐵 )
4 fsneqrn.g ( 𝜑𝐺 Fn 𝐵 )
5 dffn3 ( 𝐹 Fn 𝐵𝐹 : 𝐵 ⟶ ran 𝐹 )
6 3 5 sylib ( 𝜑𝐹 : 𝐵 ⟶ ran 𝐹 )
7 snidg ( 𝐴𝑉𝐴 ∈ { 𝐴 } )
8 1 7 syl ( 𝜑𝐴 ∈ { 𝐴 } )
9 2 a1i ( 𝜑𝐵 = { 𝐴 } )
10 9 eqcomd ( 𝜑 → { 𝐴 } = 𝐵 )
11 8 10 eleqtrd ( 𝜑𝐴𝐵 )
12 6 11 ffvelrnd ( 𝜑 → ( 𝐹𝐴 ) ∈ ran 𝐹 )
13 12 adantr ( ( 𝜑𝐹 = 𝐺 ) → ( 𝐹𝐴 ) ∈ ran 𝐹 )
14 simpr ( ( 𝜑𝐹 = 𝐺 ) → 𝐹 = 𝐺 )
15 14 rneqd ( ( 𝜑𝐹 = 𝐺 ) → ran 𝐹 = ran 𝐺 )
16 13 15 eleqtrd ( ( 𝜑𝐹 = 𝐺 ) → ( 𝐹𝐴 ) ∈ ran 𝐺 )
17 16 ex ( 𝜑 → ( 𝐹 = 𝐺 → ( 𝐹𝐴 ) ∈ ran 𝐺 ) )
18 simpr ( ( 𝜑 ∧ ( 𝐹𝐴 ) ∈ ran 𝐺 ) → ( 𝐹𝐴 ) ∈ ran 𝐺 )
19 dffn2 ( 𝐺 Fn 𝐵𝐺 : 𝐵 ⟶ V )
20 4 19 sylib ( 𝜑𝐺 : 𝐵 ⟶ V )
21 9 feq2d ( 𝜑 → ( 𝐺 : 𝐵 ⟶ V ↔ 𝐺 : { 𝐴 } ⟶ V ) )
22 20 21 mpbid ( 𝜑𝐺 : { 𝐴 } ⟶ V )
23 1 22 rnsnf ( 𝜑 → ran 𝐺 = { ( 𝐺𝐴 ) } )
24 23 adantr ( ( 𝜑 ∧ ( 𝐹𝐴 ) ∈ ran 𝐺 ) → ran 𝐺 = { ( 𝐺𝐴 ) } )
25 18 24 eleqtrd ( ( 𝜑 ∧ ( 𝐹𝐴 ) ∈ ran 𝐺 ) → ( 𝐹𝐴 ) ∈ { ( 𝐺𝐴 ) } )
26 elsni ( ( 𝐹𝐴 ) ∈ { ( 𝐺𝐴 ) } → ( 𝐹𝐴 ) = ( 𝐺𝐴 ) )
27 25 26 syl ( ( 𝜑 ∧ ( 𝐹𝐴 ) ∈ ran 𝐺 ) → ( 𝐹𝐴 ) = ( 𝐺𝐴 ) )
28 1 adantr ( ( 𝜑 ∧ ( 𝐹𝐴 ) ∈ ran 𝐺 ) → 𝐴𝑉 )
29 3 adantr ( ( 𝜑 ∧ ( 𝐹𝐴 ) ∈ ran 𝐺 ) → 𝐹 Fn 𝐵 )
30 4 adantr ( ( 𝜑 ∧ ( 𝐹𝐴 ) ∈ ran 𝐺 ) → 𝐺 Fn 𝐵 )
31 28 2 29 30 fsneq ( ( 𝜑 ∧ ( 𝐹𝐴 ) ∈ ran 𝐺 ) → ( 𝐹 = 𝐺 ↔ ( 𝐹𝐴 ) = ( 𝐺𝐴 ) ) )
32 27 31 mpbird ( ( 𝜑 ∧ ( 𝐹𝐴 ) ∈ ran 𝐺 ) → 𝐹 = 𝐺 )
33 32 ex ( 𝜑 → ( ( 𝐹𝐴 ) ∈ ran 𝐺𝐹 = 𝐺 ) )
34 17 33 impbid ( 𝜑 → ( 𝐹 = 𝐺 ↔ ( 𝐹𝐴 ) ∈ ran 𝐺 ) )