Theorem p0le

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	p0le.b	$$⊢B={\mathrm{Base}}_K$$
	p0le.g	$$⊢G=\mathrm{glb}\left(K\right)$$
	p0le.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
	p0le.0	$$⊢\underset{\dot{}}{0}=\mathrm{0.}\left(K\right)$$
	p0le.k	$$⊢\phi \to K\in V$$
	p0le.x	$$⊢\phi \to X\in B$$
	p0le.d	$$⊢\phi \to B\in \mathrm{dom}G$$
Assertion	p0le	$$⊢\phi \to \underset{\dot{}}{0}\underset{\dot{}}{\le }X$$

Proof

Step	Hyp	Ref	Expression
1		p0le.b	$$⊢B={\mathrm{Base}}_K$$
2		p0le.g	$$⊢G=\mathrm{glb}\left(K\right)$$
3		p0le.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
4		p0le.0	$$⊢\underset{\dot{}}{0}=\mathrm{0.}\left(K\right)$$
5		p0le.k	$$⊢\phi \to K\in V$$
6		p0le.x	$$⊢\phi \to X\in B$$
7		p0le.d	$$⊢\phi \to B\in \mathrm{dom}G$$
8	1 2 4	p0val	$$⊢K\in V\to \underset{\dot{}}{0}=G\left(B\right)$$
9	5 8	syl	$$⊢\phi \to \underset{\dot{}}{0}=G\left(B\right)$$
10	1 3 2 5 7 6	glble	$$⊢\phi \to G\left(B\right)\underset{\dot{}}{\le }X$$
11	9 10	eqbrtrd	$$⊢\phi \to \underset{\dot{}}{0}\underset{\dot{}}{\le }X$$