Metamath Proof Explorer

Theorem ispos

Description: The predicate "is a poset." (Contributed by NM, 18-Oct-2012) (Revised by Mario Carneiro, 4-Nov-2013)

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

Proof

Step Hyp Ref Expression
1 ispos.b 
 |-  B = ( Base ` K )
2 ispos.l 
 |-  .<_ = ( le ` K )
3 fveq2 
 |-  ( p = K -> ( Base ` p ) = ( Base ` K ) )
4 3 1 eqtr4di 
 |-  ( p = K -> ( Base ` p ) = B )
5 4 eqeq2d 
 |-  ( p = K -> ( b = ( Base ` p ) <-> b = B ) )
6 fveq2 
 |-  ( p = K -> ( le ` p ) = ( le ` K ) )
7 6 2 eqtr4di 
 |-  ( p = K -> ( le ` p ) = .<_ )
8 7 eqeq2d 
 |-  ( p = K -> ( r = ( le ` p ) <-> r = .<_ ) )
9 5 8 3anbi12d 
 |-  ( p = K -> ( ( b = ( Base ` p ) /\ r = ( le ` p ) /\ A. x e. b A. y e. b A. z e. b ( x r x /\ ( ( x r y /\ y r x ) -> x = y ) /\ ( ( x r y /\ y r z ) -> x r z ) ) ) <-> ( b = B /\ r = .<_ /\ A. x e. b A. y e. b A. z e. b ( x r x /\ ( ( x r y /\ y r x ) -> x = y ) /\ ( ( x r y /\ y r z ) -> x r z ) ) ) ) )
10 9 2exbidv 
 |-  ( p = K -> ( E. b E. r ( b = ( Base ` p ) /\ r = ( le ` p ) /\ A. x e. b A. y e. b A. z e. b ( x r x /\ ( ( x r y /\ y r x ) -> x = y ) /\ ( ( x r y /\ y r z ) -> x r z ) ) ) <-> E. b E. r ( b = B /\ r = .<_ /\ A. x e. b A. y e. b A. z e. b ( x r x /\ ( ( x r y /\ y r x ) -> x = y ) /\ ( ( x r y /\ y r z ) -> x r z ) ) ) ) )
11 df-poset 
 |-  Poset = { p | E. b E. r ( b = ( Base ` p ) /\ r = ( le ` p ) /\ A. x e. b A. y e. b A. z e. b ( x r x /\ ( ( x r y /\ y r x ) -> x = y ) /\ ( ( x r y /\ y r z ) -> x r z ) ) ) }
12 10 11 elab4g 
 |-  ( K e. Poset <-> ( K e. _V /\ E. b E. r ( b = B /\ r = .<_ /\ A. x e. b A. y e. b A. z e. b ( x r x /\ ( ( x r y /\ y r x ) -> x = y ) /\ ( ( x r y /\ y r z ) -> x r z ) ) ) ) )
13 1 fvexi 
 |-  B e. _V
14 2 fvexi 
 |-  .<_ e. _V
15 raleq 
 |-  ( b = B -> ( A. z e. b ( x r x /\ ( ( x r y /\ y r x ) -> x = y ) /\ ( ( x r y /\ y r z ) -> x r z ) ) <-> A. z e. B ( x r x /\ ( ( x r y /\ y r x ) -> x = y ) /\ ( ( x r y /\ y r z ) -> x r z ) ) ) )
16 15 raleqbi1dv 
 |-  ( b = B -> ( A. y e. b A. z e. b ( x r x /\ ( ( x r y /\ y r x ) -> x = y ) /\ ( ( 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 x ) -> x = y ) /\ ( ( x r y /\ y r z ) -> x r z ) ) ) )
17 16 raleqbi1dv 
 |-  ( b = B -> ( A. x e. b A. y e. b A. z e. b ( x r x /\ ( ( x r y /\ y r x ) -> x = y ) /\ ( ( 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 x ) -> x = y ) /\ ( ( x r y /\ y r z ) -> x r z ) ) ) )
18 breq 
 |-  ( r = .<_ -> ( x r x <-> x .<_ x ) )
19 breq 
 |-  ( r = .<_ -> ( x r y <-> x .<_ y ) )
20 breq 
 |-  ( r = .<_ -> ( y r x <-> y .<_ x ) )
21 19 20 anbi12d 
 |-  ( r = .<_ -> ( ( x r y /\ y r x ) <-> ( x .<_ y /\ y .<_ x ) ) )
22 21 imbi1d 
 |-  ( r = .<_ -> ( ( ( x r y /\ y r x ) -> x = y ) <-> ( ( x .<_ y /\ y .<_ x ) -> x = y ) ) )
23 breq 
 |-  ( r = .<_ -> ( y r z <-> y .<_ z ) )
24 19 23 anbi12d 
 |-  ( r = .<_ -> ( ( x r y /\ y r z ) <-> ( x .<_ y /\ y .<_ z ) ) )
25 breq 
 |-  ( r = .<_ -> ( x r z <-> x .<_ z ) )
26 24 25 imbi12d 
 |-  ( r = .<_ -> ( ( ( x r y /\ y r z ) -> x r z ) <-> ( ( x .<_ y /\ y .<_ z ) -> x .<_ z ) ) )
27 18 22 26 3anbi123d 
 |-  ( r = .<_ -> ( ( x r x /\ ( ( x r y /\ y r x ) -> x = y ) /\ ( ( x r y /\ y r z ) -> x r z ) ) <-> ( x .<_ x /\ ( ( x .<_ y /\ y .<_ x ) -> x = y ) /\ ( ( x .<_ y /\ y .<_ z ) -> x .<_ z ) ) ) )
28 27 ralbidv 
 |-  ( r = .<_ -> ( A. z e. B ( x r x /\ ( ( x r y /\ y r x ) -> x = y ) /\ ( ( x r y /\ y r z ) -> x r z ) ) <-> A. z e. B ( x .<_ x /\ ( ( x .<_ y /\ y .<_ x ) -> x = y ) /\ ( ( x .<_ y /\ y .<_ z ) -> x .<_ z ) ) ) )
29 28 2ralbidv 
 |-  ( r = .<_ -> ( A. x e. B A. y e. B A. z e. B ( x r x /\ ( ( x r y /\ y r x ) -> x = y ) /\ ( ( 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 .<_ x ) -> x = y ) /\ ( ( x .<_ y /\ y .<_ z ) -> x .<_ z ) ) ) )
30 13 14 17 29 ceqsex2v 
 |-  ( E. b E. r ( b = B /\ r = .<_ /\ A. x e. b A. y e. b A. z e. b ( x r x /\ ( ( x r y /\ y r x ) -> x = y ) /\ ( ( 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 .<_ x ) -> x = y ) /\ ( ( x .<_ y /\ y .<_ z ) -> x .<_ z ) ) )
31 30 anbi2i 
 |-  ( ( K e. _V /\ E. b E. r ( b = B /\ r = .<_ /\ A. x e. b A. y e. b A. z e. b ( x r x /\ ( ( x r y /\ y r x ) -> x = y ) /\ ( ( x r y /\ y r z ) -> x r z ) ) ) ) <-> ( K e. _V /\ A. x e. B A. y e. B A. z e. B ( x .<_ x /\ ( ( x .<_ y /\ y .<_ x ) -> x = y ) /\ ( ( x .<_ y /\ y .<_ z ) -> x .<_ z ) ) ) )
32 12 31 bitri 
 |-  ( K e. Poset <-> ( K e. _V /\ A. x e. B A. y e. B A. z e. B ( x .<_ x /\ ( ( x .<_ y /\ y .<_ x ) -> x = y ) /\ ( ( x .<_ y /\ y .<_ z ) -> x .<_ z ) ) ) )