caofrss

Description: Transfer a relation subset law to the function relation. (Contributed by Mario Carneiro, 28-Jul-2014)

	Ref	Expression
Hypotheses	caofref.1	$⊢ φ \to A \in V$
	caofref.2	$⊢ φ \to F : A ⟶ S$
	caofcom.3	$⊢ φ \to G : A ⟶ S$
	caofrss.4	$⊢ (φ \land (x \in S \land y \in S)) \to (x R y \to x T y)$
Assertion	caofrss	$⊢ φ \to (F R_{f} G \to F T_{f} G)$

Proof

Step	Hyp	Ref	Expression
1		caofref.1	$⊢ φ \to A \in V$
2		caofref.2	$⊢ φ \to F : A ⟶ S$
3		caofcom.3	$⊢ φ \to G : A ⟶ S$
4		caofrss.4	$⊢ (φ \land (x \in S \land y \in S)) \to (x R y \to x T y)$
5	2	ffvelcdmda	$⊢ (φ \land w \in A) \to F (w) \in S$
6	3	ffvelcdmda	$⊢ (φ \land w \in A) \to G (w) \in S$
7	4	ralrimivva	$⊢ φ \to \forall x \in S \forall y \in S (x R y \to x T y)$
8	7	adantr	$⊢ (φ \land w \in A) \to \forall x \in S \forall y \in S (x R y \to x T y)$
9		breq1	$⊢ x = F (w) \to (x R y \leftrightarrow F (w) R y)$
10		breq1	$⊢ x = F (w) \to (x T y \leftrightarrow F (w) T y)$
11	9 10	imbi12d	$⊢ x = F (w) \to ((x R y \to x T y) \leftrightarrow (F (w) R y \to F (w) T y))$
12		breq2	$⊢ y = G (w) \to (F (w) R y \leftrightarrow F (w) R G (w))$
13		breq2	$⊢ y = G (w) \to (F (w) T y \leftrightarrow F (w) T G (w))$
14	12 13	imbi12d	$⊢ y = G (w) \to ((F (w) R y \to F (w) T y) \leftrightarrow (F (w) R G (w) \to F (w) T G (w)))$
15	11 14	rspc2va	$⊢ ((F (w) \in S \land G (w) \in S) \land \forall x \in S \forall y \in S (x R y \to x T y)) \to (F (w) R G (w) \to F (w) T G (w))$
16	5 6 8 15	syl21anc	$⊢ (φ \land w \in A) \to (F (w) R G (w) \to F (w) T G (w))$
17	16	ralimdva	$⊢ φ \to (\forall w \in A F (w) R G (w) \to \forall w \in A F (w) T G (w))$
18	2	ffnd	$⊢ φ \to F Fn A$
19	3	ffnd	$⊢ φ \to G Fn A$
20		inidm	$⊢ A \cap A = A$
21		eqidd	$⊢ (φ \land w \in A) \to F (w) = F (w)$
22		eqidd	$⊢ (φ \land w \in A) \to G (w) = G (w)$
23	18 19 1 1 20 21 22	ofrfval	$⊢ φ \to (F R_{f} G \leftrightarrow \forall w \in A F (w) R G (w))$
24	18 19 1 1 20 21 22	ofrfval	$⊢ φ \to (F T_{f} G \leftrightarrow \forall w \in A F (w) T G (w))$
25	17 23 24	3imtr4d	$⊢ φ \to (F R_{f} G \to F T_{f} G)$

Metamath Proof Explorer

Theorem caofrss

Proof