This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝑈 ∧ ( 𝑈 ‘ 𝑆 ) = 𝑌 ) )