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 X. A ) C_ ( R u. ( _I u. `' R ) ) ) )

Proof

Step Hyp Ref Expression
1 df-so 
 |-  ( R Or A <-> ( R Po A /\ A. x e. A A. y e. A ( x R y \/ x = y \/ y R x ) ) )
2 opelxp 
 |-  ( <. x , y >. e. ( A X. A ) <-> ( x e. A /\ y e. A ) )
3 brun 
 |-  ( x ( _I u. `' R ) y <-> ( x _I y \/ x `' R y ) )
4 vex 
 |-  y e. _V
5 4 ideq 
 |-  ( x _I y <-> x = y )
6 vex 
 |-  x e. _V
7 6 4 brcnv 
 |-  ( x `' R y <-> y R x )
8 5 7 orbi12i 
 |-  ( ( x _I y \/ x `' R y ) <-> ( x = y \/ y R x ) )
9 3 8 bitr2i 
 |-  ( ( x = y \/ y R x ) <-> x ( _I u. `' R ) y )
10 9 orbi2i 
 |-  ( ( x R y \/ ( x = y \/ y R x ) ) <-> ( x R y \/ x ( _I u. `' R ) y ) )
11 3orass 
 |-  ( ( x R y \/ x = y \/ y R x ) <-> ( x R y \/ ( x = y \/ y R x ) ) )
12 brun 
 |-  ( x ( R u. ( _I u. `' R ) ) y <-> ( x R y \/ x ( _I u. `' R ) y ) )
13 10 11 12 3bitr4i 
 |-  ( ( x R y \/ x = y \/ y R x ) <-> x ( R u. ( _I u. `' R ) ) y )
14 df-br 
 |-  ( x ( R u. ( _I u. `' R ) ) y <-> <. x , y >. e. ( R u. ( _I u. `' R ) ) )
15 13 14 bitr2i 
 |-  ( <. x , y >. e. ( R u. ( _I u. `' R ) ) <-> ( x R y \/ x = y \/ y R x ) )
16 2 15 imbi12i 
 |-  ( ( <. x , y >. e. ( A X. A ) -> <. x , y >. e. ( R u. ( _I u. `' R ) ) ) <-> ( ( x e. A /\ y e. A ) -> ( x R y \/ x = y \/ y R x ) ) )
17 16 2albii 
 |-  ( A. x A. y ( <. x , y >. e. ( A X. A ) -> <. x , y >. e. ( R u. ( _I u. `' R ) ) ) <-> A. x A. y ( ( x e. A /\ y e. A ) -> ( x R y \/ x = y \/ y R x ) ) )
18 relxp 
 |-  Rel ( A X. A )
19 ssrel 
 |-  ( Rel ( A X. A ) -> ( ( A X. A ) C_ ( R u. ( _I u. `' R ) ) <-> A. x A. y ( <. x , y >. e. ( A X. A ) -> <. x , y >. e. ( R u. ( _I u. `' R ) ) ) ) )
20 18 19 ax-mp 
 |-  ( ( A X. A ) C_ ( R u. ( _I u. `' R ) ) <-> A. x A. y ( <. x , y >. e. ( A X. A ) -> <. x , y >. e. ( R u. ( _I u. `' R ) ) ) )
21 r2al 
 |-  ( A. x e. A A. y e. A ( x R y \/ x = y \/ y R x ) <-> A. x A. y ( ( x e. A /\ y e. A ) -> ( x R y \/ x = y \/ y R x ) ) )
22 17 20 21 3bitr4i 
 |-  ( ( A X. A ) C_ ( R u. ( _I u. `' R ) ) <-> A. x e. A A. y e. A ( x R y \/ x = y \/ y R x ) )
23 22 anbi2i 
 |-  ( ( R Po A /\ ( A X. A ) C_ ( R u. ( _I u. `' R ) ) ) <-> ( R Po A /\ A. x e. A A. y e. A ( x R y \/ x = y \/ y R x ) ) )
24 1 23 bitr4i 
 |-  ( R Or A <-> ( R Po A /\ ( A X. A ) C_ ( R u. ( _I u. `' R ) ) ) )