caofid1

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		caofid1.5	$⊢ (φ \land x \in S) \to x R B = C$
6	2	ffnd	$⊢ φ \to F Fn A$
7		fnconstg	$⊢ B \in W \to (A \times \{B\}) Fn A$
8	3 7	syl	$⊢ φ \to (A \times \{B\}) Fn A$
9		fnconstg	$⊢ C \in X \to (A \times \{C\}) Fn A$
10	4 9	syl	$⊢ φ \to (A \times \{C\}) Fn A$
11		eqidd	$⊢ (φ \land w \in A) \to F (w) = F (w)$
12		fvconst2g	$⊢ (B \in W \land w \in A) \to (A \times \{B\}) (w) = B$
13	3 12	sylan	$⊢ (φ \land w \in A) \to (A \times \{B\}) (w) = B$
14	5	ralrimiva	$⊢ φ \to \forall x \in S x R B = C$
15	2	ffvelrnda	$⊢ (φ \land w \in A) \to F (w) \in S$
16		oveq1	$⊢ x = F (w) \to x R B = F (w) R B$
17	16	eqeq1d	$⊢ x = F (w) \to (x R B = C \leftrightarrow F (w) R B = C)$
18	17	rspccva	$⊢ (\forall x \in S x R B = C \land F (w) \in S) \to F (w) R B = C$
19	14 15 18	syl2an2r	$⊢ (φ \land w \in A) \to F (w) R B = 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 F (w) R B = (A \times \{C\}) (w)$
23	1 6 8 10 11 13 22	offveq	$⊢ φ \to F R_{f} (A \times \{B\}) = A \times \{C\}$

Metamath Proof Explorer