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 ⊢ φ → A ∈ V
fsneqrn.b ⊢ B = A
fsneqrn.f ⊢ φ → F Fn B
fsneqrn.g ⊢ φ → G Fn B
Assertion fsneqrn ⊢ φ → F = G ↔ F ⁡ A ∈ ran ⁡ G

Proof

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