Metamath Proof Explorer

Definition df-ofc

Description: Define the function/constant operation map. The definition is designed so that if R is a binary operation, then oFC R is the analogous operation on functions and constants. (Contributed by Thierry Arnoux, 21-Jan-2017)

Ref Expression
Assertion df-ofc ⊢ ∘ fc ⁡ R = f ∈ V , c ∈ V ⟼ x ∈ dom ⁡ f ⟼ f ⁡ x R c

Detailed syntax breakdown

Step Hyp Ref Expression
0 cR class R
1 0 cofc class ∘ fc ⁡ R
2 vf setvar f
3 cvv class V
4 vc setvar c
5 vx setvar x
6 2 cv setvar f
7 6 cdm class dom ⁡ f
8 5 cv setvar x
9 8 6 cfv class f ⁡ x
10 4 cv setvar c
11 9 10 0 co class f ⁡ x R c
12 5 7 11 cmpt class x ∈ dom ⁡ f ⟼ f ⁡ x R c
13 2 4 3 3 12 cmpo class f ∈ V , c ∈ V ⟼ x ∈ dom ⁡ f ⟼ f ⁡ x R c
14 1 13 wceq wff ∘ fc ⁡ R = f ∈ V , c ∈ V ⟼ x ∈ dom ⁡ f ⟼ f ⁡ x R c