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=BaseK
drsdirfi.l ⊢≤˙=≤K
Assertion drsdirfi ⊢K∈Dirset∧X⊆B∧X∈Fin→∃y∈B∀z∈Xz≤˙y

Proof

Step Hyp Ref Expression
1 drsbn0.b ⊢B=BaseK
2 drsdirfi.l ⊢≤˙=≤K
3 sseq1 ⊢a=∅→a⊆B↔∅⊆B
4 3 anbi2d ⊢a=∅→K∈Dirset∧a⊆B↔K∈Dirset∧∅⊆B
5 raleq ⊢a=∅→∀z∈az≤˙y↔∀z∈∅z≤˙y
6 5 rexbidv ⊢a=∅→∃y∈B∀z∈az≤˙y↔∃y∈B∀z∈∅z≤˙y
7 4 6 imbi12d ⊢a=∅→K∈Dirset∧a⊆B→∃y∈B∀z∈az≤˙y↔K∈Dirset∧∅⊆B→∃y∈B∀z∈∅z≤˙y
8 sseq1 ⊢a=b→a⊆B↔b⊆B
9 8 anbi2d ⊢a=b→K∈Dirset∧a⊆B↔K∈Dirset∧b⊆B
10 raleq ⊢a=b→∀z∈az≤˙y↔∀z∈bz≤˙y
11 10 rexbidv ⊢a=b→∃y∈B∀z∈az≤˙y↔∃y∈B∀z∈bz≤˙y
12 9 11 imbi12d ⊢a=b→K∈Dirset∧a⊆B→∃y∈B∀z∈az≤˙y↔K∈Dirset∧b⊆B→∃y∈B∀z∈bz≤˙y
13 sseq1 ⊢a=b∪c→a⊆B↔b∪c⊆B
14 13 anbi2d ⊢a=b∪c→K∈Dirset∧a⊆B↔K∈Dirset∧b∪c⊆B
15 raleq ⊢a=b∪c→∀z∈az≤˙y↔∀z∈b∪cz≤˙y
16 15 rexbidv ⊢a=b∪c→∃y∈B∀z∈az≤˙y↔∃y∈B∀z∈b∪cz≤˙y
17 14 16 imbi12d ⊢a=b∪c→K∈Dirset∧a⊆B→∃y∈B∀z∈az≤˙y↔K∈Dirset∧b∪c⊆B→∃y∈B∀z∈b∪cz≤˙y
18 sseq1 ⊢a=X→a⊆B↔X⊆B
19 18 anbi2d ⊢a=X→K∈Dirset∧a⊆B↔K∈Dirset∧X⊆B
20 raleq ⊢a=X→∀z∈az≤˙y↔∀z∈Xz≤˙y
21 20 rexbidv ⊢a=X→∃y∈B∀z∈az≤˙y↔∃y∈B∀z∈Xz≤˙y
22 19 21 imbi12d ⊢a=X→K∈Dirset∧a⊆B→∃y∈B∀z∈az≤˙y↔K∈Dirset∧X⊆B→∃y∈B∀z∈Xz≤˙y
23 1 drsbn0 ⊢K∈Dirset→B≠∅
24 ral0 ⊢∀z∈∅z≤˙y
25 24 jctr ⊢y∈B→y∈B∧∀z∈∅z≤˙y
26 25 eximi ⊢∃yy∈B→∃yy∈B∧∀z∈∅z≤˙y
27 n0 ⊢B≠∅↔∃yy∈B
28 df-rex ⊢∃y∈B∀z∈∅z≤˙y↔∃yy∈B∧∀z∈∅z≤˙y
29 26 27 28 3imtr4i ⊢B≠∅→∃y∈B∀z∈∅z≤˙y
30 23 29 syl ⊢K∈Dirset→∃y∈B∀z∈∅z≤˙y
31 30 adantr ⊢K∈Dirset∧∅⊆B→∃y∈B∀z∈∅z≤˙y
32 ssun1 ⊢b⊆b∪c
33 sstr ⊢b⊆b∪c∧b∪c⊆B→b⊆B
34 32 33 mpan ⊢b∪c⊆B→b⊆B
35 34 anim2i ⊢K∈Dirset∧b∪c⊆B→K∈Dirset∧b⊆B
36 breq2 ⊢y=a→z≤˙y↔z≤˙a
37 36 ralbidv ⊢y=a→∀z∈bz≤˙y↔∀z∈bz≤˙a
38 37 cbvrexvw ⊢∃y∈B∀z∈bz≤˙y↔∃a∈B∀z∈bz≤˙a
39 simplrr ⊢K∈Dirset∧b∪c⊆B∧a∈B∧∀z∈bz≤˙a∧y∈B∧a≤˙y∧c≤˙y→∀z∈bz≤˙a
40 drsprs ⊢K∈Dirset→K∈Proset
41 40 ad5antr ⊢K∈Dirset∧b∪c⊆B∧a∈B∧y∈B∧a≤˙y∧c≤˙y∧z∈b∧z≤˙a→K∈Proset
42 34 ad2antlr ⊢K∈Dirset∧b∪c⊆B∧a∈B→b⊆B
43 42 adantr ⊢K∈Dirset∧b∪c⊆B∧a∈B∧y∈B∧a≤˙y∧c≤˙y→b⊆B
44 43 sselda ⊢K∈Dirset∧b∪c⊆B∧a∈B∧y∈B∧a≤˙y∧c≤˙y∧z∈b→z∈B
45 44 adantr ⊢K∈Dirset∧b∪c⊆B∧a∈B∧y∈B∧a≤˙y∧c≤˙y∧z∈b∧z≤˙a→z∈B
46 simp-4r ⊢K∈Dirset∧b∪c⊆B∧a∈B∧y∈B∧a≤˙y∧c≤˙y∧z∈b∧z≤˙a→a∈B
47 simprl ⊢K∈Dirset∧b∪c⊆B∧a∈B∧y∈B∧a≤˙y∧c≤˙y→y∈B
48 47 ad2antrr ⊢K∈Dirset∧b∪c⊆B∧a∈B∧y∈B∧a≤˙y∧c≤˙y∧z∈b∧z≤˙a→y∈B
49 simpr ⊢K∈Dirset∧b∪c⊆B∧a∈B∧y∈B∧a≤˙y∧c≤˙y∧z∈b∧z≤˙a→z≤˙a
50 simprrl ⊢K∈Dirset∧b∪c⊆B∧a∈B∧y∈B∧a≤˙y∧c≤˙y→a≤˙y
51 50 ad2antrr ⊢K∈Dirset∧b∪c⊆B∧a∈B∧y∈B∧a≤˙y∧c≤˙y∧z∈b∧z≤˙a→a≤˙y
52 1 2 prstr ⊢K∈Proset∧z∈B∧a∈B∧y∈B∧z≤˙a∧a≤˙y→z≤˙y
53 41 45 46 48 49 51 52 syl132anc ⊢K∈Dirset∧b∪c⊆B∧a∈B∧y∈B∧a≤˙y∧c≤˙y∧z∈b∧z≤˙a→z≤˙y
54 53 ex ⊢K∈Dirset∧b∪c⊆B∧a∈B∧y∈B∧a≤˙y∧c≤˙y∧z∈b→z≤˙a→z≤˙y
55 54 ralimdva ⊢K∈Dirset∧b∪c⊆B∧a∈B∧y∈B∧a≤˙y∧c≤˙y→∀z∈bz≤˙a→∀z∈bz≤˙y
56 55 adantlrr ⊢K∈Dirset∧b∪c⊆B∧a∈B∧∀z∈bz≤˙a∧y∈B∧a≤˙y∧c≤˙y→∀z∈bz≤˙a→∀z∈bz≤˙y
57 39 56 mpd ⊢K∈Dirset∧b∪c⊆B∧a∈B∧∀z∈bz≤˙a∧y∈B∧a≤˙y∧c≤˙y→∀z∈bz≤˙y
58 simprrr ⊢K∈Dirset∧b∪c⊆B∧a∈B∧∀z∈bz≤˙a∧y∈B∧a≤˙y∧c≤˙y→c≤˙y
59 vex ⊢c∈V
60 breq1 ⊢z=c→z≤˙y↔c≤˙y
61 59 60 ralsn ⊢∀z∈cz≤˙y↔c≤˙y
62 58 61 sylibr ⊢K∈Dirset∧b∪c⊆B∧a∈B∧∀z∈bz≤˙a∧y∈B∧a≤˙y∧c≤˙y→∀z∈cz≤˙y
63 ralun ⊢∀z∈bz≤˙y∧∀z∈cz≤˙y→∀z∈b∪cz≤˙y
64 57 62 63 syl2anc ⊢K∈Dirset∧b∪c⊆B∧a∈B∧∀z∈bz≤˙a∧y∈B∧a≤˙y∧c≤˙y→∀z∈b∪cz≤˙y
65 simpll ⊢K∈Dirset∧b∪c⊆B∧a∈B∧∀z∈bz≤˙a→K∈Dirset
66 simprl ⊢K∈Dirset∧b∪c⊆B∧a∈B∧∀z∈bz≤˙a→a∈B
67 ssun2 ⊢c⊆b∪c
68 sstr ⊢c⊆b∪c∧b∪c⊆B→c⊆B
69 67 68 mpan ⊢b∪c⊆B→c⊆B
70 59 snss ⊢c∈B↔c⊆B
71 69 70 sylibr ⊢b∪c⊆B→c∈B
72 71 ad2antlr ⊢K∈Dirset∧b∪c⊆B∧a∈B∧∀z∈bz≤˙a→c∈B
73 1 2 drsdir ⊢K∈Dirset∧a∈B∧c∈B→∃y∈Ba≤˙y∧c≤˙y
74 65 66 72 73 syl3anc ⊢K∈Dirset∧b∪c⊆B∧a∈B∧∀z∈bz≤˙a→∃y∈Ba≤˙y∧c≤˙y
75 64 74 reximddv ⊢K∈Dirset∧b∪c⊆B∧a∈B∧∀z∈bz≤˙a→∃y∈B∀z∈b∪cz≤˙y
76 75 rexlimdvaa ⊢K∈Dirset∧b∪c⊆B→∃a∈B∀z∈bz≤˙a→∃y∈B∀z∈b∪cz≤˙y
77 38 76 biimtrid ⊢K∈Dirset∧b∪c⊆B→∃y∈B∀z∈bz≤˙y→∃y∈B∀z∈b∪cz≤˙y
78 35 77 embantd ⊢K∈Dirset∧b∪c⊆B→K∈Dirset∧b⊆B→∃y∈B∀z∈bz≤˙y→∃y∈B∀z∈b∪cz≤˙y
79 78 com12 ⊢K∈Dirset∧b⊆B→∃y∈B∀z∈bz≤˙y→K∈Dirset∧b∪c⊆B→∃y∈B∀z∈b∪cz≤˙y
80 79 a1i ⊢b∈Fin→K∈Dirset∧b⊆B→∃y∈B∀z∈bz≤˙y→K∈Dirset∧b∪c⊆B→∃y∈B∀z∈b∪cz≤˙y
81 7 12 17 22 31 80 findcard2 ⊢X∈Fin→K∈Dirset∧X⊆B→∃y∈B∀z∈Xz≤˙y
82 81 com12 ⊢K∈Dirset∧X⊆B→X∈Fin→∃y∈B∀z∈Xz≤˙y
83 82 3impia ⊢K∈Dirset∧X⊆B∧X∈Fin→∃y∈B∀z∈Xz≤˙y