Metamath Proof Explorer

Theorem isdrs

Description: Property of being a directed set. (Contributed by Stefan O'Rear, 1-Feb-2015)

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

Proof

Step Hyp Ref Expression
1 isdrs.b 
 |-  B = ( Base ` K )
2 isdrs.l 
 |-  .<_ = ( le ` K )
3 fveq2 
 |-  ( f = K -> ( Base ` f ) = ( Base ` K ) )
4 3 1 eqtr4di 
 |-  ( f = K -> ( Base ` f ) = B )
5 fveq2 
 |-  ( f = K -> ( le ` f ) = ( le ` K ) )
6 5 2 eqtr4di 
 |-  ( f = K -> ( le ` f ) = .<_ )
7 6 sbceq1d 
 |-  ( f = K -> ( [. ( le ` f ) / r ]. ( b =/= (/) /\ A. x e. b A. y e. b E. z e. b ( x r z /\ y r z ) ) <-> [. .<_ / r ]. ( b =/= (/) /\ A. x e. b A. y e. b E. z e. b ( x r z /\ y r z ) ) ) )
8 4 7 sbceqbid 
 |-  ( f = K -> ( [. ( Base ` f ) / b ]. [. ( le ` f ) / r ]. ( b =/= (/) /\ A. x e. b A. y e. b E. z e. b ( x r z /\ y r z ) ) <-> [. B / b ]. [. .<_ / r ]. ( b =/= (/) /\ A. x e. b A. y e. b E. z e. b ( x r z /\ y r z ) ) ) )
9 1 fvexi 
 |-  B e. _V
10 2 fvexi 
 |-  .<_ e. _V
11 neeq1 
 |-  ( b = B -> ( b =/= (/) <-> B =/= (/) ) )
12 11 adantr 
 |-  ( ( b = B /\ r = .<_ ) -> ( b =/= (/) <-> B =/= (/) ) )
13 rexeq 
 |-  ( b = B -> ( E. z e. b ( x r z /\ y r z ) <-> E. z e. B ( x r z /\ y r z ) ) )
14 13 raleqbi1dv 
 |-  ( b = B -> ( A. y e. b E. z e. b ( x r z /\ y r z ) <-> A. y e. B E. z e. B ( x r z /\ y r z ) ) )
15 14 raleqbi1dv 
 |-  ( b = B -> ( A. x e. b A. y e. b E. z e. b ( x r z /\ y r z ) <-> A. x e. B A. y e. B E. z e. B ( x r z /\ y r z ) ) )
16 breq 
 |-  ( r = .<_ -> ( x r z <-> x .<_ z ) )
17 breq 
 |-  ( r = .<_ -> ( y r z <-> y .<_ z ) )
18 16 17 anbi12d 
 |-  ( r = .<_ -> ( ( x r z /\ y r z ) <-> ( x .<_ z /\ y .<_ z ) ) )
19 18 rexbidv 
 |-  ( r = .<_ -> ( E. z e. B ( x r z /\ y r z ) <-> E. z e. B ( x .<_ z /\ y .<_ z ) ) )
20 19 2ralbidv 
 |-  ( r = .<_ -> ( A. x e. B A. y e. B E. z e. B ( x r z /\ y r z ) <-> A. x e. B A. y e. B E. z e. B ( x .<_ z /\ y .<_ z ) ) )
21 15 20 sylan9bb 
 |-  ( ( b = B /\ r = .<_ ) -> ( A. x e. b A. y e. b E. z e. b ( x r z /\ y r z ) <-> A. x e. B A. y e. B E. z e. B ( x .<_ z /\ y .<_ z ) ) )
22 12 21 anbi12d 
 |-  ( ( b = B /\ r = .<_ ) -> ( ( b =/= (/) /\ A. x e. b A. y e. b E. z e. b ( x r z /\ y r z ) ) <-> ( B =/= (/) /\ A. x e. B A. y e. B E. z e. B ( x .<_ z /\ y .<_ z ) ) ) )
23 9 10 22 sbc2ie 
 |-  ( [. B / b ]. [. .<_ / r ]. ( b =/= (/) /\ A. x e. b A. y e. b E. z e. b ( x r z /\ y r z ) ) <-> ( B =/= (/) /\ A. x e. B A. y e. B E. z e. B ( x .<_ z /\ y .<_ z ) ) )
24 8 23 bitrdi 
 |-  ( f = K -> ( [. ( Base ` f ) / b ]. [. ( le ` f ) / r ]. ( b =/= (/) /\ A. x e. b A. y e. b E. z e. b ( x r z /\ y r z ) ) <-> ( B =/= (/) /\ A. x e. B A. y e. B E. z e. B ( x .<_ z /\ y .<_ z ) ) ) )
25 df-drs 
 |-  Dirset = { f e. Proset | [. ( Base ` f ) / b ]. [. ( le ` f ) / r ]. ( b =/= (/) /\ A. x e. b A. y e. b E. z e. b ( x r z /\ y r z ) ) }
26 24 25 elrab2 
 |-  ( K e. Dirset <-> ( K e. Proset /\ ( B =/= (/) /\ A. x e. B A. y e. B E. z e. B ( x .<_ z /\ y .<_ z ) ) ) )
27 3anass 
 |-  ( ( K e. Proset /\ B =/= (/) /\ A. x e. B A. y e. B E. z e. B ( x .<_ z /\ y .<_ z ) ) <-> ( K e. Proset /\ ( B =/= (/) /\ A. x e. B A. y e. B E. z e. B ( x .<_ z /\ y .<_ z ) ) ) )
28 26 27 bitr4i 
 |-  ( K e. Dirset <-> ( K e. Proset /\ B =/= (/) /\ A. x e. B A. y e. B E. z e. B ( x .<_ z /\ y .<_ z ) ) )