This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database ZF (ZERMELO-FRAENKEL) SET THEORY ZF Set Theory - add the Axiom of Power Sets Function operation df-of
Definition df-of
Description: Define the function operation map. The definition is designed so that
if R is a binary operation, then oF R is the analogous operation
on functions which corresponds to applying R pointwise to the values
of the functions. (Contributed by Mario Carneiro , 20-Jul-2014)
Ref
Expression
Assertion
df-of ⊢ ∘f 𝑅 = ( 𝑓 ∈ V , 𝑔 ∈ V ↦ ( 𝑥 ∈ ( dom 𝑓 ∩ dom 𝑔 ) ↦ ( ( 𝑓 ‘ 𝑥 ) 𝑅 ( 𝑔 ‘ 𝑥 ) ) ) )
Detailed syntax breakdown
Step
Hyp
Ref
Expression
0
cR ⊢ 𝑅
1
0
cof ⊢ ∘f 𝑅
2
vf ⊢ 𝑓
3
cvv ⊢ V
4
vg ⊢ 𝑔
5
vx ⊢ 𝑥
6
2
cv ⊢ 𝑓
7
6
cdm ⊢ dom 𝑓
8
4
cv ⊢ 𝑔
9
8
cdm ⊢ dom 𝑔
10
7 9
cin ⊢ ( dom 𝑓 ∩ dom 𝑔 )
11
5
cv ⊢ 𝑥
12
11 6
cfv ⊢ ( 𝑓 ‘ 𝑥 )
13
11 8
cfv ⊢ ( 𝑔 ‘ 𝑥 )
14
12 13 0
co ⊢ ( ( 𝑓 ‘ 𝑥 ) 𝑅 ( 𝑔 ‘ 𝑥 ) )
15
5 10 14
cmpt ⊢ ( 𝑥 ∈ ( dom 𝑓 ∩ dom 𝑔 ) ↦ ( ( 𝑓 ‘ 𝑥 ) 𝑅 ( 𝑔 ‘ 𝑥 ) ) )
16
2 4 3 3 15
cmpo ⊢ ( 𝑓 ∈ V , 𝑔 ∈ V ↦ ( 𝑥 ∈ ( dom 𝑓 ∩ dom 𝑔 ) ↦ ( ( 𝑓 ‘ 𝑥 ) 𝑅 ( 𝑔 ‘ 𝑥 ) ) ) )
17
1 16
wceq ⊢ ∘f 𝑅 = ( 𝑓 ∈ V , 𝑔 ∈ V ↦ ( 𝑥 ∈ ( dom 𝑓 ∩ dom 𝑔 ) ↦ ( ( 𝑓 ‘ 𝑥 ) 𝑅 ( 𝑔 ‘ 𝑥 ) ) ) )