# Metamath Proof Explorer

## Theorem caofcom

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

Ref Expression
Hypotheses caofref.1 ${⊢}{\phi }\to {A}\in {V}$
caofref.2 ${⊢}{\phi }\to {F}:{A}⟶{S}$
caofcom.3 ${⊢}{\phi }\to {G}:{A}⟶{S}$
caofcom.4 ${⊢}\left({\phi }\wedge \left({x}\in {S}\wedge {y}\in {S}\right)\right)\to {x}{R}{y}={y}{R}{x}$
Assertion caofcom ${⊢}{\phi }\to {F}{{R}}_{f}{G}={G}{{R}}_{f}{F}$

### Proof

Step Hyp Ref Expression
1 caofref.1 ${⊢}{\phi }\to {A}\in {V}$
2 caofref.2 ${⊢}{\phi }\to {F}:{A}⟶{S}$
3 caofcom.3 ${⊢}{\phi }\to {G}:{A}⟶{S}$
4 caofcom.4 ${⊢}\left({\phi }\wedge \left({x}\in {S}\wedge {y}\in {S}\right)\right)\to {x}{R}{y}={y}{R}{x}$
5 2 ffvelrnda ${⊢}\left({\phi }\wedge {w}\in {A}\right)\to {F}\left({w}\right)\in {S}$
6 3 ffvelrnda ${⊢}\left({\phi }\wedge {w}\in {A}\right)\to {G}\left({w}\right)\in {S}$
7 5 6 jca ${⊢}\left({\phi }\wedge {w}\in {A}\right)\to \left({F}\left({w}\right)\in {S}\wedge {G}\left({w}\right)\in {S}\right)$
8 4 caovcomg ${⊢}\left({\phi }\wedge \left({F}\left({w}\right)\in {S}\wedge {G}\left({w}\right)\in {S}\right)\right)\to {F}\left({w}\right){R}{G}\left({w}\right)={G}\left({w}\right){R}{F}\left({w}\right)$
9 7 8 syldan ${⊢}\left({\phi }\wedge {w}\in {A}\right)\to {F}\left({w}\right){R}{G}\left({w}\right)={G}\left({w}\right){R}{F}\left({w}\right)$
10 9 mpteq2dva ${⊢}{\phi }\to \left({w}\in {A}⟼{F}\left({w}\right){R}{G}\left({w}\right)\right)=\left({w}\in {A}⟼{G}\left({w}\right){R}{F}\left({w}\right)\right)$
11 2 feqmptd ${⊢}{\phi }\to {F}=\left({w}\in {A}⟼{F}\left({w}\right)\right)$
12 3 feqmptd ${⊢}{\phi }\to {G}=\left({w}\in {A}⟼{G}\left({w}\right)\right)$
13 1 5 6 11 12 offval2 ${⊢}{\phi }\to {F}{{R}}_{f}{G}=\left({w}\in {A}⟼{F}\left({w}\right){R}{G}\left({w}\right)\right)$
14 1 6 5 12 11 offval2 ${⊢}{\phi }\to {G}{{R}}_{f}{F}=\left({w}\in {A}⟼{G}\left({w}\right){R}{F}\left({w}\right)\right)$
15 10 13 14 3eqtr4d ${⊢}{\phi }\to {F}{{R}}_{f}{G}={G}{{R}}_{f}{F}$