Description: Lemma for ruc . Closure lemmas for supremum. (Contributed by Mario Carneiro, 28-May-2014)
Ref | Expression | ||
---|---|---|---|
Hypotheses | ruc.1 | |
|
ruc.2 | |
||
ruc.4 | |
||
ruc.5 | |
||
Assertion | ruclem11 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ruc.1 | |
|
2 | ruc.2 | |
|
3 | ruc.4 | |
|
4 | ruc.5 | |
|
5 | 1 2 3 4 | ruclem6 | |
6 | 1stcof | |
|
7 | 5 6 | syl | |
8 | 7 | frnd | |
9 | 7 | fdmd | |
10 | 0nn0 | |
|
11 | ne0i | |
|
12 | 10 11 | mp1i | |
13 | 9 12 | eqnetrd | |
14 | dm0rn0 | |
|
15 | 14 | necon3bii | |
16 | 13 15 | sylib | |
17 | fvco3 | |
|
18 | 5 17 | sylan | |
19 | 1 | adantr | |
20 | 2 | adantr | |
21 | simpr | |
|
22 | 10 | a1i | |
23 | 19 20 3 4 21 22 | ruclem10 | |
24 | 1 2 3 4 | ruclem4 | |
25 | 24 | fveq2d | |
26 | c0ex | |
|
27 | 1ex | |
|
28 | 26 27 | op2nd | |
29 | 25 28 | eqtrdi | |
30 | 29 | adantr | |
31 | 23 30 | breqtrd | |
32 | 5 | ffvelcdmda | |
33 | xp1st | |
|
34 | 32 33 | syl | |
35 | 1re | |
|
36 | ltle | |
|
37 | 34 35 36 | sylancl | |
38 | 31 37 | mpd | |
39 | 18 38 | eqbrtrd | |
40 | 39 | ralrimiva | |
41 | 7 | ffnd | |
42 | breq1 | |
|
43 | 42 | ralrn | |
44 | 41 43 | syl | |
45 | 40 44 | mpbird | |
46 | 8 16 45 | 3jca | |