Description: Lemma for fin23 . Weak order property of Y . (Contributed by Stefan O'Rear, 2-Nov-2014)
Ref | Expression | ||
---|---|---|---|
Hypotheses | fin23lem33.f | |
|
fin23lem.f | |
||
fin23lem.g | |
||
fin23lem.h | |
||
fin23lem.i | |
||
Assertion | fin23lem36 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fin23lem33.f | |
|
2 | fin23lem.f | |
|
3 | fin23lem.g | |
|
4 | fin23lem.h | |
|
5 | fin23lem.i | |
|
6 | fveq2 | |
|
7 | 6 | rneqd | |
8 | 7 | unieqd | |
9 | 8 | sseq1d | |
10 | 9 | imbi2d | |
11 | fveq2 | |
|
12 | 11 | rneqd | |
13 | 12 | unieqd | |
14 | 13 | sseq1d | |
15 | 14 | imbi2d | |
16 | fveq2 | |
|
17 | 16 | rneqd | |
18 | 17 | unieqd | |
19 | 18 | sseq1d | |
20 | 19 | imbi2d | |
21 | fveq2 | |
|
22 | 21 | rneqd | |
23 | 22 | unieqd | |
24 | 23 | sseq1d | |
25 | 24 | imbi2d | |
26 | ssid | |
|
27 | 26 | 2a1i | |
28 | simprr | |
|
29 | simpll | |
|
30 | 1 2 3 4 5 | fin23lem35 | |
31 | 28 29 30 | syl2anc | |
32 | 31 | pssssd | |
33 | sstr2 | |
|
34 | 32 33 | syl | |
35 | 34 | expr | |
36 | 35 | a2d | |
37 | 10 15 20 25 27 36 | findsg | |
38 | 37 | impr | |