Metamath Proof Explorer

Theorem lubeldm2

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

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

Proof

Step Hyp Ref Expression
1 lubeldm2.b ⊢ B = Base K
2 lubeldm2.l ⊢ ≤ ˙ = ≤ K
3 lubeldm2.u ⊢ U = lub ⁡ K
4 lubeldm2.p ⊢ ψ ↔ ∀ y ∈ S y ≤ ˙ x ∧ ∀ z ∈ B ∀ y ∈ S y ≤ ˙ z → x ≤ ˙ z
5 lubeldm2.k ⊢ φ → K ∈ Poset
6 1 2 3 4 5 lubeldm ⊢ φ → S ∈ dom ⁡ U ↔ S ⊆ B ∧ ∃! x ∈ B ψ
7 6 biimpa ⊢ φ ∧ S ∈ dom ⁡ U → 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 ⁡ U → S ⊆ B ∧ ∃ x ∈ B ψ
11 simpl ⊢ φ ∧ S ⊆ B ∧ ∃ x ∈ B ψ → φ
12 simprl ⊢ φ ∧ S ⊆ B ∧ ∃ x ∈ B ψ → S ⊆ B
13 2 1 poslubmo ⊢ K ∈ Poset ∧ S ⊆ B → ∃* x ∈ B ∀ y ∈ S y ≤ ˙ x ∧ ∀ z ∈ B ∀ y ∈ S y ≤ ˙ z → x ≤ ˙ z
14 5 13 sylan ⊢ φ ∧ S ⊆ B → ∃* x ∈ B ∀ y ∈ S y ≤ ˙ x ∧ ∀ z ∈ B ∀ y ∈ S y ≤ ˙ z → x ≤ ˙ z
15 4 rmobii ⊢ ∃* x ∈ B ψ ↔ ∃* x ∈ B ∀ y ∈ S y ≤ ˙ x ∧ ∀ z ∈ B ∀ y ∈ S y ≤ ˙ z → x ≤ ˙ z
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 ⁡ U
22 11 12 20 21 syl12anc ⊢ φ ∧ S ⊆ B ∧ ∃ x ∈ B ψ → S ∈ dom ⁡ U
23 10 22 impbida ⊢ φ → S ∈ dom ⁡ U ↔ S ⊆ B ∧ ∃ x ∈ B ψ