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 ⊢ ≤ ˙ = ≤ K
Assertion isdrs2 ⊢ K ∈ Dirset ↔ K ∈ Proset ∧ ∀ x ∈ 𝒫 B ∩ Fin ∃ y ∈ B ∀ z ∈ x z ≤ ˙ y

Proof

Step Hyp Ref Expression
1 drsbn0.b ⊢ B = Base K
2 drsdirfi.l ⊢ ≤ ˙ = ≤ K
3 drsprs ⊢ K ∈ Dirset → K ∈ Proset
4 simpl ⊢ K ∈ Dirset ∧ x ∈ 𝒫 B ∩ Fin → K ∈ Dirset
5 elinel1 ⊢ x ∈ 𝒫 B ∩ Fin → x ∈ 𝒫 B
6 5 elpwid ⊢ x ∈ 𝒫 B ∩ Fin → x ⊆ B
7 6 adantl ⊢ K ∈ Dirset ∧ x ∈ 𝒫 B ∩ Fin → x ⊆ B
8 elinel2 ⊢ x ∈ 𝒫 B ∩ Fin → x ∈ Fin
9 8 adantl ⊢ K ∈ Dirset ∧ x ∈ 𝒫 B ∩ Fin → x ∈ Fin
10 1 2 drsdirfi ⊢ K ∈ Dirset ∧ x ⊆ B ∧ x ∈ Fin → ∃ y ∈ B ∀ z ∈ x z ≤ ˙ y
11 4 7 9 10 syl3anc ⊢ K ∈ Dirset ∧ x ∈ 𝒫 B ∩ Fin → ∃ y ∈ B ∀ z ∈ x z ≤ ˙ y
12 11 ralrimiva ⊢ K ∈ Dirset → ∀ x ∈ 𝒫 B ∩ Fin ∃ y ∈ B ∀ z ∈ x z ≤ ˙ y
13 3 12 jca ⊢ K ∈ Dirset → K ∈ Proset ∧ ∀ x ∈ 𝒫 B ∩ Fin ∃ y ∈ B ∀ z ∈ x z ≤ ˙ y
14 simpl ⊢ K ∈ Proset ∧ ∀ x ∈ 𝒫 B ∩ Fin ∃ y ∈ B ∀ z ∈ x z ≤ ˙ y → K ∈ Proset
15 0elpw ⊢ ∅ ∈ 𝒫 B
16 0fi ⊢ ∅ ∈ Fin
17 15 16 elini ⊢ ∅ ∈ 𝒫 B ∩ Fin
18 raleq ⊢ x = ∅ → ∀ z ∈ x z ≤ ˙ y ↔ ∀ z ∈ ∅ z ≤ ˙ y
19 18 rexbidv ⊢ x = ∅ → ∃ y ∈ B ∀ z ∈ x z ≤ ˙ y ↔ ∃ y ∈ B ∀ z ∈ ∅ z ≤ ˙ y
20 19 rspcv ⊢ ∅ ∈ 𝒫 B ∩ Fin → ∀ x ∈ 𝒫 B ∩ Fin ∃ y ∈ B ∀ z ∈ x z ≤ ˙ y → ∃ y ∈ B ∀ z ∈ ∅ z ≤ ˙ y
21 17 20 ax-mp ⊢ ∀ x ∈ 𝒫 B ∩ Fin ∃ y ∈ B ∀ z ∈ x z ≤ ˙ y → ∃ y ∈ B ∀ z ∈ ∅ z ≤ ˙ y
22 rexn0 ⊢ ∃ y ∈ B ∀ z ∈ ∅ z ≤ ˙ y → B ≠ ∅
23 21 22 syl ⊢ ∀ x ∈ 𝒫 B ∩ Fin ∃ y ∈ B ∀ z ∈ x z ≤ ˙ y → B ≠ ∅
24 23 adantl ⊢ K ∈ Proset ∧ ∀ x ∈ 𝒫 B ∩ Fin ∃ y ∈ B ∀ z ∈ x z ≤ ˙ y → B ≠ ∅
25 raleq ⊢ x = a b → ∀ z ∈ x z ≤ ˙ y ↔ ∀ z ∈ a b z ≤ ˙ y
26 25 rexbidv ⊢ x = a b → ∃ y ∈ B ∀ z ∈ x z ≤ ˙ y ↔ ∃ y ∈ B ∀ z ∈ a b z ≤ ˙ y
27 simplr ⊢ K ∈ Proset ∧ ∀ x ∈ 𝒫 B ∩ Fin ∃ y ∈ B ∀ z ∈ x z ≤ ˙ y ∧ a ∈ B ∧ b ∈ B → ∀ x ∈ 𝒫 B ∩ Fin ∃ y ∈ B ∀ z ∈ x z ≤ ˙ y
28 prelpwi ⊢ a ∈ B ∧ b ∈ B → a b ∈ 𝒫 B
29 prfi ⊢ a b ∈ Fin
30 29 a1i ⊢ a ∈ B ∧ b ∈ B → a b ∈ Fin
31 28 30 elind ⊢ a ∈ B ∧ b ∈ B → a b ∈ 𝒫 B ∩ Fin
32 31 adantl ⊢ K ∈ Proset ∧ ∀ x ∈ 𝒫 B ∩ Fin ∃ y ∈ B ∀ z ∈ x z ≤ ˙ y ∧ a ∈ B ∧ b ∈ B → a b ∈ 𝒫 B ∩ Fin
33 26 27 32 rspcdva ⊢ K ∈ Proset ∧ ∀ x ∈ 𝒫 B ∩ Fin ∃ y ∈ B ∀ z ∈ x z ≤ ˙ y ∧ a ∈ B ∧ b ∈ B → ∃ y ∈ B ∀ z ∈ a b z ≤ ˙ y
34 vex ⊢ a ∈ V
35 vex ⊢ b ∈ V
36 breq1 ⊢ z = a → z ≤ ˙ y ↔ a ≤ ˙ y
37 breq1 ⊢ z = b → z ≤ ˙ y ↔ b ≤ ˙ y
38 34 35 36 37 ralpr ⊢ ∀ z ∈ a b z ≤ ˙ y ↔ a ≤ ˙ y ∧ b ≤ ˙ y
39 38 rexbii ⊢ ∃ y ∈ B ∀ z ∈ a b z ≤ ˙ y ↔ ∃ y ∈ B a ≤ ˙ y ∧ b ≤ ˙ y
40 33 39 sylib ⊢ K ∈ Proset ∧ ∀ x ∈ 𝒫 B ∩ Fin ∃ y ∈ B ∀ z ∈ x z ≤ ˙ y ∧ a ∈ B ∧ b ∈ B → ∃ y ∈ B a ≤ ˙ y ∧ b ≤ ˙ y
41 40 ralrimivva ⊢ K ∈ Proset ∧ ∀ x ∈ 𝒫 B ∩ Fin ∃ y ∈ B ∀ z ∈ x z ≤ ˙ y → ∀ a ∈ B ∀ b ∈ B ∃ y ∈ B a ≤ ˙ y ∧ b ≤ ˙ y
42 1 2 isdrs ⊢ K ∈ Dirset ↔ K ∈ Proset ∧ B ≠ ∅ ∧ ∀ a ∈ B ∀ b ∈ B ∃ y ∈ B a ≤ ˙ y ∧ b ≤ ˙ y
43 14 24 41 42 syl3anbrc ⊢ K ∈ Proset ∧ ∀ x ∈ 𝒫 B ∩ Fin ∃ y ∈ B ∀ z ∈ x z ≤ ˙ y → K ∈ Dirset
44 13 43 impbii ⊢ K ∈ Dirset ↔ K ∈ Proset ∧ ∀ x ∈ 𝒫 B ∩ Fin ∃ y ∈ B ∀ z ∈ x z ≤ ˙ y