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	ffvelcdmd	⊢ ( 𝜑 → ( 𝐹 ‘ 𝐴 ) ∈ 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 𝐺 ) )

Metamath Proof Explorer

Theorem fsneqrn

Proof