offval3

Description: General value of ( F oF R G ) with no assumptions on functionality of F and G . (Contributed by Stefan O'Rear, 24-Jan-2015)

		Ref	Expression
	Assertion	offval3	$⊢ (F \in V \land G \in W) \to F R_{f} G = (x \in (dom F \cap dom G) ⟼ F (x) R G (x))$

Step	Hyp	Ref	Expression
1		elex	$⊢ F \in V \to F \in V$
2	1	adantr	$⊢ (F \in V \land G \in W) \to F \in V$
3		elex	$⊢ G \in W \to G \in V$
4	3	adantl	$⊢ (F \in V \land G \in W) \to G \in V$
5		dmexg	$⊢ F \in V \to dom F \in V$
6		inex1g	$⊢ dom F \in V \to dom F \cap dom G \in V$
7		mptexg	$⊢ dom F \cap dom G \in V \to (x \in (dom F \cap dom G) ⟼ F (x) R G (x)) \in V$
8	5 6 7	3syl	$⊢ F \in V \to (x \in (dom F \cap dom G) ⟼ F (x) R G (x)) \in V$
9	8	adantr	$⊢ (F \in V \land G \in W) \to (x \in (dom F \cap dom G) ⟼ F (x) R G (x)) \in V$
10		dmeq	$⊢ a = F \to dom a = dom F$
11		dmeq	$⊢ b = G \to dom b = dom G$
12	10 11	ineqan12d	$⊢ (a = F \land b = G) \to dom a \cap dom b = dom F \cap dom G$
13		fveq1	$⊢ a = F \to a (x) = F (x)$
14		fveq1	$⊢ b = G \to b (x) = G (x)$
15	13 14	oveqan12d	$⊢ (a = F \land b = G) \to a (x) R b (x) = F (x) R G (x)$
16	12 15	mpteq12dv	$⊢ (a = F \land b = G) \to (x \in (dom a \cap dom b) ⟼ a (x) R b (x)) = (x \in (dom F \cap dom G) ⟼ F (x) R G (x))$
17		df-of	$⊢ \circ_{f} R = (a \in V, b \in V ⟼ (x \in (dom a \cap dom b) ⟼ a (x) R b (x)))$
18	16 17	ovmpoga	$⊢ (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))$
19	2 4 9 18	syl3anc	$⊢ (F \in V \land G \in W) \to F R_{f} G = (x \in (dom F \cap dom G) ⟼ F (x) R G (x))$

Metamath Proof Explorer