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

Metamath Proof Explorer

Theorem ofrval

Description: Exhibit a function relation at a point. (Contributed by Mario Carneiro, 28-Jul-2014)

Ref Expression
Hypotheses offval.1 ⊢ ( 𝜑 → 𝐹 Fn 𝐴 )
offval.2 ⊢ ( 𝜑 → 𝐺 Fn 𝐵 )
offval.3 ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
offval.4 ⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
offval.5 ⊢ ( 𝐴 ∩ 𝐵 ) = 𝑆
ofval.6 ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑋 ) = 𝐶 )
ofval.7 ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐵 ) → ( 𝐺 ‘ 𝑋 ) = 𝐷 )
Assertion ofrval ( ( 𝜑 ∧ 𝐹 ∘r 𝑅 𝐺 ∧ 𝑋 ∈ 𝑆 ) → 𝐶 𝑅 𝐷 )

Proof

Step Hyp Ref Expression
1 offval.1 ⊢ ( 𝜑 → 𝐹 Fn 𝐴 )
2 offval.2 ⊢ ( 𝜑 → 𝐺 Fn 𝐵 )
3 offval.3 ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
4 offval.4 ⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
5 offval.5 ⊢ ( 𝐴 ∩ 𝐵 ) = 𝑆
6 ofval.6 ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑋 ) = 𝐶 )
7 ofval.7 ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐵 ) → ( 𝐺 ‘ 𝑋 ) = 𝐷 )
8 eqidd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
9 eqidd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) )
10 1 2 3 4 5 8 9 ofrfval ⊢ ( 𝜑 → ( 𝐹 ∘r 𝑅 𝐺 ↔ ∀ 𝑥 ∈ 𝑆 ( 𝐹 ‘ 𝑥 ) 𝑅 ( 𝐺 ‘ 𝑥 ) ) )
11 10 biimpa ⊢ ( ( 𝜑 ∧ 𝐹 ∘r 𝑅 𝐺 ) → ∀ 𝑥 ∈ 𝑆 ( 𝐹 ‘ 𝑥 ) 𝑅 ( 𝐺 ‘ 𝑥 ) )
12 fveq2 ⊢ ( 𝑥 = 𝑋 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑋 ) )
13 fveq2 ⊢ ( 𝑥 = 𝑋 → ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑋 ) )
14 12 13 breq12d ⊢ ( 𝑥 = 𝑋 → ( ( 𝐹 ‘ 𝑥 ) 𝑅 ( 𝐺 ‘ 𝑥 ) ↔ ( 𝐹 ‘ 𝑋 ) 𝑅 ( 𝐺 ‘ 𝑋 ) ) )
15 14 rspccv ⊢ ( ∀ 𝑥 ∈ 𝑆 ( 𝐹 ‘ 𝑥 ) 𝑅 ( 𝐺 ‘ 𝑥 ) → ( 𝑋 ∈ 𝑆 → ( 𝐹 ‘ 𝑋 ) 𝑅 ( 𝐺 ‘ 𝑋 ) ) )
16 11 15 syl ⊢ ( ( 𝜑 ∧ 𝐹 ∘r 𝑅 𝐺 ) → ( 𝑋 ∈ 𝑆 → ( 𝐹 ‘ 𝑋 ) 𝑅 ( 𝐺 ‘ 𝑋 ) ) )
17 16 3impia ⊢ ( ( 𝜑 ∧ 𝐹 ∘r 𝑅 𝐺 ∧ 𝑋 ∈ 𝑆 ) → ( 𝐹 ‘ 𝑋 ) 𝑅 ( 𝐺 ‘ 𝑋 ) )
18 simp1 ⊢ ( ( 𝜑 ∧ 𝐹 ∘r 𝑅 𝐺 ∧ 𝑋 ∈ 𝑆 ) → 𝜑 )
19 inss1 ⊢ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐴
20 5 19 eqsstrri ⊢ 𝑆 ⊆ 𝐴
21 simp3 ⊢ ( ( 𝜑 ∧ 𝐹 ∘r 𝑅 𝐺 ∧ 𝑋 ∈ 𝑆 ) → 𝑋 ∈ 𝑆 )
22 20 21 sselid ⊢ ( ( 𝜑 ∧ 𝐹 ∘r 𝑅 𝐺 ∧ 𝑋 ∈ 𝑆 ) → 𝑋 ∈ 𝐴 )
23 18 22 6 syl2anc ⊢ ( ( 𝜑 ∧ 𝐹 ∘r 𝑅 𝐺 ∧ 𝑋 ∈ 𝑆 ) → ( 𝐹 ‘ 𝑋 ) = 𝐶 )
24 inss2 ⊢ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐵
25 5 24 eqsstrri ⊢ 𝑆 ⊆ 𝐵
26 25 21 sselid ⊢ ( ( 𝜑 ∧ 𝐹 ∘r 𝑅 𝐺 ∧ 𝑋 ∈ 𝑆 ) → 𝑋 ∈ 𝐵 )
27 18 26 7 syl2anc ⊢ ( ( 𝜑 ∧ 𝐹 ∘r 𝑅 𝐺 ∧ 𝑋 ∈ 𝑆 ) → ( 𝐺 ‘ 𝑋 ) = 𝐷 )
28 17 23 27 3brtr3d ⊢ ( ( 𝜑 ∧ 𝐹 ∘r 𝑅 𝐺 ∧ 𝑋 ∈ 𝑆 ) → 𝐶 𝑅 𝐷 )