Metamath Proof Explorer

Theorem stoweidlem31

Description: This lemma is used to prove that there exists a function x as in the proof of Lemma 2 in BrosowskiDeutsh p. 91: assuming that R is a finite subset of V , x indexes a finite set of functions in the subalgebra (of the Stone Weierstrass theorem), such that for all i ranging in the finite indexing set, 0 ≤ x_i ≤ 1, x_i < ε / m on V(t_i), and x_i > 1 - ε / m on B . Here M is used to represent m in the paper, E is used to represent ε in the paper, v_i is used to represent V(t_i). (Contributed by Glauco Siliprandi, 20-Apr-2017)

Ref Expression
Hypotheses stoweidlem31.1 
|- F/ h ph
stoweidlem31.2 
|- F/ t ph
stoweidlem31.3 
|- F/ w ph
stoweidlem31.4 
|- Y = { h e. A | A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) }
stoweidlem31.5 
|- V = { w e. J | A. e e. RR+ E. h e. A ( A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) /\ A. t e. w ( h ` t ) < e /\ A. t e. ( T \ U ) ( 1 - e ) < ( h ` t ) ) }
stoweidlem31.6 
|- G = ( w e. R |-> { h e. A | ( A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) /\ A. t e. w ( h ` t ) < ( E / M ) /\ A. t e. ( T \ U ) ( 1 - ( E / M ) ) < ( h ` t ) ) } )
stoweidlem31.7 
|- ( ph -> R C_ V )
stoweidlem31.8 
|- ( ph -> M e. NN )
stoweidlem31.9 
|- ( ph -> v : ( 1 ... M ) -1-1-onto-> R )
stoweidlem31.10 
|- ( ph -> E e. RR+ )
stoweidlem31.11 
|- ( ph -> B C_ ( T \ U ) )
stoweidlem31.12 
|- ( ph -> V e. _V )
stoweidlem31.13 
|- ( ph -> A e. _V )
stoweidlem31.14 
|- ( ph -> ran G e. Fin )
Assertion stoweidlem31 
|- ( ph -> E. x ( x : ( 1 ... M ) --> Y /\ A. i e. ( 1 ... M ) ( A. t e. ( v ` i ) ( ( x ` i ) ` t ) < ( E / M ) /\ A. t e. B ( 1 - ( E / M ) ) < ( ( x ` i ) ` t ) ) ) )

Proof

Step Hyp Ref Expression
1 stoweidlem31.1 
 |-  F/ h ph
2 stoweidlem31.2 
 |-  F/ t ph
3 stoweidlem31.3 
 |-  F/ w ph
4 stoweidlem31.4 
 |-  Y = { h e. A | A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) }
5 stoweidlem31.5 
 |-  V = { w e. J | A. e e. RR+ E. h e. A ( A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) /\ A. t e. w ( h ` t ) < e /\ A. t e. ( T \ U ) ( 1 - e ) < ( h ` t ) ) }
6 stoweidlem31.6 
 |-  G = ( w e. R |-> { h e. A | ( A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) /\ A. t e. w ( h ` t ) < ( E / M ) /\ A. t e. ( T \ U ) ( 1 - ( E / M ) ) < ( h ` t ) ) } )
7 stoweidlem31.7 
 |-  ( ph -> R C_ V )
8 stoweidlem31.8 
 |-  ( ph -> M e. NN )
9 stoweidlem31.9 
 |-  ( ph -> v : ( 1 ... M ) -1-1-onto-> R )
10 stoweidlem31.10 
 |-  ( ph -> E e. RR+ )
11 stoweidlem31.11 
 |-  ( ph -> B C_ ( T \ U ) )
12 stoweidlem31.12 
 |-  ( ph -> V e. _V )
13 stoweidlem31.13 
 |-  ( ph -> A e. _V )
14 stoweidlem31.14 
 |-  ( ph -> ran G e. Fin )
15 fnchoice 
 |-  ( ran G e. Fin -> E. l ( l Fn ran G /\ A. b e. ran G ( b =/= (/) -> ( l ` b ) e. b ) ) )
16 14 15 syl 
 |-  ( ph -> E. l ( l Fn ran G /\ A. b e. ran G ( b =/= (/) -> ( l ` b ) e. b ) ) )
17 vex 
 |-  l e. _V
18 12 7 ssexd 
 |-  ( ph -> R e. _V )
19 mptexg 
 |-  ( R e. _V -> ( w e. R |-> { h e. A | ( A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) /\ A. t e. w ( h ` t ) < ( E / M ) /\ A. t e. ( T \ U ) ( 1 - ( E / M ) ) < ( h ` t ) ) } ) e. _V )
20 18 19 syl 
 |-  ( ph -> ( w e. R |-> { h e. A | ( A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) /\ A. t e. w ( h ` t ) < ( E / M ) /\ A. t e. ( T \ U ) ( 1 - ( E / M ) ) < ( h ` t ) ) } ) e. _V )
21 6 20 eqeltrid 
 |-  ( ph -> G e. _V )
22 vex 
 |-  v e. _V
23 coexg 
 |-  ( ( G e. _V /\ v e. _V ) -> ( G o. v ) e. _V )
24 21 22 23 sylancl 
 |-  ( ph -> ( G o. v ) e. _V )
25 coexg 
 |-  ( ( l e. _V /\ ( G o. v ) e. _V ) -> ( l o. ( G o. v ) ) e. _V )
26 17 24 25 sylancr 
 |-  ( ph -> ( l o. ( G o. v ) ) e. _V )
27 26 adantr 
 |-  ( ( ph /\ ( l Fn ran G /\ A. b e. ran G ( b =/= (/) -> ( l ` b ) e. b ) ) ) -> ( l o. ( G o. v ) ) e. _V )
28 simprl 
 |-  ( ( ph /\ ( l Fn ran G /\ A. b e. ran G ( b =/= (/) -> ( l ` b ) e. b ) ) ) -> l Fn ran G )
29 nfcv 
 |-  F/_ h l
30 nfcv 
 |-  F/_ h R
31 nfrab1 
 |-  F/_ h { h e. A | ( A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) /\ A. t e. w ( h ` t ) < ( E / M ) /\ A. t e. ( T \ U ) ( 1 - ( E / M ) ) < ( h ` t ) ) }
32 30 31 nfmpt 
 |-  F/_ h ( w e. R |-> { h e. A | ( A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) /\ A. t e. w ( h ` t ) < ( E / M ) /\ A. t e. ( T \ U ) ( 1 - ( E / M ) ) < ( h ` t ) ) } )
33 6 32 nfcxfr 
 |-  F/_ h G
34 33 nfrn 
 |-  F/_ h ran G
35 29 34 nffn 
 |-  F/ h l Fn ran G
36 nfv 
 |-  F/ h ( b =/= (/) -> ( l ` b ) e. b )
37 34 36 nfralw 
 |-  F/ h A. b e. ran G ( b =/= (/) -> ( l ` b ) e. b )
38 35 37 nfan 
 |-  F/ h ( l Fn ran G /\ A. b e. ran G ( b =/= (/) -> ( l ` b ) e. b ) )
39 1 38 nfan 
 |-  F/ h ( ph /\ ( l Fn ran G /\ A. b e. ran G ( b =/= (/) -> ( l ` b ) e. b ) ) )
40 fvelrnb 
 |-  ( l Fn ran G -> ( h e. ran l <-> E. b e. ran G ( l ` b ) = h ) )
41 28 40 syl 
 |-  ( ( ph /\ ( l Fn ran G /\ A. b e. ran G ( b =/= (/) -> ( l ` b ) e. b ) ) ) -> ( h e. ran l <-> E. b e. ran G ( l ` b ) = h ) )
42 41 biimpa 
 |-  ( ( ( ph /\ ( l Fn ran G /\ A. b e. ran G ( b =/= (/) -> ( l ` b ) e. b ) ) ) /\ h e. ran l ) -> E. b e. ran G ( l ` b ) = h )
43 nfv 
 |-  F/ b ph
44 nfv 
 |-  F/ b l Fn ran G
45 nfra1 
 |-  F/ b A. b e. ran G ( b =/= (/) -> ( l ` b ) e. b )
46 44 45 nfan 
 |-  F/ b ( l Fn ran G /\ A. b e. ran G ( b =/= (/) -> ( l ` b ) e. b ) )
47 43 46 nfan 
 |-  F/ b ( ph /\ ( l Fn ran G /\ A. b e. ran G ( b =/= (/) -> ( l ` b ) e. b ) ) )
48 nfv 
 |-  F/ b h e. ran l
49 47 48 nfan 
 |-  F/ b ( ( ph /\ ( l Fn ran G /\ A. b e. ran G ( b =/= (/) -> ( l ` b ) e. b ) ) ) /\ h e. ran l )
50 simp3 
 |-  ( ( ( ( ph /\ ( l Fn ran G /\ A. b e. ran G ( b =/= (/) -> ( l ` b ) e. b ) ) ) /\ h e. ran l ) /\ b e. ran G /\ ( l ` b ) = h ) -> ( l ` b ) = h )
51 simp1ll 
 |-  ( ( ( ( ph /\ ( l Fn ran G /\ A. b e. ran G ( b =/= (/) -> ( l ` b ) e. b ) ) ) /\ h e. ran l ) /\ b e. ran G /\ ( l ` b ) = h ) -> ph )
52 simplrr 
 |-  ( ( ( ph /\ ( l Fn ran G /\ A. b e. ran G ( b =/= (/) -> ( l ` b ) e. b ) ) ) /\ h e. ran l ) -> A. b e. ran G ( b =/= (/) -> ( l ` b ) e. b ) )
53 52 3ad2ant1 
 |-  ( ( ( ( ph /\ ( l Fn ran G /\ A. b e. ran G ( b =/= (/) -> ( l ` b ) e. b ) ) ) /\ h e. ran l ) /\ b e. ran G /\ ( l ` b ) = h ) -> A. b e. ran G ( b =/= (/) -> ( l ` b ) e. b ) )
54 simp2 
 |-  ( ( ( ( ph /\ ( l Fn ran G /\ A. b e. ran G ( b =/= (/) -> ( l ` b ) e. b ) ) ) /\ h e. ran l ) /\ b e. ran G /\ ( l ` b ) = h ) -> b e. ran G )
55 simp3 
 |-  ( ( ph /\ A. b e. ran G ( b =/= (/) -> ( l ` b ) e. b ) /\ b e. ran G ) -> b e. ran G )
56 3simpc 
 |-  ( ( ph /\ A. b e. ran G ( b =/= (/) -> ( l ` b ) e. b ) /\ b e. ran G ) -> ( A. b e. ran G ( b =/= (/) -> ( l ` b ) e. b ) /\ b e. ran G ) )
57 simpr 
 |-  ( ( ph /\ b e. ran G ) -> b e. ran G )
58 rabexg 
 |-  ( A e. _V -> { h e. A | ( A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) /\ A. t e. w ( h ` t ) < ( E / M ) /\ A. t e. ( T \ U ) ( 1 - ( E / M ) ) < ( h ` t ) ) } e. _V )
59 13 58 syl 
 |-  ( ph -> { h e. A | ( A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) /\ A. t e. w ( h ` t ) < ( E / M ) /\ A. t e. ( T \ U ) ( 1 - ( E / M ) ) < ( h ` t ) ) } e. _V )
60 59 a1d 
 |-  ( ph -> ( w e. R -> { h e. A | ( A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) /\ A. t e. w ( h ` t ) < ( E / M ) /\ A. t e. ( T \ U ) ( 1 - ( E / M ) ) < ( h ` t ) ) } e. _V ) )
61 3 60 ralrimi 
 |-  ( ph -> A. w e. R { h e. A | ( A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) /\ A. t e. w ( h ` t ) < ( E / M ) /\ A. t e. ( T \ U ) ( 1 - ( E / M ) ) < ( h ` t ) ) } e. _V )
62 6 fnmpt 
 |-  ( A. w e. R { h e. A | ( A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) /\ A. t e. w ( h ` t ) < ( E / M ) /\ A. t e. ( T \ U ) ( 1 - ( E / M ) ) < ( h ` t ) ) } e. _V -> G Fn R )
63 61 62 syl 
 |-  ( ph -> G Fn R )
64 63 adantr 
 |-  ( ( ph /\ b e. ran G ) -> G Fn R )
65 fvelrnb 
 |-  ( G Fn R -> ( b e. ran G <-> E. u e. R ( G ` u ) = b ) )
66 nfmpt1 
 |-  F/_ w ( w e. R |-> { h e. A | ( A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) /\ A. t e. w ( h ` t ) < ( E / M ) /\ A. t e. ( T \ U ) ( 1 - ( E / M ) ) < ( h ` t ) ) } )
67 6 66 nfcxfr 
 |-  F/_ w G
68 nfcv 
 |-  F/_ w u
69 67 68 nffv 
 |-  F/_ w ( G ` u )
70 nfcv 
 |-  F/_ w b
71 69 70 nfeq 
 |-  F/ w ( G ` u ) = b
72 nfv 
 |-  F/ u ( G ` w ) = b
73 fveq2 
 |-  ( u = w -> ( G ` u ) = ( G ` w ) )
74 73 eqeq1d 
 |-  ( u = w -> ( ( G ` u ) = b <-> ( G ` w ) = b ) )
75 71 72 74 cbvrexw 
 |-  ( E. u e. R ( G ` u ) = b <-> E. w e. R ( G ` w ) = b )
76 65 75 bitrdi 
 |-  ( G Fn R -> ( b e. ran G <-> E. w e. R ( G ` w ) = b ) )
77 64 76 syl 
 |-  ( ( ph /\ b e. ran G ) -> ( b e. ran G <-> E. w e. R ( G ` w ) = b ) )
78 57 77 mpbid 
 |-  ( ( ph /\ b e. ran G ) -> E. w e. R ( G ` w ) = b )
79 67 nfrn 
 |-  F/_ w ran G
80 79 nfcri 
 |-  F/ w b e. ran G
81 3 80 nfan 
 |-  F/ w ( ph /\ b e. ran G )
82 nfv 
 |-  F/ w b =/= (/)
83 simp3 
 |-  ( ( ph /\ w e. R /\ ( G ` w ) = b ) -> ( G ` w ) = b )
84 simpr 
 |-  ( ( ph /\ w e. R ) -> w e. R )
85 13 adantr 
 |-  ( ( ph /\ w e. R ) -> A e. _V )
86 85 58 syl 
 |-  ( ( ph /\ w e. R ) -> { h e. A | ( A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) /\ A. t e. w ( h ` t ) < ( E / M ) /\ A. t e. ( T \ U ) ( 1 - ( E / M ) ) < ( h ` t ) ) } e. _V )
87 6 fvmpt2 
 |-  ( ( w e. R /\ { h e. A | ( A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) /\ A. t e. w ( h ` t ) < ( E / M ) /\ A. t e. ( T \ U ) ( 1 - ( E / M ) ) < ( h ` t ) ) } e. _V ) -> ( G ` w ) = { h e. A | ( A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) /\ A. t e. w ( h ` t ) < ( E / M ) /\ A. t e. ( T \ U ) ( 1 - ( E / M ) ) < ( h ` t ) ) } )
88 84 86 87 syl2anc 
 |-  ( ( ph /\ w e. R ) -> ( G ` w ) = { h e. A | ( A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) /\ A. t e. w ( h ` t ) < ( E / M ) /\ A. t e. ( T \ U ) ( 1 - ( E / M ) ) < ( h ` t ) ) } )
89 7 sselda 
 |-  ( ( ph /\ w e. R ) -> w e. V )
90 5 rabeq2i 
 |-  ( w e. V <-> ( w e. J /\ A. e e. RR+ E. h e. A ( A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) /\ A. t e. w ( h ` t ) < e /\ A. t e. ( T \ U ) ( 1 - e ) < ( h ` t ) ) ) )
91 89 90 sylib 
 |-  ( ( ph /\ w e. R ) -> ( w e. J /\ A. e e. RR+ E. h e. A ( A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) /\ A. t e. w ( h ` t ) < e /\ A. t e. ( T \ U ) ( 1 - e ) < ( h ` t ) ) ) )
92 91 simprd 
 |-  ( ( ph /\ w e. R ) -> A. e e. RR+ E. h e. A ( A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) /\ A. t e. w ( h ` t ) < e /\ A. t e. ( T \ U ) ( 1 - e ) < ( h ` t ) ) )
93 8 nnrpd 
 |-  ( ph -> M e. RR+ )
94 10 93 rpdivcld 
 |-  ( ph -> ( E / M ) e. RR+ )
95 94 adantr 
 |-  ( ( ph /\ w e. R ) -> ( E / M ) e. RR+ )
96 breq2 
 |-  ( e = ( E / M ) -> ( ( h ` t ) < e <-> ( h ` t ) < ( E / M ) ) )
97 96 ralbidv 
 |-  ( e = ( E / M ) -> ( A. t e. w ( h ` t ) < e <-> A. t e. w ( h ` t ) < ( E / M ) ) )
98 oveq2 
 |-  ( e = ( E / M ) -> ( 1 - e ) = ( 1 - ( E / M ) ) )
99 98 breq1d 
 |-  ( e = ( E / M ) -> ( ( 1 - e ) < ( h ` t ) <-> ( 1 - ( E / M ) ) < ( h ` t ) ) )
100 99 ralbidv 
 |-  ( e = ( E / M ) -> ( A. t e. ( T \ U ) ( 1 - e ) < ( h ` t ) <-> A. t e. ( T \ U ) ( 1 - ( E / M ) ) < ( h ` t ) ) )
101 97 100 3anbi23d 
 |-  ( e = ( E / M ) -> ( ( A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) /\ A. t e. w ( h ` t ) < e /\ A. t e. ( T \ U ) ( 1 - e ) < ( h ` t ) ) <-> ( A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) /\ A. t e. w ( h ` t ) < ( E / M ) /\ A. t e. ( T \ U ) ( 1 - ( E / M ) ) < ( h ` t ) ) ) )
102 101 rexbidv 
 |-  ( e = ( E / M ) -> ( E. h e. A ( A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) /\ A. t e. w ( h ` t ) < e /\ A. t e. ( T \ U ) ( 1 - e ) < ( h ` t ) ) <-> E. h e. A ( A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) /\ A. t e. w ( h ` t ) < ( E / M ) /\ A. t e. ( T \ U ) ( 1 - ( E / M ) ) < ( h ` t ) ) ) )
103 102 rspccva 
 |-  ( ( A. e e. RR+ E. h e. A ( A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) /\ A. t e. w ( h ` t ) < e /\ A. t e. ( T \ U ) ( 1 - e ) < ( h ` t ) ) /\ ( E / M ) e. RR+ ) -> E. h e. A ( A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) /\ A. t e. w ( h ` t ) < ( E / M ) /\ A. t e. ( T \ U ) ( 1 - ( E / M ) ) < ( h ` t ) ) )
104 92 95 103 syl2anc 
 |-  ( ( ph /\ w e. R ) -> E. h e. A ( A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) /\ A. t e. w ( h ` t ) < ( E / M ) /\ A. t e. ( T \ U ) ( 1 - ( E / M ) ) < ( h ` t ) ) )
105 nfv 
 |-  F/ h w e. R
106 1 105 nfan 
 |-  F/ h ( ph /\ w e. R )
107 nfcv 
 |-  F/_ h (/)
108 31 107 nfne 
 |-  F/ h { h e. A | ( A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) /\ A. t e. w ( h ` t ) < ( E / M ) /\ A. t e. ( T \ U ) ( 1 - ( E / M ) ) < ( h ` t ) ) } =/= (/)
109 3simpc 
 |-  ( ( ( ph /\ w e. R ) /\ h e. A /\ ( A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) /\ A. t e. w ( h ` t ) < ( E / M ) /\ A. t e. ( T \ U ) ( 1 - ( E / M ) ) < ( h ` t ) ) ) -> ( h e. A /\ ( A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) /\ A. t e. w ( h ` t ) < ( E / M ) /\ A. t e. ( T \ U ) ( 1 - ( E / M ) ) < ( h ` t ) ) ) )
110 rabid 
 |-  ( h e. { h e. A | ( A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) /\ A. t e. w ( h ` t ) < ( E / M ) /\ A. t e. ( T \ U ) ( 1 - ( E / M ) ) < ( h ` t ) ) } <-> ( h e. A /\ ( A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) /\ A. t e. w ( h ` t ) < ( E / M ) /\ A. t e. ( T \ U ) ( 1 - ( E / M ) ) < ( h ` t ) ) ) )
111 109 110 sylibr 
 |-  ( ( ( ph /\ w e. R ) /\ h e. A /\ ( A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) /\ A. t e. w ( h ` t ) < ( E / M ) /\ A. t e. ( T \ U ) ( 1 - ( E / M ) ) < ( h ` t ) ) ) -> h e. { h e. A | ( A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) /\ A. t e. w ( h ` t ) < ( E / M ) /\ A. t e. ( T \ U ) ( 1 - ( E / M ) ) < ( h ` t ) ) } )
112 ne0i 
 |-  ( h e. { h e. A | ( A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) /\ A. t e. w ( h ` t ) < ( E / M ) /\ A. t e. ( T \ U ) ( 1 - ( E / M ) ) < ( h ` t ) ) } -> { h e. A | ( A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) /\ A. t e. w ( h ` t ) < ( E / M ) /\ A. t e. ( T \ U ) ( 1 - ( E / M ) ) < ( h ` t ) ) } =/= (/) )
113 111 112 syl 
 |-  ( ( ( ph /\ w e. R ) /\ h e. A /\ ( A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) /\ A. t e. w ( h ` t ) < ( E / M ) /\ A. t e. ( T \ U ) ( 1 - ( E / M ) ) < ( h ` t ) ) ) -> { h e. A | ( A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) /\ A. t e. w ( h ` t ) < ( E / M ) /\ A. t e. ( T \ U ) ( 1 - ( E / M ) ) < ( h ` t ) ) } =/= (/) )
114 113 3exp 
 |-  ( ( ph /\ w e. R ) -> ( h e. A -> ( ( A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) /\ A. t e. w ( h ` t ) < ( E / M ) /\ A. t e. ( T \ U ) ( 1 - ( E / M ) ) < ( h ` t ) ) -> { h e. A | ( A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) /\ A. t e. w ( h ` t ) < ( E / M ) /\ A. t e. ( T \ U ) ( 1 - ( E / M ) ) < ( h ` t ) ) } =/= (/) ) ) )
115 106 108 114 rexlimd 
 |-  ( ( ph /\ w e. R ) -> ( E. h e. A ( A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) /\ A. t e. w ( h ` t ) < ( E / M ) /\ A. t e. ( T \ U ) ( 1 - ( E / M ) ) < ( h ` t ) ) -> { h e. A | ( A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) /\ A. t e. w ( h ` t ) < ( E / M ) /\ A. t e. ( T \ U ) ( 1 - ( E / M ) ) < ( h ` t ) ) } =/= (/) ) )
116 104 115 mpd 
 |-  ( ( ph /\ w e. R ) -> { h e. A | ( A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) /\ A. t e. w ( h ` t ) < ( E / M ) /\ A. t e. ( T \ U ) ( 1 - ( E / M ) ) < ( h ` t ) ) } =/= (/) )
117 88 116 eqnetrd 
 |-  ( ( ph /\ w e. R ) -> ( G ` w ) =/= (/) )
118 117 3adant3 
 |-  ( ( ph /\ w e. R /\ ( G ` w ) = b ) -> ( G ` w ) =/= (/) )
119 83 118 eqnetrrd 
 |-  ( ( ph /\ w e. R /\ ( G ` w ) = b ) -> b =/= (/) )
120 119 3adant1r 
 |-  ( ( ( ph /\ b e. ran G ) /\ w e. R /\ ( G ` w ) = b ) -> b =/= (/) )
121 120 3exp 
 |-  ( ( ph /\ b e. ran G ) -> ( w e. R -> ( ( G ` w ) = b -> b =/= (/) ) ) )
122 81 82 121 rexlimd 
 |-  ( ( ph /\ b e. ran G ) -> ( E. w e. R ( G ` w ) = b -> b =/= (/) ) )
123 78 122 mpd 
 |-  ( ( ph /\ b e. ran G ) -> b =/= (/) )
124 123 3adant2 
 |-  ( ( ph /\ A. b e. ran G ( b =/= (/) -> ( l ` b ) e. b ) /\ b e. ran G ) -> b =/= (/) )
125 rspa 
 |-  ( ( A. b e. ran G ( b =/= (/) -> ( l ` b ) e. b ) /\ b e. ran G ) -> ( b =/= (/) -> ( l ` b ) e. b ) )
126 56 124 125 sylc 
 |-  ( ( ph /\ A. b e. ran G ( b =/= (/) -> ( l ` b ) e. b ) /\ b e. ran G ) -> ( l ` b ) e. b )
127 55 126 jca 
 |-  ( ( ph /\ A. b e. ran G ( b =/= (/) -> ( l ` b ) e. b ) /\ b e. ran G ) -> ( b e. ran G /\ ( l ` b ) e. b ) )
128 vex 
 |-  b e. _V
129 6 elrnmpt 
 |-  ( b e. _V -> ( b e. ran G <-> E. w e. R b = { h e. A | ( A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) /\ A. t e. w ( h ` t ) < ( E / M ) /\ A. t e. ( T \ U ) ( 1 - ( E / M ) ) < ( h ` t ) ) } ) )
130 128 129 ax-mp 
 |-  ( b e. ran G <-> E. w e. R b = { h e. A | ( A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) /\ A. t e. w ( h ` t ) < ( E / M ) /\ A. t e. ( T \ U ) ( 1 - ( E / M ) ) < ( h ` t ) ) } )
131 55 130 sylib 
 |-  ( ( ph /\ A. b e. ran G ( b =/= (/) -> ( l ` b ) e. b ) /\ b e. ran G ) -> E. w e. R b = { h e. A | ( A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) /\ A. t e. w ( h ` t ) < ( E / M ) /\ A. t e. ( T \ U ) ( 1 - ( E / M ) ) < ( h ` t ) ) } )
132 nfv 
 |-  F/ w ( l ` b ) e. b
133 80 132 nfan 
 |-  F/ w ( b e. ran G /\ ( l ` b ) e. b )
134 nfv 
 |-  F/ w ( l ` b ) e. Y
135 simp1r 
 |-  ( ( ( b e. ran G /\ ( l ` b ) e. b ) /\ w e. R /\ b = { h e. A | ( A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) /\ A. t e. w ( h ` t ) < ( E / M ) /\ A. t e. ( T \ U ) ( 1 - ( E / M ) ) < ( h ` t ) ) } ) -> ( l ` b ) e. b )
136 simp3 
 |-  ( ( ( b e. ran G /\ ( l ` b ) e. b ) /\ w e. R /\ b = { h e. A | ( A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) /\ A. t e. w ( h ` t ) < ( E / M ) /\ A. t e. ( T \ U ) ( 1 - ( E / M ) ) < ( h ` t ) ) } ) -> b = { h e. A | ( A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) /\ A. t e. w ( h ` t ) < ( E / M ) /\ A. t e. ( T \ U ) ( 1 - ( E / M ) ) < ( h ` t ) ) } )
137 simpl 
 |-  ( ( ( l ` b ) e. b /\ b = { h e. A | ( A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) /\ A. t e. w ( h ` t ) < ( E / M ) /\ A. t e. ( T \ U ) ( 1 - ( E / M ) ) < ( h ` t ) ) } ) -> ( l ` b ) e. b )
138 simpr 
 |-  ( ( ( l ` b ) e. b /\ b = { h e. A | ( A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) /\ A. t e. w ( h ` t ) < ( E / M ) /\ A. t e. ( T \ U ) ( 1 - ( E / M ) ) < ( h ` t ) ) } ) -> b = { h e. A | ( A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) /\ A. t e. w ( h ` t ) < ( E / M ) /\ A. t e. ( T \ U ) ( 1 - ( E / M ) ) < ( h ` t ) ) } )
139 137 138 eleqtrd 
 |-  ( ( ( l ` b ) e. b /\ b = { h e. A | ( A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) /\ A. t e. w ( h ` t ) < ( E / M ) /\ A. t e. ( T \ U ) ( 1 - ( E / M ) ) < ( h ` t ) ) } ) -> ( l ` b ) e. { h e. A | ( A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) /\ A. t e. w ( h ` t ) < ( E / M ) /\ A. t e. ( T \ U ) ( 1 - ( E / M ) ) < ( h ` t ) ) } )
140 elrabi 
 |-  ( ( l ` b ) e. { h e. A | ( A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) /\ A. t e. w ( h ` t ) < ( E / M ) /\ A. t e. ( T \ U ) ( 1 - ( E / M ) ) < ( h ` t ) ) } -> ( l ` b ) e. A )
141 fveq1 
 |-  ( h = ( l ` b ) -> ( h ` t ) = ( ( l ` b ) ` t ) )
142 141 breq2d 
 |-  ( h = ( l ` b ) -> ( 0 <_ ( h ` t ) <-> 0 <_ ( ( l ` b ) ` t ) ) )
143 141 breq1d 
 |-  ( h = ( l ` b ) -> ( ( h ` t ) <_ 1 <-> ( ( l ` b ) ` t ) <_ 1 ) )
144 142 143 anbi12d 
 |-  ( h = ( l ` b ) -> ( ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) <-> ( 0 <_ ( ( l ` b ) ` t ) /\ ( ( l ` b ) ` t ) <_ 1 ) ) )
145 144 ralbidv 
 |-  ( h = ( l ` b ) -> ( A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) <-> A. t e. T ( 0 <_ ( ( l ` b ) ` t ) /\ ( ( l ` b ) ` t ) <_ 1 ) ) )
146 141 breq1d 
 |-  ( h = ( l ` b ) -> ( ( h ` t ) < ( E / M ) <-> ( ( l ` b ) ` t ) < ( E / M ) ) )
147 146 ralbidv 
 |-  ( h = ( l ` b ) -> ( A. t e. w ( h ` t ) < ( E / M ) <-> A. t e. w ( ( l ` b ) ` t ) < ( E / M ) ) )
148 141 breq2d 
 |-  ( h = ( l ` b ) -> ( ( 1 - ( E / M ) ) < ( h ` t ) <-> ( 1 - ( E / M ) ) < ( ( l ` b ) ` t ) ) )
149 148 ralbidv 
 |-  ( h = ( l ` b ) -> ( A. t e. ( T \ U ) ( 1 - ( E / M ) ) < ( h ` t ) <-> A. t e. ( T \ U ) ( 1 - ( E / M ) ) < ( ( l ` b ) ` t ) ) )
150 145 147 149 3anbi123d 
 |-  ( h = ( l ` b ) -> ( ( A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) /\ A. t e. w ( h ` t ) < ( E / M ) /\ A. t e. ( T \ U ) ( 1 - ( E / M ) ) < ( h ` t ) ) <-> ( A. t e. T ( 0 <_ ( ( l ` b ) ` t ) /\ ( ( l ` b ) ` t ) <_ 1 ) /\ A. t e. w ( ( l ` b ) ` t ) < ( E / M ) /\ A. t e. ( T \ U ) ( 1 - ( E / M ) ) < ( ( l ` b ) ` t ) ) ) )
151 150 elrab 
 |-  ( ( l ` b ) e. { h e. A | ( A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) /\ A. t e. w ( h ` t ) < ( E / M ) /\ A. t e. ( T \ U ) ( 1 - ( E / M ) ) < ( h ` t ) ) } <-> ( ( l ` b ) e. A /\ ( A. t e. T ( 0 <_ ( ( l ` b ) ` t ) /\ ( ( l ` b ) ` t ) <_ 1 ) /\ A. t e. w ( ( l ` b ) ` t ) < ( E / M ) /\ A. t e. ( T \ U ) ( 1 - ( E / M ) ) < ( ( l ` b ) ` t ) ) ) )
152 151 simprbi 
 |-  ( ( l ` b ) e. { h e. A | ( A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) /\ A. t e. w ( h ` t ) < ( E / M ) /\ A. t e. ( T \ U ) ( 1 - ( E / M ) ) < ( h ` t ) ) } -> ( A. t e. T ( 0 <_ ( ( l ` b ) ` t ) /\ ( ( l ` b ) ` t ) <_ 1 ) /\ A. t e. w ( ( l ` b ) ` t ) < ( E / M ) /\ A. t e. ( T \ U ) ( 1 - ( E / M ) ) < ( ( l ` b ) ` t ) ) )
153 152 simp1d 
 |-  ( ( l ` b ) e. { h e. A | ( A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) /\ A. t e. w ( h ` t ) < ( E / M ) /\ A. t e. ( T \ U ) ( 1 - ( E / M ) ) < ( h ` t ) ) } -> A. t e. T ( 0 <_ ( ( l ` b ) ` t ) /\ ( ( l ` b ) ` t ) <_ 1 ) )
154 145 elrab 
 |-  ( ( l ` b ) e. { h e. A | A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) } <-> ( ( l ` b ) e. A /\ A. t e. T ( 0 <_ ( ( l ` b ) ` t ) /\ ( ( l ` b ) ` t ) <_ 1 ) ) )
155 140 153 154 sylanbrc 
 |-  ( ( l ` b ) e. { h e. A | ( A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) /\ A. t e. w ( h ` t ) < ( E / M ) /\ A. t e. ( T \ U ) ( 1 - ( E / M ) ) < ( h ` t ) ) } -> ( l ` b ) e. { h e. A | A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) } )
156 139 155 syl 
 |-  ( ( ( l ` b ) e. b /\ b = { h e. A | ( A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) /\ A. t e. w ( h ` t ) < ( E / M ) /\ A. t e. ( T \ U ) ( 1 - ( E / M ) ) < ( h ` t ) ) } ) -> ( l ` b ) e. { h e. A | A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) } )
157 156 4 eleqtrrdi 
 |-  ( ( ( l ` b ) e. b /\ b = { h e. A | ( A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) /\ A. t e. w ( h ` t ) < ( E / M ) /\ A. t e. ( T \ U ) ( 1 - ( E / M ) ) < ( h ` t ) ) } ) -> ( l ` b ) e. Y )
158 135 136 157 syl2anc 
 |-  ( ( ( b e. ran G /\ ( l ` b ) e. b ) /\ w e. R /\ b = { h e. A | ( A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) /\ A. t e. w ( h ` t ) < ( E / M ) /\ A. t e. ( T \ U ) ( 1 - ( E / M ) ) < ( h ` t ) ) } ) -> ( l ` b ) e. Y )
159 158 3exp 
 |-  ( ( b e. ran G /\ ( l ` b ) e. b ) -> ( w e. R -> ( b = { h e. A | ( A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) /\ A. t e. w ( h ` t ) < ( E / M ) /\ A. t e. ( T \ U ) ( 1 - ( E / M ) ) < ( h ` t ) ) } -> ( l ` b ) e. Y ) ) )
160 133 134 159 rexlimd 
 |-  ( ( b e. ran G /\ ( l ` b ) e. b ) -> ( E. w e. R b = { h e. A | ( A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) /\ A. t e. w ( h ` t ) < ( E / M ) /\ A. t e. ( T \ U ) ( 1 - ( E / M ) ) < ( h ` t ) ) } -> ( l ` b ) e. Y ) )
161 127 131 160 sylc 
 |-  ( ( ph /\ A. b e. ran G ( b =/= (/) -> ( l ` b ) e. b ) /\ b e. ran G ) -> ( l ` b ) e. Y )
162 51 53 54 161 syl3anc 
 |-  ( ( ( ( ph /\ ( l Fn ran G /\ A. b e. ran G ( b =/= (/) -> ( l ` b ) e. b ) ) ) /\ h e. ran l ) /\ b e. ran G /\ ( l ` b ) = h ) -> ( l ` b ) e. Y )
163 50 162 eqeltrrd 
 |-  ( ( ( ( ph /\ ( l Fn ran G /\ A. b e. ran G ( b =/= (/) -> ( l ` b ) e. b ) ) ) /\ h e. ran l ) /\ b e. ran G /\ ( l ` b ) = h ) -> h e. Y )
164 163 3exp 
 |-  ( ( ( ph /\ ( l Fn ran G /\ A. b e. ran G ( b =/= (/) -> ( l ` b ) e. b ) ) ) /\ h e. ran l ) -> ( b e. ran G -> ( ( l ` b ) = h -> h e. Y ) ) )
165 49 164 reximdai 
 |-  ( ( ( ph /\ ( l Fn ran G /\ A. b e. ran G ( b =/= (/) -> ( l ` b ) e. b ) ) ) /\ h e. ran l ) -> ( E. b e. ran G ( l ` b ) = h -> E. b e. ran G h e. Y ) )
166 42 165 mpd 
 |-  ( ( ( ph /\ ( l Fn ran G /\ A. b e. ran G ( b =/= (/) -> ( l ` b ) e. b ) ) ) /\ h e. ran l ) -> E. b e. ran G h e. Y )
167 nfv 
 |-  F/ b h e. Y
168 idd 
 |-  ( b e. ran G -> ( h e. Y -> h e. Y ) )
169 168 a1i 
 |-  ( ( ( ph /\ ( l Fn ran G /\ A. b e. ran G ( b =/= (/) -> ( l ` b ) e. b ) ) ) /\ h e. ran l ) -> ( b e. ran G -> ( h e. Y -> h e. Y ) ) )
170 49 167 169 rexlimd 
 |-  ( ( ( ph /\ ( l Fn ran G /\ A. b e. ran G ( b =/= (/) -> ( l ` b ) e. b ) ) ) /\ h e. ran l ) -> ( E. b e. ran G h e. Y -> h e. Y ) )
171 166 170 mpd 
 |-  ( ( ( ph /\ ( l Fn ran G /\ A. b e. ran G ( b =/= (/) -> ( l ` b ) e. b ) ) ) /\ h e. ran l ) -> h e. Y )
172 171 ex 
 |-  ( ( ph /\ ( l Fn ran G /\ A. b e. ran G ( b =/= (/) -> ( l ` b ) e. b ) ) ) -> ( h e. ran l -> h e. Y ) )
173 39 172 ralrimi 
 |-  ( ( ph /\ ( l Fn ran G /\ A. b e. ran G ( b =/= (/) -> ( l ` b ) e. b ) ) ) -> A. h e. ran l h e. Y )
174 dfss3 
 |-  ( ran l C_ Y <-> A. z e. ran l z e. Y )
175 nfrab1 
 |-  F/_ h { h e. A | A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) }
176 4 175 nfcxfr 
 |-  F/_ h Y
177 176 nfcri 
 |-  F/ h z e. Y
178 nfv 
 |-  F/ z h e. Y
179 eleq1 
 |-  ( z = h -> ( z e. Y <-> h e. Y ) )
180 177 178 179 cbvralw 
 |-  ( A. z e. ran l z e. Y <-> A. h e. ran l h e. Y )
181 174 180 bitri 
 |-  ( ran l C_ Y <-> A. h e. ran l h e. Y )
182 173 181 sylibr 
 |-  ( ( ph /\ ( l Fn ran G /\ A. b e. ran G ( b =/= (/) -> ( l ` b ) e. b ) ) ) -> ran l C_ Y )
183 df-f 
 |-  ( l : ran G --> Y <-> ( l Fn ran G /\ ran l C_ Y ) )
184 28 182 183 sylanbrc 
 |-  ( ( ph /\ ( l Fn ran G /\ A. b e. ran G ( b =/= (/) -> ( l ` b ) e. b ) ) ) -> l : ran G --> Y )
185 dffn3 
 |-  ( G Fn R <-> G : R --> ran G )
186 63 185 sylib 
 |-  ( ph -> G : R --> ran G )
187 186 adantr 
 |-  ( ( ph /\ ( l Fn ran G /\ A. b e. ran G ( b =/= (/) -> ( l ` b ) e. b ) ) ) -> G : R --> ran G )
188 f1of 
 |-  ( v : ( 1 ... M ) -1-1-onto-> R -> v : ( 1 ... M ) --> R )
189 9 188 syl 
 |-  ( ph -> v : ( 1 ... M ) --> R )
190 189 adantr 
 |-  ( ( ph /\ ( l Fn ran G /\ A. b e. ran G ( b =/= (/) -> ( l ` b ) e. b ) ) ) -> v : ( 1 ... M ) --> R )
191 fco 
 |-  ( ( G : R --> ran G /\ v : ( 1 ... M ) --> R ) -> ( G o. v ) : ( 1 ... M ) --> ran G )
192 187 190 191 syl2anc 
 |-  ( ( ph /\ ( l Fn ran G /\ A. b e. ran G ( b =/= (/) -> ( l ` b ) e. b ) ) ) -> ( G o. v ) : ( 1 ... M ) --> ran G )
193 fco 
 |-  ( ( l : ran G --> Y /\ ( G o. v ) : ( 1 ... M ) --> ran G ) -> ( l o. ( G o. v ) ) : ( 1 ... M ) --> Y )
194 184 192 193 syl2anc 
 |-  ( ( ph /\ ( l Fn ran G /\ A. b e. ran G ( b =/= (/) -> ( l ` b ) e. b ) ) ) -> ( l o. ( G o. v ) ) : ( 1 ... M ) --> Y )
195 fvco3 
 |-  ( ( ( G o. v ) : ( 1 ... M ) --> ran G /\ i e. ( 1 ... M ) ) -> ( ( l o. ( G o. v ) ) ` i ) = ( l ` ( ( G o. v ) ` i ) ) )
196 192 195 sylan 
 |-  ( ( ( ph /\ ( l Fn ran G /\ A. b e. ran G ( b =/= (/) -> ( l ` b ) e. b ) ) ) /\ i e. ( 1 ... M ) ) -> ( ( l o. ( G o. v ) ) ` i ) = ( l ` ( ( G o. v ) ` i ) ) )
197 simpll 
 |-  ( ( ( ph /\ ( l Fn ran G /\ A. b e. ran G ( b =/= (/) -> ( l ` b ) e. b ) ) ) /\ i e. ( 1 ... M ) ) -> ph )
198 simplrr 
 |-  ( ( ( ph /\ ( l Fn ran G /\ A. b e. ran G ( b =/= (/) -> ( l ` b ) e. b ) ) ) /\ i e. ( 1 ... M ) ) -> A. b e. ran G ( b =/= (/) -> ( l ` b ) e. b ) )
199 192 ffvelrnda 
 |-  ( ( ( ph /\ ( l Fn ran G /\ A. b e. ran G ( b =/= (/) -> ( l ` b ) e. b ) ) ) /\ i e. ( 1 ... M ) ) -> ( ( G o. v ) ` i ) e. ran G )
200 simp3 
 |-  ( ( ph /\ A. b e. ran G ( b =/= (/) -> ( l ` b ) e. b ) /\ ( ( G o. v ) ` i ) e. ran G ) -> ( ( G o. v ) ` i ) e. ran G )
201 nfv 
 |-  F/ b ( ( G o. v ) ` i ) e. ran G
202 43 45 201 nf3an 
 |-  F/ b ( ph /\ A. b e. ran G ( b =/= (/) -> ( l ` b ) e. b ) /\ ( ( G o. v ) ` i ) e. ran G )
203 nfv 
 |-  F/ b ( l ` ( ( G o. v ) ` i ) ) e. ( ( G o. v ) ` i )
204 202 203 nfim 
 |-  F/ b ( ( ph /\ A. b e. ran G ( b =/= (/) -> ( l ` b ) e. b ) /\ ( ( G o. v ) ` i ) e. ran G ) -> ( l ` ( ( G o. v ) ` i ) ) e. ( ( G o. v ) ` i ) )
205 eleq1 
 |-  ( b = ( ( G o. v ) ` i ) -> ( b e. ran G <-> ( ( G o. v ) ` i ) e. ran G ) )
206 205 3anbi3d 
 |-  ( b = ( ( G o. v ) ` i ) -> ( ( ph /\ A. b e. ran G ( b =/= (/) -> ( l ` b ) e. b ) /\ b e. ran G ) <-> ( ph /\ A. b e. ran G ( b =/= (/) -> ( l ` b ) e. b ) /\ ( ( G o. v ) ` i ) e. ran G ) ) )
207 fveq2 
 |-  ( b = ( ( G o. v ) ` i ) -> ( l ` b ) = ( l ` ( ( G o. v ) ` i ) ) )
208 id 
 |-  ( b = ( ( G o. v ) ` i ) -> b = ( ( G o. v ) ` i ) )
209 207 208 eleq12d 
 |-  ( b = ( ( G o. v ) ` i ) -> ( ( l ` b ) e. b <-> ( l ` ( ( G o. v ) ` i ) ) e. ( ( G o. v ) ` i ) ) )
210 206 209 imbi12d 
 |-  ( b = ( ( G o. v ) ` i ) -> ( ( ( ph /\ A. b e. ran G ( b =/= (/) -> ( l ` b ) e. b ) /\ b e. ran G ) -> ( l ` b ) e. b ) <-> ( ( ph /\ A. b e. ran G ( b =/= (/) -> ( l ` b ) e. b ) /\ ( ( G o. v ) ` i ) e. ran G ) -> ( l ` ( ( G o. v ) ` i ) ) e. ( ( G o. v ) ` i ) ) ) )
211 204 210 126 vtoclg1f 
 |-  ( ( ( G o. v ) ` i ) e. ran G -> ( ( ph /\ A. b e. ran G ( b =/= (/) -> ( l ` b ) e. b ) /\ ( ( G o. v ) ` i ) e. ran G ) -> ( l ` ( ( G o. v ) ` i ) ) e. ( ( G o. v ) ` i ) ) )
212 200 211 mpcom 
 |-  ( ( ph /\ A. b e. ran G ( b =/= (/) -> ( l ` b ) e. b ) /\ ( ( G o. v ) ` i ) e. ran G ) -> ( l ` ( ( G o. v ) ` i ) ) e. ( ( G o. v ) ` i ) )
213 197 198 199 212 syl3anc 
 |-  ( ( ( ph /\ ( l Fn ran G /\ A. b e. ran G ( b =/= (/) -> ( l ` b ) e. b ) ) ) /\ i e. ( 1 ... M ) ) -> ( l ` ( ( G o. v ) ` i ) ) e. ( ( G o. v ) ` i ) )
214 196 213 eqeltrd 
 |-  ( ( ( ph /\ ( l Fn ran G /\ A. b e. ran G ( b =/= (/) -> ( l ` b ) e. b ) ) ) /\ i e. ( 1 ... M ) ) -> ( ( l o. ( G o. v ) ) ` i ) e. ( ( G o. v ) ` i ) )
215 fvco3 
 |-  ( ( v : ( 1 ... M ) --> R /\ i e. ( 1 ... M ) ) -> ( ( G o. v ) ` i ) = ( G ` ( v ` i ) ) )
216 189 215 sylan 
 |-  ( ( ph /\ i e. ( 1 ... M ) ) -> ( ( G o. v ) ` i ) = ( G ` ( v ` i ) ) )
217 raleq 
 |-  ( w = ( v ` i ) -> ( A. t e. w ( h ` t ) < ( E / M ) <-> A. t e. ( v ` i ) ( h ` t ) < ( E / M ) ) )
218 217 3anbi2d 
 |-  ( w = ( v ` i ) -> ( ( A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) /\ A. t e. w ( h ` t ) < ( E / M ) /\ A. t e. ( T \ U ) ( 1 - ( E / M ) ) < ( h ` t ) ) <-> ( A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) /\ A. t e. ( v ` i ) ( h ` t ) < ( E / M ) /\ A. t e. ( T \ U ) ( 1 - ( E / M ) ) < ( h ` t ) ) ) )
219 218 rabbidv 
 |-  ( w = ( v ` i ) -> { h e. A | ( A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) /\ A. t e. w ( h ` t ) < ( E / M ) /\ A. t e. ( T \ U ) ( 1 - ( E / M ) ) < ( h ` t ) ) } = { h e. A | ( A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) /\ A. t e. ( v ` i ) ( h ` t ) < ( E / M ) /\ A. t e. ( T \ U ) ( 1 - ( E / M ) ) < ( h ` t ) ) } )
220 189 ffvelrnda 
 |-  ( ( ph /\ i e. ( 1 ... M ) ) -> ( v ` i ) e. R )
221 13 adantr 
 |-  ( ( ph /\ i e. ( 1 ... M ) ) -> A e. _V )
222 rabexg 
 |-  ( A e. _V -> { h e. A | ( A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) /\ A. t e. ( v ` i ) ( h ` t ) < ( E / M ) /\ A. t e. ( T \ U ) ( 1 - ( E / M ) ) < ( h ` t ) ) } e. _V )
223 221 222 syl 
 |-  ( ( ph /\ i e. ( 1 ... M ) ) -> { h e. A | ( A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) /\ A. t e. ( v ` i ) ( h ` t ) < ( E / M ) /\ A. t e. ( T \ U ) ( 1 - ( E / M ) ) < ( h ` t ) ) } e. _V )
224 6 219 220 223 fvmptd3 
 |-  ( ( ph /\ i e. ( 1 ... M ) ) -> ( G ` ( v ` i ) ) = { h e. A | ( A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) /\ A. t e. ( v ` i ) ( h ` t ) < ( E / M ) /\ A. t e. ( T \ U ) ( 1 - ( E / M ) ) < ( h ` t ) ) } )
225 216 224 eqtrd 
 |-  ( ( ph /\ i e. ( 1 ... M ) ) -> ( ( G o. v ) ` i ) = { h e. A | ( A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) /\ A. t e. ( v ` i ) ( h ` t ) < ( E / M ) /\ A. t e. ( T \ U ) ( 1 - ( E / M ) ) < ( h ` t ) ) } )
226 225 adantlr 
 |-  ( ( ( ph /\ ( l Fn ran G /\ A. b e. ran G ( b =/= (/) -> ( l ` b ) e. b ) ) ) /\ i e. ( 1 ... M ) ) -> ( ( G o. v ) ` i ) = { h e. A | ( A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) /\ A. t e. ( v ` i ) ( h ` t ) < ( E / M ) /\ A. t e. ( T \ U ) ( 1 - ( E / M ) ) < ( h ` t ) ) } )
227 226 eleq2d 
 |-  ( ( ( ph /\ ( l Fn ran G /\ A. b e. ran G ( b =/= (/) -> ( l ` b ) e. b ) ) ) /\ i e. ( 1 ... M ) ) -> ( ( ( l o. ( G o. v ) ) ` i ) e. ( ( G o. v ) ` i ) <-> ( ( l o. ( G o. v ) ) ` i ) e. { h e. A | ( A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) /\ A. t e. ( v ` i ) ( h ` t ) < ( E / M ) /\ A. t e. ( T \ U ) ( 1 - ( E / M ) ) < ( h ` t ) ) } ) )
228 nfcv 
 |-  F/_ h v
229 33 228 nfco 
 |-  F/_ h ( G o. v )
230 29 229 nfco 
 |-  F/_ h ( l o. ( G o. v ) )
231 nfcv 
 |-  F/_ h i
232 230 231 nffv 
 |-  F/_ h ( ( l o. ( G o. v ) ) ` i )
233 nfcv 
 |-  F/_ h A
234 nfcv 
 |-  F/_ h T
235 nfcv 
 |-  F/_ h 0
236 nfcv 
 |-  F/_ h <_
237 nfcv 
 |-  F/_ h t
238 232 237 nffv 
 |-  F/_ h ( ( ( l o. ( G o. v ) ) ` i ) ` t )
239 235 236 238 nfbr 
 |-  F/ h 0 <_ ( ( ( l o. ( G o. v ) ) ` i ) ` t )
240 nfcv 
 |-  F/_ h 1
241 238 236 240 nfbr 
 |-  F/ h ( ( ( l o. ( G o. v ) ) ` i ) ` t ) <_ 1
242 239 241 nfan 
 |-  F/ h ( 0 <_ ( ( ( l o. ( G o. v ) ) ` i ) ` t ) /\ ( ( ( l o. ( G o. v ) ) ` i ) ` t ) <_ 1 )
243 234 242 nfralw 
 |-  F/ h A. t e. T ( 0 <_ ( ( ( l o. ( G o. v ) ) ` i ) ` t ) /\ ( ( ( l o. ( G o. v ) ) ` i ) ` t ) <_ 1 )
244 nfcv 
 |-  F/_ h ( v ` i )
245 nfcv 
 |-  F/_ h <
246 nfcv 
 |-  F/_ h ( E / M )
247 238 245 246 nfbr 
 |-  F/ h ( ( ( l o. ( G o. v ) ) ` i ) ` t ) < ( E / M )
248 244 247 nfralw 
 |-  F/ h A. t e. ( v ` i ) ( ( ( l o. ( G o. v ) ) ` i ) ` t ) < ( E / M )
249 nfcv 
 |-  F/_ h ( T \ U )
250 nfcv 
 |-  F/_ h ( 1 - ( E / M ) )
251 250 245 238 nfbr 
 |-  F/ h ( 1 - ( E / M ) ) < ( ( ( l o. ( G o. v ) ) ` i ) ` t )
252 249 251 nfralw 
 |-  F/ h A. t e. ( T \ U ) ( 1 - ( E / M ) ) < ( ( ( l o. ( G o. v ) ) ` i ) ` t )
253 243 248 252 nf3an 
 |-  F/ h ( A. t e. T ( 0 <_ ( ( ( l o. ( G o. v ) ) ` i ) ` t ) /\ ( ( ( l o. ( G o. v ) ) ` i ) ` t ) <_ 1 ) /\ A. t e. ( v ` i ) ( ( ( l o. ( G o. v ) ) ` i ) ` t ) < ( E / M ) /\ A. t e. ( T \ U ) ( 1 - ( E / M ) ) < ( ( ( l o. ( G o. v ) ) ` i ) ` t ) )
254 nfcv 
 |-  F/_ t h
255 nfcv 
 |-  F/_ t l
256 nfcv 
 |-  F/_ t R
257 nfra1 
 |-  F/ t A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 )
258 nfra1 
 |-  F/ t A. t e. w ( h ` t ) < ( E / M )
259 nfra1 
 |-  F/ t A. t e. ( T \ U ) ( 1 - ( E / M ) ) < ( h ` t )
260 257 258 259 nf3an 
 |-  F/ t ( A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) /\ A. t e. w ( h ` t ) < ( E / M ) /\ A. t e. ( T \ U ) ( 1 - ( E / M ) ) < ( h ` t ) )
261 nfcv 
 |-  F/_ t A
262 260 261 nfrabw 
 |-  F/_ t { h e. A | ( A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) /\ A. t e. w ( h ` t ) < ( E / M ) /\ A. t e. ( T \ U ) ( 1 - ( E / M ) ) < ( h ` t ) ) }
263 256 262 nfmpt 
 |-  F/_ t ( w e. R |-> { h e. A | ( A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) /\ A. t e. w ( h ` t ) < ( E / M ) /\ A. t e. ( T \ U ) ( 1 - ( E / M ) ) < ( h ` t ) ) } )
264 6 263 nfcxfr 
 |-  F/_ t G
265 nfcv 
 |-  F/_ t v
266 264 265 nfco 
 |-  F/_ t ( G o. v )
267 255 266 nfco 
 |-  F/_ t ( l o. ( G o. v ) )
268 nfcv 
 |-  F/_ t i
269 267 268 nffv 
 |-  F/_ t ( ( l o. ( G o. v ) ) ` i )
270 254 269 nfeq 
 |-  F/ t h = ( ( l o. ( G o. v ) ) ` i )
271 fveq1 
 |-  ( h = ( ( l o. ( G o. v ) ) ` i ) -> ( h ` t ) = ( ( ( l o. ( G o. v ) ) ` i ) ` t ) )
272 271 breq2d 
 |-  ( h = ( ( l o. ( G o. v ) ) ` i ) -> ( 0 <_ ( h ` t ) <-> 0 <_ ( ( ( l o. ( G o. v ) ) ` i ) ` t ) ) )
273 271 breq1d 
 |-  ( h = ( ( l o. ( G o. v ) ) ` i ) -> ( ( h ` t ) <_ 1 <-> ( ( ( l o. ( G o. v ) ) ` i ) ` t ) <_ 1 ) )
274 272 273 anbi12d 
 |-  ( h = ( ( l o. ( G o. v ) ) ` i ) -> ( ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) <-> ( 0 <_ ( ( ( l o. ( G o. v ) ) ` i ) ` t ) /\ ( ( ( l o. ( G o. v ) ) ` i ) ` t ) <_ 1 ) ) )
275 270 274 ralbid 
 |-  ( h = ( ( l o. ( G o. v ) ) ` i ) -> ( A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) <-> A. t e. T ( 0 <_ ( ( ( l o. ( G o. v ) ) ` i ) ` t ) /\ ( ( ( l o. ( G o. v ) ) ` i ) ` t ) <_ 1 ) ) )
276 271 breq1d 
 |-  ( h = ( ( l o. ( G o. v ) ) ` i ) -> ( ( h ` t ) < ( E / M ) <-> ( ( ( l o. ( G o. v ) ) ` i ) ` t ) < ( E / M ) ) )
277 270 276 ralbid 
 |-  ( h = ( ( l o. ( G o. v ) ) ` i ) -> ( A. t e. ( v ` i ) ( h ` t ) < ( E / M ) <-> A. t e. ( v ` i ) ( ( ( l o. ( G o. v ) ) ` i ) ` t ) < ( E / M ) ) )
278 271 breq2d 
 |-  ( h = ( ( l o. ( G o. v ) ) ` i ) -> ( ( 1 - ( E / M ) ) < ( h ` t ) <-> ( 1 - ( E / M ) ) < ( ( ( l o. ( G o. v ) ) ` i ) ` t ) ) )
279 270 278 ralbid 
 |-  ( h = ( ( l o. ( G o. v ) ) ` i ) -> ( A. t e. ( T \ U ) ( 1 - ( E / M ) ) < ( h ` t ) <-> A. t e. ( T \ U ) ( 1 - ( E / M ) ) < ( ( ( l o. ( G o. v ) ) ` i ) ` t ) ) )
280 275 277 279 3anbi123d 
 |-  ( h = ( ( l o. ( G o. v ) ) ` i ) -> ( ( A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) /\ A. t e. ( v ` i ) ( h ` t ) < ( E / M ) /\ A. t e. ( T \ U ) ( 1 - ( E / M ) ) < ( h ` t ) ) <-> ( A. t e. T ( 0 <_ ( ( ( l o. ( G o. v ) ) ` i ) ` t ) /\ ( ( ( l o. ( G o. v ) ) ` i ) ` t ) <_ 1 ) /\ A. t e. ( v ` i ) ( ( ( l o. ( G o. v ) ) ` i ) ` t ) < ( E / M ) /\ A. t e. ( T \ U ) ( 1 - ( E / M ) ) < ( ( ( l o. ( G o. v ) ) ` i ) ` t ) ) ) )
281 232 233 253 280 elrabf 
 |-  ( ( ( l o. ( G o. v ) ) ` i ) e. { h e. A | ( A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) /\ A. t e. ( v ` i ) ( h ` t ) < ( E / M ) /\ A. t e. ( T \ U ) ( 1 - ( E / M ) ) < ( h ` t ) ) } <-> ( ( ( l o. ( G o. v ) ) ` i ) e. A /\ ( A. t e. T ( 0 <_ ( ( ( l o. ( G o. v ) ) ` i ) ` t ) /\ ( ( ( l o. ( G o. v ) ) ` i ) ` t ) <_ 1 ) /\ A. t e. ( v ` i ) ( ( ( l o. ( G o. v ) ) ` i ) ` t ) < ( E / M ) /\ A. t e. ( T \ U ) ( 1 - ( E / M ) ) < ( ( ( l o. ( G o. v ) ) ` i ) ` t ) ) ) )
282 281 simprbi 
 |-  ( ( ( l o. ( G o. v ) ) ` i ) e. { h e. A | ( A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) /\ A. t e. ( v ` i ) ( h ` t ) < ( E / M ) /\ A. t e. ( T \ U ) ( 1 - ( E / M ) ) < ( h ` t ) ) } -> ( A. t e. T ( 0 <_ ( ( ( l o. ( G o. v ) ) ` i ) ` t ) /\ ( ( ( l o. ( G o. v ) ) ` i ) ` t ) <_ 1 ) /\ A. t e. ( v ` i ) ( ( ( l o. ( G o. v ) ) ` i ) ` t ) < ( E / M ) /\ A. t e. ( T \ U ) ( 1 - ( E / M ) ) < ( ( ( l o. ( G o. v ) ) ` i ) ` t ) ) )
283 282 simp2d 
 |-  ( ( ( l o. ( G o. v ) ) ` i ) e. { h e. A | ( A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) /\ A. t e. ( v ` i ) ( h ` t ) < ( E / M ) /\ A. t e. ( T \ U ) ( 1 - ( E / M ) ) < ( h ` t ) ) } -> A. t e. ( v ` i ) ( ( ( l o. ( G o. v ) ) ` i ) ` t ) < ( E / M ) )
284 227 283 syl6bi 
 |-  ( ( ( ph /\ ( l Fn ran G /\ A. b e. ran G ( b =/= (/) -> ( l ` b ) e. b ) ) ) /\ i e. ( 1 ... M ) ) -> ( ( ( l o. ( G o. v ) ) ` i ) e. ( ( G o. v ) ` i ) -> A. t e. ( v ` i ) ( ( ( l o. ( G o. v ) ) ` i ) ` t ) < ( E / M ) ) )
285 214 284 mpd 
 |-  ( ( ( ph /\ ( l Fn ran G /\ A. b e. ran G ( b =/= (/) -> ( l ` b ) e. b ) ) ) /\ i e. ( 1 ... M ) ) -> A. t e. ( v ` i ) ( ( ( l o. ( G o. v ) ) ` i ) ` t ) < ( E / M ) )
286 264 nfrn 
 |-  F/_ t ran G
287 255 286 nffn 
 |-  F/ t l Fn ran G
288 nfv 
 |-  F/ t ( b =/= (/) -> ( l ` b ) e. b )
289 286 288 nfralw 
 |-  F/ t A. b e. ran G ( b =/= (/) -> ( l ` b ) e. b )
290 287 289 nfan 
 |-  F/ t ( l Fn ran G /\ A. b e. ran G ( b =/= (/) -> ( l ` b ) e. b ) )
291 2 290 nfan 
 |-  F/ t ( ph /\ ( l Fn ran G /\ A. b e. ran G ( b =/= (/) -> ( l ` b ) e. b ) ) )
292 nfv 
 |-  F/ t i e. ( 1 ... M )
293 291 292 nfan 
 |-  F/ t ( ( ph /\ ( l Fn ran G /\ A. b e. ran G ( b =/= (/) -> ( l ` b ) e. b ) ) ) /\ i e. ( 1 ... M ) )
294 11 ad3antrrr 
 |-  ( ( ( ( ph /\ ( l Fn ran G /\ A. b e. ran G ( b =/= (/) -> ( l ` b ) e. b ) ) ) /\ i e. ( 1 ... M ) ) /\ t e. B ) -> B C_ ( T \ U ) )
295 simpr 
 |-  ( ( ( ( ph /\ ( l Fn ran G /\ A. b e. ran G ( b =/= (/) -> ( l ` b ) e. b ) ) ) /\ i e. ( 1 ... M ) ) /\ t e. B ) -> t e. B )
296 294 295 sseldd 
 |-  ( ( ( ( ph /\ ( l Fn ran G /\ A. b e. ran G ( b =/= (/) -> ( l ` b ) e. b ) ) ) /\ i e. ( 1 ... M ) ) /\ t e. B ) -> t e. ( T \ U ) )
297 282 simp3d 
 |-  ( ( ( l o. ( G o. v ) ) ` i ) e. { h e. A | ( A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) /\ A. t e. ( v ` i ) ( h ` t ) < ( E / M ) /\ A. t e. ( T \ U ) ( 1 - ( E / M ) ) < ( h ` t ) ) } -> A. t e. ( T \ U ) ( 1 - ( E / M ) ) < ( ( ( l o. ( G o. v ) ) ` i ) ` t ) )
298 227 297 syl6bi 
 |-  ( ( ( ph /\ ( l Fn ran G /\ A. b e. ran G ( b =/= (/) -> ( l ` b ) e. b ) ) ) /\ i e. ( 1 ... M ) ) -> ( ( ( l o. ( G o. v ) ) ` i ) e. ( ( G o. v ) ` i ) -> A. t e. ( T \ U ) ( 1 - ( E / M ) ) < ( ( ( l o. ( G o. v ) ) ` i ) ` t ) ) )
299 214 298 mpd 
 |-  ( ( ( ph /\ ( l Fn ran G /\ A. b e. ran G ( b =/= (/) -> ( l ` b ) e. b ) ) ) /\ i e. ( 1 ... M ) ) -> A. t e. ( T \ U ) ( 1 - ( E / M ) ) < ( ( ( l o. ( G o. v ) ) ` i ) ` t ) )
300 299 r19.21bi 
 |-  ( ( ( ( ph /\ ( l Fn ran G /\ A. b e. ran G ( b =/= (/) -> ( l ` b ) e. b ) ) ) /\ i e. ( 1 ... M ) ) /\ t e. ( T \ U ) ) -> ( 1 - ( E / M ) ) < ( ( ( l o. ( G o. v ) ) ` i ) ` t ) )
301 296 300 syldan 
 |-  ( ( ( ( ph /\ ( l Fn ran G /\ A. b e. ran G ( b =/= (/) -> ( l ` b ) e. b ) ) ) /\ i e. ( 1 ... M ) ) /\ t e. B ) -> ( 1 - ( E / M ) ) < ( ( ( l o. ( G o. v ) ) ` i ) ` t ) )
302 301 ex 
 |-  ( ( ( ph /\ ( l Fn ran G /\ A. b e. ran G ( b =/= (/) -> ( l ` b ) e. b ) ) ) /\ i e. ( 1 ... M ) ) -> ( t e. B -> ( 1 - ( E / M ) ) < ( ( ( l o. ( G o. v ) ) ` i ) ` t ) ) )
303 293 302 ralrimi 
 |-  ( ( ( ph /\ ( l Fn ran G /\ A. b e. ran G ( b =/= (/) -> ( l ` b ) e. b ) ) ) /\ i e. ( 1 ... M ) ) -> A. t e. B ( 1 - ( E / M ) ) < ( ( ( l o. ( G o. v ) ) ` i ) ` t ) )
304 285 303 jca 
 |-  ( ( ( ph /\ ( l Fn ran G /\ A. b e. ran G ( b =/= (/) -> ( l ` b ) e. b ) ) ) /\ i e. ( 1 ... M ) ) -> ( A. t e. ( v ` i ) ( ( ( l o. ( G o. v ) ) ` i ) ` t ) < ( E / M ) /\ A. t e. B ( 1 - ( E / M ) ) < ( ( ( l o. ( G o. v ) ) ` i ) ` t ) ) )
305 304 ralrimiva 
 |-  ( ( ph /\ ( l Fn ran G /\ A. b e. ran G ( b =/= (/) -> ( l ` b ) e. b ) ) ) -> A. i e. ( 1 ... M ) ( A. t e. ( v ` i ) ( ( ( l o. ( G o. v ) ) ` i ) ` t ) < ( E / M ) /\ A. t e. B ( 1 - ( E / M ) ) < ( ( ( l o. ( G o. v ) ) ` i ) ` t ) ) )
306 194 305 jca 
 |-  ( ( ph /\ ( l Fn ran G /\ A. b e. ran G ( b =/= (/) -> ( l ` b ) e. b ) ) ) -> ( ( l o. ( G o. v ) ) : ( 1 ... M ) --> Y /\ A. i e. ( 1 ... M ) ( A. t e. ( v ` i ) ( ( ( l o. ( G o. v ) ) ` i ) ` t ) < ( E / M ) /\ A. t e. B ( 1 - ( E / M ) ) < ( ( ( l o. ( G o. v ) ) ` i ) ` t ) ) ) )
307 feq1 
 |-  ( x = ( l o. ( G o. v ) ) -> ( x : ( 1 ... M ) --> Y <-> ( l o. ( G o. v ) ) : ( 1 ... M ) --> Y ) )
308 nfcv 
 |-  F/_ t x
309 308 267 nfeq 
 |-  F/ t x = ( l o. ( G o. v ) )
310 fveq1 
 |-  ( x = ( l o. ( G o. v ) ) -> ( x ` i ) = ( ( l o. ( G o. v ) ) ` i ) )
311 310 fveq1d 
 |-  ( x = ( l o. ( G o. v ) ) -> ( ( x ` i ) ` t ) = ( ( ( l o. ( G o. v ) ) ` i ) ` t ) )
312 311 breq1d 
 |-  ( x = ( l o. ( G o. v ) ) -> ( ( ( x ` i ) ` t ) < ( E / M ) <-> ( ( ( l o. ( G o. v ) ) ` i ) ` t ) < ( E / M ) ) )
313 309 312 ralbid 
 |-  ( x = ( l o. ( G o. v ) ) -> ( A. t e. ( v ` i ) ( ( x ` i ) ` t ) < ( E / M ) <-> A. t e. ( v ` i ) ( ( ( l o. ( G o. v ) ) ` i ) ` t ) < ( E / M ) ) )
314 311 breq2d 
 |-  ( x = ( l o. ( G o. v ) ) -> ( ( 1 - ( E / M ) ) < ( ( x ` i ) ` t ) <-> ( 1 - ( E / M ) ) < ( ( ( l o. ( G o. v ) ) ` i ) ` t ) ) )
315 309 314 ralbid 
 |-  ( x = ( l o. ( G o. v ) ) -> ( A. t e. B ( 1 - ( E / M ) ) < ( ( x ` i ) ` t ) <-> A. t e. B ( 1 - ( E / M ) ) < ( ( ( l o. ( G o. v ) ) ` i ) ` t ) ) )
316 313 315 anbi12d 
 |-  ( x = ( l o. ( G o. v ) ) -> ( ( A. t e. ( v ` i ) ( ( x ` i ) ` t ) < ( E / M ) /\ A. t e. B ( 1 - ( E / M ) ) < ( ( x ` i ) ` t ) ) <-> ( A. t e. ( v ` i ) ( ( ( l o. ( G o. v ) ) ` i ) ` t ) < ( E / M ) /\ A. t e. B ( 1 - ( E / M ) ) < ( ( ( l o. ( G o. v ) ) ` i ) ` t ) ) ) )
317 316 ralbidv 
 |-  ( x = ( l o. ( G o. v ) ) -> ( A. i e. ( 1 ... M ) ( A. t e. ( v ` i ) ( ( x ` i ) ` t ) < ( E / M ) /\ A. t e. B ( 1 - ( E / M ) ) < ( ( x ` i ) ` t ) ) <-> A. i e. ( 1 ... M ) ( A. t e. ( v ` i ) ( ( ( l o. ( G o. v ) ) ` i ) ` t ) < ( E / M ) /\ A. t e. B ( 1 - ( E / M ) ) < ( ( ( l o. ( G o. v ) ) ` i ) ` t ) ) ) )
318 307 317 anbi12d 
 |-  ( x = ( l o. ( G o. v ) ) -> ( ( x : ( 1 ... M ) --> Y /\ A. i e. ( 1 ... M ) ( A. t e. ( v ` i ) ( ( x ` i ) ` t ) < ( E / M ) /\ A. t e. B ( 1 - ( E / M ) ) < ( ( x ` i ) ` t ) ) ) <-> ( ( l o. ( G o. v ) ) : ( 1 ... M ) --> Y /\ A. i e. ( 1 ... M ) ( A. t e. ( v ` i ) ( ( ( l o. ( G o. v ) ) ` i ) ` t ) < ( E / M ) /\ A. t e. B ( 1 - ( E / M ) ) < ( ( ( l o. ( G o. v ) ) ` i ) ` t ) ) ) ) )
319 318 spcegv 
 |-  ( ( l o. ( G o. v ) ) e. _V -> ( ( ( l o. ( G o. v ) ) : ( 1 ... M ) --> Y /\ A. i e. ( 1 ... M ) ( A. t e. ( v ` i ) ( ( ( l o. ( G o. v ) ) ` i ) ` t ) < ( E / M ) /\ A. t e. B ( 1 - ( E / M ) ) < ( ( ( l o. ( G o. v ) ) ` i ) ` t ) ) ) -> E. x ( x : ( 1 ... M ) --> Y /\ A. i e. ( 1 ... M ) ( A. t e. ( v ` i ) ( ( x ` i ) ` t ) < ( E / M ) /\ A. t e. B ( 1 - ( E / M ) ) < ( ( x ` i ) ` t ) ) ) ) )
320 27 306 319 sylc 
 |-  ( ( ph /\ ( l Fn ran G /\ A. b e. ran G ( b =/= (/) -> ( l ` b ) e. b ) ) ) -> E. x ( x : ( 1 ... M ) --> Y /\ A. i e. ( 1 ... M ) ( A. t e. ( v ` i ) ( ( x ` i ) ` t ) < ( E / M ) /\ A. t e. B ( 1 - ( E / M ) ) < ( ( x ` i ) ` t ) ) ) )
321 16 320 exlimddv 
 |-  ( ph -> E. x ( x : ( 1 ... M ) --> Y /\ A. i e. ( 1 ... M ) ( A. t e. ( v ` i ) ( ( x ` i ) ` t ) < ( E / M ) /\ A. t e. B ( 1 - ( E / M ) ) < ( ( x ` i ) ` t ) ) ) )