Theorem glbeldm

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

	Ref	Expression
Hypotheses	glbeldm.b	|- B = ( Base ` K )
	glbeldm.l	|- .<_ = ( le ` K )
	glbeldm.g	|- G = ( glb ` K )
	glbeldm.p	|- ( ps <-> ( A. y e. S x .<_ y /\ A. z e. B ( A. y e. S z .<_ y -> z .<_ x ) ) )
	glbeldm.k	|- ( ph -> K e. V )
Assertion	glbeldm	|- ( ph -> ( S e. dom G <-> ( S C_ B /\ E! x e. B ps ) ) )

Proof

Step	Hyp	Ref	Expression
1		glbeldm.b	|- B = ( Base ` K )
2		glbeldm.l	|- .<_ = ( le ` K )
3		glbeldm.g	|- G = ( glb ` K )
4		glbeldm.p	|- ( ps <-> ( A. y e. S x .<_ y /\ A. z e. B ( A. y e. S z .<_ y -> z .<_ x ) ) )
5		glbeldm.k	|- ( ph -> K e. V )
6		biid	|- ( ( A. y e. s x .<_ y /\ A. z e. B ( A. y e. s z .<_ y -> z .<_ x ) ) <-> ( A. y e. s x .<_ y /\ A. z e. B ( A. y e. s z .<_ y -> z .<_ x ) ) )
7	1 2 3 6 5	glbdm	|- ( ph -> dom G = { s e. ~P B | E! x e. B ( A. y e. s x .<_ y /\ A. z e. B ( A. y e. s z .<_ y -> z .<_ x ) ) } )
8	7	eleq2d	|- ( ph -> ( S e. dom G <-> S e. { s e. ~P B | E! x e. B ( A. y e. s x .<_ y /\ A. z e. B ( A. y e. s z .<_ y -> z .<_ x ) ) } ) )
9		raleq	|- ( s = S -> ( A. y e. s x .<_ y <-> A. y e. S x .<_ y ) )
10		raleq	|- ( s = S -> ( A. y e. s z .<_ y <-> A. y e. S z .<_ y ) )
11	10	imbi1d	|- ( s = S -> ( ( A. y e. s z .<_ y -> z .<_ x ) <-> ( A. y e. S z .<_ y -> z .<_ x ) ) )
12	11	ralbidv	|- ( s = S -> ( A. z e. B ( A. y e. s z .<_ y -> z .<_ x ) <-> A. z e. B ( A. y e. S z .<_ y -> z .<_ x ) ) )
13	9 12	anbi12d	|- ( s = S -> ( ( A. y e. s x .<_ y /\ A. z e. B ( A. y e. s z .<_ y -> z .<_ x ) ) <-> ( A. y e. S x .<_ y /\ A. z e. B ( A. y e. S z .<_ y -> z .<_ x ) ) ) )
14	13	reubidv	|- ( s = S -> ( E! x e. B ( A. y e. s x .<_ y /\ A. z e. B ( A. y e. s z .<_ y -> z .<_ x ) ) <-> E! x e. B ( A. y e. S x .<_ y /\ A. z e. B ( A. y e. S z .<_ y -> z .<_ x ) ) ) )
15	4	reubii	|- ( E! x e. B ps <-> E! x e. B ( A. y e. S x .<_ y /\ A. z e. B ( A. y e. S z .<_ y -> z .<_ x ) ) )
16	14 15	bitr4di	|- ( s = S -> ( E! x e. B ( A. y e. s x .<_ y /\ A. z e. B ( A. y e. s z .<_ y -> z .<_ x ) ) <-> E! x e. B ps ) )
17	16	elrab	|- ( S e. { s e. ~P B | E! x e. B ( A. y e. s x .<_ y /\ A. z e. B ( A. y e. s z .<_ y -> z .<_ x ) ) } <-> ( S e. ~P B /\ E! x e. B ps ) )
18	1	fvexi	|- B e. _V
19	18	elpw2	|- ( S e. ~P B <-> S C_ B )
20	19	anbi1i	|- ( ( S e. ~P B /\ E! x e. B ps ) <-> ( S C_ B /\ E! x e. B ps ) )
21	17 20	bitri	|- ( S e. { s e. ~P B | E! x e. B ( A. y e. s x .<_ y /\ A. z e. B ( A. y e. s z .<_ y -> z .<_ x ) ) } <-> ( S C_ B /\ E! x e. B ps ) )
22	8 21	bitrdi	|- ( ph -> ( S e. dom G <-> ( S C_ B /\ E! x e. B ps ) ) )