Theorem psref

Description: A poset is reflexive. (Contributed by NM, 13-May-2008)

	Ref	Expression
Hypothesis	psref.1	|- X = dom R
Assertion	psref	|- ( ( R e. PosetRel /\ A e. X ) -> A R A )

Proof

Step	Hyp	Ref	Expression
1		psref.1	|- X = dom R
2		psdmrn	|- ( R e. PosetRel -> ( dom R = U. U. R /\ ran R = U. U. R ) )
3	2	simpld	|- ( R e. PosetRel -> dom R = U. U. R )
4	1 3	eqtrid	|- ( R e. PosetRel -> X = U. U. R )
5	4	eleq2d	|- ( R e. PosetRel -> ( A e. X <-> A e. U. U. R ) )
6		pslem	|- ( R e. PosetRel -> ( ( ( A R A /\ A R A ) -> A R A ) /\ ( A e. U. U. R -> A R A ) /\ ( ( A R A /\ A R A ) -> A = A ) ) )
7	6	simp2d	|- ( R e. PosetRel -> ( A e. U. U. R -> A R A ) )
8	5 7	sylbid	|- ( R e. PosetRel -> ( A e. X -> A R A ) )
9	8	imp	|- ( ( R e. PosetRel /\ A e. X ) -> A R A )