Metamath Proof Explorer

Theorem lubdm

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

Ref Expression
Hypotheses lubfval.b ⊢ B = Base K
lubfval.l ⊢ ≤ ˙ = ≤ K
lubfval.u ⊢ U = lub ⁡ K
lubfval.p ⊢ ψ ↔ ∀ y ∈ s y ≤ ˙ x ∧ ∀ z ∈ B ∀ y ∈ s y ≤ ˙ z → x ≤ ˙ z
lubfval.k ⊢ φ → K ∈ V
Assertion lubdm ⊢ φ → dom ⁡ U = s ∈ 𝒫 B | ∃! x ∈ B ψ

Proof

Step Hyp Ref Expression
1 lubfval.b ⊢ B = Base K
2 lubfval.l ⊢ ≤ ˙ = ≤ K
3 lubfval.u ⊢ U = lub ⁡ K
4 lubfval.p ⊢ ψ ↔ ∀ y ∈ s y ≤ ˙ x ∧ ∀ z ∈ B ∀ y ∈ s y ≤ ˙ z → x ≤ ˙ z
5 lubfval.k ⊢ φ → K ∈ V
6 1 2 3 4 5 lubfval ⊢ φ → U = s ∈ 𝒫 B ⟼ ι x ∈ B | ψ ↾ s | ∃! x ∈ B ψ
7 6 dmeqd ⊢ φ → dom ⁡ U = 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 ⁡ U = s ∈ 𝒫 B | ∃! x ∈ B ψ