caofid2

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

Step	Hyp	Ref	Expression
1		caofref.1	$⊢ φ \to A \in V$
2		caofref.2	$⊢ φ \to F : A ⟶ S$
3		caofid0.3	$⊢ φ \to B \in W$
4		caofid1.4	$⊢ φ \to C \in X$
5		caofid2.5	$⊢ (φ \land x \in S) \to B R x = C$
6		fnconstg	$⊢ B \in W \to (A \times \{B\}) Fn A$
7	3 6	syl	$⊢ φ \to (A \times \{B\}) Fn A$
8	2	ffnd	$⊢ φ \to F Fn A$
9		fnconstg	$⊢ C \in X \to (A \times \{C\}) Fn A$
10	4 9	syl	$⊢ φ \to (A \times \{C\}) Fn A$
11		fvconst2g	$⊢ (B \in W \land w \in A) \to (A \times \{B\}) (w) = B$
12	3 11	sylan	$⊢ (φ \land w \in A) \to (A \times \{B\}) (w) = B$
13		eqidd	$⊢ (φ \land w \in A) \to F (w) = F (w)$
14	5	ralrimiva	$⊢ φ \to \forall x \in S B R x = C$
15	2	ffvelrnda	$⊢ (φ \land w \in A) \to F (w) \in S$
16		oveq2	$⊢ x = F (w) \to B R x = B R F (w)$
17	16	eqeq1d	$⊢ x = F (w) \to (B R x = C \leftrightarrow B R F (w) = C)$
18	17	rspccva	$⊢ (\forall x \in S B R x = C \land F (w) \in S) \to B R F (w) = C$
19	14 15 18	syl2an2r	$⊢ (φ \land w \in A) \to B R F (w) = C$
20		fvconst2g	$⊢ (C \in X \land w \in A) \to (A \times \{C\}) (w) = C$
21	4 20	sylan	$⊢ (φ \land w \in A) \to (A \times \{C\}) (w) = C$
22	19 21	eqtr4d	$⊢ (φ \land w \in A) \to B R F (w) = (A \times \{C\}) (w)$
23	1 7 8 10 12 13 22	offveq	$⊢ φ \to (A \times \{B\}) R_{f} F = A \times \{C\}$

Metamath Proof Explorer