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 ) ) ) )