Theorem lubdm

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

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

Proof

Step	Hyp	Ref	Expression
1		lubfval.b	|- B = ( Base ` K )
2		lubfval.l	|- .<_ = ( le ` K )
3		lubfval.u	|- U = ( lub ` K )
4		lubfval.p	|- ( ps <-> ( A. y e. s y .<_ x /\ A. z e. B ( A. y e. s y .<_ z -> x .<_ z ) ) )
5		lubfval.k	|- ( ph -> K e. V )
6	1 2 3 4 5	lubfval	|- ( ph -> U = ( ( s e. ~P B |-> ( iota_ x e. B ps ) ) |` { s | E! x e. B ps } ) )
7	6	dmeqd	|- ( ph -> dom U = 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 U = { s e. ~P B | E! x e. B ps } )