Metamath Proof Explorer

Theorem stoweidlem35

Description: This lemma is used to prove the existence of a function p as in Lemma 1 of BrosowskiDeutsh p. 90: p is in the subalgebra, such that 0 <= p <= 1, p__(t_0) = 0, and p > 0 on T - U. Here ( qi ) is used to represent p__(t_i) in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017)

Ref Expression
Hypotheses stoweidlem35.1 
|- F/ t ph
stoweidlem35.2 
|- F/ w ph
stoweidlem35.3 
|- F/ h ph
stoweidlem35.4 
|- Q = { h e. A | ( ( h ` Z ) = 0 /\ A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) ) }
stoweidlem35.5 
|- W = { w e. J | E. h e. Q w = { t e. T | 0 < ( h ` t ) } }
stoweidlem35.6 
|- G = ( w e. X |-> { h e. Q | w = { t e. T | 0 < ( h ` t ) } } )
stoweidlem35.7 
|- ( ph -> A e. _V )
stoweidlem35.8 
|- ( ph -> X e. Fin )
stoweidlem35.9 
|- ( ph -> X C_ W )
stoweidlem35.10 
|- ( ph -> ( T \ U ) C_ U. X )
stoweidlem35.11 
|- ( ph -> ( T \ U ) =/= (/) )
Assertion stoweidlem35 
|- ( ph -> E. m E. q ( m e. NN /\ ( q : ( 1 ... m ) --> Q /\ A. t e. ( T \ U ) E. i e. ( 1 ... m ) 0 < ( ( q ` i ) ` t ) ) ) )

Proof

Step Hyp Ref Expression
1 stoweidlem35.1 
 |-  F/ t ph
2 stoweidlem35.2 
 |-  F/ w ph
3 stoweidlem35.3 
 |-  F/ h ph
4 stoweidlem35.4 
 |-  Q = { h e. A | ( ( h ` Z ) = 0 /\ A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) ) }
5 stoweidlem35.5 
 |-  W = { w e. J | E. h e. Q w = { t e. T | 0 < ( h ` t ) } }
6 stoweidlem35.6 
 |-  G = ( w e. X |-> { h e. Q | w = { t e. T | 0 < ( h ` t ) } } )
7 stoweidlem35.7 
 |-  ( ph -> A e. _V )
8 stoweidlem35.8 
 |-  ( ph -> X e. Fin )
9 stoweidlem35.9 
 |-  ( ph -> X C_ W )
10 stoweidlem35.10 
 |-  ( ph -> ( T \ U ) C_ U. X )
11 stoweidlem35.11 
 |-  ( ph -> ( T \ U ) =/= (/) )
12 6 rnmptfi 
 |-  ( X e. Fin -> ran G e. Fin )
13 8 12 syl 
 |-  ( ph -> ran G e. Fin )
14 fnchoice 
 |-  ( ran G e. Fin -> E. g ( g Fn ran G /\ A. l e. ran G ( l =/= (/) -> ( g ` l ) e. l ) ) )
15 14 adantl 
 |-  ( ( ph /\ ran G e. Fin ) -> E. g ( g Fn ran G /\ A. l e. ran G ( l =/= (/) -> ( g ` l ) e. l ) ) )
16 simprl 
 |-  ( ( ph /\ ( g Fn ran G /\ A. l e. ran G ( l =/= (/) -> ( g ` l ) e. l ) ) ) -> g Fn ran G )
17 nfmpt1 
 |-  F/_ w ( w e. X |-> { h e. Q | w = { t e. T | 0 < ( h ` t ) } } )
18 6 17 nfcxfr 
 |-  F/_ w G
19 18 nfrn 
 |-  F/_ w ran G
20 19 nfcri 
 |-  F/ w k e. ran G
21 2 20 nfan 
 |-  F/ w ( ph /\ k e. ran G )
22 9 sselda 
 |-  ( ( ph /\ w e. X ) -> w e. W )
23 22 5 eleqtrdi 
 |-  ( ( ph /\ w e. X ) -> w e. { w e. J | E. h e. Q w = { t e. T | 0 < ( h ` t ) } } )
24 rabid 
 |-  ( w e. { w e. J | E. h e. Q w = { t e. T | 0 < ( h ` t ) } } <-> ( w e. J /\ E. h e. Q w = { t e. T | 0 < ( h ` t ) } ) )
25 23 24 sylib 
 |-  ( ( ph /\ w e. X ) -> ( w e. J /\ E. h e. Q w = { t e. T | 0 < ( h ` t ) } ) )
26 25 simprd 
 |-  ( ( ph /\ w e. X ) -> E. h e. Q w = { t e. T | 0 < ( h ` t ) } )
27 df-rex 
 |-  ( E. h e. Q w = { t e. T | 0 < ( h ` t ) } <-> E. h ( h e. Q /\ w = { t e. T | 0 < ( h ` t ) } ) )
28 26 27 sylib 
 |-  ( ( ph /\ w e. X ) -> E. h ( h e. Q /\ w = { t e. T | 0 < ( h ` t ) } ) )
29 rabid 
 |-  ( h e. { h e. Q | w = { t e. T | 0 < ( h ` t ) } } <-> ( h e. Q /\ w = { t e. T | 0 < ( h ` t ) } ) )
30 29 exbii 
 |-  ( E. h h e. { h e. Q | w = { t e. T | 0 < ( h ` t ) } } <-> E. h ( h e. Q /\ w = { t e. T | 0 < ( h ` t ) } ) )
31 28 30 sylibr 
 |-  ( ( ph /\ w e. X ) -> E. h h e. { h e. Q | w = { t e. T | 0 < ( h ` t ) } } )
32 31 adantr 
 |-  ( ( ( ph /\ w e. X ) /\ k = { h e. Q | w = { t e. T | 0 < ( h ` t ) } } ) -> E. h h e. { h e. Q | w = { t e. T | 0 < ( h ` t ) } } )
33 nfv 
 |-  F/ h w e. X
34 3 33 nfan 
 |-  F/ h ( ph /\ w e. X )
35 nfrab1 
 |-  F/_ h { h e. Q | w = { t e. T | 0 < ( h ` t ) } }
36 35 nfeq2 
 |-  F/ h k = { h e. Q | w = { t e. T | 0 < ( h ` t ) } }
37 34 36 nfan 
 |-  F/ h ( ( ph /\ w e. X ) /\ k = { h e. Q | w = { t e. T | 0 < ( h ` t ) } } )
38 eleq2 
 |-  ( k = { h e. Q | w = { t e. T | 0 < ( h ` t ) } } -> ( h e. k <-> h e. { h e. Q | w = { t e. T | 0 < ( h ` t ) } } ) )
39 38 biimprd 
 |-  ( k = { h e. Q | w = { t e. T | 0 < ( h ` t ) } } -> ( h e. { h e. Q | w = { t e. T | 0 < ( h ` t ) } } -> h e. k ) )
40 39 adantl 
 |-  ( ( ( ph /\ w e. X ) /\ k = { h e. Q | w = { t e. T | 0 < ( h ` t ) } } ) -> ( h e. { h e. Q | w = { t e. T | 0 < ( h ` t ) } } -> h e. k ) )
41 37 40 eximd 
 |-  ( ( ( ph /\ w e. X ) /\ k = { h e. Q | w = { t e. T | 0 < ( h ` t ) } } ) -> ( E. h h e. { h e. Q | w = { t e. T | 0 < ( h ` t ) } } -> E. h h e. k ) )
42 32 41 mpd 
 |-  ( ( ( ph /\ w e. X ) /\ k = { h e. Q | w = { t e. T | 0 < ( h ` t ) } } ) -> E. h h e. k )
43 42 adantllr 
 |-  ( ( ( ( ph /\ k e. ran G ) /\ w e. X ) /\ k = { h e. Q | w = { t e. T | 0 < ( h ` t ) } } ) -> E. h h e. k )
44 6 elrnmpt 
 |-  ( k e. ran G -> ( k e. ran G <-> E. w e. X k = { h e. Q | w = { t e. T | 0 < ( h ` t ) } } ) )
45 44 ibi 
 |-  ( k e. ran G -> E. w e. X k = { h e. Q | w = { t e. T | 0 < ( h ` t ) } } )
46 45 adantl 
 |-  ( ( ph /\ k e. ran G ) -> E. w e. X k = { h e. Q | w = { t e. T | 0 < ( h ` t ) } } )
47 21 43 46 r19.29af 
 |-  ( ( ph /\ k e. ran G ) -> E. h h e. k )
48 n0 
 |-  ( k =/= (/) <-> E. h h e. k )
49 47 48 sylibr 
 |-  ( ( ph /\ k e. ran G ) -> k =/= (/) )
50 49 adantlr 
 |-  ( ( ( ph /\ ( g Fn ran G /\ A. l e. ran G ( l =/= (/) -> ( g ` l ) e. l ) ) ) /\ k e. ran G ) -> k =/= (/) )
51 simplrr 
 |-  ( ( ( ph /\ ( g Fn ran G /\ A. l e. ran G ( l =/= (/) -> ( g ` l ) e. l ) ) ) /\ k e. ran G ) -> A. l e. ran G ( l =/= (/) -> ( g ` l ) e. l ) )
52 neeq1 
 |-  ( l = k -> ( l =/= (/) <-> k =/= (/) ) )
53 fveq2 
 |-  ( l = k -> ( g ` l ) = ( g ` k ) )
54 53 eleq1d 
 |-  ( l = k -> ( ( g ` l ) e. l <-> ( g ` k ) e. l ) )
55 eleq2 
 |-  ( l = k -> ( ( g ` k ) e. l <-> ( g ` k ) e. k ) )
56 54 55 bitrd 
 |-  ( l = k -> ( ( g ` l ) e. l <-> ( g ` k ) e. k ) )
57 52 56 imbi12d 
 |-  ( l = k -> ( ( l =/= (/) -> ( g ` l ) e. l ) <-> ( k =/= (/) -> ( g ` k ) e. k ) ) )
58 57 rspccva 
 |-  ( ( A. l e. ran G ( l =/= (/) -> ( g ` l ) e. l ) /\ k e. ran G ) -> ( k =/= (/) -> ( g ` k ) e. k ) )
59 51 58 sylancom 
 |-  ( ( ( ph /\ ( g Fn ran G /\ A. l e. ran G ( l =/= (/) -> ( g ` l ) e. l ) ) ) /\ k e. ran G ) -> ( k =/= (/) -> ( g ` k ) e. k ) )
60 50 59 mpd 
 |-  ( ( ( ph /\ ( g Fn ran G /\ A. l e. ran G ( l =/= (/) -> ( g ` l ) e. l ) ) ) /\ k e. ran G ) -> ( g ` k ) e. k )
61 60 ralrimiva 
 |-  ( ( ph /\ ( g Fn ran G /\ A. l e. ran G ( l =/= (/) -> ( g ` l ) e. l ) ) ) -> A. k e. ran G ( g ` k ) e. k )
62 fveq2 
 |-  ( k = l -> ( g ` k ) = ( g ` l ) )
63 62 eleq1d 
 |-  ( k = l -> ( ( g ` k ) e. k <-> ( g ` l ) e. k ) )
64 eleq2 
 |-  ( k = l -> ( ( g ` l ) e. k <-> ( g ` l ) e. l ) )
65 63 64 bitrd 
 |-  ( k = l -> ( ( g ` k ) e. k <-> ( g ` l ) e. l ) )
66 65 cbvralvw 
 |-  ( A. k e. ran G ( g ` k ) e. k <-> A. l e. ran G ( g ` l ) e. l )
67 61 66 sylib 
 |-  ( ( ph /\ ( g Fn ran G /\ A. l e. ran G ( l =/= (/) -> ( g ` l ) e. l ) ) ) -> A. l e. ran G ( g ` l ) e. l )
68 16 67 jca 
 |-  ( ( ph /\ ( g Fn ran G /\ A. l e. ran G ( l =/= (/) -> ( g ` l ) e. l ) ) ) -> ( g Fn ran G /\ A. l e. ran G ( g ` l ) e. l ) )
69 68 ex 
 |-  ( ph -> ( ( g Fn ran G /\ A. l e. ran G ( l =/= (/) -> ( g ` l ) e. l ) ) -> ( g Fn ran G /\ A. l e. ran G ( g ` l ) e. l ) ) )
70 69 adantr 
 |-  ( ( ph /\ ran G e. Fin ) -> ( ( g Fn ran G /\ A. l e. ran G ( l =/= (/) -> ( g ` l ) e. l ) ) -> ( g Fn ran G /\ A. l e. ran G ( g ` l ) e. l ) ) )
71 70 eximdv 
 |-  ( ( ph /\ ran G e. Fin ) -> ( E. g ( g Fn ran G /\ A. l e. ran G ( l =/= (/) -> ( g ` l ) e. l ) ) -> E. g ( g Fn ran G /\ A. l e. ran G ( g ` l ) e. l ) ) )
72 15 71 mpd 
 |-  ( ( ph /\ ran G e. Fin ) -> E. g ( g Fn ran G /\ A. l e. ran G ( g ` l ) e. l ) )
73 13 72 mpdan 
 |-  ( ph -> E. g ( g Fn ran G /\ A. l e. ran G ( g ` l ) e. l ) )
74 73 ralrimivw 
 |-  ( ph -> A. m e. NN E. g ( g Fn ran G /\ A. l e. ran G ( g ` l ) e. l ) )
75 ssn0 
 |-  ( ( ( T \ U ) C_ U. X /\ ( T \ U ) =/= (/) ) -> U. X =/= (/) )
76 10 11 75 syl2anc 
 |-  ( ph -> U. X =/= (/) )
77 76 neneqd 
 |-  ( ph -> -. U. X = (/) )
78 unieq 
 |-  ( X = (/) -> U. X = U. (/) )
79 uni0 
 |-  U. (/) = (/)
80 78 79 eqtrdi 
 |-  ( X = (/) -> U. X = (/) )
81 77 80 nsyl 
 |-  ( ph -> -. X = (/) )
82 dm0rn0 
 |-  ( dom G = (/) <-> ran G = (/) )
83 4 7 rabexd 
 |-  ( ph -> Q e. _V )
84 nfrab1 
 |-  F/_ h { h e. A | ( ( h ` Z ) = 0 /\ A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) ) }
85 4 84 nfcxfr 
 |-  F/_ h Q
86 85 rabexgf 
 |-  ( Q e. _V -> { h e. Q | w = { t e. T | 0 < ( h ` t ) } } e. _V )
87 83 86 syl 
 |-  ( ph -> { h e. Q | w = { t e. T | 0 < ( h ` t ) } } e. _V )
88 87 adantr 
 |-  ( ( ph /\ w e. X ) -> { h e. Q | w = { t e. T | 0 < ( h ` t ) } } e. _V )
89 2 88 6 fmptdf 
 |-  ( ph -> G : X --> _V )
90 dffn2 
 |-  ( G Fn X <-> G : X --> _V )
91 89 90 sylibr 
 |-  ( ph -> G Fn X )
92 91 fndmd 
 |-  ( ph -> dom G = X )
93 92 eqeq1d 
 |-  ( ph -> ( dom G = (/) <-> X = (/) ) )
94 82 93 bitr3id 
 |-  ( ph -> ( ran G = (/) <-> X = (/) ) )
95 81 94 mtbird 
 |-  ( ph -> -. ran G = (/) )
96 fz1f1o 
 |-  ( ran G e. Fin -> ( ran G = (/) \/ ( ( # ` ran G ) e. NN /\ E. f f : ( 1 ... ( # ` ran G ) ) -1-1-onto-> ran G ) ) )
97 13 96 syl 
 |-  ( ph -> ( ran G = (/) \/ ( ( # ` ran G ) e. NN /\ E. f f : ( 1 ... ( # ` ran G ) ) -1-1-onto-> ran G ) ) )
98 97 ord 
 |-  ( ph -> ( -. ran G = (/) -> ( ( # ` ran G ) e. NN /\ E. f f : ( 1 ... ( # ` ran G ) ) -1-1-onto-> ran G ) ) )
99 95 98 mpd 
 |-  ( ph -> ( ( # ` ran G ) e. NN /\ E. f f : ( 1 ... ( # ` ran G ) ) -1-1-onto-> ran G ) )
100 oveq2 
 |-  ( m = ( # ` ran G ) -> ( 1 ... m ) = ( 1 ... ( # ` ran G ) ) )
101 100 f1oeq2d 
 |-  ( m = ( # ` ran G ) -> ( f : ( 1 ... m ) -1-1-onto-> ran G <-> f : ( 1 ... ( # ` ran G ) ) -1-1-onto-> ran G ) )
102 101 exbidv 
 |-  ( m = ( # ` ran G ) -> ( E. f f : ( 1 ... m ) -1-1-onto-> ran G <-> E. f f : ( 1 ... ( # ` ran G ) ) -1-1-onto-> ran G ) )
103 102 rspcev 
 |-  ( ( ( # ` ran G ) e. NN /\ E. f f : ( 1 ... ( # ` ran G ) ) -1-1-onto-> ran G ) -> E. m e. NN E. f f : ( 1 ... m ) -1-1-onto-> ran G )
104 99 103 syl 
 |-  ( ph -> E. m e. NN E. f f : ( 1 ... m ) -1-1-onto-> ran G )
105 r19.29 
 |-  ( ( A. m e. NN E. g ( g Fn ran G /\ A. l e. ran G ( g ` l ) e. l ) /\ E. m e. NN E. f f : ( 1 ... m ) -1-1-onto-> ran G ) -> E. m e. NN ( E. g ( g Fn ran G /\ A. l e. ran G ( g ` l ) e. l ) /\ E. f f : ( 1 ... m ) -1-1-onto-> ran G ) )
106 74 104 105 syl2anc 
 |-  ( ph -> E. m e. NN ( E. g ( g Fn ran G /\ A. l e. ran G ( g ` l ) e. l ) /\ E. f f : ( 1 ... m ) -1-1-onto-> ran G ) )
107 exdistrv 
 |-  ( E. g E. f ( ( g Fn ran G /\ A. l e. ran G ( g ` l ) e. l ) /\ f : ( 1 ... m ) -1-1-onto-> ran G ) <-> ( E. g ( g Fn ran G /\ A. l e. ran G ( g ` l ) e. l ) /\ E. f f : ( 1 ... m ) -1-1-onto-> ran G ) )
108 107 biimpri 
 |-  ( ( E. g ( g Fn ran G /\ A. l e. ran G ( g ` l ) e. l ) /\ E. f f : ( 1 ... m ) -1-1-onto-> ran G ) -> E. g E. f ( ( g Fn ran G /\ A. l e. ran G ( g ` l ) e. l ) /\ f : ( 1 ... m ) -1-1-onto-> ran G ) )
109 108 a1i 
 |-  ( ph -> ( ( E. g ( g Fn ran G /\ A. l e. ran G ( g ` l ) e. l ) /\ E. f f : ( 1 ... m ) -1-1-onto-> ran G ) -> E. g E. f ( ( g Fn ran G /\ A. l e. ran G ( g ` l ) e. l ) /\ f : ( 1 ... m ) -1-1-onto-> ran G ) ) )
110 109 reximdv 
 |-  ( ph -> ( E. m e. NN ( E. g ( g Fn ran G /\ A. l e. ran G ( g ` l ) e. l ) /\ E. f f : ( 1 ... m ) -1-1-onto-> ran G ) -> E. m e. NN E. g E. f ( ( g Fn ran G /\ A. l e. ran G ( g ` l ) e. l ) /\ f : ( 1 ... m ) -1-1-onto-> ran G ) ) )
111 106 110 mpd 
 |-  ( ph -> E. m e. NN E. g E. f ( ( g Fn ran G /\ A. l e. ran G ( g ` l ) e. l ) /\ f : ( 1 ... m ) -1-1-onto-> ran G ) )
112 df-rex 
 |-  ( E. m e. NN E. g E. f ( ( g Fn ran G /\ A. l e. ran G ( g ` l ) e. l ) /\ f : ( 1 ... m ) -1-1-onto-> ran G ) <-> E. m ( m e. NN /\ E. g E. f ( ( g Fn ran G /\ A. l e. ran G ( g ` l ) e. l ) /\ f : ( 1 ... m ) -1-1-onto-> ran G ) ) )
113 111 112 sylib 
 |-  ( ph -> E. m ( m e. NN /\ E. g E. f ( ( g Fn ran G /\ A. l e. ran G ( g ` l ) e. l ) /\ f : ( 1 ... m ) -1-1-onto-> ran G ) ) )
114 ax-5 
 |-  ( m e. NN -> A. g m e. NN )
115 19.29 
 |-  ( ( A. g m e. NN /\ E. g E. f ( ( g Fn ran G /\ A. l e. ran G ( g ` l ) e. l ) /\ f : ( 1 ... m ) -1-1-onto-> ran G ) ) -> E. g ( m e. NN /\ E. f ( ( g Fn ran G /\ A. l e. ran G ( g ` l ) e. l ) /\ f : ( 1 ... m ) -1-1-onto-> ran G ) ) )
116 114 115 sylan 
 |-  ( ( m e. NN /\ E. g E. f ( ( g Fn ran G /\ A. l e. ran G ( g ` l ) e. l ) /\ f : ( 1 ... m ) -1-1-onto-> ran G ) ) -> E. g ( m e. NN /\ E. f ( ( g Fn ran G /\ A. l e. ran G ( g ` l ) e. l ) /\ f : ( 1 ... m ) -1-1-onto-> ran G ) ) )
117 ax-5 
 |-  ( m e. NN -> A. f m e. NN )
118 19.29 
 |-  ( ( A. f m e. NN /\ E. f ( ( g Fn ran G /\ A. l e. ran G ( g ` l ) e. l ) /\ f : ( 1 ... m ) -1-1-onto-> ran G ) ) -> E. f ( m e. NN /\ ( ( g Fn ran G /\ A. l e. ran G ( g ` l ) e. l ) /\ f : ( 1 ... m ) -1-1-onto-> ran G ) ) )
119 117 118 sylan 
 |-  ( ( m e. NN /\ E. f ( ( g Fn ran G /\ A. l e. ran G ( g ` l ) e. l ) /\ f : ( 1 ... m ) -1-1-onto-> ran G ) ) -> E. f ( m e. NN /\ ( ( g Fn ran G /\ A. l e. ran G ( g ` l ) e. l ) /\ f : ( 1 ... m ) -1-1-onto-> ran G ) ) )
120 119 eximi 
 |-  ( E. g ( m e. NN /\ E. f ( ( g Fn ran G /\ A. l e. ran G ( g ` l ) e. l ) /\ f : ( 1 ... m ) -1-1-onto-> ran G ) ) -> E. g E. f ( m e. NN /\ ( ( g Fn ran G /\ A. l e. ran G ( g ` l ) e. l ) /\ f : ( 1 ... m ) -1-1-onto-> ran G ) ) )
121 116 120 syl 
 |-  ( ( m e. NN /\ E. g E. f ( ( g Fn ran G /\ A. l e. ran G ( g ` l ) e. l ) /\ f : ( 1 ... m ) -1-1-onto-> ran G ) ) -> E. g E. f ( m e. NN /\ ( ( g Fn ran G /\ A. l e. ran G ( g ` l ) e. l ) /\ f : ( 1 ... m ) -1-1-onto-> ran G ) ) )
122 df-3an 
 |-  ( ( g Fn ran G /\ A. l e. ran G ( g ` l ) e. l /\ f : ( 1 ... m ) -1-1-onto-> ran G ) <-> ( ( g Fn ran G /\ A. l e. ran G ( g ` l ) e. l ) /\ f : ( 1 ... m ) -1-1-onto-> ran G ) )
123 122 anbi2i 
 |-  ( ( m e. NN /\ ( g Fn ran G /\ A. l e. ran G ( g ` l ) e. l /\ f : ( 1 ... m ) -1-1-onto-> ran G ) ) <-> ( m e. NN /\ ( ( g Fn ran G /\ A. l e. ran G ( g ` l ) e. l ) /\ f : ( 1 ... m ) -1-1-onto-> ran G ) ) )
124 123 2exbii 
 |-  ( E. g E. f ( m e. NN /\ ( g Fn ran G /\ A. l e. ran G ( g ` l ) e. l /\ f : ( 1 ... m ) -1-1-onto-> ran G ) ) <-> E. g E. f ( m e. NN /\ ( ( g Fn ran G /\ A. l e. ran G ( g ` l ) e. l ) /\ f : ( 1 ... m ) -1-1-onto-> ran G ) ) )
125 121 124 sylibr 
 |-  ( ( m e. NN /\ E. g E. f ( ( g Fn ran G /\ A. l e. ran G ( g ` l ) e. l ) /\ f : ( 1 ... m ) -1-1-onto-> ran G ) ) -> E. g E. f ( m e. NN /\ ( g Fn ran G /\ A. l e. ran G ( g ` l ) e. l /\ f : ( 1 ... m ) -1-1-onto-> ran G ) ) )
126 125 a1i 
 |-  ( ph -> ( ( m e. NN /\ E. g E. f ( ( g Fn ran G /\ A. l e. ran G ( g ` l ) e. l ) /\ f : ( 1 ... m ) -1-1-onto-> ran G ) ) -> E. g E. f ( m e. NN /\ ( g Fn ran G /\ A. l e. ran G ( g ` l ) e. l /\ f : ( 1 ... m ) -1-1-onto-> ran G ) ) ) )
127 126 eximdv 
 |-  ( ph -> ( E. m ( m e. NN /\ E. g E. f ( ( g Fn ran G /\ A. l e. ran G ( g ` l ) e. l ) /\ f : ( 1 ... m ) -1-1-onto-> ran G ) ) -> E. m E. g E. f ( m e. NN /\ ( g Fn ran G /\ A. l e. ran G ( g ` l ) e. l /\ f : ( 1 ... m ) -1-1-onto-> ran G ) ) ) )
128 113 127 mpd 
 |-  ( ph -> E. m E. g E. f ( m e. NN /\ ( g Fn ran G /\ A. l e. ran G ( g ` l ) e. l /\ f : ( 1 ... m ) -1-1-onto-> ran G ) ) )
129 83 adantr 
 |-  ( ( ph /\ ( m e. NN /\ ( g Fn ran G /\ A. l e. ran G ( g ` l ) e. l /\ f : ( 1 ... m ) -1-1-onto-> ran G ) ) ) -> Q e. _V )
130 simprl 
 |-  ( ( ph /\ ( m e. NN /\ ( g Fn ran G /\ A. l e. ran G ( g ` l ) e. l /\ f : ( 1 ... m ) -1-1-onto-> ran G ) ) ) -> m e. NN )
131 simprr1 
 |-  ( ( ph /\ ( m e. NN /\ ( g Fn ran G /\ A. l e. ran G ( g ` l ) e. l /\ f : ( 1 ... m ) -1-1-onto-> ran G ) ) ) -> g Fn ran G )
132 elex 
 |-  ( ran G e. Fin -> ran G e. _V )
133 13 132 syl 
 |-  ( ph -> ran G e. _V )
134 133 adantr 
 |-  ( ( ph /\ ( m e. NN /\ ( g Fn ran G /\ A. l e. ran G ( g ` l ) e. l /\ f : ( 1 ... m ) -1-1-onto-> ran G ) ) ) -> ran G e. _V )
135 simprr2 
 |-  ( ( ph /\ ( m e. NN /\ ( g Fn ran G /\ A. l e. ran G ( g ` l ) e. l /\ f : ( 1 ... m ) -1-1-onto-> ran G ) ) ) -> A. l e. ran G ( g ` l ) e. l )
136 56 rspccva 
 |-  ( ( A. l e. ran G ( g ` l ) e. l /\ k e. ran G ) -> ( g ` k ) e. k )
137 135 136 sylan 
 |-  ( ( ( ph /\ ( m e. NN /\ ( g Fn ran G /\ A. l e. ran G ( g ` l ) e. l /\ f : ( 1 ... m ) -1-1-onto-> ran G ) ) ) /\ k e. ran G ) -> ( g ` k ) e. k )
138 simprr3 
 |-  ( ( ph /\ ( m e. NN /\ ( g Fn ran G /\ A. l e. ran G ( g ` l ) e. l /\ f : ( 1 ... m ) -1-1-onto-> ran G ) ) ) -> f : ( 1 ... m ) -1-1-onto-> ran G )
139 10 adantr 
 |-  ( ( ph /\ ( m e. NN /\ ( g Fn ran G /\ A. l e. ran G ( g ` l ) e. l /\ f : ( 1 ... m ) -1-1-onto-> ran G ) ) ) -> ( T \ U ) C_ U. X )
140 nfv 
 |-  F/ t m e. NN
141 nfcv 
 |-  F/_ t g
142 nfcv 
 |-  F/_ t X
143 nfrab1 
 |-  F/_ t { t e. T | 0 < ( h ` t ) }
144 143 nfeq2 
 |-  F/ t w = { t e. T | 0 < ( h ` t ) }
145 nfv 
 |-  F/ t ( h ` Z ) = 0
146 nfra1 
 |-  F/ t A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 )
147 145 146 nfan 
 |-  F/ t ( ( h ` Z ) = 0 /\ A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) )
148 nfcv 
 |-  F/_ t A
149 147 148 nfrabw 
 |-  F/_ t { h e. A | ( ( h ` Z ) = 0 /\ A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) ) }
150 4 149 nfcxfr 
 |-  F/_ t Q
151 144 150 nfrabw 
 |-  F/_ t { h e. Q | w = { t e. T | 0 < ( h ` t ) } }
152 142 151 nfmpt 
 |-  F/_ t ( w e. X |-> { h e. Q | w = { t e. T | 0 < ( h ` t ) } } )
153 6 152 nfcxfr 
 |-  F/_ t G
154 153 nfrn 
 |-  F/_ t ran G
155 141 154 nffn 
 |-  F/ t g Fn ran G
156 nfv 
 |-  F/ t ( g ` l ) e. l
157 154 156 nfralw 
 |-  F/ t A. l e. ran G ( g ` l ) e. l
158 nfcv 
 |-  F/_ t f
159 nfcv 
 |-  F/_ t ( 1 ... m )
160 158 159 154 nff1o 
 |-  F/ t f : ( 1 ... m ) -1-1-onto-> ran G
161 155 157 160 nf3an 
 |-  F/ t ( g Fn ran G /\ A. l e. ran G ( g ` l ) e. l /\ f : ( 1 ... m ) -1-1-onto-> ran G )
162 140 161 nfan 
 |-  F/ t ( m e. NN /\ ( g Fn ran G /\ A. l e. ran G ( g ` l ) e. l /\ f : ( 1 ... m ) -1-1-onto-> ran G ) )
163 1 162 nfan 
 |-  F/ t ( ph /\ ( m e. NN /\ ( g Fn ran G /\ A. l e. ran G ( g ` l ) e. l /\ f : ( 1 ... m ) -1-1-onto-> ran G ) ) )
164 nfv 
 |-  F/ w m e. NN
165 nfcv 
 |-  F/_ w g
166 165 19 nffn 
 |-  F/ w g Fn ran G
167 nfv 
 |-  F/ w ( g ` l ) e. l
168 19 167 nfralw 
 |-  F/ w A. l e. ran G ( g ` l ) e. l
169 nfcv 
 |-  F/_ w f
170 nfcv 
 |-  F/_ w ( 1 ... m )
171 169 170 19 nff1o 
 |-  F/ w f : ( 1 ... m ) -1-1-onto-> ran G
172 166 168 171 nf3an 
 |-  F/ w ( g Fn ran G /\ A. l e. ran G ( g ` l ) e. l /\ f : ( 1 ... m ) -1-1-onto-> ran G )
173 164 172 nfan 
 |-  F/ w ( m e. NN /\ ( g Fn ran G /\ A. l e. ran G ( g ` l ) e. l /\ f : ( 1 ... m ) -1-1-onto-> ran G ) )
174 2 173 nfan 
 |-  F/ w ( ph /\ ( m e. NN /\ ( g Fn ran G /\ A. l e. ran G ( g ` l ) e. l /\ f : ( 1 ... m ) -1-1-onto-> ran G ) ) )
175 6 129 130 131 134 137 138 139 163 174 85 stoweidlem27 
 |-  ( ( ph /\ ( m e. NN /\ ( g Fn ran G /\ A. l e. ran G ( g ` l ) e. l /\ f : ( 1 ... m ) -1-1-onto-> ran G ) ) ) -> E. q ( m e. NN /\ ( q : ( 1 ... m ) --> Q /\ A. t e. ( T \ U ) E. i e. ( 1 ... m ) 0 < ( ( q ` i ) ` t ) ) ) )
176 175 ex 
 |-  ( ph -> ( ( m e. NN /\ ( g Fn ran G /\ A. l e. ran G ( g ` l ) e. l /\ f : ( 1 ... m ) -1-1-onto-> ran G ) ) -> E. q ( m e. NN /\ ( q : ( 1 ... m ) --> Q /\ A. t e. ( T \ U ) E. i e. ( 1 ... m ) 0 < ( ( q ` i ) ` t ) ) ) ) )
177 176 2eximdv 
 |-  ( ph -> ( E. g E. f ( m e. NN /\ ( g Fn ran G /\ A. l e. ran G ( g ` l ) e. l /\ f : ( 1 ... m ) -1-1-onto-> ran G ) ) -> E. g E. f E. q ( m e. NN /\ ( q : ( 1 ... m ) --> Q /\ A. t e. ( T \ U ) E. i e. ( 1 ... m ) 0 < ( ( q ` i ) ` t ) ) ) ) )
178 177 eximdv 
 |-  ( ph -> ( E. m E. g E. f ( m e. NN /\ ( g Fn ran G /\ A. l e. ran G ( g ` l ) e. l /\ f : ( 1 ... m ) -1-1-onto-> ran G ) ) -> E. m E. g E. f E. q ( m e. NN /\ ( q : ( 1 ... m ) --> Q /\ A. t e. ( T \ U ) E. i e. ( 1 ... m ) 0 < ( ( q ` i ) ` t ) ) ) ) )
179 128 178 mpd 
 |-  ( ph -> E. m E. g E. f E. q ( m e. NN /\ ( q : ( 1 ... m ) --> Q /\ A. t e. ( T \ U ) E. i e. ( 1 ... m ) 0 < ( ( q ` i ) ` t ) ) ) )
180 id 
 |-  ( E. q ( m e. NN /\ ( q : ( 1 ... m ) --> Q /\ A. t e. ( T \ U ) E. i e. ( 1 ... m ) 0 < ( ( q ` i ) ` t ) ) ) -> E. q ( m e. NN /\ ( q : ( 1 ... m ) --> Q /\ A. t e. ( T \ U ) E. i e. ( 1 ... m ) 0 < ( ( q ` i ) ` t ) ) ) )
181 180 exlimivv 
 |-  ( E. g E. f E. q ( m e. NN /\ ( q : ( 1 ... m ) --> Q /\ A. t e. ( T \ U ) E. i e. ( 1 ... m ) 0 < ( ( q ` i ) ` t ) ) ) -> E. q ( m e. NN /\ ( q : ( 1 ... m ) --> Q /\ A. t e. ( T \ U ) E. i e. ( 1 ... m ) 0 < ( ( q ` i ) ` t ) ) ) )
182 181 eximi 
 |-  ( E. m E. g E. f E. q ( m e. NN /\ ( q : ( 1 ... m ) --> Q /\ A. t e. ( T \ U ) E. i e. ( 1 ... m ) 0 < ( ( q ` i ) ` t ) ) ) -> E. m E. q ( m e. NN /\ ( q : ( 1 ... m ) --> Q /\ A. t e. ( T \ U ) E. i e. ( 1 ... m ) 0 < ( ( q ` i ) ` t ) ) ) )
183 179 182 syl 
 |-  ( ph -> E. m E. q ( m e. NN /\ ( q : ( 1 ... m ) --> Q /\ A. t e. ( T \ U ) E. i e. ( 1 ... m ) 0 < ( ( q ` i ) ` t ) ) ) )