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	$⊢ φ \to F Fn B$
	eqresfnbd.1	$⊢ φ \to A \subseteq B$
Assertion	eqresfnbd	$⊢ φ \to (R = {F ↾}_{A} \leftrightarrow (R Fn A \land R \subseteq F))$

Proof

Step	Hyp	Ref	Expression
1		eqresfnbd.g	$⊢ φ \to F Fn B$
2		eqresfnbd.1	$⊢ φ \to A \subseteq B$
3	1 2	fnssresd	$⊢ φ \to ({F ↾}_{A}) Fn A$
4		resss	$⊢ {F ↾}_{A} \subseteq F$
5	3 4	jctir	$⊢ φ \to (({F ↾}_{A}) Fn A \land {F ↾}_{A} \subseteq F)$
6		fneq1	$⊢ R = {F ↾}_{A} \to (R Fn A \leftrightarrow ({F ↾}_{A}) Fn A)$
7		sseq1	$⊢ R = {F ↾}_{A} \to (R \subseteq F \leftrightarrow {F ↾}_{A} \subseteq F)$
8	6 7	anbi12d	$⊢ R = {F ↾}_{A} \to ((R Fn A \land R \subseteq F) \leftrightarrow (({F ↾}_{A}) Fn A \land {F ↾}_{A} \subseteq F))$
9	5 8	syl5ibrcom	$⊢ φ \to (R = {F ↾}_{A} \to (R Fn A \land R \subseteq F))$
10	1	fnfund	$⊢ φ \to Fun F$
11	10	adantr	$⊢ (φ \land R Fn A) \to Fun F$
12		funssres	$⊢ (Fun F \land R \subseteq F) \to {F ↾}_{dom R} = R$
13	12	eqcomd	$⊢ (Fun F \land R \subseteq F) \to R = {F ↾}_{dom R}$
14		fndm	$⊢ R Fn A \to dom R = A$
15	14	adantl	$⊢ (φ \land R Fn A) \to dom R = A$
16	15	reseq2d	$⊢ (φ \land R Fn A) \to {F ↾}_{dom R} = {F ↾}_{A}$
17	16	eqeq2d	$⊢ (φ \land R Fn A) \to (R = {F ↾}_{dom R} \leftrightarrow R = {F ↾}_{A})$
18	13 17	imbitrid	$⊢ (φ \land R Fn A) \to ((Fun F \land R \subseteq F) \to R = {F ↾}_{A})$
19	11 18	mpand	$⊢ (φ \land R Fn A) \to (R \subseteq F \to R = {F ↾}_{A})$
20	19	expimpd	$⊢ φ \to ((R Fn A \land R \subseteq F) \to R = {F ↾}_{A})$
21	9 20	impbid	$⊢ φ \to (R = {F ↾}_{A} \leftrightarrow (R Fn A \land R \subseteq F))$

Metamath Proof Explorer

Theorem eqresfnbd

Proof