Metamath Proof Explorer

Theorem isdrs2

Description: Directed sets may be defined in terms of finite subsets. Again, without nonemptiness we would need to restrict to nonempty subsets here. (Contributed by Stefan O'Rear, 1-Feb-2015)

Ref Expression
Hypotheses drsbn0.b 
|- B = ( Base ` K )
drsdirfi.l 
|- .<_ = ( le ` K )
Assertion isdrs2 
|- ( K e. Dirset <-> ( K e. Proset /\ A. x e. ( ~P B i^i Fin ) E. y e. B A. z e. x z .<_ y ) )

Proof

Step Hyp Ref Expression
1 drsbn0.b 
 |-  B = ( Base ` K )
2 drsdirfi.l 
 |-  .<_ = ( le ` K )
3 drsprs 
 |-  ( K e. Dirset -> K e. Proset )
4 simpl 
 |-  ( ( K e. Dirset /\ x e. ( ~P B i^i Fin ) ) -> K e. Dirset )
5 elinel1 
 |-  ( x e. ( ~P B i^i Fin ) -> x e. ~P B )
6 5 elpwid 
 |-  ( x e. ( ~P B i^i Fin ) -> x C_ B )
7 6 adantl 
 |-  ( ( K e. Dirset /\ x e. ( ~P B i^i Fin ) ) -> x C_ B )
8 elinel2 
 |-  ( x e. ( ~P B i^i Fin ) -> x e. Fin )
9 8 adantl 
 |-  ( ( K e. Dirset /\ x e. ( ~P B i^i Fin ) ) -> x e. Fin )
10 1 2 drsdirfi 
 |-  ( ( K e. Dirset /\ x C_ B /\ x e. Fin ) -> E. y e. B A. z e. x z .<_ y )
11 4 7 9 10 syl3anc 
 |-  ( ( K e. Dirset /\ x e. ( ~P B i^i Fin ) ) -> E. y e. B A. z e. x z .<_ y )
12 11 ralrimiva 
 |-  ( K e. Dirset -> A. x e. ( ~P B i^i Fin ) E. y e. B A. z e. x z .<_ y )
13 3 12 jca 
 |-  ( K e. Dirset -> ( K e. Proset /\ A. x e. ( ~P B i^i Fin ) E. y e. B A. z e. x z .<_ y ) )
14 simpl 
 |-  ( ( K e. Proset /\ A. x e. ( ~P B i^i Fin ) E. y e. B A. z e. x z .<_ y ) -> K e. Proset )
15 0elpw 
 |-  (/) e. ~P B
16 0fin 
 |-  (/) e. Fin
17 15 16 elini 
 |-  (/) e. ( ~P B i^i Fin )
18 raleq 
 |-  ( x = (/) -> ( A. z e. x z .<_ y <-> A. z e. (/) z .<_ y ) )
19 18 rexbidv 
 |-  ( x = (/) -> ( E. y e. B A. z e. x z .<_ y <-> E. y e. B A. z e. (/) z .<_ y ) )
20 19 rspcv 
 |-  ( (/) e. ( ~P B i^i Fin ) -> ( A. x e. ( ~P B i^i Fin ) E. y e. B A. z e. x z .<_ y -> E. y e. B A. z e. (/) z .<_ y ) )
21 17 20 ax-mp 
 |-  ( A. x e. ( ~P B i^i Fin ) E. y e. B A. z e. x z .<_ y -> E. y e. B A. z e. (/) z .<_ y )
22 rexn0 
 |-  ( E. y e. B A. z e. (/) z .<_ y -> B =/= (/) )
23 21 22 syl 
 |-  ( A. x e. ( ~P B i^i Fin ) E. y e. B A. z e. x z .<_ y -> B =/= (/) )
24 23 adantl 
 |-  ( ( K e. Proset /\ A. x e. ( ~P B i^i Fin ) E. y e. B A. z e. x z .<_ y ) -> B =/= (/) )
25 raleq 
 |-  ( x = { a , b } -> ( A. z e. x z .<_ y <-> A. z e. { a , b } z .<_ y ) )
26 25 rexbidv 
 |-  ( x = { a , b } -> ( E. y e. B A. z e. x z .<_ y <-> E. y e. B A. z e. { a , b } z .<_ y ) )
27 simplr 
 |-  ( ( ( K e. Proset /\ A. x e. ( ~P B i^i Fin ) E. y e. B A. z e. x z .<_ y ) /\ ( a e. B /\ b e. B ) ) -> A. x e. ( ~P B i^i Fin ) E. y e. B A. z e. x z .<_ y )
28 prelpwi 
 |-  ( ( a e. B /\ b e. B ) -> { a , b } e. ~P B )
29 prfi 
 |-  { a , b } e. Fin
30 29 a1i 
 |-  ( ( a e. B /\ b e. B ) -> { a , b } e. Fin )
31 28 30 elind 
 |-  ( ( a e. B /\ b e. B ) -> { a , b } e. ( ~P B i^i Fin ) )
32 31 adantl 
 |-  ( ( ( K e. Proset /\ A. x e. ( ~P B i^i Fin ) E. y e. B A. z e. x z .<_ y ) /\ ( a e. B /\ b e. B ) ) -> { a , b } e. ( ~P B i^i Fin ) )
33 26 27 32 rspcdva 
 |-  ( ( ( K e. Proset /\ A. x e. ( ~P B i^i Fin ) E. y e. B A. z e. x z .<_ y ) /\ ( a e. B /\ b e. B ) ) -> E. y e. B A. z e. { a , b } z .<_ y )
34 vex 
 |-  a e. _V
35 vex 
 |-  b e. _V
36 breq1 
 |-  ( z = a -> ( z .<_ y <-> a .<_ y ) )
37 breq1 
 |-  ( z = b -> ( z .<_ y <-> b .<_ y ) )
38 34 35 36 37 ralpr 
 |-  ( A. z e. { a , b } z .<_ y <-> ( a .<_ y /\ b .<_ y ) )
39 38 rexbii 
 |-  ( E. y e. B A. z e. { a , b } z .<_ y <-> E. y e. B ( a .<_ y /\ b .<_ y ) )
40 33 39 sylib 
 |-  ( ( ( K e. Proset /\ A. x e. ( ~P B i^i Fin ) E. y e. B A. z e. x z .<_ y ) /\ ( a e. B /\ b e. B ) ) -> E. y e. B ( a .<_ y /\ b .<_ y ) )
41 40 ralrimivva 
 |-  ( ( K e. Proset /\ A. x e. ( ~P B i^i Fin ) E. y e. B A. z e. x z .<_ y ) -> A. a e. B A. b e. B E. y e. B ( a .<_ y /\ b .<_ y ) )
42 1 2 isdrs 
 |-  ( K e. Dirset <-> ( K e. Proset /\ B =/= (/) /\ A. a e. B A. b e. B E. y e. B ( a .<_ y /\ b .<_ y ) ) )
43 14 24 41 42 syl3anbrc 
 |-  ( ( K e. Proset /\ A. x e. ( ~P B i^i Fin ) E. y e. B A. z e. x z .<_ y ) -> K e. Dirset )
44 13 43 impbii 
 |-  ( K e. Dirset <-> ( K e. Proset /\ A. x e. ( ~P B i^i Fin ) E. y e. B A. z e. x z .<_ y ) )