Description: Lemma for opsrtos . (Contributed by Mario Carneiro, 8-Feb-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | opsrso.o | |
|
opsrso.i | |
||
opsrso.r | |
||
opsrso.t | |
||
opsrso.w | |
||
opsrtoslem.s | |
||
opsrtoslem.b | |
||
opsrtoslem.q | |
||
opsrtoslem.c | |
||
opsrtoslem.d | |
||
opsrtoslem.ps | |
||
opsrtoslem.l | |
||
Assertion | opsrtoslem1 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | opsrso.o | |
|
2 | opsrso.i | |
|
3 | opsrso.r | |
|
4 | opsrso.t | |
|
5 | opsrso.w | |
|
6 | opsrtoslem.s | |
|
7 | opsrtoslem.b | |
|
8 | opsrtoslem.q | |
|
9 | opsrtoslem.c | |
|
10 | opsrtoslem.d | |
|
11 | opsrtoslem.ps | |
|
12 | opsrtoslem.l | |
|
13 | 6 1 7 8 9 10 12 4 | opsrle | |
14 | unopab | |
|
15 | inopab | |
|
16 | df-xp | |
|
17 | 16 | ineq2i | |
18 | vex | |
|
19 | vex | |
|
20 | 18 19 | prss | |
21 | 20 | anbi1i | |
22 | ancom | |
|
23 | 21 22 | bitr3i | |
24 | 23 | opabbii | |
25 | 15 17 24 | 3eqtr4i | |
26 | opabresid | |
|
27 | equcom | |
|
28 | 27 | anbi2i | |
29 | eleq1w | |
|
30 | 29 | biimpac | |
31 | 30 | pm4.71i | |
32 | 28 31 | bitr3i | |
33 | an32 | |
|
34 | 20 | anbi1i | |
35 | 32 33 34 | 3bitri | |
36 | 35 | opabbii | |
37 | 26 36 | eqtri | |
38 | 25 37 | uneq12i | |
39 | 11 | orbi1i | |
40 | 39 | anbi2i | |
41 | andi | |
|
42 | 40 41 | bitr3i | |
43 | 42 | opabbii | |
44 | 14 38 43 | 3eqtr4ri | |
45 | 13 44 | eqtrdi | |