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

Metamath Proof Explorer

Definition df-p1

Description: Define poset unit. (Contributed by NM, 22-Oct-2011)

		Ref	Expression
	Assertion	df-p1	$⊢ 1. = (p \in V ⟼ lub (p) ({Base}_{p}))$

Step	Hyp	Ref	Expression
0		cp1	$class 1.$
1		vp	$setvar p$
2		cvv	$class V$
3		club	$class lub$
4	1	cv	$setvar p$
5	4 3	cfv	$class lub (p)$
6		cbs	$class Base$
7	4 6	cfv	$class {Base}_{p}$
8	7 5	cfv	$class lub (p) ({Base}_{p})$
9	1 2 8	cmpt	$class (p \in V ⟼ lub (p) ({Base}_{p}))$
10	0 9	wceq	$wff 1. = (p \in V ⟼ lub (p) ({Base}_{p}))$