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