Metamath Proof Explorer


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 syl5eq
 |-  ( 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 )