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 
|- ( R Po A <-> ( R i^i ( A X. A ) ) Po A )

Proof

Step Hyp Ref Expression
1 brinxp 
 |-  ( ( x e. A /\ x e. A ) -> ( x R x <-> x ( R i^i ( A X. A ) ) x ) )
2 1 anidms 
 |-  ( x e. A -> ( x R x <-> x ( R i^i ( A X. A ) ) x ) )
3 2 ad2antrr 
 |-  ( ( ( x e. A /\ y e. A ) /\ z e. A ) -> ( x R x <-> x ( R i^i ( A X. A ) ) x ) )
4 3 notbid 
 |-  ( ( ( x e. A /\ y e. A ) /\ z e. A ) -> ( -. x R x <-> -. x ( R i^i ( A X. A ) ) x ) )
5 brinxp 
 |-  ( ( x e. A /\ y e. A ) -> ( x R y <-> x ( R i^i ( A X. A ) ) y ) )
6 5 adantr 
 |-  ( ( ( x e. A /\ y e. A ) /\ z e. A ) -> ( x R y <-> x ( R i^i ( A X. A ) ) y ) )
7 brinxp 
 |-  ( ( y e. A /\ z e. A ) -> ( y R z <-> y ( R i^i ( A X. A ) ) z ) )
8 7 adantll 
 |-  ( ( ( x e. A /\ y e. A ) /\ z e. A ) -> ( y R z <-> y ( R i^i ( A X. A ) ) z ) )
9 6 8 anbi12d 
 |-  ( ( ( x e. A /\ y e. A ) /\ z e. A ) -> ( ( x R y /\ y R z ) <-> ( x ( R i^i ( A X. A ) ) y /\ y ( R i^i ( A X. A ) ) z ) ) )
10 brinxp 
 |-  ( ( x e. A /\ z e. A ) -> ( x R z <-> x ( R i^i ( A X. A ) ) z ) )
11 10 adantlr 
 |-  ( ( ( x e. A /\ y e. A ) /\ z e. A ) -> ( x R z <-> x ( R i^i ( A X. A ) ) z ) )
12 9 11 imbi12d 
 |-  ( ( ( x e. A /\ y e. A ) /\ z e. A ) -> ( ( ( x R y /\ y R z ) -> x R z ) <-> ( ( x ( R i^i ( A X. A ) ) y /\ y ( R i^i ( A X. A ) ) z ) -> x ( R i^i ( A X. A ) ) z ) ) )
13 4 12 anbi12d 
 |-  ( ( ( x e. A /\ y e. A ) /\ z e. A ) -> ( ( -. x R x /\ ( ( x R y /\ y R z ) -> x R z ) ) <-> ( -. x ( R i^i ( A X. A ) ) x /\ ( ( x ( R i^i ( A X. A ) ) y /\ y ( R i^i ( A X. A ) ) z ) -> x ( R i^i ( A X. A ) ) z ) ) ) )
14 13 ralbidva 
 |-  ( ( x e. A /\ y e. A ) -> ( A. z e. A ( -. x R x /\ ( ( x R y /\ y R z ) -> x R z ) ) <-> A. z e. A ( -. x ( R i^i ( A X. A ) ) x /\ ( ( x ( R i^i ( A X. A ) ) y /\ y ( R i^i ( A X. A ) ) z ) -> x ( R i^i ( A X. A ) ) z ) ) ) )
15 14 ralbidva 
 |-  ( x e. A -> ( A. y e. A A. z e. A ( -. x R x /\ ( ( x R y /\ y R z ) -> x R z ) ) <-> A. y e. A A. z e. A ( -. x ( R i^i ( A X. A ) ) x /\ ( ( x ( R i^i ( A X. A ) ) y /\ y ( R i^i ( A X. A ) ) z ) -> x ( R i^i ( A X. A ) ) z ) ) ) )
16 15 ralbiia 
 |-  ( A. x e. A A. y e. A A. z e. A ( -. x R x /\ ( ( x R y /\ y R z ) -> x R z ) ) <-> A. x e. A A. y e. A A. z e. A ( -. x ( R i^i ( A X. A ) ) x /\ ( ( x ( R i^i ( A X. A ) ) y /\ y ( R i^i ( A X. A ) ) z ) -> x ( R i^i ( A X. A ) ) z ) ) )
17 df-po 
 |-  ( R Po A <-> A. x e. A A. y e. A A. z e. A ( -. x R x /\ ( ( x R y /\ y R z ) -> x R z ) ) )
18 df-po 
 |-  ( ( R i^i ( A X. A ) ) Po A <-> A. x e. A A. y e. A A. z e. A ( -. x ( R i^i ( A X. A ) ) x /\ ( ( x ( R i^i ( A X. A ) ) y /\ y ( R i^i ( A X. A ) ) z ) -> x ( R i^i ( A X. A ) ) z ) ) )
19 16 17 18 3bitr4i 
 |-  ( R Po A <-> ( R i^i ( A X. A ) ) Po A )