Description: Field of a subposet. (Contributed by Mario Carneiro, 9-Sep-2015)
Ref | Expression | ||
---|---|---|---|
Hypothesis | psssdm.1 | |
|
Assertion | psssdm2 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | psssdm.1 | |
|
2 | dmin | |
|
3 | 1 | eqcomi | |
4 | dmxpid | |
|
5 | 3 4 | ineq12i | |
6 | 2 5 | sseqtri | |
7 | 6 | a1i | |
8 | simpr | |
|
9 | 8 | elin2d | |
10 | elinel1 | |
|
11 | 1 | psref | |
12 | 10 11 | sylan2 | |
13 | brinxp2 | |
|
14 | 9 9 12 13 | syl21anbrc | |
15 | vex | |
|
16 | 15 15 | breldm | |
17 | 14 16 | syl | |
18 | 7 17 | eqelssd | |