Theorem lubprlem

Description: Lemma for lubprdm and lubpr . (Contributed by Zhi Wang, 26-Sep-2024)

	Ref	Expression
Hypotheses	lubpr.k	|- ( ph -> K e. Poset )
	lubpr.b	|- B = ( Base ` K )
	lubpr.x	|- ( ph -> X e. B )
	lubpr.y	|- ( ph -> Y e. B )
	lubpr.l	|- .<_ = ( le ` K )
	lubpr.c	|- ( ph -> X .<_ Y )
	lubpr.s	|- ( ph -> S = { X , Y } )
	lubpr.u	|- U = ( lub ` K )
Assertion	lubprlem	|- ( ph -> ( S e. dom U /\ ( U ` S ) = Y ) )

Proof

Step	Hyp	Ref	Expression
1		lubpr.k	|- ( ph -> K e. Poset )
2		lubpr.b	|- B = ( Base ` K )
3		lubpr.x	|- ( ph -> X e. B )
4		lubpr.y	|- ( ph -> Y e. B )
5		lubpr.l	|- .<_ = ( le ` K )
6		lubpr.c	|- ( ph -> X .<_ Y )
7		lubpr.s	|- ( ph -> S = { X , Y } )
8		lubpr.u	|- U = ( lub ` K )
9		breq1	|- ( z = X -> ( z .<_ Y <-> X .<_ Y ) )
10	9 3 6	elrabd	|- ( ph -> X e. { z e. B | z .<_ Y } )
11		breq1	|- ( z = Y -> ( z .<_ Y <-> Y .<_ Y ) )
12	2 5	posref	|- ( ( K e. Poset /\ Y e. B ) -> Y .<_ Y )
13	1 4 12	syl2anc	|- ( ph -> Y .<_ Y )
14	11 4 13	elrabd	|- ( ph -> Y e. { z e. B | z .<_ Y } )
15	10 14	prssd	|- ( ph -> { X , Y } C_ { z e. B | z .<_ Y } )
16	2 5 8 1 4	lublecl	|- ( ph -> { z e. B | z .<_ Y } e. dom U )
17	2 5 8 1 4	lubid	|- ( ph -> ( U ` { z e. B | z .<_ Y } ) = Y )
18		prid2g	|- ( Y e. B -> Y e. { X , Y } )
19	4 18	syl	|- ( ph -> Y e. { X , Y } )
20	17 19	eqeltrd	|- ( ph -> ( U ` { z e. B | z .<_ Y } ) e. { X , Y } )
21	1 15 8 16 20	lubsscl	|- ( ph -> ( { X , Y } e. dom U /\ ( U ` { X , Y } ) = ( U ` { z e. B | z .<_ Y } ) ) )
22	21	simpld	|- ( ph -> { X , Y } e. dom U )
23	7 22	eqeltrd	|- ( ph -> S e. dom U )
24	7	fveq2d	|- ( ph -> ( U ` S ) = ( U ` { X , Y } ) )
25	21	simprd	|- ( ph -> ( U ` { X , Y } ) = ( U ` { z e. B | z .<_ Y } ) )
26	24 25 17	3eqtrd	|- ( ph -> ( U ` S ) = Y )
27	23 26	jca	|- ( ph -> ( S e. dom U /\ ( U ` S ) = Y ) )