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

Metamath Proof Explorer

Theorem ple1

Description: Any element is less than or equal to a poset's upper bound (if defined). (Contributed by NM, 22-Oct-2011) (Revised by NM, 13-Sep-2018)

Ref Expression
Hypotheses ple1.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
ple1.u ⊢ 𝑈 = ( lub ‘ 𝐾 )
ple1.l ⊢ ≤ = ( le ‘ 𝐾 )
ple1.1 ⊢ 1 = ( 1. ‘ 𝐾 )
ple1.k ⊢ ( 𝜑 → 𝐾 ∈ 𝑉 )
ple1.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
ple1.d ⊢ ( 𝜑 → 𝐵 ∈ dom 𝑈 )
Assertion ple1 ( 𝜑 → 𝑋 ≤ 1 )

Proof

Step Hyp Ref Expression
1 ple1.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 ple1.u ⊢ 𝑈 = ( lub ‘ 𝐾 )
3 ple1.l ⊢ ≤ = ( le ‘ 𝐾 )
4 ple1.1 ⊢ 1 = ( 1. ‘ 𝐾 )
5 ple1.k ⊢ ( 𝜑 → 𝐾 ∈ 𝑉 )
6 ple1.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
7 ple1.d ⊢ ( 𝜑 → 𝐵 ∈ dom 𝑈 )
8 1 3 2 5 7 6 luble ⊢ ( 𝜑 → 𝑋 ≤ ( 𝑈 ‘ 𝐵 ) )
9 1 2 4 p1val ⊢ ( 𝐾 ∈ 𝑉 → 1 = ( 𝑈 ‘ 𝐵 ) )
10 5 9 syl ⊢ ( 𝜑 → 1 = ( 𝑈 ‘ 𝐵 ) )
11 8 10 breqtrrd ⊢ ( 𝜑 → 𝑋 ≤ 1 )