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 ) ) |