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 sseldi ( ( 𝜑𝐹r 𝑅 𝐺𝑋𝑆 ) → 𝑋𝐴 )
23 18 22 6 syl2anc ( ( 𝜑𝐹r 𝑅 𝐺𝑋𝑆 ) → ( 𝐹𝑋 ) = 𝐶 )
24 inss2 ( 𝐴𝐵 ) ⊆ 𝐵
25 5 24 eqsstrri 𝑆𝐵
26 25 21 sseldi ( ( 𝜑𝐹r 𝑅 𝐺𝑋𝑆 ) → 𝑋𝐵 )
27 18 26 7 syl2anc ( ( 𝜑𝐹r 𝑅 𝐺𝑋𝑆 ) → ( 𝐺𝑋 ) = 𝐷 )
28 17 23 27 3brtr3d ( ( 𝜑𝐹r 𝑅 𝐺𝑋𝑆 ) → 𝐶 𝑅 𝐷 )