Metamath Proof Explorer

Theorem nacsfix

Description: An increasing sequence of closed sets in a Noetherian-type closure system eventually fixates. (Contributed by Stefan O'Rear, 4-Apr-2015)

Ref Expression
Assertion nacsfix 
|- ( ( C e. ( NoeACS ` X ) /\ F : NN0 --> C /\ A. x e. NN0 ( F ` x ) C_ ( F ` ( x + 1 ) ) ) -> E. y e. NN0 A. z e. ( ZZ>= ` y ) ( F ` z ) = ( F ` y ) )

Proof

Step Hyp Ref Expression
1 fvssunirn 
 |-  ( F ` z ) C_ U. ran F
2 simplrr 
 |-  ( ( ( ( C e. ( NoeACS ` X ) /\ F : NN0 --> C /\ A. x e. NN0 ( F ` x ) C_ ( F ` ( x + 1 ) ) ) /\ ( y e. NN0 /\ ( F ` y ) = U. ran F ) ) /\ z e. ( ZZ>= ` y ) ) -> ( F ` y ) = U. ran F )
3 1 2 sseqtrrid 
 |-  ( ( ( ( C e. ( NoeACS ` X ) /\ F : NN0 --> C /\ A. x e. NN0 ( F ` x ) C_ ( F ` ( x + 1 ) ) ) /\ ( y e. NN0 /\ ( F ` y ) = U. ran F ) ) /\ z e. ( ZZ>= ` y ) ) -> ( F ` z ) C_ ( F ` y ) )
4 simpll3 
 |-  ( ( ( ( C e. ( NoeACS ` X ) /\ F : NN0 --> C /\ A. x e. NN0 ( F ` x ) C_ ( F ` ( x + 1 ) ) ) /\ ( y e. NN0 /\ ( F ` y ) = U. ran F ) ) /\ z e. ( ZZ>= ` y ) ) -> A. x e. NN0 ( F ` x ) C_ ( F ` ( x + 1 ) ) )
5 simplrl 
 |-  ( ( ( ( C e. ( NoeACS ` X ) /\ F : NN0 --> C /\ A. x e. NN0 ( F ` x ) C_ ( F ` ( x + 1 ) ) ) /\ ( y e. NN0 /\ ( F ` y ) = U. ran F ) ) /\ z e. ( ZZ>= ` y ) ) -> y e. NN0 )
6 simpr 
 |-  ( ( ( ( C e. ( NoeACS ` X ) /\ F : NN0 --> C /\ A. x e. NN0 ( F ` x ) C_ ( F ` ( x + 1 ) ) ) /\ ( y e. NN0 /\ ( F ` y ) = U. ran F ) ) /\ z e. ( ZZ>= ` y ) ) -> z e. ( ZZ>= ` y ) )
7 incssnn0 
 |-  ( ( A. x e. NN0 ( F ` x ) C_ ( F ` ( x + 1 ) ) /\ y e. NN0 /\ z e. ( ZZ>= ` y ) ) -> ( F ` y ) C_ ( F ` z ) )
8 4 5 6 7 syl3anc 
 |-  ( ( ( ( C e. ( NoeACS ` X ) /\ F : NN0 --> C /\ A. x e. NN0 ( F ` x ) C_ ( F ` ( x + 1 ) ) ) /\ ( y e. NN0 /\ ( F ` y ) = U. ran F ) ) /\ z e. ( ZZ>= ` y ) ) -> ( F ` y ) C_ ( F ` z ) )
9 3 8 eqssd 
 |-  ( ( ( ( C e. ( NoeACS ` X ) /\ F : NN0 --> C /\ A. x e. NN0 ( F ` x ) C_ ( F ` ( x + 1 ) ) ) /\ ( y e. NN0 /\ ( F ` y ) = U. ran F ) ) /\ z e. ( ZZ>= ` y ) ) -> ( F ` z ) = ( F ` y ) )
10 9 ralrimiva 
 |-  ( ( ( C e. ( NoeACS ` X ) /\ F : NN0 --> C /\ A. x e. NN0 ( F ` x ) C_ ( F ` ( x + 1 ) ) ) /\ ( y e. NN0 /\ ( F ` y ) = U. ran F ) ) -> A. z e. ( ZZ>= ` y ) ( F ` z ) = ( F ` y ) )
11 frn 
 |-  ( F : NN0 --> C -> ran F C_ C )
12 11 3ad2ant2 
 |-  ( ( C e. ( NoeACS ` X ) /\ F : NN0 --> C /\ A. x e. NN0 ( F ` x ) C_ ( F ` ( x + 1 ) ) ) -> ran F C_ C )
13 elpw2g 
 |-  ( C e. ( NoeACS ` X ) -> ( ran F e. ~P C <-> ran F C_ C ) )
14 13 3ad2ant1 
 |-  ( ( C e. ( NoeACS ` X ) /\ F : NN0 --> C /\ A. x e. NN0 ( F ` x ) C_ ( F ` ( x + 1 ) ) ) -> ( ran F e. ~P C <-> ran F C_ C ) )
15 12 14 mpbird 
 |-  ( ( C e. ( NoeACS ` X ) /\ F : NN0 --> C /\ A. x e. NN0 ( F ` x ) C_ ( F ` ( x + 1 ) ) ) -> ran F e. ~P C )
16 elex 
 |-  ( ran F e. ~P C -> ran F e. _V )
17 15 16 syl 
 |-  ( ( C e. ( NoeACS ` X ) /\ F : NN0 --> C /\ A. x e. NN0 ( F ` x ) C_ ( F ` ( x + 1 ) ) ) -> ran F e. _V )
18 ffn 
 |-  ( F : NN0 --> C -> F Fn NN0 )
19 18 3ad2ant2 
 |-  ( ( C e. ( NoeACS ` X ) /\ F : NN0 --> C /\ A. x e. NN0 ( F ` x ) C_ ( F ` ( x + 1 ) ) ) -> F Fn NN0 )
20 0nn0 
 |-  0 e. NN0
21 fnfvelrn 
 |-  ( ( F Fn NN0 /\ 0 e. NN0 ) -> ( F ` 0 ) e. ran F )
22 19 20 21 sylancl 
 |-  ( ( C e. ( NoeACS ` X ) /\ F : NN0 --> C /\ A. x e. NN0 ( F ` x ) C_ ( F ` ( x + 1 ) ) ) -> ( F ` 0 ) e. ran F )
23 22 ne0d 
 |-  ( ( C e. ( NoeACS ` X ) /\ F : NN0 --> C /\ A. x e. NN0 ( F ` x ) C_ ( F ` ( x + 1 ) ) ) -> ran F =/= (/) )
24 nn0re 
 |-  ( a e. NN0 -> a e. RR )
25 24 ad2antrl 
 |-  ( ( ( C e. ( NoeACS ` X ) /\ F : NN0 --> C /\ A. x e. NN0 ( F ` x ) C_ ( F ` ( x + 1 ) ) ) /\ ( a e. NN0 /\ b e. NN0 ) ) -> a e. RR )
26 nn0re 
 |-  ( b e. NN0 -> b e. RR )
27 26 ad2antll 
 |-  ( ( ( C e. ( NoeACS ` X ) /\ F : NN0 --> C /\ A. x e. NN0 ( F ` x ) C_ ( F ` ( x + 1 ) ) ) /\ ( a e. NN0 /\ b e. NN0 ) ) -> b e. RR )
28 simplrr 
 |-  ( ( ( ( C e. ( NoeACS ` X ) /\ F : NN0 --> C /\ A. x e. NN0 ( F ` x ) C_ ( F ` ( x + 1 ) ) ) /\ ( a e. NN0 /\ b e. NN0 ) ) /\ a <_ b ) -> b e. NN0 )
29 simpll3 
 |-  ( ( ( ( C e. ( NoeACS ` X ) /\ F : NN0 --> C /\ A. x e. NN0 ( F ` x ) C_ ( F ` ( x + 1 ) ) ) /\ ( a e. NN0 /\ b e. NN0 ) ) /\ a <_ b ) -> A. x e. NN0 ( F ` x ) C_ ( F ` ( x + 1 ) ) )
30 simplrl 
 |-  ( ( ( ( C e. ( NoeACS ` X ) /\ F : NN0 --> C /\ A. x e. NN0 ( F ` x ) C_ ( F ` ( x + 1 ) ) ) /\ ( a e. NN0 /\ b e. NN0 ) ) /\ a <_ b ) -> a e. NN0 )
31 nn0z 
 |-  ( a e. NN0 -> a e. ZZ )
32 nn0z 
 |-  ( b e. NN0 -> b e. ZZ )
33 eluz 
 |-  ( ( a e. ZZ /\ b e. ZZ ) -> ( b e. ( ZZ>= ` a ) <-> a <_ b ) )
34 31 32 33 syl2an 
 |-  ( ( a e. NN0 /\ b e. NN0 ) -> ( b e. ( ZZ>= ` a ) <-> a <_ b ) )
35 34 biimpar 
 |-  ( ( ( a e. NN0 /\ b e. NN0 ) /\ a <_ b ) -> b e. ( ZZ>= ` a ) )
36 35 adantll 
 |-  ( ( ( ( C e. ( NoeACS ` X ) /\ F : NN0 --> C /\ A. x e. NN0 ( F ` x ) C_ ( F ` ( x + 1 ) ) ) /\ ( a e. NN0 /\ b e. NN0 ) ) /\ a <_ b ) -> b e. ( ZZ>= ` a ) )
37 incssnn0 
 |-  ( ( A. x e. NN0 ( F ` x ) C_ ( F ` ( x + 1 ) ) /\ a e. NN0 /\ b e. ( ZZ>= ` a ) ) -> ( F ` a ) C_ ( F ` b ) )
38 29 30 36 37 syl3anc 
 |-  ( ( ( ( C e. ( NoeACS ` X ) /\ F : NN0 --> C /\ A. x e. NN0 ( F ` x ) C_ ( F ` ( x + 1 ) ) ) /\ ( a e. NN0 /\ b e. NN0 ) ) /\ a <_ b ) -> ( F ` a ) C_ ( F ` b ) )
39 ssequn1 
 |-  ( ( F ` a ) C_ ( F ` b ) <-> ( ( F ` a ) u. ( F ` b ) ) = ( F ` b ) )
40 38 39 sylib 
 |-  ( ( ( ( C e. ( NoeACS ` X ) /\ F : NN0 --> C /\ A. x e. NN0 ( F ` x ) C_ ( F ` ( x + 1 ) ) ) /\ ( a e. NN0 /\ b e. NN0 ) ) /\ a <_ b ) -> ( ( F ` a ) u. ( F ` b ) ) = ( F ` b ) )
41 eqimss 
 |-  ( ( ( F ` a ) u. ( F ` b ) ) = ( F ` b ) -> ( ( F ` a ) u. ( F ` b ) ) C_ ( F ` b ) )
42 40 41 syl 
 |-  ( ( ( ( C e. ( NoeACS ` X ) /\ F : NN0 --> C /\ A. x e. NN0 ( F ` x ) C_ ( F ` ( x + 1 ) ) ) /\ ( a e. NN0 /\ b e. NN0 ) ) /\ a <_ b ) -> ( ( F ` a ) u. ( F ` b ) ) C_ ( F ` b ) )
43 fveq2 
 |-  ( c = b -> ( F ` c ) = ( F ` b ) )
44 43 sseq2d 
 |-  ( c = b -> ( ( ( F ` a ) u. ( F ` b ) ) C_ ( F ` c ) <-> ( ( F ` a ) u. ( F ` b ) ) C_ ( F ` b ) ) )
45 44 rspcev 
 |-  ( ( b e. NN0 /\ ( ( F ` a ) u. ( F ` b ) ) C_ ( F ` b ) ) -> E. c e. NN0 ( ( F ` a ) u. ( F ` b ) ) C_ ( F ` c ) )
46 28 42 45 syl2anc 
 |-  ( ( ( ( C e. ( NoeACS ` X ) /\ F : NN0 --> C /\ A. x e. NN0 ( F ` x ) C_ ( F ` ( x + 1 ) ) ) /\ ( a e. NN0 /\ b e. NN0 ) ) /\ a <_ b ) -> E. c e. NN0 ( ( F ` a ) u. ( F ` b ) ) C_ ( F ` c ) )
47 simplrl 
 |-  ( ( ( ( C e. ( NoeACS ` X ) /\ F : NN0 --> C /\ A. x e. NN0 ( F ` x ) C_ ( F ` ( x + 1 ) ) ) /\ ( a e. NN0 /\ b e. NN0 ) ) /\ b <_ a ) -> a e. NN0 )
48 simpll3 
 |-  ( ( ( ( C e. ( NoeACS ` X ) /\ F : NN0 --> C /\ A. x e. NN0 ( F ` x ) C_ ( F ` ( x + 1 ) ) ) /\ ( a e. NN0 /\ b e. NN0 ) ) /\ b <_ a ) -> A. x e. NN0 ( F ` x ) C_ ( F ` ( x + 1 ) ) )
49 simplrr 
 |-  ( ( ( ( C e. ( NoeACS ` X ) /\ F : NN0 --> C /\ A. x e. NN0 ( F ` x ) C_ ( F ` ( x + 1 ) ) ) /\ ( a e. NN0 /\ b e. NN0 ) ) /\ b <_ a ) -> b e. NN0 )
50 eluz 
 |-  ( ( b e. ZZ /\ a e. ZZ ) -> ( a e. ( ZZ>= ` b ) <-> b <_ a ) )
51 32 31 50 syl2anr 
 |-  ( ( a e. NN0 /\ b e. NN0 ) -> ( a e. ( ZZ>= ` b ) <-> b <_ a ) )
52 51 biimpar 
 |-  ( ( ( a e. NN0 /\ b e. NN0 ) /\ b <_ a ) -> a e. ( ZZ>= ` b ) )
53 52 adantll 
 |-  ( ( ( ( C e. ( NoeACS ` X ) /\ F : NN0 --> C /\ A. x e. NN0 ( F ` x ) C_ ( F ` ( x + 1 ) ) ) /\ ( a e. NN0 /\ b e. NN0 ) ) /\ b <_ a ) -> a e. ( ZZ>= ` b ) )
54 incssnn0 
 |-  ( ( A. x e. NN0 ( F ` x ) C_ ( F ` ( x + 1 ) ) /\ b e. NN0 /\ a e. ( ZZ>= ` b ) ) -> ( F ` b ) C_ ( F ` a ) )
55 48 49 53 54 syl3anc 
 |-  ( ( ( ( C e. ( NoeACS ` X ) /\ F : NN0 --> C /\ A. x e. NN0 ( F ` x ) C_ ( F ` ( x + 1 ) ) ) /\ ( a e. NN0 /\ b e. NN0 ) ) /\ b <_ a ) -> ( F ` b ) C_ ( F ` a ) )
56 ssequn2 
 |-  ( ( F ` b ) C_ ( F ` a ) <-> ( ( F ` a ) u. ( F ` b ) ) = ( F ` a ) )
57 55 56 sylib 
 |-  ( ( ( ( C e. ( NoeACS ` X ) /\ F : NN0 --> C /\ A. x e. NN0 ( F ` x ) C_ ( F ` ( x + 1 ) ) ) /\ ( a e. NN0 /\ b e. NN0 ) ) /\ b <_ a ) -> ( ( F ` a ) u. ( F ` b ) ) = ( F ` a ) )
58 eqimss 
 |-  ( ( ( F ` a ) u. ( F ` b ) ) = ( F ` a ) -> ( ( F ` a ) u. ( F ` b ) ) C_ ( F ` a ) )
59 57 58 syl 
 |-  ( ( ( ( C e. ( NoeACS ` X ) /\ F : NN0 --> C /\ A. x e. NN0 ( F ` x ) C_ ( F ` ( x + 1 ) ) ) /\ ( a e. NN0 /\ b e. NN0 ) ) /\ b <_ a ) -> ( ( F ` a ) u. ( F ` b ) ) C_ ( F ` a ) )
60 fveq2 
 |-  ( c = a -> ( F ` c ) = ( F ` a ) )
61 60 sseq2d 
 |-  ( c = a -> ( ( ( F ` a ) u. ( F ` b ) ) C_ ( F ` c ) <-> ( ( F ` a ) u. ( F ` b ) ) C_ ( F ` a ) ) )
62 61 rspcev 
 |-  ( ( a e. NN0 /\ ( ( F ` a ) u. ( F ` b ) ) C_ ( F ` a ) ) -> E. c e. NN0 ( ( F ` a ) u. ( F ` b ) ) C_ ( F ` c ) )
63 47 59 62 syl2anc 
 |-  ( ( ( ( C e. ( NoeACS ` X ) /\ F : NN0 --> C /\ A. x e. NN0 ( F ` x ) C_ ( F ` ( x + 1 ) ) ) /\ ( a e. NN0 /\ b e. NN0 ) ) /\ b <_ a ) -> E. c e. NN0 ( ( F ` a ) u. ( F ` b ) ) C_ ( F ` c ) )
64 25 27 46 63 lecasei 
 |-  ( ( ( C e. ( NoeACS ` X ) /\ F : NN0 --> C /\ A. x e. NN0 ( F ` x ) C_ ( F ` ( x + 1 ) ) ) /\ ( a e. NN0 /\ b e. NN0 ) ) -> E. c e. NN0 ( ( F ` a ) u. ( F ` b ) ) C_ ( F ` c ) )
65 64 ralrimivva 
 |-  ( ( C e. ( NoeACS ` X ) /\ F : NN0 --> C /\ A. x e. NN0 ( F ` x ) C_ ( F ` ( x + 1 ) ) ) -> A. a e. NN0 A. b e. NN0 E. c e. NN0 ( ( F ` a ) u. ( F ` b ) ) C_ ( F ` c ) )
66 uneq1 
 |-  ( y = ( F ` a ) -> ( y u. z ) = ( ( F ` a ) u. z ) )
67 66 sseq1d 
 |-  ( y = ( F ` a ) -> ( ( y u. z ) C_ w <-> ( ( F ` a ) u. z ) C_ w ) )
68 67 rexbidv 
 |-  ( y = ( F ` a ) -> ( E. w e. ran F ( y u. z ) C_ w <-> E. w e. ran F ( ( F ` a ) u. z ) C_ w ) )
69 68 ralbidv 
 |-  ( y = ( F ` a ) -> ( A. z e. ran F E. w e. ran F ( y u. z ) C_ w <-> A. z e. ran F E. w e. ran F ( ( F ` a ) u. z ) C_ w ) )
70 69 ralrn 
 |-  ( F Fn NN0 -> ( A. y e. ran F A. z e. ran F E. w e. ran F ( y u. z ) C_ w <-> A. a e. NN0 A. z e. ran F E. w e. ran F ( ( F ` a ) u. z ) C_ w ) )
71 uneq2 
 |-  ( z = ( F ` b ) -> ( ( F ` a ) u. z ) = ( ( F ` a ) u. ( F ` b ) ) )
72 71 sseq1d 
 |-  ( z = ( F ` b ) -> ( ( ( F ` a ) u. z ) C_ w <-> ( ( F ` a ) u. ( F ` b ) ) C_ w ) )
73 72 rexbidv 
 |-  ( z = ( F ` b ) -> ( E. w e. ran F ( ( F ` a ) u. z ) C_ w <-> E. w e. ran F ( ( F ` a ) u. ( F ` b ) ) C_ w ) )
74 73 ralrn 
 |-  ( F Fn NN0 -> ( A. z e. ran F E. w e. ran F ( ( F ` a ) u. z ) C_ w <-> A. b e. NN0 E. w e. ran F ( ( F ` a ) u. ( F ` b ) ) C_ w ) )
75 sseq2 
 |-  ( w = ( F ` c ) -> ( ( ( F ` a ) u. ( F ` b ) ) C_ w <-> ( ( F ` a ) u. ( F ` b ) ) C_ ( F ` c ) ) )
76 75 rexrn 
 |-  ( F Fn NN0 -> ( E. w e. ran F ( ( F ` a ) u. ( F ` b ) ) C_ w <-> E. c e. NN0 ( ( F ` a ) u. ( F ` b ) ) C_ ( F ` c ) ) )
77 76 ralbidv 
 |-  ( F Fn NN0 -> ( A. b e. NN0 E. w e. ran F ( ( F ` a ) u. ( F ` b ) ) C_ w <-> A. b e. NN0 E. c e. NN0 ( ( F ` a ) u. ( F ` b ) ) C_ ( F ` c ) ) )
78 74 77 bitrd 
 |-  ( F Fn NN0 -> ( A. z e. ran F E. w e. ran F ( ( F ` a ) u. z ) C_ w <-> A. b e. NN0 E. c e. NN0 ( ( F ` a ) u. ( F ` b ) ) C_ ( F ` c ) ) )
79 78 ralbidv 
 |-  ( F Fn NN0 -> ( A. a e. NN0 A. z e. ran F E. w e. ran F ( ( F ` a ) u. z ) C_ w <-> A. a e. NN0 A. b e. NN0 E. c e. NN0 ( ( F ` a ) u. ( F ` b ) ) C_ ( F ` c ) ) )
80 70 79 bitrd 
 |-  ( F Fn NN0 -> ( A. y e. ran F A. z e. ran F E. w e. ran F ( y u. z ) C_ w <-> A. a e. NN0 A. b e. NN0 E. c e. NN0 ( ( F ` a ) u. ( F ` b ) ) C_ ( F ` c ) ) )
81 19 80 syl 
 |-  ( ( C e. ( NoeACS ` X ) /\ F : NN0 --> C /\ A. x e. NN0 ( F ` x ) C_ ( F ` ( x + 1 ) ) ) -> ( A. y e. ran F A. z e. ran F E. w e. ran F ( y u. z ) C_ w <-> A. a e. NN0 A. b e. NN0 E. c e. NN0 ( ( F ` a ) u. ( F ` b ) ) C_ ( F ` c ) ) )
82 65 81 mpbird 
 |-  ( ( C e. ( NoeACS ` X ) /\ F : NN0 --> C /\ A. x e. NN0 ( F ` x ) C_ ( F ` ( x + 1 ) ) ) -> A. y e. ran F A. z e. ran F E. w e. ran F ( y u. z ) C_ w )
83 isipodrs 
 |-  ( ( toInc ` ran F ) e. Dirset <-> ( ran F e. _V /\ ran F =/= (/) /\ A. y e. ran F A. z e. ran F E. w e. ran F ( y u. z ) C_ w ) )
84 17 23 82 83 syl3anbrc 
 |-  ( ( C e. ( NoeACS ` X ) /\ F : NN0 --> C /\ A. x e. NN0 ( F ` x ) C_ ( F ` ( x + 1 ) ) ) -> ( toInc ` ran F ) e. Dirset )
85 isnacs3 
 |-  ( C e. ( NoeACS ` X ) <-> ( C e. ( Moore ` X ) /\ A. y e. ~P C ( ( toInc ` y ) e. Dirset -> U. y e. y ) ) )
86 85 simprbi 
 |-  ( C e. ( NoeACS ` X ) -> A. y e. ~P C ( ( toInc ` y ) e. Dirset -> U. y e. y ) )
87 86 3ad2ant1 
 |-  ( ( C e. ( NoeACS ` X ) /\ F : NN0 --> C /\ A. x e. NN0 ( F ` x ) C_ ( F ` ( x + 1 ) ) ) -> A. y e. ~P C ( ( toInc ` y ) e. Dirset -> U. y e. y ) )
88 fveq2 
 |-  ( y = ran F -> ( toInc ` y ) = ( toInc ` ran F ) )
89 88 eleq1d 
 |-  ( y = ran F -> ( ( toInc ` y ) e. Dirset <-> ( toInc ` ran F ) e. Dirset ) )
90 unieq 
 |-  ( y = ran F -> U. y = U. ran F )
91 id 
 |-  ( y = ran F -> y = ran F )
92 90 91 eleq12d 
 |-  ( y = ran F -> ( U. y e. y <-> U. ran F e. ran F ) )
93 89 92 imbi12d 
 |-  ( y = ran F -> ( ( ( toInc ` y ) e. Dirset -> U. y e. y ) <-> ( ( toInc ` ran F ) e. Dirset -> U. ran F e. ran F ) ) )
94 93 rspcva 
 |-  ( ( ran F e. ~P C /\ A. y e. ~P C ( ( toInc ` y ) e. Dirset -> U. y e. y ) ) -> ( ( toInc ` ran F ) e. Dirset -> U. ran F e. ran F ) )
95 15 87 94 syl2anc 
 |-  ( ( C e. ( NoeACS ` X ) /\ F : NN0 --> C /\ A. x e. NN0 ( F ` x ) C_ ( F ` ( x + 1 ) ) ) -> ( ( toInc ` ran F ) e. Dirset -> U. ran F e. ran F ) )
96 84 95 mpd 
 |-  ( ( C e. ( NoeACS ` X ) /\ F : NN0 --> C /\ A. x e. NN0 ( F ` x ) C_ ( F ` ( x + 1 ) ) ) -> U. ran F e. ran F )
97 fvelrnb 
 |-  ( F Fn NN0 -> ( U. ran F e. ran F <-> E. y e. NN0 ( F ` y ) = U. ran F ) )
98 19 97 syl 
 |-  ( ( C e. ( NoeACS ` X ) /\ F : NN0 --> C /\ A. x e. NN0 ( F ` x ) C_ ( F ` ( x + 1 ) ) ) -> ( U. ran F e. ran F <-> E. y e. NN0 ( F ` y ) = U. ran F ) )
99 96 98 mpbid 
 |-  ( ( C e. ( NoeACS ` X ) /\ F : NN0 --> C /\ A. x e. NN0 ( F ` x ) C_ ( F ` ( x + 1 ) ) ) -> E. y e. NN0 ( F ` y ) = U. ran F )
100 10 99 reximddv 
 |-  ( ( C e. ( NoeACS ` X ) /\ F : NN0 --> C /\ A. x e. NN0 ( F ` x ) C_ ( F ` ( x + 1 ) ) ) -> E. y e. NN0 A. z e. ( ZZ>= ` y ) ( F ` z ) = ( F ` y ) )