Metamath Proof Explorer


Theorem soinxp

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

Ref Expression
Assertion soinxp R Or A R A × A Or A

Proof

Step Hyp Ref Expression
1 poinxp R Po A R A × A Po A
2 brinxp x A y A x R y x R A × A y
3 biidd x A y A x = y x = y
4 brinxp y A x A y R x y R A × A x
5 4 ancoms x A y A y R x y R A × A x
6 2 3 5 3orbi123d x A y A x R y x = y y R x x R A × A y x = y y R A × A x
7 6 ralbidva x A y A x R y x = y y R x y A x R A × A y x = y y R A × A x
8 7 ralbiia x A y A x R y x = y y R x x A y A x R A × A y x = y y R A × A x
9 1 8 anbi12i R Po A x A y A x R y x = y y R x R A × A Po A x A y A x R A × A y x = y y R A × A x
10 df-so R Or A R Po A x A y A x R y x = y y R x
11 df-so R A × A Or A R A × A Po A x A y A x R A × A y x = y y R A × A x
12 9 10 11 3bitr4i R Or A R A × A Or A