Description: Value of the less-than relationship. (Contributed by Thierry Arnoux, 21-Jun-2019)
Ref | Expression | ||
---|---|---|---|
Hypotheses | legval.p | |
|
legval.d | |
||
legval.i | |
||
legval.l | |
||
legval.g | |
||
Assertion | legval | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | legval.p | |
|
2 | legval.d | |
|
3 | legval.i | |
|
4 | legval.l | |
|
5 | legval.g | |
|
6 | elex | |
|
7 | simp1 | |
|
8 | 7 | eqcomd | |
9 | simp2 | |
|
10 | 9 | eqcomd | |
11 | 10 | oveqd | |
12 | 11 | eqeq2d | |
13 | simp3 | |
|
14 | 13 | eqcomd | |
15 | 14 | oveqd | |
16 | 15 | eleq2d | |
17 | 10 | oveqd | |
18 | 17 | eqeq2d | |
19 | 16 18 | anbi12d | |
20 | 8 19 | rexeqbidv | |
21 | 12 20 | anbi12d | |
22 | 8 21 | rexeqbidv | |
23 | 8 22 | rexeqbidv | |
24 | 1 2 3 23 | sbcie3s | |
25 | 24 | opabbidv | |
26 | df-leg | |
|
27 | 2 | fvexi | |
28 | 27 | imaex | |
29 | p0ex | |
|
30 | 28 29 | unex | |
31 | 30 | a1i | |
32 | simprr | |
|
33 | ovima0 | |
|
34 | 33 | ad5ant14 | |
35 | 32 34 | eqeltrd | |
36 | simpllr | |
|
37 | 36 | simpld | |
38 | ovima0 | |
|
39 | 38 | ad3antrrr | |
40 | 37 39 | eqeltrd | |
41 | 35 40 | jca | |
42 | simprr | |
|
43 | eleq1w | |
|
44 | oveq2 | |
|
45 | 44 | eqeq2d | |
46 | 43 45 | anbi12d | |
47 | 46 | cbvrexvw | |
48 | 42 47 | sylib | |
49 | 41 48 | r19.29a | |
50 | 49 | ex | |
51 | 50 | rexlimivv | |
52 | 51 | adantl | |
53 | 52 | simpld | |
54 | 52 | simprd | |
55 | 31 31 53 54 | opabex2 | |
56 | 55 | mptru | |
57 | 25 26 56 | fvmpt | |
58 | 5 6 57 | 3syl | |
59 | 4 58 | eqtrid | |