Step |
Hyp |
Ref |
Expression |
1 |
|
smflimsuplem5.a |
|- F/ n ph |
2 |
|
smflimsuplem5.b |
|- F/ m ph |
3 |
|
smflimsuplem5.m |
|- ( ph -> M e. ZZ ) |
4 |
|
smflimsuplem5.z |
|- Z = ( ZZ>= ` M ) |
5 |
|
smflimsuplem5.s |
|- ( ph -> S e. SAlg ) |
6 |
|
smflimsuplem5.f |
|- ( ph -> F : Z --> ( SMblFn ` S ) ) |
7 |
|
smflimsuplem5.e |
|- E = ( n e. Z |-> { x e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) e. RR } ) |
8 |
|
smflimsuplem5.h |
|- H = ( n e. Z |-> ( x e. ( E ` n ) |-> sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) ) ) |
9 |
|
smflimsuplem5.r |
|- ( ph -> ( limsup ` ( m e. Z |-> ( ( F ` m ) ` X ) ) ) e. RR ) |
10 |
|
smflimsuplem5.n |
|- ( ph -> N e. Z ) |
11 |
|
smflimsuplem5.x |
|- ( ph -> X e. |^|_ m e. ( ZZ>= ` N ) dom ( F ` m ) ) |
12 |
4
|
eleq2i |
|- ( N e. Z <-> N e. ( ZZ>= ` M ) ) |
13 |
12
|
biimpi |
|- ( N e. Z -> N e. ( ZZ>= ` M ) ) |
14 |
|
uzss |
|- ( N e. ( ZZ>= ` M ) -> ( ZZ>= ` N ) C_ ( ZZ>= ` M ) ) |
15 |
13 14
|
syl |
|- ( N e. Z -> ( ZZ>= ` N ) C_ ( ZZ>= ` M ) ) |
16 |
15 4
|
sseqtrrdi |
|- ( N e. Z -> ( ZZ>= ` N ) C_ Z ) |
17 |
10 16
|
syl |
|- ( ph -> ( ZZ>= ` N ) C_ Z ) |
18 |
17
|
sselda |
|- ( ( ph /\ n e. ( ZZ>= ` N ) ) -> n e. Z ) |
19 |
|
nfcv |
|- F/_ x Z |
20 |
|
nfrab1 |
|- F/_ x { x e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) e. RR } |
21 |
19 20
|
nfmpt |
|- F/_ x ( n e. Z |-> { x e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) e. RR } ) |
22 |
7 21
|
nfcxfr |
|- F/_ x E |
23 |
|
nfcv |
|- F/_ x n |
24 |
22 23
|
nffv |
|- F/_ x ( E ` n ) |
25 |
|
fvex |
|- ( E ` n ) e. _V |
26 |
24 25
|
mptexf |
|- ( x e. ( E ` n ) |-> sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) ) e. _V |
27 |
26
|
a1i |
|- ( ( ph /\ n e. ( ZZ>= ` N ) ) -> ( x e. ( E ` n ) |-> sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) ) e. _V ) |
28 |
8
|
fvmpt2 |
|- ( ( n e. Z /\ ( x e. ( E ` n ) |-> sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) ) e. _V ) -> ( H ` n ) = ( x e. ( E ` n ) |-> sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) ) ) |
29 |
18 27 28
|
syl2anc |
|- ( ( ph /\ n e. ( ZZ>= ` N ) ) -> ( H ` n ) = ( x e. ( E ` n ) |-> sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) ) ) |
30 |
29
|
fveq1d |
|- ( ( ph /\ n e. ( ZZ>= ` N ) ) -> ( ( H ` n ) ` X ) = ( ( x e. ( E ` n ) |-> sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) ) ` X ) ) |
31 |
|
nfcv |
|- F/_ y ( E ` n ) |
32 |
|
nfcv |
|- F/_ y sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) |
33 |
|
nfcv |
|- F/_ x sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` y ) ) , RR* , < ) |
34 |
|
fveq2 |
|- ( x = y -> ( ( F ` m ) ` x ) = ( ( F ` m ) ` y ) ) |
35 |
34
|
mpteq2dv |
|- ( x = y -> ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) = ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` y ) ) ) |
36 |
35
|
rneqd |
|- ( x = y -> ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) = ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` y ) ) ) |
37 |
36
|
supeq1d |
|- ( x = y -> sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) = sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` y ) ) , RR* , < ) ) |
38 |
24 31 32 33 37
|
cbvmptf |
|- ( x e. ( E ` n ) |-> sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) ) = ( y e. ( E ` n ) |-> sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` y ) ) , RR* , < ) ) |
39 |
|
simpl |
|- ( ( y = X /\ m e. ( ZZ>= ` n ) ) -> y = X ) |
40 |
39
|
fveq2d |
|- ( ( y = X /\ m e. ( ZZ>= ` n ) ) -> ( ( F ` m ) ` y ) = ( ( F ` m ) ` X ) ) |
41 |
40
|
mpteq2dva |
|- ( y = X -> ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` y ) ) = ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` X ) ) ) |
42 |
41
|
rneqd |
|- ( y = X -> ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` y ) ) = ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` X ) ) ) |
43 |
42
|
supeq1d |
|- ( y = X -> sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` y ) ) , RR* , < ) = sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` X ) ) , RR* , < ) ) |
44 |
43
|
eleq1d |
|- ( y = X -> ( sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` y ) ) , RR* , < ) e. RR <-> sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` X ) ) , RR* , < ) e. RR ) ) |
45 |
|
uzss |
|- ( n e. ( ZZ>= ` N ) -> ( ZZ>= ` n ) C_ ( ZZ>= ` N ) ) |
46 |
|
iinss1 |
|- ( ( ZZ>= ` n ) C_ ( ZZ>= ` N ) -> |^|_ m e. ( ZZ>= ` N ) dom ( F ` m ) C_ |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) ) |
47 |
45 46
|
syl |
|- ( n e. ( ZZ>= ` N ) -> |^|_ m e. ( ZZ>= ` N ) dom ( F ` m ) C_ |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) ) |
48 |
47
|
adantl |
|- ( ( ph /\ n e. ( ZZ>= ` N ) ) -> |^|_ m e. ( ZZ>= ` N ) dom ( F ` m ) C_ |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) ) |
49 |
11
|
adantr |
|- ( ( ph /\ n e. ( ZZ>= ` N ) ) -> X e. |^|_ m e. ( ZZ>= ` N ) dom ( F ` m ) ) |
50 |
48 49
|
sseldd |
|- ( ( ph /\ n e. ( ZZ>= ` N ) ) -> X e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) ) |
51 |
|
nfv |
|- F/ m n e. ( ZZ>= ` N ) |
52 |
2 51
|
nfan |
|- F/ m ( ph /\ n e. ( ZZ>= ` N ) ) |
53 |
|
eqid |
|- ( ZZ>= ` n ) = ( ZZ>= ` n ) |
54 |
|
simpll |
|- ( ( ( ph /\ n e. ( ZZ>= ` N ) ) /\ m e. ( ZZ>= ` n ) ) -> ph ) |
55 |
45
|
sselda |
|- ( ( n e. ( ZZ>= ` N ) /\ m e. ( ZZ>= ` n ) ) -> m e. ( ZZ>= ` N ) ) |
56 |
55
|
adantll |
|- ( ( ( ph /\ n e. ( ZZ>= ` N ) ) /\ m e. ( ZZ>= ` n ) ) -> m e. ( ZZ>= ` N ) ) |
57 |
5
|
adantr |
|- ( ( ph /\ m e. ( ZZ>= ` N ) ) -> S e. SAlg ) |
58 |
|
simpl |
|- ( ( ph /\ m e. ( ZZ>= ` N ) ) -> ph ) |
59 |
17
|
sselda |
|- ( ( ph /\ m e. ( ZZ>= ` N ) ) -> m e. Z ) |
60 |
6
|
ffvelrnda |
|- ( ( ph /\ m e. Z ) -> ( F ` m ) e. ( SMblFn ` S ) ) |
61 |
58 59 60
|
syl2anc |
|- ( ( ph /\ m e. ( ZZ>= ` N ) ) -> ( F ` m ) e. ( SMblFn ` S ) ) |
62 |
|
eqid |
|- dom ( F ` m ) = dom ( F ` m ) |
63 |
57 61 62
|
smff |
|- ( ( ph /\ m e. ( ZZ>= ` N ) ) -> ( F ` m ) : dom ( F ` m ) --> RR ) |
64 |
|
eliin |
|- ( X e. |^|_ m e. ( ZZ>= ` N ) dom ( F ` m ) -> ( X e. |^|_ m e. ( ZZ>= ` N ) dom ( F ` m ) <-> A. m e. ( ZZ>= ` N ) X e. dom ( F ` m ) ) ) |
65 |
11 64
|
syl |
|- ( ph -> ( X e. |^|_ m e. ( ZZ>= ` N ) dom ( F ` m ) <-> A. m e. ( ZZ>= ` N ) X e. dom ( F ` m ) ) ) |
66 |
11 65
|
mpbid |
|- ( ph -> A. m e. ( ZZ>= ` N ) X e. dom ( F ` m ) ) |
67 |
66
|
adantr |
|- ( ( ph /\ m e. ( ZZ>= ` N ) ) -> A. m e. ( ZZ>= ` N ) X e. dom ( F ` m ) ) |
68 |
|
simpr |
|- ( ( ph /\ m e. ( ZZ>= ` N ) ) -> m e. ( ZZ>= ` N ) ) |
69 |
|
rspa |
|- ( ( A. m e. ( ZZ>= ` N ) X e. dom ( F ` m ) /\ m e. ( ZZ>= ` N ) ) -> X e. dom ( F ` m ) ) |
70 |
67 68 69
|
syl2anc |
|- ( ( ph /\ m e. ( ZZ>= ` N ) ) -> X e. dom ( F ` m ) ) |
71 |
63 70
|
ffvelrnd |
|- ( ( ph /\ m e. ( ZZ>= ` N ) ) -> ( ( F ` m ) ` X ) e. RR ) |
72 |
54 56 71
|
syl2anc |
|- ( ( ( ph /\ n e. ( ZZ>= ` N ) ) /\ m e. ( ZZ>= ` n ) ) -> ( ( F ` m ) ` X ) e. RR ) |
73 |
|
eluzelz |
|- ( n e. ( ZZ>= ` N ) -> n e. ZZ ) |
74 |
73
|
adantl |
|- ( ( ph /\ n e. ( ZZ>= ` N ) ) -> n e. ZZ ) |
75 |
3
|
adantr |
|- ( ( ph /\ n e. ( ZZ>= ` N ) ) -> M e. ZZ ) |
76 |
|
fvex |
|- ( ( F ` m ) ` X ) e. _V |
77 |
76
|
a1i |
|- ( ( ( ph /\ n e. ( ZZ>= ` N ) ) /\ m e. Z ) -> ( ( F ` m ) ` X ) e. _V ) |
78 |
52 74 75 53 4 72 77
|
limsupequzmpt |
|- ( ( ph /\ n e. ( ZZ>= ` N ) ) -> ( limsup ` ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` X ) ) ) = ( limsup ` ( m e. Z |-> ( ( F ` m ) ` X ) ) ) ) |
79 |
9
|
adantr |
|- ( ( ph /\ n e. ( ZZ>= ` N ) ) -> ( limsup ` ( m e. Z |-> ( ( F ` m ) ` X ) ) ) e. RR ) |
80 |
78 79
|
eqeltrd |
|- ( ( ph /\ n e. ( ZZ>= ` N ) ) -> ( limsup ` ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` X ) ) ) e. RR ) |
81 |
80
|
renepnfd |
|- ( ( ph /\ n e. ( ZZ>= ` N ) ) -> ( limsup ` ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` X ) ) ) =/= +oo ) |
82 |
52 53 72 81
|
limsupubuzmpt |
|- ( ( ph /\ n e. ( ZZ>= ` N ) ) -> E. y e. RR A. m e. ( ZZ>= ` n ) ( ( F ` m ) ` X ) <_ y ) |
83 |
|
uzid2 |
|- ( n e. ( ZZ>= ` N ) -> n e. ( ZZ>= ` n ) ) |
84 |
83
|
ne0d |
|- ( n e. ( ZZ>= ` N ) -> ( ZZ>= ` n ) =/= (/) ) |
85 |
84
|
adantl |
|- ( ( ph /\ n e. ( ZZ>= ` N ) ) -> ( ZZ>= ` n ) =/= (/) ) |
86 |
52 85 72
|
supxrre3rnmpt |
|- ( ( ph /\ n e. ( ZZ>= ` N ) ) -> ( sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` X ) ) , RR* , < ) e. RR <-> E. y e. RR A. m e. ( ZZ>= ` n ) ( ( F ` m ) ` X ) <_ y ) ) |
87 |
82 86
|
mpbird |
|- ( ( ph /\ n e. ( ZZ>= ` N ) ) -> sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` X ) ) , RR* , < ) e. RR ) |
88 |
44 50 87
|
elrabd |
|- ( ( ph /\ n e. ( ZZ>= ` N ) ) -> X e. { y e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` y ) ) , RR* , < ) e. RR } ) |
89 |
|
simpl |
|- ( ( y = x /\ m e. ( ZZ>= ` n ) ) -> y = x ) |
90 |
89
|
fveq2d |
|- ( ( y = x /\ m e. ( ZZ>= ` n ) ) -> ( ( F ` m ) ` y ) = ( ( F ` m ) ` x ) ) |
91 |
90
|
mpteq2dva |
|- ( y = x -> ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` y ) ) = ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) ) |
92 |
91
|
rneqd |
|- ( y = x -> ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` y ) ) = ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) ) |
93 |
92
|
supeq1d |
|- ( y = x -> sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` y ) ) , RR* , < ) = sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) ) |
94 |
93
|
eleq1d |
|- ( y = x -> ( sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` y ) ) , RR* , < ) e. RR <-> sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) e. RR ) ) |
95 |
94
|
cbvrabv |
|- { y e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` y ) ) , RR* , < ) e. RR } = { x e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) e. RR } |
96 |
88 95
|
eleqtrdi |
|- ( ( ph /\ n e. ( ZZ>= ` N ) ) -> X e. { x e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) e. RR } ) |
97 |
|
eqid |
|- { x e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) e. RR } = { x e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) e. RR } |
98 |
|
fvex |
|- ( F ` m ) e. _V |
99 |
98
|
dmex |
|- dom ( F ` m ) e. _V |
100 |
99
|
rgenw |
|- A. m e. ( ZZ>= ` n ) dom ( F ` m ) e. _V |
101 |
100
|
a1i |
|- ( n e. ( ZZ>= ` N ) -> A. m e. ( ZZ>= ` n ) dom ( F ` m ) e. _V ) |
102 |
84 101
|
iinexd |
|- ( n e. ( ZZ>= ` N ) -> |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) e. _V ) |
103 |
102
|
adantl |
|- ( ( ph /\ n e. ( ZZ>= ` N ) ) -> |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) e. _V ) |
104 |
97 103
|
rabexd |
|- ( ( ph /\ n e. ( ZZ>= ` N ) ) -> { x e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) e. RR } e. _V ) |
105 |
7
|
fvmpt2 |
|- ( ( n e. Z /\ { x e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) e. RR } e. _V ) -> ( E ` n ) = { x e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) e. RR } ) |
106 |
18 104 105
|
syl2anc |
|- ( ( ph /\ n e. ( ZZ>= ` N ) ) -> ( E ` n ) = { x e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) e. RR } ) |
107 |
96 106
|
eleqtrrd |
|- ( ( ph /\ n e. ( ZZ>= ` N ) ) -> X e. ( E ` n ) ) |
108 |
38 43 107 87
|
fvmptd3 |
|- ( ( ph /\ n e. ( ZZ>= ` N ) ) -> ( ( x e. ( E ` n ) |-> sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) ) ` X ) = sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` X ) ) , RR* , < ) ) |
109 |
30 108
|
eqtrd |
|- ( ( ph /\ n e. ( ZZ>= ` N ) ) -> ( ( H ` n ) ` X ) = sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` X ) ) , RR* , < ) ) |
110 |
1 109
|
mpteq2da |
|- ( ph -> ( n e. ( ZZ>= ` N ) |-> ( ( H ` n ) ` X ) ) = ( n e. ( ZZ>= ` N ) |-> sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` X ) ) , RR* , < ) ) ) |
111 |
4
|
eluzelz2 |
|- ( N e. Z -> N e. ZZ ) |
112 |
10 111
|
syl |
|- ( ph -> N e. ZZ ) |
113 |
|
eqid |
|- ( ZZ>= ` N ) = ( ZZ>= ` N ) |
114 |
76
|
a1i |
|- ( ( ph /\ m e. ( ZZ>= ` N ) ) -> ( ( F ` m ) ` X ) e. _V ) |
115 |
76
|
a1i |
|- ( ( ph /\ m e. Z ) -> ( ( F ` m ) ` X ) e. _V ) |
116 |
2 112 3 113 4 114 115
|
limsupequzmpt |
|- ( ph -> ( limsup ` ( m e. ( ZZ>= ` N ) |-> ( ( F ` m ) ` X ) ) ) = ( limsup ` ( m e. Z |-> ( ( F ` m ) ` X ) ) ) ) |
117 |
116 9
|
eqeltrd |
|- ( ph -> ( limsup ` ( m e. ( ZZ>= ` N ) |-> ( ( F ` m ) ` X ) ) ) e. RR ) |
118 |
2 112 113 71 117
|
supcnvlimsupmpt |
|- ( ph -> ( n e. ( ZZ>= ` N ) |-> sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` X ) ) , RR* , < ) ) ~~> ( limsup ` ( m e. ( ZZ>= ` N ) |-> ( ( F ` m ) ` X ) ) ) ) |
119 |
110 118
|
eqbrtrd |
|- ( ph -> ( n e. ( ZZ>= ` N ) |-> ( ( H ` n ) ` X ) ) ~~> ( limsup ` ( m e. ( ZZ>= ` N ) |-> ( ( F ` m ) ` X ) ) ) ) |