Theorem lubprlem

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

	Ref	Expression
Hypotheses	lubpr.k	⊢ ( 𝜑 → 𝐾 ∈ Poset )
	lubpr.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
	lubpr.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
	lubpr.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
	lubpr.l	⊢ ≤ = ( le ‘ 𝐾 )
	lubpr.c	⊢ ( 𝜑 → 𝑋 ≤ 𝑌 )
	lubpr.s	⊢ ( 𝜑 → 𝑆 = { 𝑋 , 𝑌 } )
	lubpr.u	⊢ 𝑈 = ( lub ‘ 𝐾 )
Assertion	lubprlem	⊢ ( 𝜑 → ( 𝑆 ∈ dom 𝑈 ∧ ( 𝑈 ‘ 𝑆 ) = 𝑌 ) )

Proof

Step	Hyp	Ref	Expression
1		lubpr.k	⊢ ( 𝜑 → 𝐾 ∈ Poset )
2		lubpr.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
3		lubpr.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
4		lubpr.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
5		lubpr.l	⊢ ≤ = ( le ‘ 𝐾 )
6		lubpr.c	⊢ ( 𝜑 → 𝑋 ≤ 𝑌 )
7		lubpr.s	⊢ ( 𝜑 → 𝑆 = { 𝑋 , 𝑌 } )
8		lubpr.u	⊢ 𝑈 = ( lub ‘ 𝐾 )
9		breq1	⊢ ( 𝑧 = 𝑋 → ( 𝑧 ≤ 𝑌 ↔ 𝑋 ≤ 𝑌 ) )
10	9 3 6	elrabd	⊢ ( 𝜑 → 𝑋 ∈ { 𝑧 ∈ 𝐵 ∣ 𝑧 ≤ 𝑌 } )
11		breq1	⊢ ( 𝑧 = 𝑌 → ( 𝑧 ≤ 𝑌 ↔ 𝑌 ≤ 𝑌 ) )
12	2 5	posref	⊢ ( ( 𝐾 ∈ Poset ∧ 𝑌 ∈ 𝐵 ) → 𝑌 ≤ 𝑌 )
13	1 4 12	syl2anc	⊢ ( 𝜑 → 𝑌 ≤ 𝑌 )
14	11 4 13	elrabd	⊢ ( 𝜑 → 𝑌 ∈ { 𝑧 ∈ 𝐵 ∣ 𝑧 ≤ 𝑌 } )
15	10 14	prssd	⊢ ( 𝜑 → { 𝑋 , 𝑌 } ⊆ { 𝑧 ∈ 𝐵 ∣ 𝑧 ≤ 𝑌 } )
16	2 5 8 1 4	lublecl	⊢ ( 𝜑 → { 𝑧 ∈ 𝐵 ∣ 𝑧 ≤ 𝑌 } ∈ dom 𝑈 )
17	2 5 8 1 4	lubid	⊢ ( 𝜑 → ( 𝑈 ‘ { 𝑧 ∈ 𝐵 ∣ 𝑧 ≤ 𝑌 } ) = 𝑌 )
18		prid2g	⊢ ( 𝑌 ∈ 𝐵 → 𝑌 ∈ { 𝑋 , 𝑌 } )
19	4 18	syl	⊢ ( 𝜑 → 𝑌 ∈ { 𝑋 , 𝑌 } )
20	17 19	eqeltrd	⊢ ( 𝜑 → ( 𝑈 ‘ { 𝑧 ∈ 𝐵 ∣ 𝑧 ≤ 𝑌 } ) ∈ { 𝑋 , 𝑌 } )
21	1 15 8 16 20	lubsscl	⊢ ( 𝜑 → ( { 𝑋 , 𝑌 } ∈ dom 𝑈 ∧ ( 𝑈 ‘ { 𝑋 , 𝑌 } ) = ( 𝑈 ‘ { 𝑧 ∈ 𝐵 ∣ 𝑧 ≤ 𝑌 } ) ) )
22	21	simpld	⊢ ( 𝜑 → { 𝑋 , 𝑌 } ∈ dom 𝑈 )
23	7 22	eqeltrd	⊢ ( 𝜑 → 𝑆 ∈ dom 𝑈 )
24	7	fveq2d	⊢ ( 𝜑 → ( 𝑈 ‘ 𝑆 ) = ( 𝑈 ‘ { 𝑋 , 𝑌 } ) )
25	21	simprd	⊢ ( 𝜑 → ( 𝑈 ‘ { 𝑋 , 𝑌 } ) = ( 𝑈 ‘ { 𝑧 ∈ 𝐵 ∣ 𝑧 ≤ 𝑌 } ) )
26	24 25 17	3eqtrd	⊢ ( 𝜑 → ( 𝑈 ‘ 𝑆 ) = 𝑌 )
27	23 26	jca	⊢ ( 𝜑 → ( 𝑆 ∈ dom 𝑈 ∧ ( 𝑈 ‘ 𝑆 ) = 𝑌 ) )