unitcl

Description: A unit is an element of the base set. (Contributed by Mario Carneiro, 1-Dec-2014)

Step	Hyp	Ref	Expression
1		unitcl.1	$⊢ B = {Base}_{R}$
2		unitcl.2	$⊢ U = Unit (R)$
3		eqid	$⊢ 1_{R} = 1_{R}$
4		eqid	$⊢ ∥_{r} (R) = ∥_{r} (R)$
5		eqid	$⊢ {opp}_{r} (R) = {opp}_{r} (R)$
6		eqid	$⊢ ∥_{r} ({opp}_{r} (R)) = ∥_{r} ({opp}_{r} (R))$
7	2 3 4 5 6	isunit	$⊢ X \in U \leftrightarrow (X ∥_{r} (R) 1_{R} \land X ∥_{r} ({opp}_{r} (R)) 1_{R})$
8	7	simplbi	$⊢ X \in U \to X ∥_{r} (R) 1_{R}$
9	1 4	dvdsrcl	$⊢ X ∥_{r} (R) 1_{R} \to X \in B$
10	8 9	syl	$⊢ X \in U \to X \in B$

Metamath Proof Explorer