ofmres

Description: Equivalent expressions for a restriction of the function operation map. Unlike oF R which is a proper class, ` ( oF R |`( A X. B ) ) can be a set by ofmresex , allowing it to be used as a function or structure argument. By ofmresval , the restricted operation map values are the same as the original values, allowing theorems for oF R to be reused. (Contributed by NM, 20-Oct-2014)

		Ref	Expression
	Assertion	ofmres	$⊢ {\circ_{f} R ↾}_{(A \times B)} = (f \in A, g \in B ⟼ f R_{f} g)$

Proof

Step	Hyp	Ref	Expression
1		ssv	$⊢ A \subseteq V$
2		ssv	$⊢ B \subseteq V$
3		resmpo	$⊢ (A \subseteq V \land B \subseteq V) \to {(f \in V, g \in V ⟼ (x \in (dom f \cap dom g) ⟼ f (x) R g (x))) ↾}_{(A \times B)} = (f \in A, g \in B ⟼ (x \in (dom f \cap dom g) ⟼ f (x) R g (x)))$
4	1 2 3	mp2an	$⊢ {(f \in V, g \in V ⟼ (x \in (dom f \cap dom g) ⟼ f (x) R g (x))) ↾}_{(A \times B)} = (f \in A, g \in B ⟼ (x \in (dom f \cap dom g) ⟼ f (x) R g (x)))$
5		df-of	$⊢ \circ_{f} R = (f \in V, g \in V ⟼ (x \in (dom f \cap dom g) ⟼ f (x) R g (x)))$
6	5	reseq1i	$⊢ {\circ_{f} R ↾}_{(A \times B)} = {(f \in V, g \in V ⟼ (x \in (dom f \cap dom g) ⟼ f (x) R g (x))) ↾}_{(A \times B)}$
7		eqid	$⊢ A = A$
8		eqid	$⊢ B = B$
9		vex	$⊢ f \in V$
10		vex	$⊢ g \in V$
11	9	dmex	$⊢ dom f \in V$
12	11	inex1	$⊢ dom f \cap dom g \in V$
13	12	mptex	$⊢ (x \in (dom f \cap dom g) ⟼ f (x) R g (x)) \in V$
14	5	ovmpt4g	$⊢ (f \in V \land g \in V \land (x \in (dom f \cap dom g) ⟼ f (x) R g (x)) \in V) \to f R_{f} g = (x \in (dom f \cap dom g) ⟼ f (x) R g (x))$
15	9 10 13 14	mp3an	$⊢ f R_{f} g = (x \in (dom f \cap dom g) ⟼ f (x) R g (x))$
16	7 8 15	mpoeq123i	$⊢ (f \in A, g \in B ⟼ f R_{f} g) = (f \in A, g \in B ⟼ (x \in (dom f \cap dom g) ⟼ f (x) R g (x)))$
17	4 6 16	3eqtr4i	$⊢ {\circ_{f} R ↾}_{(A \times B)} = (f \in A, g \in B ⟼ f R_{f} g)$

Metamath Proof Explorer

Theorem ofmres

Proof