Theorem glbprlem

Description: Lemma for glbprdm and glbpr . (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\}$$
	glbpr.g	$$⊢G=\mathrm{glb}\left(K\right)$$
Assertion	glbprlem	$$⊢\phi \to \left(S\in \mathrm{dom}G\wedge G\left(S\right)=X\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		glbpr.g	$$⊢G=\mathrm{glb}\left(K\right)$$
9		eqid	$$⊢\mathrm{ODual}\left(K\right)=\mathrm{ODual}\left(K\right)$$
10	9	odupos	$$⊢K\in \mathrm{Poset}\to \mathrm{ODual}\left(K\right)\in \mathrm{Poset}$$
11	1 10	syl	$$⊢\phi \to \mathrm{ODual}\left(K\right)\in \mathrm{Poset}$$
12	9 2	odubas	$$⊢B={\mathrm{Base}}_{\mathrm{ODual}\left(K\right)}$$
13	9 5	oduleval	$$⊢{\underset{\dot{}}{\le }}^{-1}={\le }_{\mathrm{ODual}\left(K\right)}$$
14		brcnvg	$$⊢\left(Y\in B\wedge X\in B\right)\to \left(Y{\underset{\dot{}}{\le }}^{-1}X\leftrightarrow X\underset{\dot{}}{\le }Y\right)$$
15	4 3 14	syl2anc	$$⊢\phi \to \left(Y{\underset{\dot{}}{\le }}^{-1}X\leftrightarrow X\underset{\dot{}}{\le }Y\right)$$
16	6 15	mpbird	$$⊢\phi \to Y{\underset{\dot{}}{\le }}^{-1}X$$
17		prcom	$$⊢\left\{X,Y\right\}=\left\{Y,X\right\}$$
18	7 17	eqtrdi	$$⊢\phi \to S=\left\{Y,X\right\}$$
19		eqid	$$⊢\mathrm{lub}\left(\mathrm{ODual}\left(K\right)\right)=\mathrm{lub}\left(\mathrm{ODual}\left(K\right)\right)$$
20	11 12 4 3 13 16 18 19	lubprdm	$$⊢\phi \to S\in \mathrm{dom}\mathrm{lub}\left(\mathrm{ODual}\left(K\right)\right)$$
21	9 8	odulub	$$⊢K\in \mathrm{Poset}\to G=\mathrm{lub}\left(\mathrm{ODual}\left(K\right)\right)$$
22	1 21	syl	$$⊢\phi \to G=\mathrm{lub}\left(\mathrm{ODual}\left(K\right)\right)$$
23	22	dmeqd	$$⊢\phi \to \mathrm{dom}G=\mathrm{dom}\mathrm{lub}\left(\mathrm{ODual}\left(K\right)\right)$$
24	20 23	eleqtrrd	$$⊢\phi \to S\in \mathrm{dom}G$$
25	22	fveq1d	$$⊢\phi \to G\left(S\right)=\mathrm{lub}\left(\mathrm{ODual}\left(K\right)\right)\left(S\right)$$
26	11 12 4 3 13 16 18 19	lubpr	$$⊢\phi \to \mathrm{lub}\left(\mathrm{ODual}\left(K\right)\right)\left(S\right)=X$$
27	25 26	eqtrd	$$⊢\phi \to G\left(S\right)=X$$
28	24 27	jca	$$⊢\phi \to \left(S\in \mathrm{dom}G\wedge G\left(S\right)=X\right)$$