Description: Intersection of partial order with Cartesian product of its field. (Contributed by Mario Carneiro, 10-Jul-2014)
Ref | Expression | ||
---|---|---|---|
Assertion | poinxp | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | brinxp | |
|
2 | 1 | anidms | |
3 | 2 | ad2antrr | |
4 | 3 | notbid | |
5 | brinxp | |
|
6 | 5 | adantr | |
7 | brinxp | |
|
8 | 7 | adantll | |
9 | 6 8 | anbi12d | |
10 | brinxp | |
|
11 | 10 | adantlr | |
12 | 9 11 | imbi12d | |
13 | 4 12 | anbi12d | |
14 | 13 | ralbidva | |
15 | 14 | ralbidva | |
16 | 15 | ralbiia | |
17 | df-po | |
|
18 | df-po | |
|
19 | 16 17 18 | 3bitr4i | |