Theorem lubeldm

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

	Ref	Expression
Hypotheses	lubeldm.b	$$⊢B={\mathrm{Base}}_K$$
	lubeldm.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
	lubeldm.u	$$⊢U=\mathrm{lub}\left(K\right)$$
	lubeldm.p	$$⊢\psi \leftrightarrow \left(\forall y\in Sy\underset{\dot{}}{\le }x\wedge \forall z\in B\left(\forall y\in Sy\underset{\dot{}}{\le }z\to x\underset{\dot{}}{\le }z\right)\right)$$
	lubeldm.k	$$⊢\phi \to K\in V$$
Assertion	lubeldm	$$⊢\phi \to \left(S\in \mathrm{dom}U\leftrightarrow \left(S\subseteq B\wedge \exists !x\in B\psi \right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		lubeldm.b	$$⊢B={\mathrm{Base}}_K$$
2		lubeldm.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
3		lubeldm.u	$$⊢U=\mathrm{lub}\left(K\right)$$
4		lubeldm.p	$$⊢\psi \leftrightarrow \left(\forall y\in Sy\underset{\dot{}}{\le }x\wedge \forall z\in B\left(\forall y\in Sy\underset{\dot{}}{\le }z\to x\underset{\dot{}}{\le }z\right)\right)$$
5		lubeldm.k	$$⊢\phi \to K\in V$$
6		biid	$$⊢\left(\forall y\in sy\underset{\dot{}}{\le }x\wedge \forall z\in B\left(\forall y\in sy\underset{\dot{}}{\le }z\to x\underset{\dot{}}{\le }z\right)\right)\leftrightarrow \left(\forall y\in sy\underset{\dot{}}{\le }x\wedge \forall z\in B\left(\forall y\in sy\underset{\dot{}}{\le }z\to x\underset{\dot{}}{\le }z\right)\right)$$
7	1 2 3 6 5	lubdm	$$⊢\phi \to \mathrm{dom}U=\left\{s\in 𝒫B|\exists !x\in B\left(\forall y\in sy\underset{\dot{}}{\le }x\wedge \forall z\in B\left(\forall y\in sy\underset{\dot{}}{\le }z\to x\underset{\dot{}}{\le }z\right)\right)\right\}$$
8	7	eleq2d	$$⊢\phi \to \left(S\in \mathrm{dom}U\leftrightarrow S\in \left\{s\in 𝒫B|\exists !x\in B\left(\forall y\in sy\underset{\dot{}}{\le }x\wedge \forall z\in B\left(\forall y\in sy\underset{\dot{}}{\le }z\to x\underset{\dot{}}{\le }z\right)\right)\right\}\right)$$
9		raleq	$$⊢s=S\to \left(\forall y\in sy\underset{\dot{}}{\le }x\leftrightarrow \forall y\in Sy\underset{\dot{}}{\le }x\right)$$
10		raleq	$$⊢s=S\to \left(\forall y\in sy\underset{\dot{}}{\le }z\leftrightarrow \forall y\in Sy\underset{\dot{}}{\le }z\right)$$
11	10	imbi1d	$$⊢s=S\to \left(\left(\forall y\in sy\underset{\dot{}}{\le }z\to x\underset{\dot{}}{\le }z\right)\leftrightarrow \left(\forall y\in Sy\underset{\dot{}}{\le }z\to x\underset{\dot{}}{\le }z\right)\right)$$
12	11	ralbidv	$$⊢s=S\to \left(\forall z\in B\left(\forall y\in sy\underset{\dot{}}{\le }z\to x\underset{\dot{}}{\le }z\right)\leftrightarrow \forall z\in B\left(\forall y\in Sy\underset{\dot{}}{\le }z\to x\underset{\dot{}}{\le }z\right)\right)$$
13	9 12	anbi12d	$$⊢s=S\to \left(\left(\forall y\in sy\underset{\dot{}}{\le }x\wedge \forall z\in B\left(\forall y\in sy\underset{\dot{}}{\le }z\to x\underset{\dot{}}{\le }z\right)\right)\leftrightarrow \left(\forall y\in Sy\underset{\dot{}}{\le }x\wedge \forall z\in B\left(\forall y\in Sy\underset{\dot{}}{\le }z\to x\underset{\dot{}}{\le }z\right)\right)\right)$$
14	13	reubidv	$$⊢s=S\to \left(\exists !x\in B\left(\forall y\in sy\underset{\dot{}}{\le }x\wedge \forall z\in B\left(\forall y\in sy\underset{\dot{}}{\le }z\to x\underset{\dot{}}{\le }z\right)\right)\leftrightarrow \exists !x\in B\left(\forall y\in Sy\underset{\dot{}}{\le }x\wedge \forall z\in B\left(\forall y\in Sy\underset{\dot{}}{\le }z\to x\underset{\dot{}}{\le }z\right)\right)\right)$$
15	4	reubii	$$⊢\exists !x\in B\psi \leftrightarrow \exists !x\in B\left(\forall y\in Sy\underset{\dot{}}{\le }x\wedge \forall z\in B\left(\forall y\in Sy\underset{\dot{}}{\le }z\to x\underset{\dot{}}{\le }z\right)\right)$$
16	14 15	bitr4di	$$⊢s=S\to \left(\exists !x\in B\left(\forall y\in sy\underset{\dot{}}{\le }x\wedge \forall z\in B\left(\forall y\in sy\underset{\dot{}}{\le }z\to x\underset{\dot{}}{\le }z\right)\right)\leftrightarrow \exists !x\in B\psi \right)$$
17	16	elrab	$$⊢S\in \left\{s\in 𝒫B|\exists !x\in B\left(\forall y\in sy\underset{\dot{}}{\le }x\wedge \forall z\in B\left(\forall y\in sy\underset{\dot{}}{\le }z\to x\underset{\dot{}}{\le }z\right)\right)\right\}\leftrightarrow \left(S\in 𝒫B\wedge \exists !x\in B\psi \right)$$
18	1	fvexi	$$⊢B\in \mathrm{V}$$
19	18	elpw2	$$⊢S\in 𝒫B\leftrightarrow S\subseteq B$$
20	19	anbi1i	$$⊢\left(S\in 𝒫B\wedge \exists !x\in B\psi \right)\leftrightarrow \left(S\subseteq B\wedge \exists !x\in B\psi \right)$$
21	17 20	bitri	$$⊢S\in \left\{s\in 𝒫B|\exists !x\in B\left(\forall y\in sy\underset{\dot{}}{\le }x\wedge \forall z\in B\left(\forall y\in sy\underset{\dot{}}{\le }z\to x\underset{\dot{}}{\le }z\right)\right)\right\}\leftrightarrow \left(S\subseteq B\wedge \exists !x\in B\psi \right)$$
22	8 21	bitrdi	$$⊢\phi \to \left(S\in \mathrm{dom}U\leftrightarrow \left(S\subseteq B\wedge \exists !x\in B\psi \right)\right)$$