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	$⊢ B = {Base}_{K}$
		ple1.u	$⊢ U = lub (K)$
		ple1.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
		ple1.1	$⊢ \underset{˙}{1} = 1. (K)$
		ple1.k	$⊢ φ \to K \in V$
		ple1.x	$⊢ φ \to X \in B$
		ple1.d	$⊢ φ \to B \in dom U$
	Assertion	ple1	$⊢ φ \to X \underset{˙}{\leq} \underset{˙}{1}$

Proof

Step	Hyp	Ref	Expression
1		ple1.b	$⊢ B = {Base}_{K}$
2		ple1.u	$⊢ U = lub (K)$
3		ple1.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
4		ple1.1	$⊢ \underset{˙}{1} = 1. (K)$
5		ple1.k	$⊢ φ \to K \in V$
6		ple1.x	$⊢ φ \to X \in B$
7		ple1.d	$⊢ φ \to B \in dom U$
8	1 3 2 5 7 6	luble	$⊢ φ \to X \underset{˙}{\leq} U (B)$
9	1 2 4	p1val	$⊢ K \in V \to \underset{˙}{1} = U (B)$
10	5 9	syl	$⊢ φ \to \underset{˙}{1} = U (B)$
11	8 10	breqtrrd	$⊢ φ \to X \underset{˙}{\leq} \underset{˙}{1}$