ofres

Description: Restrict the operands of a function operation to the same domain as that of the operation itself. (Contributed by Mario Carneiro, 15-Sep-2014)

	Ref	Expression
Hypotheses	ofres.1	$⊢ φ \to F Fn A$
	ofres.2	$⊢ φ \to G Fn B$
	ofres.3	$⊢ φ \to A \in V$
	ofres.4	$⊢ φ \to B \in W$
	ofres.5	$⊢ A \cap B = C$
Assertion	ofres	$⊢ φ \to F R_{f} G = ({F ↾}_{C}) R_{f} ({G ↾}_{C})$

Proof

Step	Hyp	Ref	Expression
1		ofres.1	$⊢ φ \to F Fn A$
2		ofres.2	$⊢ φ \to G Fn B$
3		ofres.3	$⊢ φ \to A \in V$
4		ofres.4	$⊢ φ \to B \in W$
5		ofres.5	$⊢ A \cap B = C$
6		eqidd	$⊢ (φ \land x \in A) \to F (x) = F (x)$
7		eqidd	$⊢ (φ \land x \in B) \to G (x) = G (x)$
8	1 2 3 4 5 6 7	offval	$⊢ φ \to F R_{f} G = (x \in C ⟼ F (x) R G (x))$
9		inss1	$⊢ A \cap B \subseteq A$
10	5 9	eqsstrri	$⊢ C \subseteq A$
11		fnssres	$⊢ (F Fn A \land C \subseteq A) \to ({F ↾}_{C}) Fn C$
12	1 10 11	sylancl	$⊢ φ \to ({F ↾}_{C}) Fn C$
13		inss2	$⊢ A \cap B \subseteq B$
14	5 13	eqsstrri	$⊢ C \subseteq B$
15		fnssres	$⊢ (G Fn B \land C \subseteq B) \to ({G ↾}_{C}) Fn C$
16	2 14 15	sylancl	$⊢ φ \to ({G ↾}_{C}) Fn C$
17		ssexg	$⊢ (C \subseteq A \land A \in V) \to C \in V$
18	10 3 17	sylancr	$⊢ φ \to C \in V$
19		inidm	$⊢ C \cap C = C$
20		fvres	$⊢ x \in C \to ({F ↾}_{C}) (x) = F (x)$
21	20	adantl	$⊢ (φ \land x \in C) \to ({F ↾}_{C}) (x) = F (x)$
22		fvres	$⊢ x \in C \to ({G ↾}_{C}) (x) = G (x)$
23	22	adantl	$⊢ (φ \land x \in C) \to ({G ↾}_{C}) (x) = G (x)$
24	12 16 18 18 19 21 23	offval	$⊢ φ \to ({F ↾}_{C}) R_{f} ({G ↾}_{C}) = (x \in C ⟼ F (x) R G (x))$
25	8 24	eqtr4d	$⊢ φ \to F R_{f} G = ({F ↾}_{C}) R_{f} ({G ↾}_{C})$

Metamath Proof Explorer

Theorem ofres

Proof