Metamath Proof Explorer

Theorem drsdirfi

Description: Anyfinite number of elements in a directed set have a common upper bound. Here is where the nonemptiness constraint in df-drs first comes into play; without it we would need an additional constraint that X not be empty. (Contributed by Stefan O'Rear, 1-Feb-2015)

Ref Expression
Hypotheses drsbn0.b 
|- B = ( Base ` K )
drsdirfi.l 
|- .<_ = ( le ` K )
Assertion drsdirfi 
|- ( ( K e. Dirset /\ X C_ B /\ X e. 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 sseq1 
 |-  ( a = (/) -> ( a C_ B <-> (/) C_ B ) )
4 3 anbi2d 
 |-  ( a = (/) -> ( ( K e. Dirset /\ a C_ B ) <-> ( K e. Dirset /\ (/) C_ B ) ) )
5 raleq 
 |-  ( a = (/) -> ( A. z e. a z .<_ y <-> A. z e. (/) z .<_ y ) )
6 5 rexbidv 
 |-  ( a = (/) -> ( E. y e. B A. z e. a z .<_ y <-> E. y e. B A. z e. (/) z .<_ y ) )
7 4 6 imbi12d 
 |-  ( a = (/) -> ( ( ( K e. Dirset /\ a C_ B ) -> E. y e. B A. z e. a z .<_ y ) <-> ( ( K e. Dirset /\ (/) C_ B ) -> E. y e. B A. z e. (/) z .<_ y ) ) )
8 sseq1 
 |-  ( a = b -> ( a C_ B <-> b C_ B ) )
9 8 anbi2d 
 |-  ( a = b -> ( ( K e. Dirset /\ a C_ B ) <-> ( K e. Dirset /\ b C_ B ) ) )
10 raleq 
 |-  ( a = b -> ( A. z e. a z .<_ y <-> A. z e. b z .<_ y ) )
11 10 rexbidv 
 |-  ( a = b -> ( E. y e. B A. z e. a z .<_ y <-> E. y e. B A. z e. b z .<_ y ) )
12 9 11 imbi12d 
 |-  ( a = b -> ( ( ( K e. Dirset /\ a C_ B ) -> E. y e. B A. z e. a z .<_ y ) <-> ( ( K e. Dirset /\ b C_ B ) -> E. y e. B A. z e. b z .<_ y ) ) )
13 sseq1 
 |-  ( a = ( b u. { c } ) -> ( a C_ B <-> ( b u. { c } ) C_ B ) )
14 13 anbi2d 
 |-  ( a = ( b u. { c } ) -> ( ( K e. Dirset /\ a C_ B ) <-> ( K e. Dirset /\ ( b u. { c } ) C_ B ) ) )
15 raleq 
 |-  ( a = ( b u. { c } ) -> ( A. z e. a z .<_ y <-> A. z e. ( b u. { c } ) z .<_ y ) )
16 15 rexbidv 
 |-  ( a = ( b u. { c } ) -> ( E. y e. B A. z e. a z .<_ y <-> E. y e. B A. z e. ( b u. { c } ) z .<_ y ) )
17 14 16 imbi12d 
 |-  ( a = ( b u. { c } ) -> ( ( ( K e. Dirset /\ a C_ B ) -> E. y e. B A. z e. a z .<_ y ) <-> ( ( K e. Dirset /\ ( b u. { c } ) C_ B ) -> E. y e. B A. z e. ( b u. { c } ) z .<_ y ) ) )
18 sseq1 
 |-  ( a = X -> ( a C_ B <-> X C_ B ) )
19 18 anbi2d 
 |-  ( a = X -> ( ( K e. Dirset /\ a C_ B ) <-> ( K e. Dirset /\ X C_ B ) ) )
20 raleq 
 |-  ( a = X -> ( A. z e. a z .<_ y <-> A. z e. X z .<_ y ) )
21 20 rexbidv 
 |-  ( a = X -> ( E. y e. B A. z e. a z .<_ y <-> E. y e. B A. z e. X z .<_ y ) )
22 19 21 imbi12d 
 |-  ( a = X -> ( ( ( K e. Dirset /\ a C_ B ) -> E. y e. B A. z e. a z .<_ y ) <-> ( ( K e. Dirset /\ X C_ B ) -> E. y e. B A. z e. X z .<_ y ) ) )
23 1 drsbn0 
 |-  ( K e. Dirset -> B =/= (/) )
24 ral0 
 |-  A. z e. (/) z .<_ y
25 24 jctr 
 |-  ( y e. B -> ( y e. B /\ A. z e. (/) z .<_ y ) )
26 25 eximi 
 |-  ( E. y y e. B -> E. y ( y e. B /\ A. z e. (/) z .<_ y ) )
27 n0 
 |-  ( B =/= (/) <-> E. y y e. B )
28 df-rex 
 |-  ( E. y e. B A. z e. (/) z .<_ y <-> E. y ( y e. B /\ A. z e. (/) z .<_ y ) )
29 26 27 28 3imtr4i 
 |-  ( B =/= (/) -> E. y e. B A. z e. (/) z .<_ y )
30 23 29 syl 
 |-  ( K e. Dirset -> E. y e. B A. z e. (/) z .<_ y )
31 30 adantr 
 |-  ( ( K e. Dirset /\ (/) C_ B ) -> E. y e. B A. z e. (/) z .<_ y )
32 ssun1 
 |-  b C_ ( b u. { c } )
33 sstr 
 |-  ( ( b C_ ( b u. { c } ) /\ ( b u. { c } ) C_ B ) -> b C_ B )
34 32 33 mpan 
 |-  ( ( b u. { c } ) C_ B -> b C_ B )
35 34 anim2i 
 |-  ( ( K e. Dirset /\ ( b u. { c } ) C_ B ) -> ( K e. Dirset /\ b C_ B ) )
36 breq2 
 |-  ( y = a -> ( z .<_ y <-> z .<_ a ) )
37 36 ralbidv 
 |-  ( y = a -> ( A. z e. b z .<_ y <-> A. z e. b z .<_ a ) )
38 37 cbvrexvw 
 |-  ( E. y e. B A. z e. b z .<_ y <-> E. a e. B A. z e. b z .<_ a )
39 simplrr 
 |-  ( ( ( ( K e. Dirset /\ ( b u. { c } ) C_ B ) /\ ( a e. B /\ A. z e. b z .<_ a ) ) /\ ( y e. B /\ ( a .<_ y /\ c .<_ y ) ) ) -> A. z e. b z .<_ a )
40 drsprs 
 |-  ( K e. Dirset -> K e. Proset )
41 40 ad5antr 
 |-  ( ( ( ( ( ( K e. Dirset /\ ( b u. { c } ) C_ B ) /\ a e. B ) /\ ( y e. B /\ ( a .<_ y /\ c .<_ y ) ) ) /\ z e. b ) /\ z .<_ a ) -> K e. Proset )
42 34 ad2antlr 
 |-  ( ( ( K e. Dirset /\ ( b u. { c } ) C_ B ) /\ a e. B ) -> b C_ B )
43 42 adantr 
 |-  ( ( ( ( K e. Dirset /\ ( b u. { c } ) C_ B ) /\ a e. B ) /\ ( y e. B /\ ( a .<_ y /\ c .<_ y ) ) ) -> b C_ B )
44 43 sselda 
 |-  ( ( ( ( ( K e. Dirset /\ ( b u. { c } ) C_ B ) /\ a e. B ) /\ ( y e. B /\ ( a .<_ y /\ c .<_ y ) ) ) /\ z e. b ) -> z e. B )
45 44 adantr 
 |-  ( ( ( ( ( ( K e. Dirset /\ ( b u. { c } ) C_ B ) /\ a e. B ) /\ ( y e. B /\ ( a .<_ y /\ c .<_ y ) ) ) /\ z e. b ) /\ z .<_ a ) -> z e. B )
46 simp-4r 
 |-  ( ( ( ( ( ( K e. Dirset /\ ( b u. { c } ) C_ B ) /\ a e. B ) /\ ( y e. B /\ ( a .<_ y /\ c .<_ y ) ) ) /\ z e. b ) /\ z .<_ a ) -> a e. B )
47 simprl 
 |-  ( ( ( ( K e. Dirset /\ ( b u. { c } ) C_ B ) /\ a e. B ) /\ ( y e. B /\ ( a .<_ y /\ c .<_ y ) ) ) -> y e. B )
48 47 ad2antrr 
 |-  ( ( ( ( ( ( K e. Dirset /\ ( b u. { c } ) C_ B ) /\ a e. B ) /\ ( y e. B /\ ( a .<_ y /\ c .<_ y ) ) ) /\ z e. b ) /\ z .<_ a ) -> y e. B )
49 simpr 
 |-  ( ( ( ( ( ( K e. Dirset /\ ( b u. { c } ) C_ B ) /\ a e. B ) /\ ( y e. B /\ ( a .<_ y /\ c .<_ y ) ) ) /\ z e. b ) /\ z .<_ a ) -> z .<_ a )
50 simprrl 
 |-  ( ( ( ( K e. Dirset /\ ( b u. { c } ) C_ B ) /\ a e. B ) /\ ( y e. B /\ ( a .<_ y /\ c .<_ y ) ) ) -> a .<_ y )
51 50 ad2antrr 
 |-  ( ( ( ( ( ( K e. Dirset /\ ( b u. { c } ) C_ B ) /\ a e. B ) /\ ( y e. B /\ ( a .<_ y /\ c .<_ y ) ) ) /\ z e. b ) /\ z .<_ a ) -> a .<_ y )
52 1 2 prstr 
 |-  ( ( K e. Proset /\ ( z e. B /\ a e. B /\ y e. B ) /\ ( z .<_ a /\ a .<_ y ) ) -> z .<_ y )
53 41 45 46 48 49 51 52 syl132anc 
 |-  ( ( ( ( ( ( K e. Dirset /\ ( b u. { c } ) C_ B ) /\ a e. B ) /\ ( y e. B /\ ( a .<_ y /\ c .<_ y ) ) ) /\ z e. b ) /\ z .<_ a ) -> z .<_ y )
54 53 ex 
 |-  ( ( ( ( ( K e. Dirset /\ ( b u. { c } ) C_ B ) /\ a e. B ) /\ ( y e. B /\ ( a .<_ y /\ c .<_ y ) ) ) /\ z e. b ) -> ( z .<_ a -> z .<_ y ) )
55 54 ralimdva 
 |-  ( ( ( ( K e. Dirset /\ ( b u. { c } ) C_ B ) /\ a e. B ) /\ ( y e. B /\ ( a .<_ y /\ c .<_ y ) ) ) -> ( A. z e. b z .<_ a -> A. z e. b z .<_ y ) )
56 55 adantlrr 
 |-  ( ( ( ( K e. Dirset /\ ( b u. { c } ) C_ B ) /\ ( a e. B /\ A. z e. b z .<_ a ) ) /\ ( y e. B /\ ( a .<_ y /\ c .<_ y ) ) ) -> ( A. z e. b z .<_ a -> A. z e. b z .<_ y ) )
57 39 56 mpd 
 |-  ( ( ( ( K e. Dirset /\ ( b u. { c } ) C_ B ) /\ ( a e. B /\ A. z e. b z .<_ a ) ) /\ ( y e. B /\ ( a .<_ y /\ c .<_ y ) ) ) -> A. z e. b z .<_ y )
58 simprrr 
 |-  ( ( ( ( K e. Dirset /\ ( b u. { c } ) C_ B ) /\ ( a e. B /\ A. z e. b z .<_ a ) ) /\ ( y e. B /\ ( a .<_ y /\ c .<_ y ) ) ) -> c .<_ y )
59 vex 
 |-  c e. _V
60 breq1 
 |-  ( z = c -> ( z .<_ y <-> c .<_ y ) )
61 59 60 ralsn 
 |-  ( A. z e. { c } z .<_ y <-> c .<_ y )
62 58 61 sylibr 
 |-  ( ( ( ( K e. Dirset /\ ( b u. { c } ) C_ B ) /\ ( a e. B /\ A. z e. b z .<_ a ) ) /\ ( y e. B /\ ( a .<_ y /\ c .<_ y ) ) ) -> A. z e. { c } z .<_ y )
63 ralun 
 |-  ( ( A. z e. b z .<_ y /\ A. z e. { c } z .<_ y ) -> A. z e. ( b u. { c } ) z .<_ y )
64 57 62 63 syl2anc 
 |-  ( ( ( ( K e. Dirset /\ ( b u. { c } ) C_ B ) /\ ( a e. B /\ A. z e. b z .<_ a ) ) /\ ( y e. B /\ ( a .<_ y /\ c .<_ y ) ) ) -> A. z e. ( b u. { c } ) z .<_ y )
65 simpll 
 |-  ( ( ( K e. Dirset /\ ( b u. { c } ) C_ B ) /\ ( a e. B /\ A. z e. b z .<_ a ) ) -> K e. Dirset )
66 simprl 
 |-  ( ( ( K e. Dirset /\ ( b u. { c } ) C_ B ) /\ ( a e. B /\ A. z e. b z .<_ a ) ) -> a e. B )
67 ssun2 
 |-  { c } C_ ( b u. { c } )
68 sstr 
 |-  ( ( { c } C_ ( b u. { c } ) /\ ( b u. { c } ) C_ B ) -> { c } C_ B )
69 67 68 mpan 
 |-  ( ( b u. { c } ) C_ B -> { c } C_ B )
70 59 snss 
 |-  ( c e. B <-> { c } C_ B )
71 69 70 sylibr 
 |-  ( ( b u. { c } ) C_ B -> c e. B )
72 71 ad2antlr 
 |-  ( ( ( K e. Dirset /\ ( b u. { c } ) C_ B ) /\ ( a e. B /\ A. z e. b z .<_ a ) ) -> c e. B )
73 1 2 drsdir 
 |-  ( ( K e. Dirset /\ a e. B /\ c e. B ) -> E. y e. B ( a .<_ y /\ c .<_ y ) )
74 65 66 72 73 syl3anc 
 |-  ( ( ( K e. Dirset /\ ( b u. { c } ) C_ B ) /\ ( a e. B /\ A. z e. b z .<_ a ) ) -> E. y e. B ( a .<_ y /\ c .<_ y ) )
75 64 74 reximddv 
 |-  ( ( ( K e. Dirset /\ ( b u. { c } ) C_ B ) /\ ( a e. B /\ A. z e. b z .<_ a ) ) -> E. y e. B A. z e. ( b u. { c } ) z .<_ y )
76 75 rexlimdvaa 
 |-  ( ( K e. Dirset /\ ( b u. { c } ) C_ B ) -> ( E. a e. B A. z e. b z .<_ a -> E. y e. B A. z e. ( b u. { c } ) z .<_ y ) )
77 38 76 syl5bi 
 |-  ( ( K e. Dirset /\ ( b u. { c } ) C_ B ) -> ( E. y e. B A. z e. b z .<_ y -> E. y e. B A. z e. ( b u. { c } ) z .<_ y ) )
78 35 77 embantd 
 |-  ( ( K e. Dirset /\ ( b u. { c } ) C_ B ) -> ( ( ( K e. Dirset /\ b C_ B ) -> E. y e. B A. z e. b z .<_ y ) -> E. y e. B A. z e. ( b u. { c } ) z .<_ y ) )
79 78 com12 
 |-  ( ( ( K e. Dirset /\ b C_ B ) -> E. y e. B A. z e. b z .<_ y ) -> ( ( K e. Dirset /\ ( b u. { c } ) C_ B ) -> E. y e. B A. z e. ( b u. { c } ) z .<_ y ) )
80 79 a1i 
 |-  ( b e. Fin -> ( ( ( K e. Dirset /\ b C_ B ) -> E. y e. B A. z e. b z .<_ y ) -> ( ( K e. Dirset /\ ( b u. { c } ) C_ B ) -> E. y e. B A. z e. ( b u. { c } ) z .<_ y ) ) )
81 7 12 17 22 31 80 findcard2 
 |-  ( X e. Fin -> ( ( K e. Dirset /\ X C_ B ) -> E. y e. B A. z e. X z .<_ y ) )
82 81 com12 
 |-  ( ( K e. Dirset /\ X C_ B ) -> ( X e. Fin -> E. y e. B A. z e. X z .<_ y ) )
83 82 3impia 
 |-  ( ( K e. Dirset /\ X C_ B /\ X e. Fin ) -> E. y e. B A. z e. X z .<_ y )