Metamath Proof Explorer


Theorem psssdm2

Description: Field of a subposet. (Contributed by Mario Carneiro, 9-Sep-2015)

Ref Expression
Hypothesis psssdm.1 X=domR
Assertion psssdm2 RPosetReldomRA×A=XA

Proof

Step Hyp Ref Expression
1 psssdm.1 X=domR
2 dmin domRA×AdomRdomA×A
3 1 eqcomi domR=X
4 dmxpid domA×A=A
5 3 4 ineq12i domRdomA×A=XA
6 2 5 sseqtri domRA×AXA
7 6 a1i RPosetReldomRA×AXA
8 simpr RPosetRelxXAxXA
9 8 elin2d RPosetRelxXAxA
10 elinel1 xXAxX
11 1 psref RPosetRelxXxRx
12 10 11 sylan2 RPosetRelxXAxRx
13 brinxp2 xRA×AxxAxAxRx
14 9 9 12 13 syl21anbrc RPosetRelxXAxRA×Ax
15 vex xV
16 15 15 breldm xRA×AxxdomRA×A
17 14 16 syl RPosetRelxXAxdomRA×A
18 7 17 eqelssd RPosetReldomRA×A=XA