Theorem ofrval

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

	Ref	Expression
Hypotheses	offval.1	|- ( ph -> F Fn A )
	offval.2	|- ( ph -> G Fn B )
	offval.3	|- ( ph -> A e. V )
	offval.4	|- ( ph -> B e. W )
	offval.5	|- ( A i^i B ) = S
	ofval.6	|- ( ( ph /\ X e. A ) -> ( F ` X ) = C )
	ofval.7	|- ( ( ph /\ X e. B ) -> ( G ` X ) = D )
Assertion	ofrval	|- ( ( ph /\ F oR R G /\ X e. S ) -> C R D )

Proof

Step	Hyp	Ref	Expression
1		offval.1	|- ( ph -> F Fn A )
2		offval.2	|- ( ph -> G Fn B )
3		offval.3	|- ( ph -> A e. V )
4		offval.4	|- ( ph -> B e. W )
5		offval.5	|- ( A i^i B ) = S
6		ofval.6	|- ( ( ph /\ X e. A ) -> ( F ` X ) = C )
7		ofval.7	|- ( ( ph /\ X e. B ) -> ( G ` X ) = D )
8		eqidd	|- ( ( ph /\ x e. A ) -> ( F ` x ) = ( F ` x ) )
9		eqidd	|- ( ( ph /\ x e. B ) -> ( G ` x ) = ( G ` x ) )
10	1 2 3 4 5 8 9	ofrfval	|- ( ph -> ( F oR R G <-> A. x e. S ( F ` x ) R ( G ` x ) ) )
11	10	biimpa	|- ( ( ph /\ F oR R G ) -> A. x e. S ( F ` x ) R ( G ` x ) )
12		fveq2	|- ( x = X -> ( F ` x ) = ( F ` X ) )
13		fveq2	|- ( x = X -> ( G ` x ) = ( G ` X ) )
14	12 13	breq12d	|- ( x = X -> ( ( F ` x ) R ( G ` x ) <-> ( F ` X ) R ( G ` X ) ) )
15	14	rspccv	|- ( A. x e. S ( F ` x ) R ( G ` x ) -> ( X e. S -> ( F ` X ) R ( G ` X ) ) )
16	11 15	syl	|- ( ( ph /\ F oR R G ) -> ( X e. S -> ( F ` X ) R ( G ` X ) ) )
17	16	3impia	|- ( ( ph /\ F oR R G /\ X e. S ) -> ( F ` X ) R ( G ` X ) )
18		simp1	|- ( ( ph /\ F oR R G /\ X e. S ) -> ph )
19		inss1	|- ( A i^i B ) C_ A
20	5 19	eqsstrri	|- S C_ A
21		simp3	|- ( ( ph /\ F oR R G /\ X e. S ) -> X e. S )
22	20 21	sseldi	|- ( ( ph /\ F oR R G /\ X e. S ) -> X e. A )
23	18 22 6	syl2anc	|- ( ( ph /\ F oR R G /\ X e. S ) -> ( F ` X ) = C )
24		inss2	|- ( A i^i B ) C_ B
25	5 24	eqsstrri	|- S C_ B
26	25 21	sseldi	|- ( ( ph /\ F oR R G /\ X e. S ) -> X e. B )
27	18 26 7	syl2anc	|- ( ( ph /\ F oR R G /\ X e. S ) -> ( G ` X ) = D )
28	17 23 27	3brtr3d	|- ( ( ph /\ F oR R G /\ X e. S ) -> C R D )