Theorem lubprlem

Description: Lemma for lubprdm and lubpr . (Contributed by Zhi Wang, 26-Sep-2024)

	Ref	Expression
Hypotheses	lubpr.k	$$⊢\phi \to K\in \mathrm{Poset}$$
	lubpr.b	$$⊢B={\mathrm{Base}}_K$$
	lubpr.x	$$⊢\phi \to X\in B$$
	lubpr.y	$$⊢\phi \to Y\in B$$
	lubpr.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
	lubpr.c	$$⊢\phi \to X\underset{\dot{}}{\le }Y$$
	lubpr.s	$$⊢\phi \to S=\left\{X,Y\right\}$$
	lubpr.u	$$⊢U=\mathrm{lub}\left(K\right)$$
Assertion	lubprlem	$$⊢\phi \to \left(S\in \mathrm{dom}U\wedge U\left(S\right)=Y\right)$$

Proof

Step	Hyp	Ref	Expression
1		lubpr.k	$$⊢\phi \to K\in \mathrm{Poset}$$
2		lubpr.b	$$⊢B={\mathrm{Base}}_K$$
3		lubpr.x	$$⊢\phi \to X\in B$$
4		lubpr.y	$$⊢\phi \to Y\in B$$
5		lubpr.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
6		lubpr.c	$$⊢\phi \to X\underset{\dot{}}{\le }Y$$
7		lubpr.s	$$⊢\phi \to S=\left\{X,Y\right\}$$
8		lubpr.u	$$⊢U=\mathrm{lub}\left(K\right)$$
9		breq1	$$⊢z=X\to \left(z\underset{\dot{}}{\le }Y\leftrightarrow X\underset{\dot{}}{\le }Y\right)$$
10	9 3 6	elrabd	$$⊢\phi \to X\in \left\{z\in B|z\underset{\dot{}}{\le }Y\right\}$$
11		breq1	$$⊢z=Y\to \left(z\underset{\dot{}}{\le }Y\leftrightarrow Y\underset{\dot{}}{\le }Y\right)$$
12	2 5	posref	$$⊢\left(K\in \mathrm{Poset}\wedge Y\in B\right)\to Y\underset{\dot{}}{\le }Y$$
13	1 4 12	syl2anc	$$⊢\phi \to Y\underset{\dot{}}{\le }Y$$
14	11 4 13	elrabd	$$⊢\phi \to Y\in \left\{z\in B|z\underset{\dot{}}{\le }Y\right\}$$
15	10 14	prssd	$$⊢\phi \to \left\{X,Y\right\}\subseteq \left\{z\in B|z\underset{\dot{}}{\le }Y\right\}$$
16	2 5 8 1 4	lublecl	$$⊢\phi \to \left\{z\in B|z\underset{\dot{}}{\le }Y\right\}\in \mathrm{dom}U$$
17	2 5 8 1 4	lubid	$$⊢\phi \to U\left(\left\{z\in B|z\underset{\dot{}}{\le }Y\right\}\right)=Y$$
18		prid2g	$$⊢Y\in B\to Y\in \left\{X,Y\right\}$$
19	4 18	syl	$$⊢\phi \to Y\in \left\{X,Y\right\}$$
20	17 19	eqeltrd	$$⊢\phi \to U\left(\left\{z\in B|z\underset{\dot{}}{\le }Y\right\}\right)\in \left\{X,Y\right\}$$
21	1 15 8 16 20	lubsscl	$$⊢\phi \to \left(\left\{X,Y\right\}\in \mathrm{dom}U\wedge U\left(\left\{X,Y\right\}\right)=U\left(\left\{z\in B|z\underset{\dot{}}{\le }Y\right\}\right)\right)$$
22	21	simpld	$$⊢\phi \to \left\{X,Y\right\}\in \mathrm{dom}U$$
23	7 22	eqeltrd	$$⊢\phi \to S\in \mathrm{dom}U$$
24	7	fveq2d	$$⊢\phi \to U\left(S\right)=U\left(\left\{X,Y\right\}\right)$$
25	21	simprd	$$⊢\phi \to U\left(\left\{X,Y\right\}\right)=U\left(\left\{z\in B|z\underset{\dot{}}{\le }Y\right\}\right)$$
26	24 25 17	3eqtrd	$$⊢\phi \to U\left(S\right)=Y$$
27	23 26	jca	$$⊢\phi \to \left(S\in \mathrm{dom}U\wedge U\left(S\right)=Y\right)$$