Metamath Proof Explorer

Theorem rlimcn2

Description: Image of a limit under a continuous map, two-arg version. (Contributed by Mario Carneiro, 17-Sep-2014)

Ref Expression
Hypotheses rlimcn2.1a 
|- ( ( ph /\ z e. A ) -> B e. X )
rlimcn2.1b 
|- ( ( ph /\ z e. A ) -> C e. Y )
rlimcn2.2a 
|- ( ph -> R e. X )
rlimcn2.2b 
|- ( ph -> S e. Y )
rlimcn2.3a 
|- ( ph -> ( z e. A |-> B ) ~~>r R )
rlimcn2.3b 
|- ( ph -> ( z e. A |-> C ) ~~>r S )
rlimcn2.4 
|- ( ph -> F : ( X X. Y ) --> CC )
rlimcn2.5 
|- ( ( ph /\ x e. RR+ ) -> E. r e. RR+ E. s e. RR+ A. u e. X A. v e. Y ( ( ( abs ` ( u - R ) ) < r /\ ( abs ` ( v - S ) ) < s ) -> ( abs ` ( ( u F v ) - ( R F S ) ) ) < x ) )
Assertion rlimcn2 
|- ( ph -> ( z e. A |-> ( B F C ) ) ~~>r ( R F S ) )

Proof

Step Hyp Ref Expression
1 rlimcn2.1a 
 |-  ( ( ph /\ z e. A ) -> B e. X )
2 rlimcn2.1b 
 |-  ( ( ph /\ z e. A ) -> C e. Y )
3 rlimcn2.2a 
 |-  ( ph -> R e. X )
4 rlimcn2.2b 
 |-  ( ph -> S e. Y )
5 rlimcn2.3a 
 |-  ( ph -> ( z e. A |-> B ) ~~>r R )
6 rlimcn2.3b 
 |-  ( ph -> ( z e. A |-> C ) ~~>r S )
7 rlimcn2.4 
 |-  ( ph -> F : ( X X. Y ) --> CC )
8 rlimcn2.5 
 |-  ( ( ph /\ x e. RR+ ) -> E. r e. RR+ E. s e. RR+ A. u e. X A. v e. Y ( ( ( abs ` ( u - R ) ) < r /\ ( abs ` ( v - S ) ) < s ) -> ( abs ` ( ( u F v ) - ( R F S ) ) ) < x ) )
9 1 ralrimiva 
 |-  ( ph -> A. z e. A B e. X )
10 9 adantr 
 |-  ( ( ph /\ ( r e. RR+ /\ s e. RR+ ) ) -> A. z e. A B e. X )
11 simprl 
 |-  ( ( ph /\ ( r e. RR+ /\ s e. RR+ ) ) -> r e. RR+ )
12 5 adantr 
 |-  ( ( ph /\ ( r e. RR+ /\ s e. RR+ ) ) -> ( z e. A |-> B ) ~~>r R )
13 10 11 12 rlimi 
 |-  ( ( ph /\ ( r e. RR+ /\ s e. RR+ ) ) -> E. a e. RR A. z e. A ( a <_ z -> ( abs ` ( B - R ) ) < r ) )
14 2 ralrimiva 
 |-  ( ph -> A. z e. A C e. Y )
15 14 adantr 
 |-  ( ( ph /\ ( r e. RR+ /\ s e. RR+ ) ) -> A. z e. A C e. Y )
16 simprr 
 |-  ( ( ph /\ ( r e. RR+ /\ s e. RR+ ) ) -> s e. RR+ )
17 6 adantr 
 |-  ( ( ph /\ ( r e. RR+ /\ s e. RR+ ) ) -> ( z e. A |-> C ) ~~>r S )
18 15 16 17 rlimi 
 |-  ( ( ph /\ ( r e. RR+ /\ s e. RR+ ) ) -> E. b e. RR A. z e. A ( b <_ z -> ( abs ` ( C - S ) ) < s ) )
19 reeanv 
 |-  ( E. a e. RR E. b e. RR ( A. z e. A ( a <_ z -> ( abs ` ( B - R ) ) < r ) /\ A. z e. A ( b <_ z -> ( abs ` ( C - S ) ) < s ) ) <-> ( E. a e. RR A. z e. A ( a <_ z -> ( abs ` ( B - R ) ) < r ) /\ E. b e. RR A. z e. A ( b <_ z -> ( abs ` ( C - S ) ) < s ) ) )
20 r19.26 
 |-  ( A. z e. A ( ( a <_ z -> ( abs ` ( B - R ) ) < r ) /\ ( b <_ z -> ( abs ` ( C - S ) ) < s ) ) <-> ( A. z e. A ( a <_ z -> ( abs ` ( B - R ) ) < r ) /\ A. z e. A ( b <_ z -> ( abs ` ( C - S ) ) < s ) ) )
21 anim12 
 |-  ( ( ( a <_ z -> ( abs ` ( B - R ) ) < r ) /\ ( b <_ z -> ( abs ` ( C - S ) ) < s ) ) -> ( ( a <_ z /\ b <_ z ) -> ( ( abs ` ( B - R ) ) < r /\ ( abs ` ( C - S ) ) < s ) ) )
22 simplrl 
 |-  ( ( ( ( ph /\ ( r e. RR+ /\ s e. RR+ ) ) /\ ( a e. RR /\ b e. RR ) ) /\ z e. A ) -> a e. RR )
23 simplrr 
 |-  ( ( ( ( ph /\ ( r e. RR+ /\ s e. RR+ ) ) /\ ( a e. RR /\ b e. RR ) ) /\ z e. A ) -> b e. RR )
24 eqid 
 |-  ( z e. A |-> B ) = ( z e. A |-> B )
25 24 1 dmmptd 
 |-  ( ph -> dom ( z e. A |-> B ) = A )
26 rlimss 
 |-  ( ( z e. A |-> B ) ~~>r R -> dom ( z e. A |-> B ) C_ RR )
27 5 26 syl 
 |-  ( ph -> dom ( z e. A |-> B ) C_ RR )
28 25 27 eqsstrrd 
 |-  ( ph -> A C_ RR )
29 28 ad2antrr 
 |-  ( ( ( ph /\ ( r e. RR+ /\ s e. RR+ ) ) /\ ( a e. RR /\ b e. RR ) ) -> A C_ RR )
30 29 sselda 
 |-  ( ( ( ( ph /\ ( r e. RR+ /\ s e. RR+ ) ) /\ ( a e. RR /\ b e. RR ) ) /\ z e. A ) -> z e. RR )
31 maxle 
 |-  ( ( a e. RR /\ b e. RR /\ z e. RR ) -> ( if ( a <_ b , b , a ) <_ z <-> ( a <_ z /\ b <_ z ) ) )
32 22 23 30 31 syl3anc 
 |-  ( ( ( ( ph /\ ( r e. RR+ /\ s e. RR+ ) ) /\ ( a e. RR /\ b e. RR ) ) /\ z e. A ) -> ( if ( a <_ b , b , a ) <_ z <-> ( a <_ z /\ b <_ z ) ) )
33 32 imbi1d 
 |-  ( ( ( ( ph /\ ( r e. RR+ /\ s e. RR+ ) ) /\ ( a e. RR /\ b e. RR ) ) /\ z e. A ) -> ( ( if ( a <_ b , b , a ) <_ z -> ( ( abs ` ( B - R ) ) < r /\ ( abs ` ( C - S ) ) < s ) ) <-> ( ( a <_ z /\ b <_ z ) -> ( ( abs ` ( B - R ) ) < r /\ ( abs ` ( C - S ) ) < s ) ) ) )
34 21 33 syl5ibr 
 |-  ( ( ( ( ph /\ ( r e. RR+ /\ s e. RR+ ) ) /\ ( a e. RR /\ b e. RR ) ) /\ z e. A ) -> ( ( ( a <_ z -> ( abs ` ( B - R ) ) < r ) /\ ( b <_ z -> ( abs ` ( C - S ) ) < s ) ) -> ( if ( a <_ b , b , a ) <_ z -> ( ( abs ` ( B - R ) ) < r /\ ( abs ` ( C - S ) ) < s ) ) ) )
35 34 ralimdva 
 |-  ( ( ( ph /\ ( r e. RR+ /\ s e. RR+ ) ) /\ ( a e. RR /\ b e. RR ) ) -> ( A. z e. A ( ( a <_ z -> ( abs ` ( B - R ) ) < r ) /\ ( b <_ z -> ( abs ` ( C - S ) ) < s ) ) -> A. z e. A ( if ( a <_ b , b , a ) <_ z -> ( ( abs ` ( B - R ) ) < r /\ ( abs ` ( C - S ) ) < s ) ) ) )
36 ifcl 
 |-  ( ( b e. RR /\ a e. RR ) -> if ( a <_ b , b , a ) e. RR )
37 36 ancoms 
 |-  ( ( a e. RR /\ b e. RR ) -> if ( a <_ b , b , a ) e. RR )
38 37 ad2antlr 
 |-  ( ( ( ( ph /\ ( r e. RR+ /\ s e. RR+ ) ) /\ ( a e. RR /\ b e. RR ) ) /\ A. u e. X A. v e. Y ( ( ( abs ` ( u - R ) ) < r /\ ( abs ` ( v - S ) ) < s ) -> ( abs ` ( ( u F v ) - ( R F S ) ) ) < x ) ) -> if ( a <_ b , b , a ) e. RR )
39 1 adantlr 
 |-  ( ( ( ph /\ ( r e. RR+ /\ s e. RR+ ) ) /\ z e. A ) -> B e. X )
40 2 adantlr 
 |-  ( ( ( ph /\ ( r e. RR+ /\ s e. RR+ ) ) /\ z e. A ) -> C e. Y )
41 39 40 jca 
 |-  ( ( ( ph /\ ( r e. RR+ /\ s e. RR+ ) ) /\ z e. A ) -> ( B e. X /\ C e. Y ) )
42 fvoveq1 
 |-  ( u = B -> ( abs ` ( u - R ) ) = ( abs ` ( B - R ) ) )
43 42 breq1d 
 |-  ( u = B -> ( ( abs ` ( u - R ) ) < r <-> ( abs ` ( B - R ) ) < r ) )
44 43 anbi1d 
 |-  ( u = B -> ( ( ( abs ` ( u - R ) ) < r /\ ( abs ` ( v - S ) ) < s ) <-> ( ( abs ` ( B - R ) ) < r /\ ( abs ` ( v - S ) ) < s ) ) )
45 oveq1 
 |-  ( u = B -> ( u F v ) = ( B F v ) )
46 45 fvoveq1d 
 |-  ( u = B -> ( abs ` ( ( u F v ) - ( R F S ) ) ) = ( abs ` ( ( B F v ) - ( R F S ) ) ) )
47 46 breq1d 
 |-  ( u = B -> ( ( abs ` ( ( u F v ) - ( R F S ) ) ) < x <-> ( abs ` ( ( B F v ) - ( R F S ) ) ) < x ) )
48 44 47 imbi12d 
 |-  ( u = B -> ( ( ( ( abs ` ( u - R ) ) < r /\ ( abs ` ( v - S ) ) < s ) -> ( abs ` ( ( u F v ) - ( R F S ) ) ) < x ) <-> ( ( ( abs ` ( B - R ) ) < r /\ ( abs ` ( v - S ) ) < s ) -> ( abs ` ( ( B F v ) - ( R F S ) ) ) < x ) ) )
49 fvoveq1 
 |-  ( v = C -> ( abs ` ( v - S ) ) = ( abs ` ( C - S ) ) )
50 49 breq1d 
 |-  ( v = C -> ( ( abs ` ( v - S ) ) < s <-> ( abs ` ( C - S ) ) < s ) )
51 50 anbi2d 
 |-  ( v = C -> ( ( ( abs ` ( B - R ) ) < r /\ ( abs ` ( v - S ) ) < s ) <-> ( ( abs ` ( B - R ) ) < r /\ ( abs ` ( C - S ) ) < s ) ) )
52 oveq2 
 |-  ( v = C -> ( B F v ) = ( B F C ) )
53 52 fvoveq1d 
 |-  ( v = C -> ( abs ` ( ( B F v ) - ( R F S ) ) ) = ( abs ` ( ( B F C ) - ( R F S ) ) ) )
54 53 breq1d 
 |-  ( v = C -> ( ( abs ` ( ( B F v ) - ( R F S ) ) ) < x <-> ( abs ` ( ( B F C ) - ( R F S ) ) ) < x ) )
55 51 54 imbi12d 
 |-  ( v = C -> ( ( ( ( abs ` ( B - R ) ) < r /\ ( abs ` ( v - S ) ) < s ) -> ( abs ` ( ( B F v ) - ( R F S ) ) ) < x ) <-> ( ( ( abs ` ( B - R ) ) < r /\ ( abs ` ( C - S ) ) < s ) -> ( abs ` ( ( B F C ) - ( R F S ) ) ) < x ) ) )
56 48 55 rspc2va 
 |-  ( ( ( B e. X /\ C e. Y ) /\ A. u e. X A. v e. Y ( ( ( abs ` ( u - R ) ) < r /\ ( abs ` ( v - S ) ) < s ) -> ( abs ` ( ( u F v ) - ( R F S ) ) ) < x ) ) -> ( ( ( abs ` ( B - R ) ) < r /\ ( abs ` ( C - S ) ) < s ) -> ( abs ` ( ( B F C ) - ( R F S ) ) ) < x ) )
57 41 56 sylan 
 |-  ( ( ( ( ph /\ ( r e. RR+ /\ s e. RR+ ) ) /\ z e. A ) /\ A. u e. X A. v e. Y ( ( ( abs ` ( u - R ) ) < r /\ ( abs ` ( v - S ) ) < s ) -> ( abs ` ( ( u F v ) - ( R F S ) ) ) < x ) ) -> ( ( ( abs ` ( B - R ) ) < r /\ ( abs ` ( C - S ) ) < s ) -> ( abs ` ( ( B F C ) - ( R F S ) ) ) < x ) )
58 57 imim2d 
 |-  ( ( ( ( ph /\ ( r e. RR+ /\ s e. RR+ ) ) /\ z e. A ) /\ A. u e. X A. v e. Y ( ( ( abs ` ( u - R ) ) < r /\ ( abs ` ( v - S ) ) < s ) -> ( abs ` ( ( u F v ) - ( R F S ) ) ) < x ) ) -> ( ( if ( a <_ b , b , a ) <_ z -> ( ( abs ` ( B - R ) ) < r /\ ( abs ` ( C - S ) ) < s ) ) -> ( if ( a <_ b , b , a ) <_ z -> ( abs ` ( ( B F C ) - ( R F S ) ) ) < x ) ) )
59 58 an32s 
 |-  ( ( ( ( ph /\ ( r e. RR+ /\ s e. RR+ ) ) /\ A. u e. X A. v e. Y ( ( ( abs ` ( u - R ) ) < r /\ ( abs ` ( v - S ) ) < s ) -> ( abs ` ( ( u F v ) - ( R F S ) ) ) < x ) ) /\ z e. A ) -> ( ( if ( a <_ b , b , a ) <_ z -> ( ( abs ` ( B - R ) ) < r /\ ( abs ` ( C - S ) ) < s ) ) -> ( if ( a <_ b , b , a ) <_ z -> ( abs ` ( ( B F C ) - ( R F S ) ) ) < x ) ) )
60 59 ralimdva 
 |-  ( ( ( ph /\ ( r e. RR+ /\ s e. RR+ ) ) /\ A. u e. X A. v e. Y ( ( ( abs ` ( u - R ) ) < r /\ ( abs ` ( v - S ) ) < s ) -> ( abs ` ( ( u F v ) - ( R F S ) ) ) < x ) ) -> ( A. z e. A ( if ( a <_ b , b , a ) <_ z -> ( ( abs ` ( B - R ) ) < r /\ ( abs ` ( C - S ) ) < s ) ) -> A. z e. A ( if ( a <_ b , b , a ) <_ z -> ( abs ` ( ( B F C ) - ( R F S ) ) ) < x ) ) )
61 60 adantlr 
 |-  ( ( ( ( ph /\ ( r e. RR+ /\ s e. RR+ ) ) /\ ( a e. RR /\ b e. RR ) ) /\ A. u e. X A. v e. Y ( ( ( abs ` ( u - R ) ) < r /\ ( abs ` ( v - S ) ) < s ) -> ( abs ` ( ( u F v ) - ( R F S ) ) ) < x ) ) -> ( A. z e. A ( if ( a <_ b , b , a ) <_ z -> ( ( abs ` ( B - R ) ) < r /\ ( abs ` ( C - S ) ) < s ) ) -> A. z e. A ( if ( a <_ b , b , a ) <_ z -> ( abs ` ( ( B F C ) - ( R F S ) ) ) < x ) ) )
62 breq1 
 |-  ( c = if ( a <_ b , b , a ) -> ( c <_ z <-> if ( a <_ b , b , a ) <_ z ) )
63 62 rspceaimv 
 |-  ( ( if ( a <_ b , b , a ) e. RR /\ A. z e. A ( if ( a <_ b , b , a ) <_ z -> ( abs ` ( ( B F C ) - ( R F S ) ) ) < x ) ) -> E. c e. RR A. z e. A ( c <_ z -> ( abs ` ( ( B F C ) - ( R F S ) ) ) < x ) )
64 38 61 63 syl6an 
 |-  ( ( ( ( ph /\ ( r e. RR+ /\ s e. RR+ ) ) /\ ( a e. RR /\ b e. RR ) ) /\ A. u e. X A. v e. Y ( ( ( abs ` ( u - R ) ) < r /\ ( abs ` ( v - S ) ) < s ) -> ( abs ` ( ( u F v ) - ( R F S ) ) ) < x ) ) -> ( A. z e. A ( if ( a <_ b , b , a ) <_ z -> ( ( abs ` ( B - R ) ) < r /\ ( abs ` ( C - S ) ) < s ) ) -> E. c e. RR A. z e. A ( c <_ z -> ( abs ` ( ( B F C ) - ( R F S ) ) ) < x ) ) )
65 64 ex 
 |-  ( ( ( ph /\ ( r e. RR+ /\ s e. RR+ ) ) /\ ( a e. RR /\ b e. RR ) ) -> ( A. u e. X A. v e. Y ( ( ( abs ` ( u - R ) ) < r /\ ( abs ` ( v - S ) ) < s ) -> ( abs ` ( ( u F v ) - ( R F S ) ) ) < x ) -> ( A. z e. A ( if ( a <_ b , b , a ) <_ z -> ( ( abs ` ( B - R ) ) < r /\ ( abs ` ( C - S ) ) < s ) ) -> E. c e. RR A. z e. A ( c <_ z -> ( abs ` ( ( B F C ) - ( R F S ) ) ) < x ) ) ) )
66 65 com23 
 |-  ( ( ( ph /\ ( r e. RR+ /\ s e. RR+ ) ) /\ ( a e. RR /\ b e. RR ) ) -> ( A. z e. A ( if ( a <_ b , b , a ) <_ z -> ( ( abs ` ( B - R ) ) < r /\ ( abs ` ( C - S ) ) < s ) ) -> ( A. u e. X A. v e. Y ( ( ( abs ` ( u - R ) ) < r /\ ( abs ` ( v - S ) ) < s ) -> ( abs ` ( ( u F v ) - ( R F S ) ) ) < x ) -> E. c e. RR A. z e. A ( c <_ z -> ( abs ` ( ( B F C ) - ( R F S ) ) ) < x ) ) ) )
67 35 66 syld 
 |-  ( ( ( ph /\ ( r e. RR+ /\ s e. RR+ ) ) /\ ( a e. RR /\ b e. RR ) ) -> ( A. z e. A ( ( a <_ z -> ( abs ` ( B - R ) ) < r ) /\ ( b <_ z -> ( abs ` ( C - S ) ) < s ) ) -> ( A. u e. X A. v e. Y ( ( ( abs ` ( u - R ) ) < r /\ ( abs ` ( v - S ) ) < s ) -> ( abs ` ( ( u F v ) - ( R F S ) ) ) < x ) -> E. c e. RR A. z e. A ( c <_ z -> ( abs ` ( ( B F C ) - ( R F S ) ) ) < x ) ) ) )
68 20 67 syl5bir 
 |-  ( ( ( ph /\ ( r e. RR+ /\ s e. RR+ ) ) /\ ( a e. RR /\ b e. RR ) ) -> ( ( A. z e. A ( a <_ z -> ( abs ` ( B - R ) ) < r ) /\ A. z e. A ( b <_ z -> ( abs ` ( C - S ) ) < s ) ) -> ( A. u e. X A. v e. Y ( ( ( abs ` ( u - R ) ) < r /\ ( abs ` ( v - S ) ) < s ) -> ( abs ` ( ( u F v ) - ( R F S ) ) ) < x ) -> E. c e. RR A. z e. A ( c <_ z -> ( abs ` ( ( B F C ) - ( R F S ) ) ) < x ) ) ) )
69 68 rexlimdvva 
 |-  ( ( ph /\ ( r e. RR+ /\ s e. RR+ ) ) -> ( E. a e. RR E. b e. RR ( A. z e. A ( a <_ z -> ( abs ` ( B - R ) ) < r ) /\ A. z e. A ( b <_ z -> ( abs ` ( C - S ) ) < s ) ) -> ( A. u e. X A. v e. Y ( ( ( abs ` ( u - R ) ) < r /\ ( abs ` ( v - S ) ) < s ) -> ( abs ` ( ( u F v ) - ( R F S ) ) ) < x ) -> E. c e. RR A. z e. A ( c <_ z -> ( abs ` ( ( B F C ) - ( R F S ) ) ) < x ) ) ) )
70 19 69 syl5bir 
 |-  ( ( ph /\ ( r e. RR+ /\ s e. RR+ ) ) -> ( ( E. a e. RR A. z e. A ( a <_ z -> ( abs ` ( B - R ) ) < r ) /\ E. b e. RR A. z e. A ( b <_ z -> ( abs ` ( C - S ) ) < s ) ) -> ( A. u e. X A. v e. Y ( ( ( abs ` ( u - R ) ) < r /\ ( abs ` ( v - S ) ) < s ) -> ( abs ` ( ( u F v ) - ( R F S ) ) ) < x ) -> E. c e. RR A. z e. A ( c <_ z -> ( abs ` ( ( B F C ) - ( R F S ) ) ) < x ) ) ) )
71 13 18 70 mp2and 
 |-  ( ( ph /\ ( r e. RR+ /\ s e. RR+ ) ) -> ( A. u e. X A. v e. Y ( ( ( abs ` ( u - R ) ) < r /\ ( abs ` ( v - S ) ) < s ) -> ( abs ` ( ( u F v ) - ( R F S ) ) ) < x ) -> E. c e. RR A. z e. A ( c <_ z -> ( abs ` ( ( B F C ) - ( R F S ) ) ) < x ) ) )
72 71 rexlimdvva 
 |-  ( ph -> ( E. r e. RR+ E. s e. RR+ A. u e. X A. v e. Y ( ( ( abs ` ( u - R ) ) < r /\ ( abs ` ( v - S ) ) < s ) -> ( abs ` ( ( u F v ) - ( R F S ) ) ) < x ) -> E. c e. RR A. z e. A ( c <_ z -> ( abs ` ( ( B F C ) - ( R F S ) ) ) < x ) ) )
73 72 imp 
 |-  ( ( ph /\ E. r e. RR+ E. s e. RR+ A. u e. X A. v e. Y ( ( ( abs ` ( u - R ) ) < r /\ ( abs ` ( v - S ) ) < s ) -> ( abs ` ( ( u F v ) - ( R F S ) ) ) < x ) ) -> E. c e. RR A. z e. A ( c <_ z -> ( abs ` ( ( B F C ) - ( R F S ) ) ) < x ) )
74 8 73 syldan 
 |-  ( ( ph /\ x e. RR+ ) -> E. c e. RR A. z e. A ( c <_ z -> ( abs ` ( ( B F C ) - ( R F S ) ) ) < x ) )
75 74 ralrimiva 
 |-  ( ph -> A. x e. RR+ E. c e. RR A. z e. A ( c <_ z -> ( abs ` ( ( B F C ) - ( R F S ) ) ) < x ) )
76 7 adantr 
 |-  ( ( ph /\ z e. A ) -> F : ( X X. Y ) --> CC )
77 76 1 2 fovrnd 
 |-  ( ( ph /\ z e. A ) -> ( B F C ) e. CC )
78 77 ralrimiva 
 |-  ( ph -> A. z e. A ( B F C ) e. CC )
79 7 3 4 fovrnd 
 |-  ( ph -> ( R F S ) e. CC )
80 78 28 79 rlim2 
 |-  ( ph -> ( ( z e. A |-> ( B F C ) ) ~~>r ( R F S ) <-> A. x e. RR+ E. c e. RR A. z e. A ( c <_ z -> ( abs ` ( ( B F C ) - ( R F S ) ) ) < x ) ) )
81 75 80 mpbird 
 |-  ( ph -> ( z e. A |-> ( B F C ) ) ~~>r ( R F S ) )