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 f/c 𝑅 = ( 𝑓 ∈ V , 𝑐 ∈ V ↦ ( 𝑥 ∈ dom 𝑓 ↦ ( ( 𝑓𝑥 ) 𝑅 𝑐 ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cR 𝑅
1 0 cofc f/c 𝑅
2 vf 𝑓
3 cvv V
4 vc 𝑐
5 vx 𝑥
6 2 cv 𝑓
7 6 cdm dom 𝑓
8 5 cv 𝑥
9 8 6 cfv ( 𝑓𝑥 )
10 4 cv 𝑐
11 9 10 0 co ( ( 𝑓𝑥 ) 𝑅 𝑐 )
12 5 7 11 cmpt ( 𝑥 ∈ dom 𝑓 ↦ ( ( 𝑓𝑥 ) 𝑅 𝑐 ) )
13 2 4 3 3 12 cmpo ( 𝑓 ∈ V , 𝑐 ∈ V ↦ ( 𝑥 ∈ dom 𝑓 ↦ ( ( 𝑓𝑥 ) 𝑅 𝑐 ) ) )
14 1 13 wceq f/c 𝑅 = ( 𝑓 ∈ V , 𝑐 ∈ V ↦ ( 𝑥 ∈ dom 𝑓 ↦ ( ( 𝑓𝑥 ) 𝑅 𝑐 ) ) )