Metamath Proof Explorer

Theorem istos

Description: The predicate "is a toset". (Contributed by FL, 17-Nov-2014)

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

Proof

Step Hyp Ref Expression
1 istos.b 
 |-  B = ( Base ` K )
2 istos.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 ( x r y \/ y r x ) <-> [. ( le ` K ) / r ]. A. x e. b A. y e. b ( x r y \/ y r x ) ) )
6 3 5 sbceqbid 
 |-  ( f = K -> ( [. ( Base ` f ) / b ]. [. ( le ` f ) / r ]. A. x e. b A. y e. b ( x r y \/ y r x ) <-> [. ( Base ` K ) / b ]. [. ( le ` K ) / r ]. A. x e. b A. y e. b ( x r y \/ y r x ) ) )
7 fvex 
 |-  ( Base ` K ) e. _V
8 fvex 
 |-  ( le ` K ) e. _V
9 eqtr 
 |-  ( ( b = ( Base ` K ) /\ ( Base ` K ) = B ) -> b = B )
10 eqtr 
 |-  ( ( r = ( le ` K ) /\ ( le ` K ) = .<_ ) -> r = .<_ )
11 breq 
 |-  ( r = .<_ -> ( x r y <-> x .<_ y ) )
12 breq 
 |-  ( r = .<_ -> ( y r x <-> y .<_ x ) )
13 11 12 orbi12d 
 |-  ( r = .<_ -> ( ( x r y \/ y r x ) <-> ( x .<_ y \/ y .<_ x ) ) )
14 13 2ralbidv 
 |-  ( r = .<_ -> ( A. x e. b A. y e. b ( x r y \/ y r x ) <-> A. x e. b A. y e. b ( x .<_ y \/ y .<_ x ) ) )
15 raleq 
 |-  ( b = B -> ( A. y e. b ( x .<_ y \/ y .<_ x ) <-> A. y e. B ( x .<_ y \/ y .<_ x ) ) )
16 15 raleqbi1dv 
 |-  ( b = B -> ( A. x e. b A. y e. b ( x .<_ y \/ y .<_ x ) <-> A. x e. B A. y e. B ( x .<_ y \/ y .<_ x ) ) )
17 14 16 sylan9bb 
 |-  ( ( r = .<_ /\ b = B ) -> ( A. x e. b A. y e. b ( x r y \/ y r x ) <-> A. x e. B A. y e. B ( x .<_ y \/ y .<_ x ) ) )
18 17 ex 
 |-  ( r = .<_ -> ( b = B -> ( A. x e. b A. y e. b ( x r y \/ y r x ) <-> A. x e. B A. y e. B ( x .<_ y \/ y .<_ x ) ) ) )
19 10 18 syl 
 |-  ( ( r = ( le ` K ) /\ ( le ` K ) = .<_ ) -> ( b = B -> ( A. x e. b A. y e. b ( x r y \/ y r x ) <-> A. x e. B A. y e. B ( x .<_ y \/ y .<_ x ) ) ) )
20 19 expcom 
 |-  ( ( le ` K ) = .<_ -> ( r = ( le ` K ) -> ( b = B -> ( A. x e. b A. y e. b ( x r y \/ y r x ) <-> A. x e. B A. y e. B ( x .<_ y \/ y .<_ x ) ) ) ) )
21 20 eqcoms 
 |-  ( .<_ = ( le ` K ) -> ( r = ( le ` K ) -> ( b = B -> ( A. x e. b A. y e. b ( x r y \/ y r x ) <-> A. x e. B A. y e. B ( x .<_ y \/ y .<_ x ) ) ) ) )
22 2 21 ax-mp 
 |-  ( r = ( le ` K ) -> ( b = B -> ( A. x e. b A. y e. b ( x r y \/ y r x ) <-> A. x e. B A. y e. B ( x .<_ y \/ y .<_ x ) ) ) )
23 9 22 syl5com 
 |-  ( ( b = ( Base ` K ) /\ ( Base ` K ) = B ) -> ( r = ( le ` K ) -> ( A. x e. b A. y e. b ( x r y \/ y r x ) <-> A. x e. B A. y e. B ( x .<_ y \/ y .<_ x ) ) ) )
24 23 expcom 
 |-  ( ( Base ` K ) = B -> ( b = ( Base ` K ) -> ( r = ( le ` K ) -> ( A. x e. b A. y e. b ( x r y \/ y r x ) <-> A. x e. B A. y e. B ( x .<_ y \/ y .<_ x ) ) ) ) )
25 24 eqcoms 
 |-  ( B = ( Base ` K ) -> ( b = ( Base ` K ) -> ( r = ( le ` K ) -> ( A. x e. b A. y e. b ( x r y \/ y r x ) <-> A. x e. B A. y e. B ( x .<_ y \/ y .<_ x ) ) ) ) )
26 1 25 ax-mp 
 |-  ( b = ( Base ` K ) -> ( r = ( le ` K ) -> ( A. x e. b A. y e. b ( x r y \/ y r x ) <-> A. x e. B A. y e. B ( x .<_ y \/ y .<_ x ) ) ) )
27 26 imp 
 |-  ( ( b = ( Base ` K ) /\ r = ( le ` K ) ) -> ( A. x e. b A. y e. b ( x r y \/ y r x ) <-> A. x e. B A. y e. B ( x .<_ y \/ y .<_ x ) ) )
28 7 8 27 sbc2ie 
 |-  ( [. ( Base ` K ) / b ]. [. ( le ` K ) / r ]. A. x e. b A. y e. b ( x r y \/ y r x ) <-> A. x e. B A. y e. B ( x .<_ y \/ y .<_ x ) )
29 6 28 bitrdi 
 |-  ( f = K -> ( [. ( Base ` f ) / b ]. [. ( le ` f ) / r ]. A. x e. b A. y e. b ( x r y \/ y r x ) <-> A. x e. B A. y e. B ( x .<_ y \/ y .<_ x ) ) )
30 df-toset 
 |-  Toset = { f e. Poset | [. ( Base ` f ) / b ]. [. ( le ` f ) / r ]. A. x e. b A. y e. b ( x r y \/ y r x ) }
31 29 30 elrab2 
 |-  ( K e. Toset <-> ( K e. Poset /\ A. x e. B A. y e. B ( x .<_ y \/ y .<_ x ) ) )