Theorem lubeldm

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

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

Proof

Step	Hyp	Ref	Expression
1		lubeldm.b	|- B = ( Base ` K )
2		lubeldm.l	|- .<_ = ( le ` K )
3		lubeldm.u	|- U = ( lub ` K )
4		lubeldm.p	|- ( ps <-> ( A. y e. S y .<_ x /\ A. z e. B ( A. y e. S y .<_ z -> x .<_ z ) ) )
5		lubeldm.k	|- ( ph -> K e. V )
6		biid	|- ( ( A. y e. s y .<_ x /\ A. z e. B ( A. y e. s y .<_ z -> x .<_ z ) ) <-> ( A. y e. s y .<_ x /\ A. z e. B ( A. y e. s y .<_ z -> x .<_ z ) ) )
7	1 2 3 6 5	lubdm	|- ( ph -> dom U = { s e. ~P B | E! x e. B ( A. y e. s y .<_ x /\ A. z e. B ( A. y e. s y .<_ z -> x .<_ z ) ) } )
8	7	eleq2d	|- ( ph -> ( S e. dom U <-> S e. { s e. ~P B | E! x e. B ( A. y e. s y .<_ x /\ A. z e. B ( A. y e. s y .<_ z -> x .<_ z ) ) } ) )
9		raleq	|- ( s = S -> ( A. y e. s y .<_ x <-> A. y e. S y .<_ x ) )
10		raleq	|- ( s = S -> ( A. y e. s y .<_ z <-> A. y e. S y .<_ z ) )
11	10	imbi1d	|- ( s = S -> ( ( A. y e. s y .<_ z -> x .<_ z ) <-> ( A. y e. S y .<_ z -> x .<_ z ) ) )
12	11	ralbidv	|- ( s = S -> ( A. z e. B ( A. y e. s y .<_ z -> x .<_ z ) <-> A. z e. B ( A. y e. S y .<_ z -> x .<_ z ) ) )
13	9 12	anbi12d	|- ( s = S -> ( ( A. y e. s y .<_ x /\ A. z e. B ( A. y e. s y .<_ z -> x .<_ z ) ) <-> ( A. y e. S y .<_ x /\ A. z e. B ( A. y e. S y .<_ z -> x .<_ z ) ) ) )
14	13	reubidv	|- ( s = S -> ( E! x e. B ( A. y e. s y .<_ x /\ A. z e. B ( A. y e. s y .<_ z -> x .<_ z ) ) <-> E! x e. B ( A. y e. S y .<_ x /\ A. z e. B ( A. y e. S y .<_ z -> x .<_ z ) ) ) )
15	4	reubii	|- ( E! x e. B ps <-> E! x e. B ( A. y e. S y .<_ x /\ A. z e. B ( A. y e. S y .<_ z -> x .<_ z ) ) )
16	14 15	bitr4di	|- ( s = S -> ( E! x e. B ( A. y e. s y .<_ x /\ A. z e. B ( A. y e. s y .<_ z -> x .<_ z ) ) <-> E! x e. B ps ) )
17	16	elrab	|- ( S e. { s e. ~P B | E! x e. B ( A. y e. s y .<_ x /\ A. z e. B ( A. y e. s y .<_ z -> x .<_ z ) ) } <-> ( 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 y .<_ x /\ A. z e. B ( A. y e. s y .<_ z -> x .<_ z ) ) } <-> ( S C_ B /\ E! x e. B ps ) )
22	8 21	bitrdi	|- ( ph -> ( S e. dom U <-> ( S C_ B /\ E! x e. B ps ) ) )