Theorem glbdm

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

	Ref	Expression
Hypotheses	glbfval.b	|- B = ( Base ` K )
	glbfval.l	|- .<_ = ( le ` K )
	glbfval.g	|- G = ( glb ` K )
	glbfval.p	|- ( ps <-> ( A. y e. s x .<_ y /\ A. z e. B ( A. y e. s z .<_ y -> z .<_ x ) ) )
	glbfval.k	|- ( ph -> K e. V )
Assertion	glbdm	|- ( ph -> dom G = { s e. ~P B | E! x e. B ps } )

Proof

Step	Hyp	Ref	Expression
1		glbfval.b	|- B = ( Base ` K )
2		glbfval.l	|- .<_ = ( le ` K )
3		glbfval.g	|- G = ( glb ` K )
4		glbfval.p	|- ( ps <-> ( A. y e. s x .<_ y /\ A. z e. B ( A. y e. s z .<_ y -> z .<_ x ) ) )
5		glbfval.k	|- ( ph -> K e. V )
6	1 2 3 4 5	glbfval	|- ( ph -> G = ( ( s e. ~P B |-> ( iota_ x e. B ps ) ) |` { s | E! x e. B ps } ) )
7	6	dmeqd	|- ( ph -> dom G = dom ( ( s e. ~P B |-> ( iota_ x e. B ps ) ) |` { s | E! x e. B ps } ) )
8		riotaex	|- ( iota_ x e. B ps ) e. _V
9		eqid	|- ( s e. ~P B |-> ( iota_ x e. B ps ) ) = ( s e. ~P B |-> ( iota_ x e. B ps ) )
10	8 9	dmmpti	|- dom ( s e. ~P B |-> ( iota_ x e. B ps ) ) = ~P B
11	10	ineq2i	|- ( { s | E! x e. B ps } i^i dom ( s e. ~P B |-> ( iota_ x e. B ps ) ) ) = ( { s | E! x e. B ps } i^i ~P B )
12		dmres	|- dom ( ( s e. ~P B |-> ( iota_ x e. B ps ) ) |` { s | E! x e. B ps } ) = ( { s | E! x e. B ps } i^i dom ( s e. ~P B |-> ( iota_ x e. B ps ) ) )
13		dfrab2	|- { s e. ~P B | E! x e. B ps } = ( { s | E! x e. B ps } i^i ~P B )
14	11 12 13	3eqtr4i	|- dom ( ( s e. ~P B |-> ( iota_ x e. B ps ) ) |` { s | E! x e. B ps } ) = { s e. ~P B | E! x e. B ps }
15	7 14	eqtrdi	|- ( ph -> dom G = { s e. ~P B | E! x e. B ps } )