Metamath Proof Explorer

Theorem isprs

Description: Property of being a preordered set. (Contributed by Stefan O'Rear, 31-Jan-2015)

Ref Expression
Hypotheses isprs.b 
|- B = ( Base ` K )
isprs.l 
|- .<_ = ( le ` K )
Assertion isprs 
|- ( K e. Proset <-> ( K e. _V /\ A. x e. B A. y e. B A. z e. B ( x .<_ x /\ ( ( x .<_ y /\ y .<_ z ) -> x .<_ z ) ) ) )

Proof

Step Hyp Ref Expression
1 isprs.b 
 |-  B = ( Base ` K )
2 isprs.l 
 |-  .<_ = ( le ` K )
3 fveq2 
 |-  ( f = K -> ( Base ` f ) = ( Base ` K ) )
4 fveq2 
 |-  ( f = K -> ( le ` f ) = ( le ` K ) )
5 4 sbceq1d 
 |-  ( f = K -> ( [. ( le ` f ) / r ]. A. x e. b A. y e. b A. z e. b ( x r x /\ ( ( x r y /\ y r z ) -> x r z ) ) <-> [. ( le ` K ) / r ]. A. x e. b A. y e. b A. z e. b ( x r x /\ ( ( x r y /\ y r z ) -> x r z ) ) ) )
6 3 5 sbceqbid 
 |-  ( f = K -> ( [. ( Base ` f ) / b ]. [. ( le ` f ) / r ]. A. x e. b A. y e. b A. z e. b ( x r x /\ ( ( x r y /\ y r z ) -> x r z ) ) <-> [. ( Base ` K ) / b ]. [. ( le ` K ) / r ]. A. x e. b A. y e. b A. z e. b ( x r x /\ ( ( x r y /\ y r z ) -> x r z ) ) ) )
7 fvex 
 |-  ( Base ` K ) e. _V
8 fvex 
 |-  ( le ` K ) e. _V
9 eqtr3 
 |-  ( ( b = ( Base ` K ) /\ B = ( Base ` K ) ) -> b = B )
10 1 9 mpan2 
 |-  ( b = ( Base ` K ) -> b = B )
11 raleq 
 |-  ( b = B -> ( A. z e. b ( x r x /\ ( ( x r y /\ y r z ) -> x r z ) ) <-> A. z e. B ( x r x /\ ( ( x r y /\ y r z ) -> x r z ) ) ) )
12 11 raleqbi1dv 
 |-  ( b = B -> ( A. y e. b A. z e. b ( x r x /\ ( ( x r y /\ y r z ) -> x r z ) ) <-> A. y e. B A. z e. B ( x r x /\ ( ( x r y /\ y r z ) -> x r z ) ) ) )
13 12 raleqbi1dv 
 |-  ( b = B -> ( A. x e. b A. y e. b A. z e. b ( x r x /\ ( ( x r y /\ y r z ) -> x r z ) ) <-> A. x e. B A. y e. B A. z e. B ( x r x /\ ( ( x r y /\ y r z ) -> x r z ) ) ) )
14 10 13 syl 
 |-  ( b = ( Base ` K ) -> ( A. x e. b A. y e. b A. z e. b ( x r x /\ ( ( x r y /\ y r z ) -> x r z ) ) <-> A. x e. B A. y e. B A. z e. B ( x r x /\ ( ( x r y /\ y r z ) -> x r z ) ) ) )
15 eqtr3 
 |-  ( ( r = ( le ` K ) /\ .<_ = ( le ` K ) ) -> r = .<_ )
16 2 15 mpan2 
 |-  ( r = ( le ` K ) -> r = .<_ )
17 breq 
 |-  ( r = .<_ -> ( x r x <-> x .<_ x ) )
18 breq 
 |-  ( r = .<_ -> ( x r y <-> x .<_ y ) )
19 breq 
 |-  ( r = .<_ -> ( y r z <-> y .<_ z ) )
20 18 19 anbi12d 
 |-  ( r = .<_ -> ( ( x r y /\ y r z ) <-> ( x .<_ y /\ y .<_ z ) ) )
21 breq 
 |-  ( r = .<_ -> ( x r z <-> x .<_ z ) )
22 20 21 imbi12d 
 |-  ( r = .<_ -> ( ( ( x r y /\ y r z ) -> x r z ) <-> ( ( x .<_ y /\ y .<_ z ) -> x .<_ z ) ) )
23 17 22 anbi12d 
 |-  ( r = .<_ -> ( ( x r x /\ ( ( x r y /\ y r z ) -> x r z ) ) <-> ( x .<_ x /\ ( ( x .<_ y /\ y .<_ z ) -> x .<_ z ) ) ) )
24 23 ralbidv 
 |-  ( r = .<_ -> ( A. z e. B ( x r x /\ ( ( x r y /\ y r z ) -> x r z ) ) <-> A. z e. B ( x .<_ x /\ ( ( x .<_ y /\ y .<_ z ) -> x .<_ z ) ) ) )
25 24 2ralbidv 
 |-  ( r = .<_ -> ( A. x e. B A. y e. B A. z e. B ( x r x /\ ( ( x r y /\ y r z ) -> x r z ) ) <-> A. x e. B A. y e. B A. z e. B ( x .<_ x /\ ( ( x .<_ y /\ y .<_ z ) -> x .<_ z ) ) ) )
26 16 25 syl 
 |-  ( r = ( le ` K ) -> ( A. x e. B A. y e. B A. z e. B ( x r x /\ ( ( x r y /\ y r z ) -> x r z ) ) <-> A. x e. B A. y e. B A. z e. B ( x .<_ x /\ ( ( x .<_ y /\ y .<_ z ) -> x .<_ z ) ) ) )
27 14 26 sylan9bb 
 |-  ( ( b = ( Base ` K ) /\ r = ( le ` K ) ) -> ( A. x e. b A. y e. b A. z e. b ( x r x /\ ( ( x r y /\ y r z ) -> x r z ) ) <-> A. x e. B A. y e. B A. z e. B ( x .<_ x /\ ( ( x .<_ y /\ y .<_ z ) -> x .<_ z ) ) ) )
28 7 8 27 sbc2ie 
 |-  ( [. ( Base ` K ) / b ]. [. ( le ` K ) / r ]. A. x e. b A. y e. b A. z e. b ( x r x /\ ( ( x r y /\ y r z ) -> x r z ) ) <-> A. x e. B A. y e. B A. z e. B ( x .<_ x /\ ( ( x .<_ y /\ y .<_ z ) -> x .<_ z ) ) )
29 6 28 bitrdi 
 |-  ( f = K -> ( [. ( Base ` f ) / b ]. [. ( le ` f ) / r ]. A. x e. b A. y e. b A. z e. b ( x r x /\ ( ( x r y /\ y r z ) -> x r z ) ) <-> A. x e. B A. y e. B A. z e. B ( x .<_ x /\ ( ( x .<_ y /\ y .<_ z ) -> x .<_ z ) ) ) )
30 df-proset 
 |-  Proset = { f | [. ( Base ` f ) / b ]. [. ( le ` f ) / r ]. A. x e. b A. y e. b A. z e. b ( x r x /\ ( ( x r y /\ y r z ) -> x r z ) ) }
31 29 30 elab4g 
 |-  ( K e. Proset <-> ( K e. _V /\ A. x e. B A. y e. B A. z e. B ( x .<_ x /\ ( ( x .<_ y /\ y .<_ z ) -> x .<_ z ) ) ) )