ofrco

Description: Function relation between function compositions. (Contributed by Thierry Arnoux, 15-Jan-2026)

	Ref	Expression
Hypotheses	ofrco.1	$⊢ φ \to F Fn A$
	ofrco.2	$⊢ φ \to G Fn A$
	ofrco.3	$⊢ φ \to H : C ⟶ A$
	ofrco.4	$⊢ φ \to A \in V$
	ofrco.5	$⊢ φ \to C \in W$
	ofrco.6	$⊢ φ \to F R_{f} G$
Assertion	ofrco	$⊢ φ \to (F \circ H) R_{f} (G \circ H)$

Proof

Step	Hyp	Ref	Expression
1		ofrco.1	$⊢ φ \to F Fn A$
2		ofrco.2	$⊢ φ \to G Fn A$
3		ofrco.3	$⊢ φ \to H : C ⟶ A$
4		ofrco.4	$⊢ φ \to A \in V$
5		ofrco.5	$⊢ φ \to C \in W$
6		ofrco.6	$⊢ φ \to F R_{f} G$
7		fveq2	$⊢ y = H (x) \to F (y) = F (H (x))$
8		fveq2	$⊢ y = H (x) \to G (y) = G (H (x))$
9	7 8	breq12d	$⊢ y = H (x) \to (F (y) R G (y) \leftrightarrow F (H (x)) R G (H (x)))$
10		inidm	$⊢ A \cap A = A$
11		eqidd	$⊢ (φ \land y \in A) \to F (y) = F (y)$
12		eqidd	$⊢ (φ \land y \in A) \to G (y) = G (y)$
13	1 2 4 4 10 11 12	ofrfval	$⊢ φ \to (F R_{f} G \leftrightarrow \forall y \in A F (y) R G (y))$
14	6 13	mpbid	$⊢ φ \to \forall y \in A F (y) R G (y)$
15	14	adantr	$⊢ (φ \land x \in C) \to \forall y \in A F (y) R G (y)$
16	3	ffvelcdmda	$⊢ (φ \land x \in C) \to H (x) \in A$
17	9 15 16	rspcdva	$⊢ (φ \land x \in C) \to F (H (x)) R G (H (x))$
18	17	ralrimiva	$⊢ φ \to \forall x \in C F (H (x)) R G (H (x))$
19		fnfco	$⊢ (F Fn A \land H : C ⟶ A) \to (F \circ H) Fn C$
20	1 3 19	syl2anc	$⊢ φ \to (F \circ H) Fn C$
21		fnfco	$⊢ (G Fn A \land H : C ⟶ A) \to (G \circ H) Fn C$
22	2 3 21	syl2anc	$⊢ φ \to (G \circ H) Fn C$
23		inidm	$⊢ C \cap C = C$
24	3	adantr	$⊢ (φ \land x \in C) \to H : C ⟶ A$
25		simpr	$⊢ (φ \land x \in C) \to x \in C$
26	24 25	fvco3d	$⊢ (φ \land x \in C) \to (F \circ H) (x) = F (H (x))$
27	24 25	fvco3d	$⊢ (φ \land x \in C) \to (G \circ H) (x) = G (H (x))$
28	20 22 5 5 23 26 27	ofrfval	$⊢ φ \to ((F \circ H) R_{f} (G \circ H) \leftrightarrow \forall x \in C F (H (x)) R G (H (x)))$
29	18 28	mpbird	$⊢ φ \to (F \circ H) R_{f} (G \circ H)$

Metamath Proof Explorer

Theorem ofrco

Proof