Metamath Proof Explorer

Theorem glbdm

Description: Domain of the greatest lower bound function of a poset. (Contributed by NM, 6-Sep-2018)

Ref Expression
Hypotheses glbfval.b ⊢ B = Base K
glbfval.l ⊢ ≤ ˙ = ≤ K
glbfval.g ⊢ G = glb ⁡ K
glbfval.p ⊢ ψ ↔ ∀ y ∈ s x ≤ ˙ y ∧ ∀ z ∈ B ∀ y ∈ s z ≤ ˙ y → z ≤ ˙ x
glbfval.k ⊢ φ → K ∈ V
Assertion glbdm ⊢ φ → dom ⁡ G = s ∈ 𝒫 B | ∃! x ∈ B ψ

Proof

Step Hyp Ref Expression
1 glbfval.b ⊢ B = Base K
2 glbfval.l ⊢ ≤ ˙ = ≤ K
3 glbfval.g ⊢ G = glb ⁡ K
4 glbfval.p ⊢ ψ ↔ ∀ y ∈ s x ≤ ˙ y ∧ ∀ z ∈ B ∀ y ∈ s z ≤ ˙ y → z ≤ ˙ x
5 glbfval.k ⊢ φ → K ∈ V
6 1 2 3 4 5 glbfval ⊢ φ → G = s ∈ 𝒫 B ⟼ ι x ∈ B | ψ ↾ s | ∃! x ∈ B ψ
7 6 dmeqd ⊢ φ → dom ⁡ G = dom ⁡ s ∈ 𝒫 B ⟼ ι x ∈ B | ψ ↾ s | ∃! x ∈ B ψ
8 riotaex ⊢ ι x ∈ B | ψ ∈ V
9 eqid ⊢ s ∈ 𝒫 B ⟼ ι x ∈ B | ψ = s ∈ 𝒫 B ⟼ ι x ∈ B | ψ
10 8 9 dmmpti ⊢ dom ⁡ s ∈ 𝒫 B ⟼ ι x ∈ B | ψ = 𝒫 B
11 10 ineq2i ⊢ s | ∃! x ∈ B ψ ∩ dom ⁡ s ∈ 𝒫 B ⟼ ι x ∈ B | ψ = s | ∃! x ∈ B ψ ∩ 𝒫 B
12 dmres ⊢ dom ⁡ s ∈ 𝒫 B ⟼ ι x ∈ B | ψ ↾ s | ∃! x ∈ B ψ = s | ∃! x ∈ B ψ ∩ dom ⁡ s ∈ 𝒫 B ⟼ ι x ∈ B | ψ
13 dfrab2 ⊢ s ∈ 𝒫 B | ∃! x ∈ B ψ = s | ∃! x ∈ B ψ ∩ 𝒫 B
14 11 12 13 3eqtr4i ⊢ dom ⁡ s ∈ 𝒫 B ⟼ ι x ∈ B | ψ ↾ s | ∃! x ∈ B ψ = s ∈ 𝒫 B | ∃! x ∈ B ψ
15 7 14 eqtrdi ⊢ φ → dom ⁡ G = s ∈ 𝒫 B | ∃! x ∈ B ψ