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 bitrid 
 |-  ( 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 biimtrid 
 |-  ( ( ( ( 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 biimtrid 
 |-  ( ( ( 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 biimtrid 
 |-  ( ( 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 ) )