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 )