Metamath Proof Explorer

Theorem dfso3

Description: Expansion of the definition of a strict order. (Contributed by Scott Fenton, 6-Jun-2016)

Ref Expression
Assertion dfso3 
|- ( R Or 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 ) /\ ( x R y \/ x = y \/ y R x ) ) )

Proof

Step Hyp Ref Expression
1 ne0i 
 |-  ( y e. A -> A =/= (/) )
2 r19.27zv 
 |-  ( A =/= (/) -> ( A. z e. A ( ( -. x R x /\ ( ( x R y /\ y R z ) -> x R z ) ) /\ ( x R y \/ x = y \/ y R x ) ) <-> ( A. z e. A ( -. x R x /\ ( ( x R y /\ y R z ) -> x R z ) ) /\ ( x R y \/ x = y \/ y R x ) ) ) )
3 1 2 syl 
 |-  ( y e. A -> ( A. z e. A ( ( -. x R x /\ ( ( x R y /\ y R z ) -> x R z ) ) /\ ( x R y \/ x = y \/ y R x ) ) <-> ( A. z e. A ( -. x R x /\ ( ( x R y /\ y R z ) -> x R z ) ) /\ ( x R y \/ x = y \/ y R x ) ) ) )
4 3 ralbiia 
 |-  ( A. y e. A A. z e. A ( ( -. x R x /\ ( ( x R y /\ y R z ) -> x R z ) ) /\ ( x R y \/ x = y \/ y R x ) ) <-> A. y e. A ( A. z e. A ( -. x R x /\ ( ( x R y /\ y R z ) -> x R z ) ) /\ ( x R y \/ x = y \/ y R x ) ) )
5 4 ralbii 
 |-  ( A. x e. A A. y e. A A. z e. A ( ( -. x R x /\ ( ( x R y /\ y R z ) -> x R z ) ) /\ ( x R y \/ x = y \/ y R x ) ) <-> A. x e. A A. y e. A ( A. z e. A ( -. x R x /\ ( ( x R y /\ y R z ) -> x R z ) ) /\ ( x R y \/ x = y \/ y R x ) ) )
6 df-3an 
 |-  ( ( -. x R x /\ ( ( x R y /\ y R z ) -> x R z ) /\ ( x R y \/ x = y \/ y R x ) ) <-> ( ( -. x R x /\ ( ( x R y /\ y R z ) -> x R z ) ) /\ ( x R y \/ x = y \/ y R x ) ) )
7 6 ralbii 
 |-  ( A. z e. A ( -. x R x /\ ( ( x R y /\ y R z ) -> x R z ) /\ ( x R y \/ x = y \/ y R x ) ) <-> A. z e. A ( ( -. x R x /\ ( ( x R y /\ y R z ) -> x R z ) ) /\ ( x R y \/ x = y \/ y R x ) ) )
8 7 2ralbii 
 |-  ( A. x e. A A. y e. A A. z e. A ( -. x R x /\ ( ( x R y /\ y R z ) -> x R z ) /\ ( x R y \/ x = y \/ y R x ) ) <-> A. x e. A A. y e. A A. z e. A ( ( -. x R x /\ ( ( x R y /\ y R z ) -> x R z ) ) /\ ( x R y \/ x = y \/ y R x ) ) )
9 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 ) ) )
10 9 anbi1i 
 |-  ( ( R Po A /\ A. x e. A A. y e. A ( x R y \/ x = y \/ y R x ) ) <-> ( 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 ( x R y \/ x = y \/ y R x ) ) )
11 df-so 
 |-  ( R Or A <-> ( R Po A /\ A. x e. A A. y e. A ( x R y \/ x = y \/ y R x ) ) )
12 r19.26-2 
 |-  ( A. x e. A A. y e. A ( A. z e. A ( -. x R x /\ ( ( x R y /\ y R z ) -> x R z ) ) /\ ( x R y \/ x = y \/ y R x ) ) <-> ( 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 ( x R y \/ x = y \/ y R x ) ) )
13 10 11 12 3bitr4i 
 |-  ( R Or 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 ) ) /\ ( x R y \/ x = y \/ y R x ) ) )
14 5 8 13 3bitr4ri 
 |-  ( R Or 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 ) /\ ( x R y \/ x = y \/ y R x ) ) )