Metamath Proof Explorer


Theorem dfso2

Description: Quantifier-free definition of a strict order. (Contributed by Scott Fenton, 22-Feb-2013)

Ref Expression
Assertion dfso2 R Or A R Po A A × A R I R -1

Proof

Step Hyp Ref Expression
1 df-so R Or A R Po A x A y A x R y x = y y R x
2 opelxp x y A × A x A y A
3 brun x I R -1 y x I y x R -1 y
4 vex y V
5 4 ideq x I y x = y
6 vex x V
7 6 4 brcnv x R -1 y y R x
8 5 7 orbi12i x I y x R -1 y x = y y R x
9 3 8 bitr2i x = y y R x x I R -1 y
10 9 orbi2i x R y x = y y R x x R y x I R -1 y
11 3orass x R y x = y y R x x R y x = y y R x
12 brun x R I R -1 y x R y x I R -1 y
13 10 11 12 3bitr4i x R y x = y y R x x R I R -1 y
14 df-br x R I R -1 y x y R I R -1
15 13 14 bitr2i x y R I R -1 x R y x = y y R x
16 2 15 imbi12i x y A × A x y R I R -1 x A y A x R y x = y y R x
17 16 2albii x y x y A × A x y R I R -1 x y x A y A x R y x = y y R x
18 relxp Rel A × A
19 ssrel Rel A × A A × A R I R -1 x y x y A × A x y R I R -1
20 18 19 ax-mp A × A R I R -1 x y x y A × A x y R I R -1
21 r2al x A y A x R y x = y y R x x y x A y A x R y x = y y R x
22 17 20 21 3bitr4i A × A R I R -1 x A y A x R y x = y y R x
23 22 anbi2i R Po A A × A R I R -1 R Po A x A y A x R y x = y y R x
24 1 23 bitr4i R Or A R Po A A × A R I R -1