Theorem eqresfnbd

Description: Property of being the restriction of a function. Note that this is closer to funssres than fnssres . (Contributed by SN, 11-Mar-2025)

	Ref	Expression
Hypotheses	eqresfnbd.g	⊢ ( 𝜑 → 𝐹 Fn 𝐵 )
	eqresfnbd.1	⊢ ( 𝜑 → 𝐴 ⊆ 𝐵 )
Assertion	eqresfnbd	⊢ ( 𝜑 → ( 𝑅 = ( 𝐹 ↾ 𝐴 ) ↔ ( 𝑅 Fn 𝐴 ∧ 𝑅 ⊆ 𝐹 ) ) )

Proof

Step	Hyp	Ref	Expression
1		eqresfnbd.g	⊢ ( 𝜑 → 𝐹 Fn 𝐵 )
2		eqresfnbd.1	⊢ ( 𝜑 → 𝐴 ⊆ 𝐵 )
3	1 2	fnssresd	⊢ ( 𝜑 → ( 𝐹 ↾ 𝐴 ) Fn 𝐴 )
4		resss	⊢ ( 𝐹 ↾ 𝐴 ) ⊆ 𝐹
5	3 4	jctir	⊢ ( 𝜑 → ( ( 𝐹 ↾ 𝐴 ) Fn 𝐴 ∧ ( 𝐹 ↾ 𝐴 ) ⊆ 𝐹 ) )
6		fneq1	⊢ ( 𝑅 = ( 𝐹 ↾ 𝐴 ) → ( 𝑅 Fn 𝐴 ↔ ( 𝐹 ↾ 𝐴 ) Fn 𝐴 ) )
7		sseq1	⊢ ( 𝑅 = ( 𝐹 ↾ 𝐴 ) → ( 𝑅 ⊆ 𝐹 ↔ ( 𝐹 ↾ 𝐴 ) ⊆ 𝐹 ) )
8	6 7	anbi12d	⊢ ( 𝑅 = ( 𝐹 ↾ 𝐴 ) → ( ( 𝑅 Fn 𝐴 ∧ 𝑅 ⊆ 𝐹 ) ↔ ( ( 𝐹 ↾ 𝐴 ) Fn 𝐴 ∧ ( 𝐹 ↾ 𝐴 ) ⊆ 𝐹 ) ) )
9	5 8	syl5ibrcom	⊢ ( 𝜑 → ( 𝑅 = ( 𝐹 ↾ 𝐴 ) → ( 𝑅 Fn 𝐴 ∧ 𝑅 ⊆ 𝐹 ) ) )
10	1	fnfund	⊢ ( 𝜑 → Fun 𝐹 )
11	10	adantr	⊢ ( ( 𝜑 ∧ 𝑅 Fn 𝐴 ) → Fun 𝐹 )
12		funssres	⊢ ( ( Fun 𝐹 ∧ 𝑅 ⊆ 𝐹 ) → ( 𝐹 ↾ dom 𝑅 ) = 𝑅 )
13	12	eqcomd	⊢ ( ( Fun 𝐹 ∧ 𝑅 ⊆ 𝐹 ) → 𝑅 = ( 𝐹 ↾ dom 𝑅 ) )
14		fndm	⊢ ( 𝑅 Fn 𝐴 → dom 𝑅 = 𝐴 )
15	14	adantl	⊢ ( ( 𝜑 ∧ 𝑅 Fn 𝐴 ) → dom 𝑅 = 𝐴 )
16	15	reseq2d	⊢ ( ( 𝜑 ∧ 𝑅 Fn 𝐴 ) → ( 𝐹 ↾ dom 𝑅 ) = ( 𝐹 ↾ 𝐴 ) )
17	16	eqeq2d	⊢ ( ( 𝜑 ∧ 𝑅 Fn 𝐴 ) → ( 𝑅 = ( 𝐹 ↾ dom 𝑅 ) ↔ 𝑅 = ( 𝐹 ↾ 𝐴 ) ) )
18	13 17	imbitrid	⊢ ( ( 𝜑 ∧ 𝑅 Fn 𝐴 ) → ( ( Fun 𝐹 ∧ 𝑅 ⊆ 𝐹 ) → 𝑅 = ( 𝐹 ↾ 𝐴 ) ) )
19	11 18	mpand	⊢ ( ( 𝜑 ∧ 𝑅 Fn 𝐴 ) → ( 𝑅 ⊆ 𝐹 → 𝑅 = ( 𝐹 ↾ 𝐴 ) ) )
20	19	expimpd	⊢ ( 𝜑 → ( ( 𝑅 Fn 𝐴 ∧ 𝑅 ⊆ 𝐹 ) → 𝑅 = ( 𝐹 ↾ 𝐴 ) ) )
21	9 20	impbid	⊢ ( 𝜑 → ( 𝑅 = ( 𝐹 ↾ 𝐴 ) ↔ ( 𝑅 Fn 𝐴 ∧ 𝑅 ⊆ 𝐹 ) ) )