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	$⊢ \underset{˙}{\leq} = \leq_{K}$
	lubfval.u	$⊢ U = lub (K)$
	lubfval.p	$⊢ ψ \leftrightarrow (\forall y \in s y \underset{˙}{\leq} x \land \forall z \in B (\forall y \in s y \underset{˙}{\leq} z \to x \underset{˙}{\leq} z))$
	lubfval.k	$⊢ φ \to K \in V$
Assertion	lubdm	$⊢ φ \to dom U = \{s \in 𝒫 B \| \exists! x \in B ψ\}$

Step	Hyp	Ref	Expression
1		lubfval.b	$⊢ B = {Base}_{K}$
2		lubfval.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		lubfval.u	$⊢ U = lub (K)$
4		lubfval.p	$⊢ ψ \leftrightarrow (\forall y \in s y \underset{˙}{\leq} x \land \forall z \in B (\forall y \in s y \underset{˙}{\leq} z \to x \underset{˙}{\leq} z))$
5		lubfval.k	$⊢ φ \to K \in V$
6	1 2 3 4 5	lubfval	$⊢ φ \to U = {(s \in 𝒫 B ⟼ (ι x \in B \| ψ)) ↾}_{\{s \| \exists! x \in B ψ\}}$
7	6	dmeqd	$⊢ φ \to dom U = dom ({(s \in 𝒫 B ⟼ (ι x \in B \| ψ)) ↾}_{\{s \| \exists! x \in B ψ\}})$
8		riotaex	$⊢ (ι x \in B \| ψ) \in V$
9		eqid	$⊢ (s \in 𝒫 B ⟼ (ι x \in B \| ψ)) = (s \in 𝒫 B ⟼ (ι x \in B \| ψ))$
10	8 9	dmmpti	$⊢ dom (s \in 𝒫 B ⟼ (ι x \in B \| ψ)) = 𝒫 B$
11	10	ineq2i	$⊢ \{s \| \exists! x \in B ψ\} \cap dom (s \in 𝒫 B ⟼ (ι x \in B \| ψ)) = \{s \| \exists! x \in B ψ\} \cap 𝒫 B$
12		dmres	$⊢ dom ({(s \in 𝒫 B ⟼ (ι x \in B \| ψ)) ↾}_{\{s \| \exists! x \in B ψ\}}) = \{s \| \exists! x \in B ψ\} \cap dom (s \in 𝒫 B ⟼ (ι x \in B \| ψ))$
13		dfrab2	$⊢ \{s \in 𝒫 B \| \exists! x \in B ψ\} = \{s \| \exists! x \in B ψ\} \cap 𝒫 B$
14	11 12 13	3eqtr4i	$⊢ dom ({(s \in 𝒫 B ⟼ (ι x \in B \| ψ)) ↾}_{\{s \| \exists! x \in B ψ\}}) = \{s \in 𝒫 B \| \exists! x \in B ψ\}$
15	7 14	eqtrdi	$⊢ φ \to dom U = \{s \in 𝒫 B \| \exists! x \in B ψ\}$

Metamath Proof Explorer