Metamath Proof Explorer


Theorem poinxp

Description: Intersection of partial order with Cartesian product of its field. (Contributed by Mario Carneiro, 10-Jul-2014)

Ref Expression
Assertion poinxp RPoARA×APoA

Proof

Step Hyp Ref Expression
1 brinxp xAxAxRxxRA×Ax
2 1 anidms xAxRxxRA×Ax
3 2 ad2antrr xAyAzAxRxxRA×Ax
4 3 notbid xAyAzA¬xRx¬xRA×Ax
5 brinxp xAyAxRyxRA×Ay
6 5 adantr xAyAzAxRyxRA×Ay
7 brinxp yAzAyRzyRA×Az
8 7 adantll xAyAzAyRzyRA×Az
9 6 8 anbi12d xAyAzAxRyyRzxRA×AyyRA×Az
10 brinxp xAzAxRzxRA×Az
11 10 adantlr xAyAzAxRzxRA×Az
12 9 11 imbi12d xAyAzAxRyyRzxRzxRA×AyyRA×AzxRA×Az
13 4 12 anbi12d xAyAzA¬xRxxRyyRzxRz¬xRA×AxxRA×AyyRA×AzxRA×Az
14 13 ralbidva xAyAzA¬xRxxRyyRzxRzzA¬xRA×AxxRA×AyyRA×AzxRA×Az
15 14 ralbidva xAyAzA¬xRxxRyyRzxRzyAzA¬xRA×AxxRA×AyyRA×AzxRA×Az
16 15 ralbiia xAyAzA¬xRxxRyyRzxRzxAyAzA¬xRA×AxxRA×AyyRA×AzxRA×Az
17 df-po RPoAxAyAzA¬xRxxRyyRzxRz
18 df-po RA×APoAxAyAzA¬xRA×AxxRA×AyyRA×AzxRA×Az
19 16 17 18 3bitr4i RPoARA×APoA