Metamath Proof Explorer


Theorem dyadmax

Description: Any nonempty set of dyadic rational intervals has a maximal element. (Contributed by Mario Carneiro, 26-Mar-2015)

Ref Expression
Hypothesis dyadmbl.1
|- F = ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. )
Assertion dyadmax
|- ( ( A C_ ran F /\ A =/= (/) ) -> E. z e. A A. w e. A ( ( [,] ` z ) C_ ( [,] ` w ) -> z = w ) )

Proof

Step Hyp Ref Expression
1 dyadmbl.1
 |-  F = ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. )
2 ltweuz
 |-  < We ( ZZ>= ` 0 )
3 2 a1i
 |-  ( ( A C_ ran F /\ A =/= (/) ) -> < We ( ZZ>= ` 0 ) )
4 nn0ex
 |-  NN0 e. _V
5 4 rabex
 |-  { n e. NN0 | E. z e. A E. a e. ZZ z = ( a F n ) } e. _V
6 5 a1i
 |-  ( ( A C_ ran F /\ A =/= (/) ) -> { n e. NN0 | E. z e. A E. a e. ZZ z = ( a F n ) } e. _V )
7 ssrab2
 |-  { n e. NN0 | E. z e. A E. a e. ZZ z = ( a F n ) } C_ NN0
8 nn0uz
 |-  NN0 = ( ZZ>= ` 0 )
9 7 8 sseqtri
 |-  { n e. NN0 | E. z e. A E. a e. ZZ z = ( a F n ) } C_ ( ZZ>= ` 0 )
10 9 a1i
 |-  ( ( A C_ ran F /\ A =/= (/) ) -> { n e. NN0 | E. z e. A E. a e. ZZ z = ( a F n ) } C_ ( ZZ>= ` 0 ) )
11 id
 |-  ( A =/= (/) -> A =/= (/) )
12 1 dyadf
 |-  F : ( ZZ X. NN0 ) --> ( <_ i^i ( RR X. RR ) )
13 ffn
 |-  ( F : ( ZZ X. NN0 ) --> ( <_ i^i ( RR X. RR ) ) -> F Fn ( ZZ X. NN0 ) )
14 ovelrn
 |-  ( F Fn ( ZZ X. NN0 ) -> ( z e. ran F <-> E. a e. ZZ E. n e. NN0 z = ( a F n ) ) )
15 12 13 14 mp2b
 |-  ( z e. ran F <-> E. a e. ZZ E. n e. NN0 z = ( a F n ) )
16 rexcom
 |-  ( E. a e. ZZ E. n e. NN0 z = ( a F n ) <-> E. n e. NN0 E. a e. ZZ z = ( a F n ) )
17 15 16 sylbb
 |-  ( z e. ran F -> E. n e. NN0 E. a e. ZZ z = ( a F n ) )
18 17 rgen
 |-  A. z e. ran F E. n e. NN0 E. a e. ZZ z = ( a F n )
19 ssralv
 |-  ( A C_ ran F -> ( A. z e. ran F E. n e. NN0 E. a e. ZZ z = ( a F n ) -> A. z e. A E. n e. NN0 E. a e. ZZ z = ( a F n ) ) )
20 18 19 mpi
 |-  ( A C_ ran F -> A. z e. A E. n e. NN0 E. a e. ZZ z = ( a F n ) )
21 r19.2z
 |-  ( ( A =/= (/) /\ A. z e. A E. n e. NN0 E. a e. ZZ z = ( a F n ) ) -> E. z e. A E. n e. NN0 E. a e. ZZ z = ( a F n ) )
22 11 20 21 syl2anr
 |-  ( ( A C_ ran F /\ A =/= (/) ) -> E. z e. A E. n e. NN0 E. a e. ZZ z = ( a F n ) )
23 rexcom
 |-  ( E. z e. A E. n e. NN0 E. a e. ZZ z = ( a F n ) <-> E. n e. NN0 E. z e. A E. a e. ZZ z = ( a F n ) )
24 22 23 sylib
 |-  ( ( A C_ ran F /\ A =/= (/) ) -> E. n e. NN0 E. z e. A E. a e. ZZ z = ( a F n ) )
25 rabn0
 |-  ( { n e. NN0 | E. z e. A E. a e. ZZ z = ( a F n ) } =/= (/) <-> E. n e. NN0 E. z e. A E. a e. ZZ z = ( a F n ) )
26 24 25 sylibr
 |-  ( ( A C_ ran F /\ A =/= (/) ) -> { n e. NN0 | E. z e. A E. a e. ZZ z = ( a F n ) } =/= (/) )
27 wereu
 |-  ( ( < We ( ZZ>= ` 0 ) /\ ( { n e. NN0 | E. z e. A E. a e. ZZ z = ( a F n ) } e. _V /\ { n e. NN0 | E. z e. A E. a e. ZZ z = ( a F n ) } C_ ( ZZ>= ` 0 ) /\ { n e. NN0 | E. z e. A E. a e. ZZ z = ( a F n ) } =/= (/) ) ) -> E! c e. { n e. NN0 | E. z e. A E. a e. ZZ z = ( a F n ) } A. d e. { n e. NN0 | E. z e. A E. a e. ZZ z = ( a F n ) } -. d < c )
28 3 6 10 26 27 syl13anc
 |-  ( ( A C_ ran F /\ A =/= (/) ) -> E! c e. { n e. NN0 | E. z e. A E. a e. ZZ z = ( a F n ) } A. d e. { n e. NN0 | E. z e. A E. a e. ZZ z = ( a F n ) } -. d < c )
29 reurex
 |-  ( E! c e. { n e. NN0 | E. z e. A E. a e. ZZ z = ( a F n ) } A. d e. { n e. NN0 | E. z e. A E. a e. ZZ z = ( a F n ) } -. d < c -> E. c e. { n e. NN0 | E. z e. A E. a e. ZZ z = ( a F n ) } A. d e. { n e. NN0 | E. z e. A E. a e. ZZ z = ( a F n ) } -. d < c )
30 28 29 syl
 |-  ( ( A C_ ran F /\ A =/= (/) ) -> E. c e. { n e. NN0 | E. z e. A E. a e. ZZ z = ( a F n ) } A. d e. { n e. NN0 | E. z e. A E. a e. ZZ z = ( a F n ) } -. d < c )
31 oveq2
 |-  ( n = c -> ( a F n ) = ( a F c ) )
32 31 eqeq2d
 |-  ( n = c -> ( z = ( a F n ) <-> z = ( a F c ) ) )
33 32 2rexbidv
 |-  ( n = c -> ( E. z e. A E. a e. ZZ z = ( a F n ) <-> E. z e. A E. a e. ZZ z = ( a F c ) ) )
34 33 elrab
 |-  ( c e. { n e. NN0 | E. z e. A E. a e. ZZ z = ( a F n ) } <-> ( c e. NN0 /\ E. z e. A E. a e. ZZ z = ( a F c ) ) )
35 eqeq1
 |-  ( z = w -> ( z = ( a F n ) <-> w = ( a F n ) ) )
36 oveq1
 |-  ( a = b -> ( a F n ) = ( b F n ) )
37 36 eqeq2d
 |-  ( a = b -> ( w = ( a F n ) <-> w = ( b F n ) ) )
38 35 37 cbvrex2vw
 |-  ( E. z e. A E. a e. ZZ z = ( a F n ) <-> E. w e. A E. b e. ZZ w = ( b F n ) )
39 oveq2
 |-  ( n = d -> ( b F n ) = ( b F d ) )
40 39 eqeq2d
 |-  ( n = d -> ( w = ( b F n ) <-> w = ( b F d ) ) )
41 40 2rexbidv
 |-  ( n = d -> ( E. w e. A E. b e. ZZ w = ( b F n ) <-> E. w e. A E. b e. ZZ w = ( b F d ) ) )
42 38 41 syl5bb
 |-  ( n = d -> ( E. z e. A E. a e. ZZ z = ( a F n ) <-> E. w e. A E. b e. ZZ w = ( b F d ) ) )
43 42 ralrab
 |-  ( A. d e. { n e. NN0 | E. z e. A E. a e. ZZ z = ( a F n ) } -. d < c <-> A. d e. NN0 ( E. w e. A E. b e. ZZ w = ( b F d ) -> -. d < c ) )
44 r19.23v
 |-  ( A. w e. A ( E. b e. ZZ w = ( b F d ) -> -. d < c ) <-> ( E. w e. A E. b e. ZZ w = ( b F d ) -> -. d < c ) )
45 44 ralbii
 |-  ( A. d e. NN0 A. w e. A ( E. b e. ZZ w = ( b F d ) -> -. d < c ) <-> A. d e. NN0 ( E. w e. A E. b e. ZZ w = ( b F d ) -> -. d < c ) )
46 ralcom
 |-  ( A. d e. NN0 A. w e. A ( E. b e. ZZ w = ( b F d ) -> -. d < c ) <-> A. w e. A A. d e. NN0 ( E. b e. ZZ w = ( b F d ) -> -. d < c ) )
47 45 46 bitr3i
 |-  ( A. d e. NN0 ( E. w e. A E. b e. ZZ w = ( b F d ) -> -. d < c ) <-> A. w e. A A. d e. NN0 ( E. b e. ZZ w = ( b F d ) -> -. d < c ) )
48 simplll
 |-  ( ( ( ( A C_ ran F /\ A =/= (/) ) /\ c e. NN0 ) /\ ( z e. A /\ a e. ZZ ) ) -> A C_ ran F )
49 48 sselda
 |-  ( ( ( ( ( A C_ ran F /\ A =/= (/) ) /\ c e. NN0 ) /\ ( z e. A /\ a e. ZZ ) ) /\ w e. A ) -> w e. ran F )
50 ovelrn
 |-  ( F Fn ( ZZ X. NN0 ) -> ( w e. ran F <-> E. b e. ZZ E. d e. NN0 w = ( b F d ) ) )
51 12 13 50 mp2b
 |-  ( w e. ran F <-> E. b e. ZZ E. d e. NN0 w = ( b F d ) )
52 49 51 sylib
 |-  ( ( ( ( ( A C_ ran F /\ A =/= (/) ) /\ c e. NN0 ) /\ ( z e. A /\ a e. ZZ ) ) /\ w e. A ) -> E. b e. ZZ E. d e. NN0 w = ( b F d ) )
53 rexcom
 |-  ( E. b e. ZZ E. d e. NN0 w = ( b F d ) <-> E. d e. NN0 E. b e. ZZ w = ( b F d ) )
54 r19.29
 |-  ( ( A. d e. NN0 ( E. b e. ZZ w = ( b F d ) -> -. d < c ) /\ E. d e. NN0 E. b e. ZZ w = ( b F d ) ) -> E. d e. NN0 ( ( E. b e. ZZ w = ( b F d ) -> -. d < c ) /\ E. b e. ZZ w = ( b F d ) ) )
55 54 expcom
 |-  ( E. d e. NN0 E. b e. ZZ w = ( b F d ) -> ( A. d e. NN0 ( E. b e. ZZ w = ( b F d ) -> -. d < c ) -> E. d e. NN0 ( ( E. b e. ZZ w = ( b F d ) -> -. d < c ) /\ E. b e. ZZ w = ( b F d ) ) ) )
56 53 55 sylbi
 |-  ( E. b e. ZZ E. d e. NN0 w = ( b F d ) -> ( A. d e. NN0 ( E. b e. ZZ w = ( b F d ) -> -. d < c ) -> E. d e. NN0 ( ( E. b e. ZZ w = ( b F d ) -> -. d < c ) /\ E. b e. ZZ w = ( b F d ) ) ) )
57 52 56 syl
 |-  ( ( ( ( ( A C_ ran F /\ A =/= (/) ) /\ c e. NN0 ) /\ ( z e. A /\ a e. ZZ ) ) /\ w e. A ) -> ( A. d e. NN0 ( E. b e. ZZ w = ( b F d ) -> -. d < c ) -> E. d e. NN0 ( ( E. b e. ZZ w = ( b F d ) -> -. d < c ) /\ E. b e. ZZ w = ( b F d ) ) ) )
58 simplrr
 |-  ( ( ( ( ( A C_ ran F /\ A =/= (/) ) /\ c e. NN0 ) /\ ( z e. A /\ a e. ZZ ) ) /\ w e. A ) -> a e. ZZ )
59 58 ad2antrr
 |-  ( ( ( ( ( ( ( A C_ ran F /\ A =/= (/) ) /\ c e. NN0 ) /\ ( z e. A /\ a e. ZZ ) ) /\ w e. A ) /\ ( d e. NN0 /\ b e. ZZ ) ) /\ ( -. d < c /\ ( [,] ` ( a F c ) ) C_ ( [,] ` ( b F d ) ) ) ) -> a e. ZZ )
60 simplrr
 |-  ( ( ( ( ( ( ( A C_ ran F /\ A =/= (/) ) /\ c e. NN0 ) /\ ( z e. A /\ a e. ZZ ) ) /\ w e. A ) /\ ( d e. NN0 /\ b e. ZZ ) ) /\ ( -. d < c /\ ( [,] ` ( a F c ) ) C_ ( [,] ` ( b F d ) ) ) ) -> b e. ZZ )
61 simp-5r
 |-  ( ( ( ( ( ( ( A C_ ran F /\ A =/= (/) ) /\ c e. NN0 ) /\ ( z e. A /\ a e. ZZ ) ) /\ w e. A ) /\ ( d e. NN0 /\ b e. ZZ ) ) /\ ( -. d < c /\ ( [,] ` ( a F c ) ) C_ ( [,] ` ( b F d ) ) ) ) -> c e. NN0 )
62 simplrl
 |-  ( ( ( ( ( ( ( A C_ ran F /\ A =/= (/) ) /\ c e. NN0 ) /\ ( z e. A /\ a e. ZZ ) ) /\ w e. A ) /\ ( d e. NN0 /\ b e. ZZ ) ) /\ ( -. d < c /\ ( [,] ` ( a F c ) ) C_ ( [,] ` ( b F d ) ) ) ) -> d e. NN0 )
63 simprl
 |-  ( ( ( ( ( ( ( A C_ ran F /\ A =/= (/) ) /\ c e. NN0 ) /\ ( z e. A /\ a e. ZZ ) ) /\ w e. A ) /\ ( d e. NN0 /\ b e. ZZ ) ) /\ ( -. d < c /\ ( [,] ` ( a F c ) ) C_ ( [,] ` ( b F d ) ) ) ) -> -. d < c )
64 simprr
 |-  ( ( ( ( ( ( ( A C_ ran F /\ A =/= (/) ) /\ c e. NN0 ) /\ ( z e. A /\ a e. ZZ ) ) /\ w e. A ) /\ ( d e. NN0 /\ b e. ZZ ) ) /\ ( -. d < c /\ ( [,] ` ( a F c ) ) C_ ( [,] ` ( b F d ) ) ) ) -> ( [,] ` ( a F c ) ) C_ ( [,] ` ( b F d ) ) )
65 1 59 60 61 62 63 64 dyadmaxlem
 |-  ( ( ( ( ( ( ( A C_ ran F /\ A =/= (/) ) /\ c e. NN0 ) /\ ( z e. A /\ a e. ZZ ) ) /\ w e. A ) /\ ( d e. NN0 /\ b e. ZZ ) ) /\ ( -. d < c /\ ( [,] ` ( a F c ) ) C_ ( [,] ` ( b F d ) ) ) ) -> ( a = b /\ c = d ) )
66 oveq12
 |-  ( ( a = b /\ c = d ) -> ( a F c ) = ( b F d ) )
67 65 66 syl
 |-  ( ( ( ( ( ( ( A C_ ran F /\ A =/= (/) ) /\ c e. NN0 ) /\ ( z e. A /\ a e. ZZ ) ) /\ w e. A ) /\ ( d e. NN0 /\ b e. ZZ ) ) /\ ( -. d < c /\ ( [,] ` ( a F c ) ) C_ ( [,] ` ( b F d ) ) ) ) -> ( a F c ) = ( b F d ) )
68 67 exp32
 |-  ( ( ( ( ( ( A C_ ran F /\ A =/= (/) ) /\ c e. NN0 ) /\ ( z e. A /\ a e. ZZ ) ) /\ w e. A ) /\ ( d e. NN0 /\ b e. ZZ ) ) -> ( -. d < c -> ( ( [,] ` ( a F c ) ) C_ ( [,] ` ( b F d ) ) -> ( a F c ) = ( b F d ) ) ) )
69 fveq2
 |-  ( w = ( b F d ) -> ( [,] ` w ) = ( [,] ` ( b F d ) ) )
70 69 sseq2d
 |-  ( w = ( b F d ) -> ( ( [,] ` ( a F c ) ) C_ ( [,] ` w ) <-> ( [,] ` ( a F c ) ) C_ ( [,] ` ( b F d ) ) ) )
71 eqeq2
 |-  ( w = ( b F d ) -> ( ( a F c ) = w <-> ( a F c ) = ( b F d ) ) )
72 70 71 imbi12d
 |-  ( w = ( b F d ) -> ( ( ( [,] ` ( a F c ) ) C_ ( [,] ` w ) -> ( a F c ) = w ) <-> ( ( [,] ` ( a F c ) ) C_ ( [,] ` ( b F d ) ) -> ( a F c ) = ( b F d ) ) ) )
73 72 imbi2d
 |-  ( w = ( b F d ) -> ( ( -. d < c -> ( ( [,] ` ( a F c ) ) C_ ( [,] ` w ) -> ( a F c ) = w ) ) <-> ( -. d < c -> ( ( [,] ` ( a F c ) ) C_ ( [,] ` ( b F d ) ) -> ( a F c ) = ( b F d ) ) ) ) )
74 68 73 syl5ibrcom
 |-  ( ( ( ( ( ( A C_ ran F /\ A =/= (/) ) /\ c e. NN0 ) /\ ( z e. A /\ a e. ZZ ) ) /\ w e. A ) /\ ( d e. NN0 /\ b e. ZZ ) ) -> ( w = ( b F d ) -> ( -. d < c -> ( ( [,] ` ( a F c ) ) C_ ( [,] ` w ) -> ( a F c ) = w ) ) ) )
75 74 anassrs
 |-  ( ( ( ( ( ( ( A C_ ran F /\ A =/= (/) ) /\ c e. NN0 ) /\ ( z e. A /\ a e. ZZ ) ) /\ w e. A ) /\ d e. NN0 ) /\ b e. ZZ ) -> ( w = ( b F d ) -> ( -. d < c -> ( ( [,] ` ( a F c ) ) C_ ( [,] ` w ) -> ( a F c ) = w ) ) ) )
76 75 rexlimdva
 |-  ( ( ( ( ( ( A C_ ran F /\ A =/= (/) ) /\ c e. NN0 ) /\ ( z e. A /\ a e. ZZ ) ) /\ w e. A ) /\ d e. NN0 ) -> ( E. b e. ZZ w = ( b F d ) -> ( -. d < c -> ( ( [,] ` ( a F c ) ) C_ ( [,] ` w ) -> ( a F c ) = w ) ) ) )
77 76 a2d
 |-  ( ( ( ( ( ( A C_ ran F /\ A =/= (/) ) /\ c e. NN0 ) /\ ( z e. A /\ a e. ZZ ) ) /\ w e. A ) /\ d e. NN0 ) -> ( ( E. b e. ZZ w = ( b F d ) -> -. d < c ) -> ( E. b e. ZZ w = ( b F d ) -> ( ( [,] ` ( a F c ) ) C_ ( [,] ` w ) -> ( a F c ) = w ) ) ) )
78 77 impd
 |-  ( ( ( ( ( ( A C_ ran F /\ A =/= (/) ) /\ c e. NN0 ) /\ ( z e. A /\ a e. ZZ ) ) /\ w e. A ) /\ d e. NN0 ) -> ( ( ( E. b e. ZZ w = ( b F d ) -> -. d < c ) /\ E. b e. ZZ w = ( b F d ) ) -> ( ( [,] ` ( a F c ) ) C_ ( [,] ` w ) -> ( a F c ) = w ) ) )
79 78 rexlimdva
 |-  ( ( ( ( ( A C_ ran F /\ A =/= (/) ) /\ c e. NN0 ) /\ ( z e. A /\ a e. ZZ ) ) /\ w e. A ) -> ( E. d e. NN0 ( ( E. b e. ZZ w = ( b F d ) -> -. d < c ) /\ E. b e. ZZ w = ( b F d ) ) -> ( ( [,] ` ( a F c ) ) C_ ( [,] ` w ) -> ( a F c ) = w ) ) )
80 57 79 syld
 |-  ( ( ( ( ( A C_ ran F /\ A =/= (/) ) /\ c e. NN0 ) /\ ( z e. A /\ a e. ZZ ) ) /\ w e. A ) -> ( A. d e. NN0 ( E. b e. ZZ w = ( b F d ) -> -. d < c ) -> ( ( [,] ` ( a F c ) ) C_ ( [,] ` w ) -> ( a F c ) = w ) ) )
81 80 ralimdva
 |-  ( ( ( ( A C_ ran F /\ A =/= (/) ) /\ c e. NN0 ) /\ ( z e. A /\ a e. ZZ ) ) -> ( A. w e. A A. d e. NN0 ( E. b e. ZZ w = ( b F d ) -> -. d < c ) -> A. w e. A ( ( [,] ` ( a F c ) ) C_ ( [,] ` w ) -> ( a F c ) = w ) ) )
82 47 81 syl5bi
 |-  ( ( ( ( A C_ ran F /\ A =/= (/) ) /\ c e. NN0 ) /\ ( z e. A /\ a e. ZZ ) ) -> ( A. d e. NN0 ( E. w e. A E. b e. ZZ w = ( b F d ) -> -. d < c ) -> A. w e. A ( ( [,] ` ( a F c ) ) C_ ( [,] ` w ) -> ( a F c ) = w ) ) )
83 82 imp
 |-  ( ( ( ( ( A C_ ran F /\ A =/= (/) ) /\ c e. NN0 ) /\ ( z e. A /\ a e. ZZ ) ) /\ A. d e. NN0 ( E. w e. A E. b e. ZZ w = ( b F d ) -> -. d < c ) ) -> A. w e. A ( ( [,] ` ( a F c ) ) C_ ( [,] ` w ) -> ( a F c ) = w ) )
84 83 an32s
 |-  ( ( ( ( ( A C_ ran F /\ A =/= (/) ) /\ c e. NN0 ) /\ A. d e. NN0 ( E. w e. A E. b e. ZZ w = ( b F d ) -> -. d < c ) ) /\ ( z e. A /\ a e. ZZ ) ) -> A. w e. A ( ( [,] ` ( a F c ) ) C_ ( [,] ` w ) -> ( a F c ) = w ) )
85 fveq2
 |-  ( z = ( a F c ) -> ( [,] ` z ) = ( [,] ` ( a F c ) ) )
86 85 sseq1d
 |-  ( z = ( a F c ) -> ( ( [,] ` z ) C_ ( [,] ` w ) <-> ( [,] ` ( a F c ) ) C_ ( [,] ` w ) ) )
87 eqeq1
 |-  ( z = ( a F c ) -> ( z = w <-> ( a F c ) = w ) )
88 86 87 imbi12d
 |-  ( z = ( a F c ) -> ( ( ( [,] ` z ) C_ ( [,] ` w ) -> z = w ) <-> ( ( [,] ` ( a F c ) ) C_ ( [,] ` w ) -> ( a F c ) = w ) ) )
89 88 ralbidv
 |-  ( z = ( a F c ) -> ( A. w e. A ( ( [,] ` z ) C_ ( [,] ` w ) -> z = w ) <-> A. w e. A ( ( [,] ` ( a F c ) ) C_ ( [,] ` w ) -> ( a F c ) = w ) ) )
90 84 89 syl5ibrcom
 |-  ( ( ( ( ( A C_ ran F /\ A =/= (/) ) /\ c e. NN0 ) /\ A. d e. NN0 ( E. w e. A E. b e. ZZ w = ( b F d ) -> -. d < c ) ) /\ ( z e. A /\ a e. ZZ ) ) -> ( z = ( a F c ) -> A. w e. A ( ( [,] ` z ) C_ ( [,] ` w ) -> z = w ) ) )
91 90 anassrs
 |-  ( ( ( ( ( ( A C_ ran F /\ A =/= (/) ) /\ c e. NN0 ) /\ A. d e. NN0 ( E. w e. A E. b e. ZZ w = ( b F d ) -> -. d < c ) ) /\ z e. A ) /\ a e. ZZ ) -> ( z = ( a F c ) -> A. w e. A ( ( [,] ` z ) C_ ( [,] ` w ) -> z = w ) ) )
92 91 rexlimdva
 |-  ( ( ( ( ( A C_ ran F /\ A =/= (/) ) /\ c e. NN0 ) /\ A. d e. NN0 ( E. w e. A E. b e. ZZ w = ( b F d ) -> -. d < c ) ) /\ z e. A ) -> ( E. a e. ZZ z = ( a F c ) -> A. w e. A ( ( [,] ` z ) C_ ( [,] ` w ) -> z = w ) ) )
93 92 reximdva
 |-  ( ( ( ( A C_ ran F /\ A =/= (/) ) /\ c e. NN0 ) /\ A. d e. NN0 ( E. w e. A E. b e. ZZ w = ( b F d ) -> -. d < c ) ) -> ( E. z e. A E. a e. ZZ z = ( a F c ) -> E. z e. A A. w e. A ( ( [,] ` z ) C_ ( [,] ` w ) -> z = w ) ) )
94 93 ex
 |-  ( ( ( A C_ ran F /\ A =/= (/) ) /\ c e. NN0 ) -> ( A. d e. NN0 ( E. w e. A E. b e. ZZ w = ( b F d ) -> -. d < c ) -> ( E. z e. A E. a e. ZZ z = ( a F c ) -> E. z e. A A. w e. A ( ( [,] ` z ) C_ ( [,] ` w ) -> z = w ) ) ) )
95 43 94 syl5bi
 |-  ( ( ( A C_ ran F /\ A =/= (/) ) /\ c e. NN0 ) -> ( A. d e. { n e. NN0 | E. z e. A E. a e. ZZ z = ( a F n ) } -. d < c -> ( E. z e. A E. a e. ZZ z = ( a F c ) -> E. z e. A A. w e. A ( ( [,] ` z ) C_ ( [,] ` w ) -> z = w ) ) ) )
96 95 com23
 |-  ( ( ( A C_ ran F /\ A =/= (/) ) /\ c e. NN0 ) -> ( E. z e. A E. a e. ZZ z = ( a F c ) -> ( A. d e. { n e. NN0 | E. z e. A E. a e. ZZ z = ( a F n ) } -. d < c -> E. z e. A A. w e. A ( ( [,] ` z ) C_ ( [,] ` w ) -> z = w ) ) ) )
97 96 expimpd
 |-  ( ( A C_ ran F /\ A =/= (/) ) -> ( ( c e. NN0 /\ E. z e. A E. a e. ZZ z = ( a F c ) ) -> ( A. d e. { n e. NN0 | E. z e. A E. a e. ZZ z = ( a F n ) } -. d < c -> E. z e. A A. w e. A ( ( [,] ` z ) C_ ( [,] ` w ) -> z = w ) ) ) )
98 34 97 syl5bi
 |-  ( ( A C_ ran F /\ A =/= (/) ) -> ( c e. { n e. NN0 | E. z e. A E. a e. ZZ z = ( a F n ) } -> ( A. d e. { n e. NN0 | E. z e. A E. a e. ZZ z = ( a F n ) } -. d < c -> E. z e. A A. w e. A ( ( [,] ` z ) C_ ( [,] ` w ) -> z = w ) ) ) )
99 98 rexlimdv
 |-  ( ( A C_ ran F /\ A =/= (/) ) -> ( E. c e. { n e. NN0 | E. z e. A E. a e. ZZ z = ( a F n ) } A. d e. { n e. NN0 | E. z e. A E. a e. ZZ z = ( a F n ) } -. d < c -> E. z e. A A. w e. A ( ( [,] ` z ) C_ ( [,] ` w ) -> z = w ) ) )
100 30 99 mpd
 |-  ( ( A C_ ran F /\ A =/= (/) ) -> E. z e. A A. w e. A ( ( [,] ` z ) C_ ( [,] ` w ) -> z = w ) )