Metamath Proof Explorer


Theorem ofrfval2

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

Ref Expression
Hypotheses offval2.1 φ A V
offval2.2 φ x A B W
offval2.3 φ x A C X
offval2.4 φ F = x A B
offval2.5 φ G = x A C
Assertion ofrfval2 φ F R f G x A B R C

Proof

Step Hyp Ref Expression
1 offval2.1 φ A V
2 offval2.2 φ x A B W
3 offval2.3 φ x A C X
4 offval2.4 φ F = x A B
5 offval2.5 φ G = x A C
6 2 ralrimiva φ x A B W
7 eqid x A B = x A B
8 7 fnmpt x A B W x A B Fn A
9 6 8 syl φ x A B Fn A
10 4 fneq1d φ F Fn A x A B Fn A
11 9 10 mpbird φ F Fn A
12 3 ralrimiva φ x A C X
13 eqid x A C = x A C
14 13 fnmpt x A C X x A C Fn A
15 12 14 syl φ x A C Fn A
16 5 fneq1d φ G Fn A x A C Fn A
17 15 16 mpbird φ G Fn A
18 inidm A A = A
19 4 adantr φ y A F = x A B
20 19 fveq1d φ y A F y = x A B y
21 5 adantr φ y A G = x A C
22 21 fveq1d φ y A G y = x A C y
23 11 17 1 1 18 20 22 ofrfval φ F R f G y A x A B y R x A C y
24 nffvmpt1 _ x x A B y
25 nfcv _ x R
26 nffvmpt1 _ x x A C y
27 24 25 26 nfbr x x A B y R x A C y
28 nfv y x A B x R x A C x
29 fveq2 y = x x A B y = x A B x
30 fveq2 y = x x A C y = x A C x
31 29 30 breq12d y = x x A B y R x A C y x A B x R x A C x
32 27 28 31 cbvralw y A x A B y R x A C y x A x A B x R x A C x
33 simpr φ x A x A
34 7 fvmpt2 x A B W x A B x = B
35 33 2 34 syl2anc φ x A x A B x = B
36 13 fvmpt2 x A C X x A C x = C
37 33 3 36 syl2anc φ x A x A C x = C
38 35 37 breq12d φ x A x A B x R x A C x B R C
39 38 ralbidva φ x A x A B x R x A C x x A B R C
40 32 39 syl5bb φ y A x A B y R x A C y x A B R C
41 23 40 bitrd φ F R f G x A B R C