This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ofrfval2

Description: The function relation acting on maps. (Contributed by Mario Carneiro, 20-Jul-2014)

Ref Expression
Hypotheses offval2.1 ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
offval2.2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑊 )
offval2.3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ 𝑋 )
offval2.4 ⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) )
offval2.5 ⊢ ( 𝜑 → 𝐺 = ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) )
Assertion ofrfval2 ( 𝜑 → ( 𝐹 ∘r 𝑅 𝐺 ↔ ∀ 𝑥 ∈ 𝐴 𝐵 𝑅 𝐶 ) )

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 ofrfval ⊢ ( 𝜑 → ( 𝐹 ∘r 𝑅 𝐺 ↔ ∀ 𝑦 ∈ 𝐴 ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑦 ) 𝑅 ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑦 ) ) )
24 nffvmpt1 ⊢ Ⅎ 𝑥 ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑦 )
25 nfcv ⊢ Ⅎ 𝑥 𝑅
26 nffvmpt1 ⊢ Ⅎ 𝑥 ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑦 )
27 24 25 26 nfbr ⊢ Ⅎ 𝑥 ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑦 ) 𝑅 ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑦 )
28 nfv ⊢ Ⅎ 𝑦 ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) 𝑅 ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑥 )
29 fveq2 ⊢ ( 𝑦 = 𝑥 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑦 ) = ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) )
30 fveq2 ⊢ ( 𝑦 = 𝑥 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑦 ) = ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑥 ) )
31 29 30 breq12d ⊢ ( 𝑦 = 𝑥 → ( ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑦 ) 𝑅 ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑦 ) ↔ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) 𝑅 ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑥 ) ) )
32 27 28 31 cbvralw ⊢ ( ∀ 𝑦 ∈ 𝐴 ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑦 ) 𝑅 ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑦 ) ↔ ∀ 𝑥 ∈ 𝐴 ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) 𝑅 ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑥 ) )
33 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ 𝐴 )
34 7 fvmpt2 ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝑊 ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) = 𝐵 )
35 33 2 34 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) = 𝐵 )
36 13 fvmpt2 ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝐶 ∈ 𝑋 ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑥 ) = 𝐶 )
37 33 3 36 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑥 ) = 𝐶 )
38 35 37 breq12d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) 𝑅 ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑥 ) ↔ 𝐵 𝑅 𝐶 ) )
39 38 ralbidva ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝐴 ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) 𝑅 ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑥 ) ↔ ∀ 𝑥 ∈ 𝐴 𝐵 𝑅 𝐶 ) )
40 32 39 bitrid ⊢ ( 𝜑 → ( ∀ 𝑦 ∈ 𝐴 ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑦 ) 𝑅 ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑦 ) ↔ ∀ 𝑥 ∈ 𝐴 𝐵 𝑅 𝐶 ) )
41 23 40 bitrd ⊢ ( 𝜑 → ( 𝐹 ∘r 𝑅 𝐺 ↔ ∀ 𝑥 ∈ 𝐴 𝐵 𝑅 𝐶 ) )