Description: Any subset of a partially ordered set is partially ordered. (Contributed by FL, 24-Jan-2010)
Ref | Expression | ||
---|---|---|---|
Assertion | psss | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | inss1 | |
|
2 | psrel | |
|
3 | relss | |
|
4 | 1 2 3 | mpsyl | |
5 | pstr2 | |
|
6 | trinxp | |
|
7 | 5 6 | syl | |
8 | uniin | |
|
9 | 8 | unissi | |
10 | uniin | |
|
11 | 9 10 | sstri | |
12 | elin | |
|
13 | unixpid | |
|
14 | 13 | eleq2i | |
15 | simprr | |
|
16 | psdmrn | |
|
17 | 16 | simpld | |
18 | 17 | eleq2d | |
19 | 18 | biimpar | |
20 | eqid | |
|
21 | 20 | psref | |
22 | 19 21 | syldan | |
23 | 22 | adantrr | |
24 | brinxp2 | |
|
25 | 15 15 23 24 | syl21anbrc | |
26 | 25 | expr | |
27 | 14 26 | syl5bi | |
28 | 27 | expimpd | |
29 | 12 28 | syl5bi | |
30 | 29 | ralrimiv | |
31 | ssralv | |
|
32 | 11 30 31 | mpsyl | |
33 | 1 | ssbri | |
34 | 1 | ssbri | |
35 | psasym | |
|
36 | 35 | 3expib | |
37 | 33 34 36 | syl2ani | |
38 | 37 | alrimivv | |
39 | asymref2 | |
|
40 | 32 38 39 | sylanbrc | |
41 | inex1g | |
|
42 | isps | |
|
43 | 41 42 | syl | |
44 | 4 7 40 43 | mpbir3and | |