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

Proof

Step Hyp Ref Expression
1 drsbn0.b ⊢ B = Base K
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 ∈ a z ≤ ˙ y ↔ ∀ z ∈ ∅ z ≤ ˙ y
6 5 rexbidv ⊢ a = ∅ → ∃ y ∈ B ∀ z ∈ a z ≤ ˙ y ↔ ∃ y ∈ B ∀ z ∈ ∅ z ≤ ˙ y
7 4 6 imbi12d ⊢ a = ∅ → K ∈ Dirset ∧ a ⊆ B → ∃ y ∈ B ∀ z ∈ a z ≤ ˙ 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 ∈ a z ≤ ˙ y ↔ ∀ z ∈ b z ≤ ˙ y
11 10 rexbidv ⊢ a = b → ∃ y ∈ B ∀ z ∈ a z ≤ ˙ y ↔ ∃ y ∈ B ∀ z ∈ b z ≤ ˙ y
12 9 11 imbi12d ⊢ a = b → K ∈ Dirset ∧ a ⊆ B → ∃ y ∈ B ∀ z ∈ a z ≤ ˙ y ↔ K ∈ Dirset ∧ b ⊆ B → ∃ y ∈ B ∀ z ∈ b z ≤ ˙ 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 ∈ a z ≤ ˙ y ↔ ∀ z ∈ b ∪ c z ≤ ˙ y
16 15 rexbidv ⊢ a = b ∪ c → ∃ y ∈ B ∀ z ∈ a z ≤ ˙ y ↔ ∃ y ∈ B ∀ z ∈ b ∪ c z ≤ ˙ y
17 14 16 imbi12d ⊢ a = b ∪ c → K ∈ Dirset ∧ a ⊆ B → ∃ y ∈ B ∀ z ∈ a z ≤ ˙ y ↔ K ∈ Dirset ∧ b ∪ c ⊆ B → ∃ y ∈ B ∀ z ∈ b ∪ c z ≤ ˙ 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 ∈ a z ≤ ˙ y ↔ ∀ z ∈ X z ≤ ˙ y
21 20 rexbidv ⊢ a = X → ∃ y ∈ B ∀ z ∈ a z ≤ ˙ y ↔ ∃ y ∈ B ∀ z ∈ X z ≤ ˙ y
22 19 21 imbi12d ⊢ a = X → K ∈ Dirset ∧ a ⊆ B → ∃ y ∈ B ∀ z ∈ a z ≤ ˙ y ↔ K ∈ Dirset ∧ X ⊆ B → ∃ y ∈ B ∀ z ∈ X z ≤ ˙ 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 ⊢ ∃ y y ∈ B → ∃ y y ∈ B ∧ ∀ z ∈ ∅ z ≤ ˙ y
27 n0 ⊢ B ≠ ∅ ↔ ∃ y y ∈ B
28 df-rex ⊢ ∃ y ∈ B ∀ z ∈ ∅ z ≤ ˙ y ↔ ∃ y y ∈ 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 ∈ b z ≤ ˙ y ↔ ∀ z ∈ b z ≤ ˙ a
38 37 cbvrexvw ⊢ ∃ y ∈ B ∀ z ∈ b z ≤ ˙ y ↔ ∃ a ∈ B ∀ z ∈ b z ≤ ˙ a
39 simplrr ⊢ K ∈ Dirset ∧ b ∪ c ⊆ B ∧ a ∈ B ∧ ∀ z ∈ b z ≤ ˙ a ∧ y ∈ B ∧ a ≤ ˙ y ∧ c ≤ ˙ y → ∀ z ∈ b z ≤ ˙ 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 ∈ b z ≤ ˙ a → ∀ z ∈ b z ≤ ˙ y
56 55 adantlrr ⊢ K ∈ Dirset ∧ b ∪ c ⊆ B ∧ a ∈ B ∧ ∀ z ∈ b z ≤ ˙ a ∧ y ∈ B ∧ a ≤ ˙ y ∧ c ≤ ˙ y → ∀ z ∈ b z ≤ ˙ a → ∀ z ∈ b z ≤ ˙ y
57 39 56 mpd ⊢ K ∈ Dirset ∧ b ∪ c ⊆ B ∧ a ∈ B ∧ ∀ z ∈ b z ≤ ˙ a ∧ y ∈ B ∧ a ≤ ˙ y ∧ c ≤ ˙ y → ∀ z ∈ b z ≤ ˙ y
58 simprrr ⊢ K ∈ Dirset ∧ b ∪ c ⊆ B ∧ a ∈ B ∧ ∀ z ∈ b z ≤ ˙ 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 ∈ c z ≤ ˙ y ↔ c ≤ ˙ y
62 58 61 sylibr ⊢ K ∈ Dirset ∧ b ∪ c ⊆ B ∧ a ∈ B ∧ ∀ z ∈ b z ≤ ˙ a ∧ y ∈ B ∧ a ≤ ˙ y ∧ c ≤ ˙ y → ∀ z ∈ c z ≤ ˙ y
63 ralun ⊢ ∀ z ∈ b z ≤ ˙ y ∧ ∀ z ∈ c z ≤ ˙ y → ∀ z ∈ b ∪ c z ≤ ˙ y
64 57 62 63 syl2anc ⊢ K ∈ Dirset ∧ b ∪ c ⊆ B ∧ a ∈ B ∧ ∀ z ∈ b z ≤ ˙ a ∧ y ∈ B ∧ a ≤ ˙ y ∧ c ≤ ˙ y → ∀ z ∈ b ∪ c z ≤ ˙ y
65 simpll ⊢ K ∈ Dirset ∧ b ∪ c ⊆ B ∧ a ∈ B ∧ ∀ z ∈ b z ≤ ˙ a → K ∈ Dirset
66 simprl ⊢ K ∈ Dirset ∧ b ∪ c ⊆ B ∧ a ∈ B ∧ ∀ z ∈ b z ≤ ˙ 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 ∈ b z ≤ ˙ a → c ∈ B
73 1 2 drsdir ⊢ K ∈ Dirset ∧ a ∈ B ∧ c ∈ B → ∃ y ∈ B a ≤ ˙ y ∧ c ≤ ˙ y
74 65 66 72 73 syl3anc ⊢ K ∈ Dirset ∧ b ∪ c ⊆ B ∧ a ∈ B ∧ ∀ z ∈ b z ≤ ˙ a → ∃ y ∈ B a ≤ ˙ y ∧ c ≤ ˙ y
75 64 74 reximddv ⊢ K ∈ Dirset ∧ b ∪ c ⊆ B ∧ a ∈ B ∧ ∀ z ∈ b z ≤ ˙ a → ∃ y ∈ B ∀ z ∈ b ∪ c z ≤ ˙ y
76 75 rexlimdvaa ⊢ K ∈ Dirset ∧ b ∪ c ⊆ B → ∃ a ∈ B ∀ z ∈ b z ≤ ˙ a → ∃ y ∈ B ∀ z ∈ b ∪ c z ≤ ˙ y
77 38 76 syl5bi ⊢ K ∈ Dirset ∧ b ∪ c ⊆ B → ∃ y ∈ B ∀ z ∈ b z ≤ ˙ y → ∃ y ∈ B ∀ z ∈ b ∪ c z ≤ ˙ y
78 35 77 embantd ⊢ K ∈ Dirset ∧ b ∪ c ⊆ B → K ∈ Dirset ∧ b ⊆ B → ∃ y ∈ B ∀ z ∈ b z ≤ ˙ y → ∃ y ∈ B ∀ z ∈ b ∪ c z ≤ ˙ y
79 78 com12 ⊢ K ∈ Dirset ∧ b ⊆ B → ∃ y ∈ B ∀ z ∈ b z ≤ ˙ y → K ∈ Dirset ∧ b ∪ c ⊆ B → ∃ y ∈ B ∀ z ∈ b ∪ c z ≤ ˙ y
80 79 a1i ⊢ b ∈ Fin → K ∈ Dirset ∧ b ⊆ B → ∃ y ∈ B ∀ z ∈ b z ≤ ˙ y → K ∈ Dirset ∧ b ∪ c ⊆ B → ∃ y ∈ B ∀ z ∈ b ∪ c z ≤ ˙ y
81 7 12 17 22 31 80 findcard2 ⊢ X ∈ Fin → K ∈ Dirset ∧ X ⊆ B → ∃ y ∈ B ∀ z ∈ X z ≤ ˙ y
82 81 com12 ⊢ K ∈ Dirset ∧ X ⊆ B → X ∈ Fin → ∃ y ∈ B ∀ z ∈ X z ≤ ˙ y
83 82 3impia ⊢ K ∈ Dirset ∧ X ⊆ B ∧ X ∈ Fin → ∃ y ∈ B ∀ z ∈ X z ≤ ˙ y