Metamath Proof Explorer

Theorem glbeldm2

Description: Member of the domain of the greatest lower bound function of a poset. (Contributed by Zhi Wang, 26-Sep-2024)

Ref Expression
Hypotheses lubeldm2.b ⊢ B = Base K
lubeldm2.l ⊢ ≤ ˙ = ≤ K
glbeldm2.g ⊢ G = glb ⁡ K
glbeldm2.p ⊢ ψ ↔ ∀ y ∈ S x ≤ ˙ y ∧ ∀ z ∈ B ∀ y ∈ S z ≤ ˙ y → z ≤ ˙ x
glbeldm2.k ⊢ φ → K ∈ Poset
Assertion glbeldm2 ⊢ φ → S ∈ dom ⁡ G ↔ S ⊆ B ∧ ∃ x ∈ B ψ

Proof

Step Hyp Ref Expression
1 lubeldm2.b ⊢ B = Base K
2 lubeldm2.l ⊢ ≤ ˙ = ≤ K
3 glbeldm2.g ⊢ G = glb ⁡ K
4 glbeldm2.p ⊢ ψ ↔ ∀ y ∈ S x ≤ ˙ y ∧ ∀ z ∈ B ∀ y ∈ S z ≤ ˙ y → z ≤ ˙ x
5 glbeldm2.k ⊢ φ → K ∈ Poset
6 1 2 3 4 5 glbeldm ⊢ φ → S ∈ dom ⁡ G ↔ S ⊆ B ∧ ∃! x ∈ B ψ
7 6 biimpa ⊢ φ ∧ S ∈ dom ⁡ G → S ⊆ B ∧ ∃! x ∈ B ψ
8 reurex ⊢ ∃! x ∈ B ψ → ∃ x ∈ B ψ
9 8 anim2i ⊢ S ⊆ B ∧ ∃! x ∈ B ψ → S ⊆ B ∧ ∃ x ∈ B ψ
10 7 9 syl ⊢ φ ∧ S ∈ dom ⁡ G → S ⊆ B ∧ ∃ x ∈ B ψ
11 simpl ⊢ φ ∧ S ⊆ B ∧ ∃ x ∈ B ψ → φ
12 simprl ⊢ φ ∧ S ⊆ B ∧ ∃ x ∈ B ψ → S ⊆ B
13 2 1 posglbmo ⊢ K ∈ Poset ∧ S ⊆ B → ∃* x ∈ B ∀ y ∈ S x ≤ ˙ y ∧ ∀ z ∈ B ∀ y ∈ S z ≤ ˙ y → z ≤ ˙ x
14 5 13 sylan ⊢ φ ∧ S ⊆ B → ∃* x ∈ B ∀ y ∈ S x ≤ ˙ y ∧ ∀ z ∈ B ∀ y ∈ S z ≤ ˙ y → z ≤ ˙ x
15 4 rmobii ⊢ ∃* x ∈ B ψ ↔ ∃* x ∈ B ∀ y ∈ S x ≤ ˙ y ∧ ∀ z ∈ B ∀ y ∈ S z ≤ ˙ y → z ≤ ˙ x
16 14 15 sylibr ⊢ φ ∧ S ⊆ B → ∃* x ∈ B ψ
17 16 anim1ci ⊢ φ ∧ S ⊆ B ∧ ∃ x ∈ B ψ → ∃ x ∈ B ψ ∧ ∃* x ∈ B ψ
18 reu5 ⊢ ∃! x ∈ B ψ ↔ ∃ x ∈ B ψ ∧ ∃* x ∈ B ψ
19 17 18 sylibr ⊢ φ ∧ S ⊆ B ∧ ∃ x ∈ B ψ → ∃! x ∈ B ψ
20 19 anasss ⊢ φ ∧ S ⊆ B ∧ ∃ x ∈ B ψ → ∃! x ∈ B ψ
21 6 biimpar ⊢ φ ∧ S ⊆ B ∧ ∃! x ∈ B ψ → S ∈ dom ⁡ G
22 11 12 20 21 syl12anc ⊢ φ ∧ S ⊆ B ∧ ∃ x ∈ B ψ → S ∈ dom ⁡ G
23 10 22 impbida ⊢ φ → S ∈ dom ⁡ G ↔ S ⊆ B ∧ ∃ x ∈ B ψ