Metamath Proof Explorer


Theorem rrncmslem

Description: Lemma for rrncms . (Contributed by Jeff Madsen, 6-Jun-2014) (Revised by Mario Carneiro, 13-Sep-2015)

Ref Expression
Hypotheses rrnval.1
|- X = ( RR ^m I )
rrndstprj1.1
|- M = ( ( abs o. - ) |` ( RR X. RR ) )
rrncms.3
|- J = ( MetOpen ` ( Rn ` I ) )
rrncms.4
|- ( ph -> I e. Fin )
rrncms.5
|- ( ph -> F e. ( Cau ` ( Rn ` I ) ) )
rrncms.6
|- ( ph -> F : NN --> X )
rrncms.7
|- P = ( m e. I |-> ( ~~> ` ( t e. NN |-> ( ( F ` t ) ` m ) ) ) )
Assertion rrncmslem
|- ( ph -> F e. dom ( ~~>t ` J ) )

Proof

Step Hyp Ref Expression
1 rrnval.1
 |-  X = ( RR ^m I )
2 rrndstprj1.1
 |-  M = ( ( abs o. - ) |` ( RR X. RR ) )
3 rrncms.3
 |-  J = ( MetOpen ` ( Rn ` I ) )
4 rrncms.4
 |-  ( ph -> I e. Fin )
5 rrncms.5
 |-  ( ph -> F e. ( Cau ` ( Rn ` I ) ) )
6 rrncms.6
 |-  ( ph -> F : NN --> X )
7 rrncms.7
 |-  P = ( m e. I |-> ( ~~> ` ( t e. NN |-> ( ( F ` t ) ` m ) ) ) )
8 lmrel
 |-  Rel ( ~~>t ` J )
9 fvex
 |-  ( ~~> ` ( t e. NN |-> ( ( F ` t ) ` m ) ) ) e. _V
10 9 7 fnmpti
 |-  P Fn I
11 10 a1i
 |-  ( ph -> P Fn I )
12 nnuz
 |-  NN = ( ZZ>= ` 1 )
13 1zzd
 |-  ( ( ph /\ n e. I ) -> 1 e. ZZ )
14 fveq2
 |-  ( t = k -> ( F ` t ) = ( F ` k ) )
15 14 fveq1d
 |-  ( t = k -> ( ( F ` t ) ` n ) = ( ( F ` k ) ` n ) )
16 eqid
 |-  ( t e. NN |-> ( ( F ` t ) ` n ) ) = ( t e. NN |-> ( ( F ` t ) ` n ) )
17 fvex
 |-  ( ( F ` k ) ` n ) e. _V
18 15 16 17 fvmpt
 |-  ( k e. NN -> ( ( t e. NN |-> ( ( F ` t ) ` n ) ) ` k ) = ( ( F ` k ) ` n ) )
19 18 adantl
 |-  ( ( ( ph /\ n e. I ) /\ k e. NN ) -> ( ( t e. NN |-> ( ( F ` t ) ` n ) ) ` k ) = ( ( F ` k ) ` n ) )
20 6 ffvelrnda
 |-  ( ( ph /\ k e. NN ) -> ( F ` k ) e. X )
21 20 1 eleqtrdi
 |-  ( ( ph /\ k e. NN ) -> ( F ` k ) e. ( RR ^m I ) )
22 elmapi
 |-  ( ( F ` k ) e. ( RR ^m I ) -> ( F ` k ) : I --> RR )
23 21 22 syl
 |-  ( ( ph /\ k e. NN ) -> ( F ` k ) : I --> RR )
24 23 ffvelrnda
 |-  ( ( ( ph /\ k e. NN ) /\ n e. I ) -> ( ( F ` k ) ` n ) e. RR )
25 24 an32s
 |-  ( ( ( ph /\ n e. I ) /\ k e. NN ) -> ( ( F ` k ) ` n ) e. RR )
26 19 25 eqeltrd
 |-  ( ( ( ph /\ n e. I ) /\ k e. NN ) -> ( ( t e. NN |-> ( ( F ` t ) ` n ) ) ` k ) e. RR )
27 26 recnd
 |-  ( ( ( ph /\ n e. I ) /\ k e. NN ) -> ( ( t e. NN |-> ( ( F ` t ) ` n ) ) ` k ) e. CC )
28 1 rrnmet
 |-  ( I e. Fin -> ( Rn ` I ) e. ( Met ` X ) )
29 4 28 syl
 |-  ( ph -> ( Rn ` I ) e. ( Met ` X ) )
30 metxmet
 |-  ( ( Rn ` I ) e. ( Met ` X ) -> ( Rn ` I ) e. ( *Met ` X ) )
31 29 30 syl
 |-  ( ph -> ( Rn ` I ) e. ( *Met ` X ) )
32 1zzd
 |-  ( ph -> 1 e. ZZ )
33 eqidd
 |-  ( ( ph /\ k e. NN ) -> ( F ` k ) = ( F ` k ) )
34 eqidd
 |-  ( ( ph /\ j e. NN ) -> ( F ` j ) = ( F ` j ) )
35 12 31 32 33 34 6 iscauf
 |-  ( ph -> ( F e. ( Cau ` ( Rn ` I ) ) <-> A. x e. RR+ E. j e. NN A. k e. ( ZZ>= ` j ) ( ( F ` j ) ( Rn ` I ) ( F ` k ) ) < x ) )
36 5 35 mpbid
 |-  ( ph -> A. x e. RR+ E. j e. NN A. k e. ( ZZ>= ` j ) ( ( F ` j ) ( Rn ` I ) ( F ` k ) ) < x )
37 36 adantr
 |-  ( ( ph /\ n e. I ) -> A. x e. RR+ E. j e. NN A. k e. ( ZZ>= ` j ) ( ( F ` j ) ( Rn ` I ) ( F ` k ) ) < x )
38 4 ad3antrrr
 |-  ( ( ( ( ph /\ n e. I ) /\ j e. NN ) /\ k e. ( ZZ>= ` j ) ) -> I e. Fin )
39 simpllr
 |-  ( ( ( ( ph /\ n e. I ) /\ j e. NN ) /\ k e. ( ZZ>= ` j ) ) -> n e. I )
40 6 ad3antrrr
 |-  ( ( ( ( ph /\ n e. I ) /\ j e. NN ) /\ k e. ( ZZ>= ` j ) ) -> F : NN --> X )
41 eluznn
 |-  ( ( j e. NN /\ k e. ( ZZ>= ` j ) ) -> k e. NN )
42 41 adantll
 |-  ( ( ( ( ph /\ n e. I ) /\ j e. NN ) /\ k e. ( ZZ>= ` j ) ) -> k e. NN )
43 40 42 ffvelrnd
 |-  ( ( ( ( ph /\ n e. I ) /\ j e. NN ) /\ k e. ( ZZ>= ` j ) ) -> ( F ` k ) e. X )
44 simplr
 |-  ( ( ( ( ph /\ n e. I ) /\ j e. NN ) /\ k e. ( ZZ>= ` j ) ) -> j e. NN )
45 40 44 ffvelrnd
 |-  ( ( ( ( ph /\ n e. I ) /\ j e. NN ) /\ k e. ( ZZ>= ` j ) ) -> ( F ` j ) e. X )
46 1 2 rrndstprj1
 |-  ( ( ( I e. Fin /\ n e. I ) /\ ( ( F ` k ) e. X /\ ( F ` j ) e. X ) ) -> ( ( ( F ` k ) ` n ) M ( ( F ` j ) ` n ) ) <_ ( ( F ` k ) ( Rn ` I ) ( F ` j ) ) )
47 38 39 43 45 46 syl22anc
 |-  ( ( ( ( ph /\ n e. I ) /\ j e. NN ) /\ k e. ( ZZ>= ` j ) ) -> ( ( ( F ` k ) ` n ) M ( ( F ` j ) ` n ) ) <_ ( ( F ` k ) ( Rn ` I ) ( F ` j ) ) )
48 29 ad3antrrr
 |-  ( ( ( ( ph /\ n e. I ) /\ j e. NN ) /\ k e. ( ZZ>= ` j ) ) -> ( Rn ` I ) e. ( Met ` X ) )
49 metsym
 |-  ( ( ( Rn ` I ) e. ( Met ` X ) /\ ( F ` k ) e. X /\ ( F ` j ) e. X ) -> ( ( F ` k ) ( Rn ` I ) ( F ` j ) ) = ( ( F ` j ) ( Rn ` I ) ( F ` k ) ) )
50 48 43 45 49 syl3anc
 |-  ( ( ( ( ph /\ n e. I ) /\ j e. NN ) /\ k e. ( ZZ>= ` j ) ) -> ( ( F ` k ) ( Rn ` I ) ( F ` j ) ) = ( ( F ` j ) ( Rn ` I ) ( F ` k ) ) )
51 47 50 breqtrd
 |-  ( ( ( ( ph /\ n e. I ) /\ j e. NN ) /\ k e. ( ZZ>= ` j ) ) -> ( ( ( F ` k ) ` n ) M ( ( F ` j ) ` n ) ) <_ ( ( F ` j ) ( Rn ` I ) ( F ` k ) ) )
52 51 adantllr
 |-  ( ( ( ( ( ph /\ n e. I ) /\ x e. RR+ ) /\ j e. NN ) /\ k e. ( ZZ>= ` j ) ) -> ( ( ( F ` k ) ` n ) M ( ( F ` j ) ` n ) ) <_ ( ( F ` j ) ( Rn ` I ) ( F ` k ) ) )
53 2 remet
 |-  M e. ( Met ` RR )
54 53 a1i
 |-  ( ( ( ( ph /\ n e. I ) /\ j e. NN ) /\ k e. ( ZZ>= ` j ) ) -> M e. ( Met ` RR ) )
55 simpll
 |-  ( ( ( ( ph /\ n e. I ) /\ j e. NN ) /\ k e. ( ZZ>= ` j ) ) -> ( ph /\ n e. I ) )
56 55 42 25 syl2anc
 |-  ( ( ( ( ph /\ n e. I ) /\ j e. NN ) /\ k e. ( ZZ>= ` j ) ) -> ( ( F ` k ) ` n ) e. RR )
57 6 ffvelrnda
 |-  ( ( ph /\ j e. NN ) -> ( F ` j ) e. X )
58 57 1 eleqtrdi
 |-  ( ( ph /\ j e. NN ) -> ( F ` j ) e. ( RR ^m I ) )
59 elmapi
 |-  ( ( F ` j ) e. ( RR ^m I ) -> ( F ` j ) : I --> RR )
60 58 59 syl
 |-  ( ( ph /\ j e. NN ) -> ( F ` j ) : I --> RR )
61 60 ffvelrnda
 |-  ( ( ( ph /\ j e. NN ) /\ n e. I ) -> ( ( F ` j ) ` n ) e. RR )
62 61 an32s
 |-  ( ( ( ph /\ n e. I ) /\ j e. NN ) -> ( ( F ` j ) ` n ) e. RR )
63 62 adantr
 |-  ( ( ( ( ph /\ n e. I ) /\ j e. NN ) /\ k e. ( ZZ>= ` j ) ) -> ( ( F ` j ) ` n ) e. RR )
64 metcl
 |-  ( ( M e. ( Met ` RR ) /\ ( ( F ` k ) ` n ) e. RR /\ ( ( F ` j ) ` n ) e. RR ) -> ( ( ( F ` k ) ` n ) M ( ( F ` j ) ` n ) ) e. RR )
65 54 56 63 64 syl3anc
 |-  ( ( ( ( ph /\ n e. I ) /\ j e. NN ) /\ k e. ( ZZ>= ` j ) ) -> ( ( ( F ` k ) ` n ) M ( ( F ` j ) ` n ) ) e. RR )
66 65 adantllr
 |-  ( ( ( ( ( ph /\ n e. I ) /\ x e. RR+ ) /\ j e. NN ) /\ k e. ( ZZ>= ` j ) ) -> ( ( ( F ` k ) ` n ) M ( ( F ` j ) ` n ) ) e. RR )
67 metcl
 |-  ( ( ( Rn ` I ) e. ( Met ` X ) /\ ( F ` j ) e. X /\ ( F ` k ) e. X ) -> ( ( F ` j ) ( Rn ` I ) ( F ` k ) ) e. RR )
68 48 45 43 67 syl3anc
 |-  ( ( ( ( ph /\ n e. I ) /\ j e. NN ) /\ k e. ( ZZ>= ` j ) ) -> ( ( F ` j ) ( Rn ` I ) ( F ` k ) ) e. RR )
69 68 adantllr
 |-  ( ( ( ( ( ph /\ n e. I ) /\ x e. RR+ ) /\ j e. NN ) /\ k e. ( ZZ>= ` j ) ) -> ( ( F ` j ) ( Rn ` I ) ( F ` k ) ) e. RR )
70 rpre
 |-  ( x e. RR+ -> x e. RR )
71 70 adantl
 |-  ( ( ( ph /\ n e. I ) /\ x e. RR+ ) -> x e. RR )
72 71 ad2antrr
 |-  ( ( ( ( ( ph /\ n e. I ) /\ x e. RR+ ) /\ j e. NN ) /\ k e. ( ZZ>= ` j ) ) -> x e. RR )
73 lelttr
 |-  ( ( ( ( ( F ` k ) ` n ) M ( ( F ` j ) ` n ) ) e. RR /\ ( ( F ` j ) ( Rn ` I ) ( F ` k ) ) e. RR /\ x e. RR ) -> ( ( ( ( ( F ` k ) ` n ) M ( ( F ` j ) ` n ) ) <_ ( ( F ` j ) ( Rn ` I ) ( F ` k ) ) /\ ( ( F ` j ) ( Rn ` I ) ( F ` k ) ) < x ) -> ( ( ( F ` k ) ` n ) M ( ( F ` j ) ` n ) ) < x ) )
74 66 69 72 73 syl3anc
 |-  ( ( ( ( ( ph /\ n e. I ) /\ x e. RR+ ) /\ j e. NN ) /\ k e. ( ZZ>= ` j ) ) -> ( ( ( ( ( F ` k ) ` n ) M ( ( F ` j ) ` n ) ) <_ ( ( F ` j ) ( Rn ` I ) ( F ` k ) ) /\ ( ( F ` j ) ( Rn ` I ) ( F ` k ) ) < x ) -> ( ( ( F ` k ) ` n ) M ( ( F ` j ) ` n ) ) < x ) )
75 52 74 mpand
 |-  ( ( ( ( ( ph /\ n e. I ) /\ x e. RR+ ) /\ j e. NN ) /\ k e. ( ZZ>= ` j ) ) -> ( ( ( F ` j ) ( Rn ` I ) ( F ` k ) ) < x -> ( ( ( F ` k ) ` n ) M ( ( F ` j ) ` n ) ) < x ) )
76 75 ralimdva
 |-  ( ( ( ( ph /\ n e. I ) /\ x e. RR+ ) /\ j e. NN ) -> ( A. k e. ( ZZ>= ` j ) ( ( F ` j ) ( Rn ` I ) ( F ` k ) ) < x -> A. k e. ( ZZ>= ` j ) ( ( ( F ` k ) ` n ) M ( ( F ` j ) ` n ) ) < x ) )
77 76 reximdva
 |-  ( ( ( ph /\ n e. I ) /\ x e. RR+ ) -> ( E. j e. NN A. k e. ( ZZ>= ` j ) ( ( F ` j ) ( Rn ` I ) ( F ` k ) ) < x -> E. j e. NN A. k e. ( ZZ>= ` j ) ( ( ( F ` k ) ` n ) M ( ( F ` j ) ` n ) ) < x ) )
78 77 ralimdva
 |-  ( ( ph /\ n e. I ) -> ( A. x e. RR+ E. j e. NN A. k e. ( ZZ>= ` j ) ( ( F ` j ) ( Rn ` I ) ( F ` k ) ) < x -> A. x e. RR+ E. j e. NN A. k e. ( ZZ>= ` j ) ( ( ( F ` k ) ` n ) M ( ( F ` j ) ` n ) ) < x ) )
79 2 remetdval
 |-  ( ( ( ( F ` k ) ` n ) e. RR /\ ( ( F ` j ) ` n ) e. RR ) -> ( ( ( F ` k ) ` n ) M ( ( F ` j ) ` n ) ) = ( abs ` ( ( ( F ` k ) ` n ) - ( ( F ` j ) ` n ) ) ) )
80 56 63 79 syl2anc
 |-  ( ( ( ( ph /\ n e. I ) /\ j e. NN ) /\ k e. ( ZZ>= ` j ) ) -> ( ( ( F ` k ) ` n ) M ( ( F ` j ) ` n ) ) = ( abs ` ( ( ( F ` k ) ` n ) - ( ( F ` j ) ` n ) ) ) )
81 42 18 syl
 |-  ( ( ( ( ph /\ n e. I ) /\ j e. NN ) /\ k e. ( ZZ>= ` j ) ) -> ( ( t e. NN |-> ( ( F ` t ) ` n ) ) ` k ) = ( ( F ` k ) ` n ) )
82 fveq2
 |-  ( t = j -> ( F ` t ) = ( F ` j ) )
83 82 fveq1d
 |-  ( t = j -> ( ( F ` t ) ` n ) = ( ( F ` j ) ` n ) )
84 fvex
 |-  ( ( F ` j ) ` n ) e. _V
85 83 16 84 fvmpt
 |-  ( j e. NN -> ( ( t e. NN |-> ( ( F ` t ) ` n ) ) ` j ) = ( ( F ` j ) ` n ) )
86 85 ad2antlr
 |-  ( ( ( ( ph /\ n e. I ) /\ j e. NN ) /\ k e. ( ZZ>= ` j ) ) -> ( ( t e. NN |-> ( ( F ` t ) ` n ) ) ` j ) = ( ( F ` j ) ` n ) )
87 81 86 oveq12d
 |-  ( ( ( ( ph /\ n e. I ) /\ j e. NN ) /\ k e. ( ZZ>= ` j ) ) -> ( ( ( t e. NN |-> ( ( F ` t ) ` n ) ) ` k ) - ( ( t e. NN |-> ( ( F ` t ) ` n ) ) ` j ) ) = ( ( ( F ` k ) ` n ) - ( ( F ` j ) ` n ) ) )
88 87 fveq2d
 |-  ( ( ( ( ph /\ n e. I ) /\ j e. NN ) /\ k e. ( ZZ>= ` j ) ) -> ( abs ` ( ( ( t e. NN |-> ( ( F ` t ) ` n ) ) ` k ) - ( ( t e. NN |-> ( ( F ` t ) ` n ) ) ` j ) ) ) = ( abs ` ( ( ( F ` k ) ` n ) - ( ( F ` j ) ` n ) ) ) )
89 80 88 eqtr4d
 |-  ( ( ( ( ph /\ n e. I ) /\ j e. NN ) /\ k e. ( ZZ>= ` j ) ) -> ( ( ( F ` k ) ` n ) M ( ( F ` j ) ` n ) ) = ( abs ` ( ( ( t e. NN |-> ( ( F ` t ) ` n ) ) ` k ) - ( ( t e. NN |-> ( ( F ` t ) ` n ) ) ` j ) ) ) )
90 89 breq1d
 |-  ( ( ( ( ph /\ n e. I ) /\ j e. NN ) /\ k e. ( ZZ>= ` j ) ) -> ( ( ( ( F ` k ) ` n ) M ( ( F ` j ) ` n ) ) < x <-> ( abs ` ( ( ( t e. NN |-> ( ( F ` t ) ` n ) ) ` k ) - ( ( t e. NN |-> ( ( F ` t ) ` n ) ) ` j ) ) ) < x ) )
91 90 ralbidva
 |-  ( ( ( ph /\ n e. I ) /\ j e. NN ) -> ( A. k e. ( ZZ>= ` j ) ( ( ( F ` k ) ` n ) M ( ( F ` j ) ` n ) ) < x <-> A. k e. ( ZZ>= ` j ) ( abs ` ( ( ( t e. NN |-> ( ( F ` t ) ` n ) ) ` k ) - ( ( t e. NN |-> ( ( F ` t ) ` n ) ) ` j ) ) ) < x ) )
92 91 rexbidva
 |-  ( ( ph /\ n e. I ) -> ( E. j e. NN A. k e. ( ZZ>= ` j ) ( ( ( F ` k ) ` n ) M ( ( F ` j ) ` n ) ) < x <-> E. j e. NN A. k e. ( ZZ>= ` j ) ( abs ` ( ( ( t e. NN |-> ( ( F ` t ) ` n ) ) ` k ) - ( ( t e. NN |-> ( ( F ` t ) ` n ) ) ` j ) ) ) < x ) )
93 92 ralbidv
 |-  ( ( ph /\ n e. I ) -> ( A. x e. RR+ E. j e. NN A. k e. ( ZZ>= ` j ) ( ( ( F ` k ) ` n ) M ( ( F ` j ) ` n ) ) < x <-> A. x e. RR+ E. j e. NN A. k e. ( ZZ>= ` j ) ( abs ` ( ( ( t e. NN |-> ( ( F ` t ) ` n ) ) ` k ) - ( ( t e. NN |-> ( ( F ` t ) ` n ) ) ` j ) ) ) < x ) )
94 78 93 sylibd
 |-  ( ( ph /\ n e. I ) -> ( A. x e. RR+ E. j e. NN A. k e. ( ZZ>= ` j ) ( ( F ` j ) ( Rn ` I ) ( F ` k ) ) < x -> A. x e. RR+ E. j e. NN A. k e. ( ZZ>= ` j ) ( abs ` ( ( ( t e. NN |-> ( ( F ` t ) ` n ) ) ` k ) - ( ( t e. NN |-> ( ( F ` t ) ` n ) ) ` j ) ) ) < x ) )
95 37 94 mpd
 |-  ( ( ph /\ n e. I ) -> A. x e. RR+ E. j e. NN A. k e. ( ZZ>= ` j ) ( abs ` ( ( ( t e. NN |-> ( ( F ` t ) ` n ) ) ` k ) - ( ( t e. NN |-> ( ( F ` t ) ` n ) ) ` j ) ) ) < x )
96 nnex
 |-  NN e. _V
97 96 mptex
 |-  ( t e. NN |-> ( ( F ` t ) ` n ) ) e. _V
98 97 a1i
 |-  ( ( ph /\ n e. I ) -> ( t e. NN |-> ( ( F ` t ) ` n ) ) e. _V )
99 12 27 95 98 caucvg
 |-  ( ( ph /\ n e. I ) -> ( t e. NN |-> ( ( F ` t ) ` n ) ) e. dom ~~> )
100 climdm
 |-  ( ( t e. NN |-> ( ( F ` t ) ` n ) ) e. dom ~~> <-> ( t e. NN |-> ( ( F ` t ) ` n ) ) ~~> ( ~~> ` ( t e. NN |-> ( ( F ` t ) ` n ) ) ) )
101 99 100 sylib
 |-  ( ( ph /\ n e. I ) -> ( t e. NN |-> ( ( F ` t ) ` n ) ) ~~> ( ~~> ` ( t e. NN |-> ( ( F ` t ) ` n ) ) ) )
102 fveq2
 |-  ( m = n -> ( ( F ` t ) ` m ) = ( ( F ` t ) ` n ) )
103 102 mpteq2dv
 |-  ( m = n -> ( t e. NN |-> ( ( F ` t ) ` m ) ) = ( t e. NN |-> ( ( F ` t ) ` n ) ) )
104 103 fveq2d
 |-  ( m = n -> ( ~~> ` ( t e. NN |-> ( ( F ` t ) ` m ) ) ) = ( ~~> ` ( t e. NN |-> ( ( F ` t ) ` n ) ) ) )
105 fvex
 |-  ( ~~> ` ( t e. NN |-> ( ( F ` t ) ` n ) ) ) e. _V
106 104 7 105 fvmpt
 |-  ( n e. I -> ( P ` n ) = ( ~~> ` ( t e. NN |-> ( ( F ` t ) ` n ) ) ) )
107 106 adantl
 |-  ( ( ph /\ n e. I ) -> ( P ` n ) = ( ~~> ` ( t e. NN |-> ( ( F ` t ) ` n ) ) ) )
108 101 107 breqtrrd
 |-  ( ( ph /\ n e. I ) -> ( t e. NN |-> ( ( F ` t ) ` n ) ) ~~> ( P ` n ) )
109 12 13 108 26 climrecl
 |-  ( ( ph /\ n e. I ) -> ( P ` n ) e. RR )
110 109 ralrimiva
 |-  ( ph -> A. n e. I ( P ` n ) e. RR )
111 ffnfv
 |-  ( P : I --> RR <-> ( P Fn I /\ A. n e. I ( P ` n ) e. RR ) )
112 11 110 111 sylanbrc
 |-  ( ph -> P : I --> RR )
113 reex
 |-  RR e. _V
114 elmapg
 |-  ( ( RR e. _V /\ I e. Fin ) -> ( P e. ( RR ^m I ) <-> P : I --> RR ) )
115 113 4 114 sylancr
 |-  ( ph -> ( P e. ( RR ^m I ) <-> P : I --> RR ) )
116 112 115 mpbird
 |-  ( ph -> P e. ( RR ^m I ) )
117 116 1 eleqtrrdi
 |-  ( ph -> P e. X )
118 1nn
 |-  1 e. NN
119 4 ad2antrr
 |-  ( ( ( ph /\ ( x e. RR+ /\ I = (/) ) ) /\ k e. NN ) -> I e. Fin )
120 20 adantlr
 |-  ( ( ( ph /\ ( x e. RR+ /\ I = (/) ) ) /\ k e. NN ) -> ( F ` k ) e. X )
121 117 ad2antrr
 |-  ( ( ( ph /\ ( x e. RR+ /\ I = (/) ) ) /\ k e. NN ) -> P e. X )
122 1 rrnmval
 |-  ( ( I e. Fin /\ ( F ` k ) e. X /\ P e. X ) -> ( ( F ` k ) ( Rn ` I ) P ) = ( sqrt ` sum_ y e. I ( ( ( ( F ` k ) ` y ) - ( P ` y ) ) ^ 2 ) ) )
123 119 120 121 122 syl3anc
 |-  ( ( ( ph /\ ( x e. RR+ /\ I = (/) ) ) /\ k e. NN ) -> ( ( F ` k ) ( Rn ` I ) P ) = ( sqrt ` sum_ y e. I ( ( ( ( F ` k ) ` y ) - ( P ` y ) ) ^ 2 ) ) )
124 simplrr
 |-  ( ( ( ph /\ ( x e. RR+ /\ I = (/) ) ) /\ k e. NN ) -> I = (/) )
125 124 sumeq1d
 |-  ( ( ( ph /\ ( x e. RR+ /\ I = (/) ) ) /\ k e. NN ) -> sum_ y e. I ( ( ( ( F ` k ) ` y ) - ( P ` y ) ) ^ 2 ) = sum_ y e. (/) ( ( ( ( F ` k ) ` y ) - ( P ` y ) ) ^ 2 ) )
126 sum0
 |-  sum_ y e. (/) ( ( ( ( F ` k ) ` y ) - ( P ` y ) ) ^ 2 ) = 0
127 125 126 eqtrdi
 |-  ( ( ( ph /\ ( x e. RR+ /\ I = (/) ) ) /\ k e. NN ) -> sum_ y e. I ( ( ( ( F ` k ) ` y ) - ( P ` y ) ) ^ 2 ) = 0 )
128 127 fveq2d
 |-  ( ( ( ph /\ ( x e. RR+ /\ I = (/) ) ) /\ k e. NN ) -> ( sqrt ` sum_ y e. I ( ( ( ( F ` k ) ` y ) - ( P ` y ) ) ^ 2 ) ) = ( sqrt ` 0 ) )
129 123 128 eqtrd
 |-  ( ( ( ph /\ ( x e. RR+ /\ I = (/) ) ) /\ k e. NN ) -> ( ( F ` k ) ( Rn ` I ) P ) = ( sqrt ` 0 ) )
130 sqrt0
 |-  ( sqrt ` 0 ) = 0
131 129 130 eqtrdi
 |-  ( ( ( ph /\ ( x e. RR+ /\ I = (/) ) ) /\ k e. NN ) -> ( ( F ` k ) ( Rn ` I ) P ) = 0 )
132 simplrl
 |-  ( ( ( ph /\ ( x e. RR+ /\ I = (/) ) ) /\ k e. NN ) -> x e. RR+ )
133 132 rpgt0d
 |-  ( ( ( ph /\ ( x e. RR+ /\ I = (/) ) ) /\ k e. NN ) -> 0 < x )
134 131 133 eqbrtrd
 |-  ( ( ( ph /\ ( x e. RR+ /\ I = (/) ) ) /\ k e. NN ) -> ( ( F ` k ) ( Rn ` I ) P ) < x )
135 134 ralrimiva
 |-  ( ( ph /\ ( x e. RR+ /\ I = (/) ) ) -> A. k e. NN ( ( F ` k ) ( Rn ` I ) P ) < x )
136 fveq2
 |-  ( j = 1 -> ( ZZ>= ` j ) = ( ZZ>= ` 1 ) )
137 136 12 eqtr4di
 |-  ( j = 1 -> ( ZZ>= ` j ) = NN )
138 137 raleqdv
 |-  ( j = 1 -> ( A. k e. ( ZZ>= ` j ) ( ( F ` k ) ( Rn ` I ) P ) < x <-> A. k e. NN ( ( F ` k ) ( Rn ` I ) P ) < x ) )
139 138 rspcev
 |-  ( ( 1 e. NN /\ A. k e. NN ( ( F ` k ) ( Rn ` I ) P ) < x ) -> E. j e. NN A. k e. ( ZZ>= ` j ) ( ( F ` k ) ( Rn ` I ) P ) < x )
140 118 135 139 sylancr
 |-  ( ( ph /\ ( x e. RR+ /\ I = (/) ) ) -> E. j e. NN A. k e. ( ZZ>= ` j ) ( ( F ` k ) ( Rn ` I ) P ) < x )
141 140 expr
 |-  ( ( ph /\ x e. RR+ ) -> ( I = (/) -> E. j e. NN A. k e. ( ZZ>= ` j ) ( ( F ` k ) ( Rn ` I ) P ) < x ) )
142 1zzd
 |-  ( ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) /\ n e. I ) -> 1 e. ZZ )
143 simprl
 |-  ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) -> x e. RR+ )
144 simprr
 |-  ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) -> I =/= (/) )
145 4 adantr
 |-  ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) -> I e. Fin )
146 hashnncl
 |-  ( I e. Fin -> ( ( # ` I ) e. NN <-> I =/= (/) ) )
147 145 146 syl
 |-  ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) -> ( ( # ` I ) e. NN <-> I =/= (/) ) )
148 144 147 mpbird
 |-  ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) -> ( # ` I ) e. NN )
149 148 nnrpd
 |-  ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) -> ( # ` I ) e. RR+ )
150 149 rpsqrtcld
 |-  ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) -> ( sqrt ` ( # ` I ) ) e. RR+ )
151 143 150 rpdivcld
 |-  ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) -> ( x / ( sqrt ` ( # ` I ) ) ) e. RR+ )
152 151 adantr
 |-  ( ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) /\ n e. I ) -> ( x / ( sqrt ` ( # ` I ) ) ) e. RR+ )
153 18 adantl
 |-  ( ( ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) /\ n e. I ) /\ k e. NN ) -> ( ( t e. NN |-> ( ( F ` t ) ` n ) ) ` k ) = ( ( F ` k ) ` n ) )
154 108 adantlr
 |-  ( ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) /\ n e. I ) -> ( t e. NN |-> ( ( F ` t ) ` n ) ) ~~> ( P ` n ) )
155 12 142 152 153 154 climi2
 |-  ( ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) /\ n e. I ) -> E. j e. NN A. k e. ( ZZ>= ` j ) ( abs ` ( ( ( F ` k ) ` n ) - ( P ` n ) ) ) < ( x / ( sqrt ` ( # ` I ) ) ) )
156 1z
 |-  1 e. ZZ
157 12 rexuz3
 |-  ( 1 e. ZZ -> ( E. j e. NN A. k e. ( ZZ>= ` j ) ( ( ( F ` k ) ` n ) M ( P ` n ) ) < ( x / ( sqrt ` ( # ` I ) ) ) <-> E. j e. ZZ A. k e. ( ZZ>= ` j ) ( ( ( F ` k ) ` n ) M ( P ` n ) ) < ( x / ( sqrt ` ( # ` I ) ) ) ) )
158 156 157 ax-mp
 |-  ( E. j e. NN A. k e. ( ZZ>= ` j ) ( ( ( F ` k ) ` n ) M ( P ` n ) ) < ( x / ( sqrt ` ( # ` I ) ) ) <-> E. j e. ZZ A. k e. ( ZZ>= ` j ) ( ( ( F ` k ) ` n ) M ( P ` n ) ) < ( x / ( sqrt ` ( # ` I ) ) ) )
159 25 adantllr
 |-  ( ( ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) /\ n e. I ) /\ k e. NN ) -> ( ( F ` k ) ` n ) e. RR )
160 109 adantlr
 |-  ( ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) /\ n e. I ) -> ( P ` n ) e. RR )
161 160 adantr
 |-  ( ( ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) /\ n e. I ) /\ k e. NN ) -> ( P ` n ) e. RR )
162 2 remetdval
 |-  ( ( ( ( F ` k ) ` n ) e. RR /\ ( P ` n ) e. RR ) -> ( ( ( F ` k ) ` n ) M ( P ` n ) ) = ( abs ` ( ( ( F ` k ) ` n ) - ( P ` n ) ) ) )
163 159 161 162 syl2anc
 |-  ( ( ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) /\ n e. I ) /\ k e. NN ) -> ( ( ( F ` k ) ` n ) M ( P ` n ) ) = ( abs ` ( ( ( F ` k ) ` n ) - ( P ` n ) ) ) )
164 163 breq1d
 |-  ( ( ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) /\ n e. I ) /\ k e. NN ) -> ( ( ( ( F ` k ) ` n ) M ( P ` n ) ) < ( x / ( sqrt ` ( # ` I ) ) ) <-> ( abs ` ( ( ( F ` k ) ` n ) - ( P ` n ) ) ) < ( x / ( sqrt ` ( # ` I ) ) ) ) )
165 41 164 sylan2
 |-  ( ( ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) /\ n e. I ) /\ ( j e. NN /\ k e. ( ZZ>= ` j ) ) ) -> ( ( ( ( F ` k ) ` n ) M ( P ` n ) ) < ( x / ( sqrt ` ( # ` I ) ) ) <-> ( abs ` ( ( ( F ` k ) ` n ) - ( P ` n ) ) ) < ( x / ( sqrt ` ( # ` I ) ) ) ) )
166 165 anassrs
 |-  ( ( ( ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) /\ n e. I ) /\ j e. NN ) /\ k e. ( ZZ>= ` j ) ) -> ( ( ( ( F ` k ) ` n ) M ( P ` n ) ) < ( x / ( sqrt ` ( # ` I ) ) ) <-> ( abs ` ( ( ( F ` k ) ` n ) - ( P ` n ) ) ) < ( x / ( sqrt ` ( # ` I ) ) ) ) )
167 166 ralbidva
 |-  ( ( ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) /\ n e. I ) /\ j e. NN ) -> ( A. k e. ( ZZ>= ` j ) ( ( ( F ` k ) ` n ) M ( P ` n ) ) < ( x / ( sqrt ` ( # ` I ) ) ) <-> A. k e. ( ZZ>= ` j ) ( abs ` ( ( ( F ` k ) ` n ) - ( P ` n ) ) ) < ( x / ( sqrt ` ( # ` I ) ) ) ) )
168 167 rexbidva
 |-  ( ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) /\ n e. I ) -> ( E. j e. NN A. k e. ( ZZ>= ` j ) ( ( ( F ` k ) ` n ) M ( P ` n ) ) < ( x / ( sqrt ` ( # ` I ) ) ) <-> E. j e. NN A. k e. ( ZZ>= ` j ) ( abs ` ( ( ( F ` k ) ` n ) - ( P ` n ) ) ) < ( x / ( sqrt ` ( # ` I ) ) ) ) )
169 158 168 bitr3id
 |-  ( ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) /\ n e. I ) -> ( E. j e. ZZ A. k e. ( ZZ>= ` j ) ( ( ( F ` k ) ` n ) M ( P ` n ) ) < ( x / ( sqrt ` ( # ` I ) ) ) <-> E. j e. NN A. k e. ( ZZ>= ` j ) ( abs ` ( ( ( F ` k ) ` n ) - ( P ` n ) ) ) < ( x / ( sqrt ` ( # ` I ) ) ) ) )
170 155 169 mpbird
 |-  ( ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) /\ n e. I ) -> E. j e. ZZ A. k e. ( ZZ>= ` j ) ( ( ( F ` k ) ` n ) M ( P ` n ) ) < ( x / ( sqrt ` ( # ` I ) ) ) )
171 170 ralrimiva
 |-  ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) -> A. n e. I E. j e. ZZ A. k e. ( ZZ>= ` j ) ( ( ( F ` k ) ` n ) M ( P ` n ) ) < ( x / ( sqrt ` ( # ` I ) ) ) )
172 12 rexuz3
 |-  ( 1 e. ZZ -> ( E. j e. NN A. k e. ( ZZ>= ` j ) A. n e. I ( ( ( F ` k ) ` n ) M ( P ` n ) ) < ( x / ( sqrt ` ( # ` I ) ) ) <-> E. j e. ZZ A. k e. ( ZZ>= ` j ) A. n e. I ( ( ( F ` k ) ` n ) M ( P ` n ) ) < ( x / ( sqrt ` ( # ` I ) ) ) ) )
173 156 172 ax-mp
 |-  ( E. j e. NN A. k e. ( ZZ>= ` j ) A. n e. I ( ( ( F ` k ) ` n ) M ( P ` n ) ) < ( x / ( sqrt ` ( # ` I ) ) ) <-> E. j e. ZZ A. k e. ( ZZ>= ` j ) A. n e. I ( ( ( F ` k ) ` n ) M ( P ` n ) ) < ( x / ( sqrt ` ( # ` I ) ) ) )
174 rexfiuz
 |-  ( I e. Fin -> ( E. j e. ZZ A. k e. ( ZZ>= ` j ) A. n e. I ( ( ( F ` k ) ` n ) M ( P ` n ) ) < ( x / ( sqrt ` ( # ` I ) ) ) <-> A. n e. I E. j e. ZZ A. k e. ( ZZ>= ` j ) ( ( ( F ` k ) ` n ) M ( P ` n ) ) < ( x / ( sqrt ` ( # ` I ) ) ) ) )
175 145 174 syl
 |-  ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) -> ( E. j e. ZZ A. k e. ( ZZ>= ` j ) A. n e. I ( ( ( F ` k ) ` n ) M ( P ` n ) ) < ( x / ( sqrt ` ( # ` I ) ) ) <-> A. n e. I E. j e. ZZ A. k e. ( ZZ>= ` j ) ( ( ( F ` k ) ` n ) M ( P ` n ) ) < ( x / ( sqrt ` ( # ` I ) ) ) ) )
176 173 175 syl5bb
 |-  ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) -> ( E. j e. NN A. k e. ( ZZ>= ` j ) A. n e. I ( ( ( F ` k ) ` n ) M ( P ` n ) ) < ( x / ( sqrt ` ( # ` I ) ) ) <-> A. n e. I E. j e. ZZ A. k e. ( ZZ>= ` j ) ( ( ( F ` k ) ` n ) M ( P ` n ) ) < ( x / ( sqrt ` ( # ` I ) ) ) ) )
177 171 176 mpbird
 |-  ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) -> E. j e. NN A. k e. ( ZZ>= ` j ) A. n e. I ( ( ( F ` k ) ` n ) M ( P ` n ) ) < ( x / ( sqrt ` ( # ` I ) ) ) )
178 4 ad2antrr
 |-  ( ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) /\ k e. NN ) -> I e. Fin )
179 simplrr
 |-  ( ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) /\ k e. NN ) -> I =/= (/) )
180 eldifsn
 |-  ( I e. ( Fin \ { (/) } ) <-> ( I e. Fin /\ I =/= (/) ) )
181 178 179 180 sylanbrc
 |-  ( ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) /\ k e. NN ) -> I e. ( Fin \ { (/) } ) )
182 6 adantr
 |-  ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) -> F : NN --> X )
183 182 ffvelrnda
 |-  ( ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) /\ k e. NN ) -> ( F ` k ) e. X )
184 117 ad2antrr
 |-  ( ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) /\ k e. NN ) -> P e. X )
185 151 adantr
 |-  ( ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) /\ k e. NN ) -> ( x / ( sqrt ` ( # ` I ) ) ) e. RR+ )
186 1 2 rrndstprj2
 |-  ( ( ( I e. ( Fin \ { (/) } ) /\ ( F ` k ) e. X /\ P e. X ) /\ ( ( x / ( sqrt ` ( # ` I ) ) ) e. RR+ /\ A. n e. I ( ( ( F ` k ) ` n ) M ( P ` n ) ) < ( x / ( sqrt ` ( # ` I ) ) ) ) ) -> ( ( F ` k ) ( Rn ` I ) P ) < ( ( x / ( sqrt ` ( # ` I ) ) ) x. ( sqrt ` ( # ` I ) ) ) )
187 186 expr
 |-  ( ( ( I e. ( Fin \ { (/) } ) /\ ( F ` k ) e. X /\ P e. X ) /\ ( x / ( sqrt ` ( # ` I ) ) ) e. RR+ ) -> ( A. n e. I ( ( ( F ` k ) ` n ) M ( P ` n ) ) < ( x / ( sqrt ` ( # ` I ) ) ) -> ( ( F ` k ) ( Rn ` I ) P ) < ( ( x / ( sqrt ` ( # ` I ) ) ) x. ( sqrt ` ( # ` I ) ) ) ) )
188 181 183 184 185 187 syl31anc
 |-  ( ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) /\ k e. NN ) -> ( A. n e. I ( ( ( F ` k ) ` n ) M ( P ` n ) ) < ( x / ( sqrt ` ( # ` I ) ) ) -> ( ( F ` k ) ( Rn ` I ) P ) < ( ( x / ( sqrt ` ( # ` I ) ) ) x. ( sqrt ` ( # ` I ) ) ) ) )
189 simplrl
 |-  ( ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) /\ k e. NN ) -> x e. RR+ )
190 189 rpcnd
 |-  ( ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) /\ k e. NN ) -> x e. CC )
191 150 adantr
 |-  ( ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) /\ k e. NN ) -> ( sqrt ` ( # ` I ) ) e. RR+ )
192 191 rpcnd
 |-  ( ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) /\ k e. NN ) -> ( sqrt ` ( # ` I ) ) e. CC )
193 191 rpne0d
 |-  ( ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) /\ k e. NN ) -> ( sqrt ` ( # ` I ) ) =/= 0 )
194 190 192 193 divcan1d
 |-  ( ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) /\ k e. NN ) -> ( ( x / ( sqrt ` ( # ` I ) ) ) x. ( sqrt ` ( # ` I ) ) ) = x )
195 194 breq2d
 |-  ( ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) /\ k e. NN ) -> ( ( ( F ` k ) ( Rn ` I ) P ) < ( ( x / ( sqrt ` ( # ` I ) ) ) x. ( sqrt ` ( # ` I ) ) ) <-> ( ( F ` k ) ( Rn ` I ) P ) < x ) )
196 188 195 sylibd
 |-  ( ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) /\ k e. NN ) -> ( A. n e. I ( ( ( F ` k ) ` n ) M ( P ` n ) ) < ( x / ( sqrt ` ( # ` I ) ) ) -> ( ( F ` k ) ( Rn ` I ) P ) < x ) )
197 41 196 sylan2
 |-  ( ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) /\ ( j e. NN /\ k e. ( ZZ>= ` j ) ) ) -> ( A. n e. I ( ( ( F ` k ) ` n ) M ( P ` n ) ) < ( x / ( sqrt ` ( # ` I ) ) ) -> ( ( F ` k ) ( Rn ` I ) P ) < x ) )
198 197 anassrs
 |-  ( ( ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) /\ j e. NN ) /\ k e. ( ZZ>= ` j ) ) -> ( A. n e. I ( ( ( F ` k ) ` n ) M ( P ` n ) ) < ( x / ( sqrt ` ( # ` I ) ) ) -> ( ( F ` k ) ( Rn ` I ) P ) < x ) )
199 198 ralimdva
 |-  ( ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) /\ j e. NN ) -> ( A. k e. ( ZZ>= ` j ) A. n e. I ( ( ( F ` k ) ` n ) M ( P ` n ) ) < ( x / ( sqrt ` ( # ` I ) ) ) -> A. k e. ( ZZ>= ` j ) ( ( F ` k ) ( Rn ` I ) P ) < x ) )
200 199 reximdva
 |-  ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) -> ( E. j e. NN A. k e. ( ZZ>= ` j ) A. n e. I ( ( ( F ` k ) ` n ) M ( P ` n ) ) < ( x / ( sqrt ` ( # ` I ) ) ) -> E. j e. NN A. k e. ( ZZ>= ` j ) ( ( F ` k ) ( Rn ` I ) P ) < x ) )
201 177 200 mpd
 |-  ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) -> E. j e. NN A. k e. ( ZZ>= ` j ) ( ( F ` k ) ( Rn ` I ) P ) < x )
202 201 expr
 |-  ( ( ph /\ x e. RR+ ) -> ( I =/= (/) -> E. j e. NN A. k e. ( ZZ>= ` j ) ( ( F ` k ) ( Rn ` I ) P ) < x ) )
203 141 202 pm2.61dne
 |-  ( ( ph /\ x e. RR+ ) -> E. j e. NN A. k e. ( ZZ>= ` j ) ( ( F ` k ) ( Rn ` I ) P ) < x )
204 203 ralrimiva
 |-  ( ph -> A. x e. RR+ E. j e. NN A. k e. ( ZZ>= ` j ) ( ( F ` k ) ( Rn ` I ) P ) < x )
205 3 31 12 32 33 6 lmmbrf
 |-  ( ph -> ( F ( ~~>t ` J ) P <-> ( P e. X /\ A. x e. RR+ E. j e. NN A. k e. ( ZZ>= ` j ) ( ( F ` k ) ( Rn ` I ) P ) < x ) ) )
206 117 204 205 mpbir2and
 |-  ( ph -> F ( ~~>t ` J ) P )
207 releldm
 |-  ( ( Rel ( ~~>t ` J ) /\ F ( ~~>t ` J ) P ) -> F e. dom ( ~~>t ` J ) )
208 8 206 207 sylancr
 |-  ( ph -> F e. dom ( ~~>t ` J ) )