Metamath Proof Explorer


Theorem psss

Description: Any subset of a partially ordered set is partially ordered. (Contributed by FL, 24-Jan-2010)

Ref Expression
Assertion psss RPosetRelRA×APosetRel

Proof

Step Hyp Ref Expression
1 inss1 RA×AR
2 psrel RPosetRelRelR
3 relss RA×ARRelRRelRA×A
4 1 2 3 mpsyl RPosetRelRelRA×A
5 pstr2 RPosetRelRRR
6 trinxp RRRRA×ARA×ARA×A
7 5 6 syl RPosetRelRA×ARA×ARA×A
8 uniin RA×ARA×A
9 8 unissi RA×ARA×A
10 uniin RA×ARA×A
11 9 10 sstri RA×ARA×A
12 elin xRA×AxRxA×A
13 unixpid A×A=A
14 13 eleq2i xA×AxA
15 simprr RPosetRelxRxAxA
16 psdmrn RPosetReldomR=RranR=R
17 16 simpld RPosetReldomR=R
18 17 eleq2d RPosetRelxdomRxR
19 18 biimpar RPosetRelxRxdomR
20 eqid domR=domR
21 20 psref RPosetRelxdomRxRx
22 19 21 syldan RPosetRelxRxRx
23 22 adantrr RPosetRelxRxAxRx
24 brinxp2 xRA×AxxAxAxRx
25 15 15 23 24 syl21anbrc RPosetRelxRxAxRA×Ax
26 25 expr RPosetRelxRxAxRA×Ax
27 14 26 syl5bi RPosetRelxRxA×AxRA×Ax
28 27 expimpd RPosetRelxRxA×AxRA×Ax
29 12 28 syl5bi RPosetRelxRA×AxRA×Ax
30 29 ralrimiv RPosetRelxRA×AxRA×Ax
31 ssralv RA×ARA×AxRA×AxRA×AxxRA×AxRA×Ax
32 11 30 31 mpsyl RPosetRelxRA×AxRA×Ax
33 1 ssbri xRA×AyxRy
34 1 ssbri yRA×AxyRx
35 psasym RPosetRelxRyyRxx=y
36 35 3expib RPosetRelxRyyRxx=y
37 33 34 36 syl2ani RPosetRelxRA×AyyRA×Axx=y
38 37 alrimivv RPosetRelxyxRA×AyyRA×Axx=y
39 asymref2 RA×ARA×A-1=IRA×AxRA×AxRA×AxxyxRA×AyyRA×Axx=y
40 32 38 39 sylanbrc RPosetRelRA×ARA×A-1=IRA×A
41 inex1g RPosetRelRA×AV
42 isps RA×AVRA×APosetRelRelRA×ARA×ARA×ARA×ARA×ARA×A-1=IRA×A
43 41 42 syl RPosetRelRA×APosetRelRelRA×ARA×ARA×ARA×ARA×ARA×A-1=IRA×A
44 4 7 40 43 mpbir3and RPosetRelRA×APosetRel