Metamath Proof Explorer


Theorem psref

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

Ref Expression
Hypothesis psref.1 𝑋 = dom 𝑅
Assertion psref ( ( 𝑅 ∈ PosetRel ∧ 𝐴𝑋 ) → 𝐴 𝑅 𝐴 )

Proof

Step Hyp Ref Expression
1 psref.1 𝑋 = dom 𝑅
2 psdmrn ( 𝑅 ∈ PosetRel → ( dom 𝑅 = 𝑅 ∧ ran 𝑅 = 𝑅 ) )
3 2 simpld ( 𝑅 ∈ PosetRel → dom 𝑅 = 𝑅 )
4 1 3 syl5eq ( 𝑅 ∈ PosetRel → 𝑋 = 𝑅 )
5 4 eleq2d ( 𝑅 ∈ PosetRel → ( 𝐴𝑋𝐴 𝑅 ) )
6 pslem ( 𝑅 ∈ PosetRel → ( ( ( 𝐴 𝑅 𝐴𝐴 𝑅 𝐴 ) → 𝐴 𝑅 𝐴 ) ∧ ( 𝐴 𝑅𝐴 𝑅 𝐴 ) ∧ ( ( 𝐴 𝑅 𝐴𝐴 𝑅 𝐴 ) → 𝐴 = 𝐴 ) ) )
7 6 simp2d ( 𝑅 ∈ PosetRel → ( 𝐴 𝑅𝐴 𝑅 𝐴 ) )
8 5 7 sylbid ( 𝑅 ∈ PosetRel → ( 𝐴𝑋𝐴 𝑅 𝐴 ) )
9 8 imp ( ( 𝑅 ∈ PosetRel ∧ 𝐴𝑋 ) → 𝐴 𝑅 𝐴 )