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	$$⊢B={\mathrm{Base}}_K$$
	ple1.u	$$⊢U=\mathrm{lub}\left(K\right)$$
	ple1.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
	ple1.1	$$⊢\underset{\dot{}}{1}=\mathrm{1.}\left(K\right)$$
	ple1.k	$$⊢\phi \to K\in V$$
	ple1.x	$$⊢\phi \to X\in B$$
	ple1.d	$$⊢\phi \to B\in \mathrm{dom}U$$
Assertion	ple1	$$⊢\phi \to X\underset{\dot{}}{\le }\underset{\dot{}}{1}$$

Proof

Step	Hyp	Ref	Expression
1		ple1.b	$$⊢B={\mathrm{Base}}_K$$
2		ple1.u	$$⊢U=\mathrm{lub}\left(K\right)$$
3		ple1.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
4		ple1.1	$$⊢\underset{\dot{}}{1}=\mathrm{1.}\left(K\right)$$
5		ple1.k	$$⊢\phi \to K\in V$$
6		ple1.x	$$⊢\phi \to X\in B$$
7		ple1.d	$$⊢\phi \to B\in \mathrm{dom}U$$
8	1 3 2 5 7 6	luble	$$⊢\phi \to X\underset{\dot{}}{\le }U\left(B\right)$$
9	1 2 4	p1val	$$⊢K\in V\to \underset{\dot{}}{1}=U\left(B\right)$$
10	5 9	syl	$$⊢\phi \to \underset{\dot{}}{1}=U\left(B\right)$$
11	8 10	breqtrrd	$$⊢\phi \to X\underset{\dot{}}{\le }\underset{\dot{}}{1}$$