# Metamath Proof Explorer

## Theorem caofid2

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

Ref Expression
Hypotheses caofref.1 ${⊢}{\phi }\to {A}\in {V}$
caofref.2 ${⊢}{\phi }\to {F}:{A}⟶{S}$
caofid0.3 ${⊢}{\phi }\to {B}\in {W}$
caofid1.4 ${⊢}{\phi }\to {C}\in {X}$
caofid2.5 ${⊢}\left({\phi }\wedge {x}\in {S}\right)\to {B}{R}{x}={C}$
Assertion caofid2 ${⊢}{\phi }\to \left({A}×\left\{{B}\right\}\right){{R}}_{f}{F}={A}×\left\{{C}\right\}$

### Proof

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