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

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