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

Metamath Proof Explorer

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 = {Base}_{K}$
		p0le.g	$⊢ G = glb (K)$
		p0le.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
		p0le.0	$⊢ \underset{˙}{0} = 0. (K)$
		p0le.k	$⊢ φ \to K \in V$
		p0le.x	$⊢ φ \to X \in B$
		p0le.d	$⊢ φ \to B \in dom G$
	Assertion	p0le	$⊢ φ \to \underset{˙}{0} \underset{˙}{\leq} X$

Proof

Step	Hyp	Ref	Expression
1		p0le.b	$⊢ B = {Base}_{K}$
2		p0le.g	$⊢ G = glb (K)$
3		p0le.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
4		p0le.0	$⊢ \underset{˙}{0} = 0. (K)$
5		p0le.k	$⊢ φ \to K \in V$
6		p0le.x	$⊢ φ \to X \in B$
7		p0le.d	$⊢ φ \to B \in dom G$
8	1 2 4	p0val	$⊢ K \in V \to \underset{˙}{0} = G (B)$
9	5 8	syl	$⊢ φ \to \underset{˙}{0} = G (B)$
10	1 3 2 5 7 6	glble	$⊢ φ \to G (B) \underset{˙}{\leq} X$
11	9 10	eqbrtrd	$⊢ φ \to \underset{˙}{0} \underset{˙}{\leq} X$