# Metamath Proof Explorer

## Theorem offval2

Description: The function operation expressed as a mapping. (Contributed by Mario Carneiro, 20-Jul-2014)

Ref Expression
Hypotheses offval2.1 ( 𝜑𝐴𝑉 )
offval2.2 ( ( 𝜑𝑥𝐴 ) → 𝐵𝑊 )
offval2.3 ( ( 𝜑𝑥𝐴 ) → 𝐶𝑋 )
offval2.4 ( 𝜑𝐹 = ( 𝑥𝐴𝐵 ) )
offval2.5 ( 𝜑𝐺 = ( 𝑥𝐴𝐶 ) )
Assertion offval2 ( 𝜑 → ( 𝐹f 𝑅 𝐺 ) = ( 𝑥𝐴 ↦ ( 𝐵 𝑅 𝐶 ) ) )

### Proof

Step Hyp Ref Expression
1 offval2.1 ( 𝜑𝐴𝑉 )
2 offval2.2 ( ( 𝜑𝑥𝐴 ) → 𝐵𝑊 )
3 offval2.3 ( ( 𝜑𝑥𝐴 ) → 𝐶𝑋 )
4 offval2.4 ( 𝜑𝐹 = ( 𝑥𝐴𝐵 ) )
5 offval2.5 ( 𝜑𝐺 = ( 𝑥𝐴𝐶 ) )
6 2 ralrimiva ( 𝜑 → ∀ 𝑥𝐴 𝐵𝑊 )
7 eqid ( 𝑥𝐴𝐵 ) = ( 𝑥𝐴𝐵 )
8 7 fnmpt ( ∀ 𝑥𝐴 𝐵𝑊 → ( 𝑥𝐴𝐵 ) Fn 𝐴 )
9 6 8 syl ( 𝜑 → ( 𝑥𝐴𝐵 ) Fn 𝐴 )
10 4 fneq1d ( 𝜑 → ( 𝐹 Fn 𝐴 ↔ ( 𝑥𝐴𝐵 ) Fn 𝐴 ) )
11 9 10 mpbird ( 𝜑𝐹 Fn 𝐴 )
12 3 ralrimiva ( 𝜑 → ∀ 𝑥𝐴 𝐶𝑋 )
13 eqid ( 𝑥𝐴𝐶 ) = ( 𝑥𝐴𝐶 )
14 13 fnmpt ( ∀ 𝑥𝐴 𝐶𝑋 → ( 𝑥𝐴𝐶 ) Fn 𝐴 )
15 12 14 syl ( 𝜑 → ( 𝑥𝐴𝐶 ) Fn 𝐴 )
16 5 fneq1d ( 𝜑 → ( 𝐺 Fn 𝐴 ↔ ( 𝑥𝐴𝐶 ) Fn 𝐴 ) )
17 15 16 mpbird ( 𝜑𝐺 Fn 𝐴 )
18 inidm ( 𝐴𝐴 ) = 𝐴
19 4 adantr ( ( 𝜑𝑦𝐴 ) → 𝐹 = ( 𝑥𝐴𝐵 ) )
20 19 fveq1d ( ( 𝜑𝑦𝐴 ) → ( 𝐹𝑦 ) = ( ( 𝑥𝐴𝐵 ) ‘ 𝑦 ) )
21 5 adantr ( ( 𝜑𝑦𝐴 ) → 𝐺 = ( 𝑥𝐴𝐶 ) )
22 21 fveq1d ( ( 𝜑𝑦𝐴 ) → ( 𝐺𝑦 ) = ( ( 𝑥𝐴𝐶 ) ‘ 𝑦 ) )
23 11 17 1 1 18 20 22 offval ( 𝜑 → ( 𝐹f 𝑅 𝐺 ) = ( 𝑦𝐴 ↦ ( ( ( 𝑥𝐴𝐵 ) ‘ 𝑦 ) 𝑅 ( ( 𝑥𝐴𝐶 ) ‘ 𝑦 ) ) ) )
24 nffvmpt1 𝑥 ( ( 𝑥𝐴𝐵 ) ‘ 𝑦 )
25 nfcv 𝑥 𝑅
26 nffvmpt1 𝑥 ( ( 𝑥𝐴𝐶 ) ‘ 𝑦 )
27 24 25 26 nfov 𝑥 ( ( ( 𝑥𝐴𝐵 ) ‘ 𝑦 ) 𝑅 ( ( 𝑥𝐴𝐶 ) ‘ 𝑦 ) )
28 nfcv 𝑦 ( ( ( 𝑥𝐴𝐵 ) ‘ 𝑥 ) 𝑅 ( ( 𝑥𝐴𝐶 ) ‘ 𝑥 ) )
29 fveq2 ( 𝑦 = 𝑥 → ( ( 𝑥𝐴𝐵 ) ‘ 𝑦 ) = ( ( 𝑥𝐴𝐵 ) ‘ 𝑥 ) )
30 fveq2 ( 𝑦 = 𝑥 → ( ( 𝑥𝐴𝐶 ) ‘ 𝑦 ) = ( ( 𝑥𝐴𝐶 ) ‘ 𝑥 ) )
31 29 30 oveq12d ( 𝑦 = 𝑥 → ( ( ( 𝑥𝐴𝐵 ) ‘ 𝑦 ) 𝑅 ( ( 𝑥𝐴𝐶 ) ‘ 𝑦 ) ) = ( ( ( 𝑥𝐴𝐵 ) ‘ 𝑥 ) 𝑅 ( ( 𝑥𝐴𝐶 ) ‘ 𝑥 ) ) )
32 27 28 31 cbvmpt ( 𝑦𝐴 ↦ ( ( ( 𝑥𝐴𝐵 ) ‘ 𝑦 ) 𝑅 ( ( 𝑥𝐴𝐶 ) ‘ 𝑦 ) ) ) = ( 𝑥𝐴 ↦ ( ( ( 𝑥𝐴𝐵 ) ‘ 𝑥 ) 𝑅 ( ( 𝑥𝐴𝐶 ) ‘ 𝑥 ) ) )
33 simpr ( ( 𝜑𝑥𝐴 ) → 𝑥𝐴 )
34 7 fvmpt2 ( ( 𝑥𝐴𝐵𝑊 ) → ( ( 𝑥𝐴𝐵 ) ‘ 𝑥 ) = 𝐵 )
35 33 2 34 syl2anc ( ( 𝜑𝑥𝐴 ) → ( ( 𝑥𝐴𝐵 ) ‘ 𝑥 ) = 𝐵 )
36 13 fvmpt2 ( ( 𝑥𝐴𝐶𝑋 ) → ( ( 𝑥𝐴𝐶 ) ‘ 𝑥 ) = 𝐶 )
37 33 3 36 syl2anc ( ( 𝜑𝑥𝐴 ) → ( ( 𝑥𝐴𝐶 ) ‘ 𝑥 ) = 𝐶 )
38 35 37 oveq12d ( ( 𝜑𝑥𝐴 ) → ( ( ( 𝑥𝐴𝐵 ) ‘ 𝑥 ) 𝑅 ( ( 𝑥𝐴𝐶 ) ‘ 𝑥 ) ) = ( 𝐵 𝑅 𝐶 ) )
39 38 mpteq2dva ( 𝜑 → ( 𝑥𝐴 ↦ ( ( ( 𝑥𝐴𝐵 ) ‘ 𝑥 ) 𝑅 ( ( 𝑥𝐴𝐶 ) ‘ 𝑥 ) ) ) = ( 𝑥𝐴 ↦ ( 𝐵 𝑅 𝐶 ) ) )
40 32 39 syl5eq ( 𝜑 → ( 𝑦𝐴 ↦ ( ( ( 𝑥𝐴𝐵 ) ‘ 𝑦 ) 𝑅 ( ( 𝑥𝐴𝐶 ) ‘ 𝑦 ) ) ) = ( 𝑥𝐴 ↦ ( 𝐵 𝑅 𝐶 ) ) )
41 23 40 eqtrd ( 𝜑 → ( 𝐹f 𝑅 𝐺 ) = ( 𝑥𝐴 ↦ ( 𝐵 𝑅 𝐶 ) ) )