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 ⊢ 𝑋 = 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 eqtrid ⊢ ( 𝑅 ∈ PosetRel → 𝑋 = ∪ ∪ 𝑅 )
5 4 eleq2d ⊢ ( 𝑅 ∈ PosetRel → ( 𝐴 ∈ 𝑋 ↔ 𝐴 ∈ ∪ ∪ 𝑅 ) )
6 pslem ⊢ ( 𝑅 ∈ PosetRel → ( ( ( 𝐴 𝑅 𝐴 ∧ 𝐴 𝑅 𝐴 ) → 𝐴 𝑅 𝐴 ) ∧ ( 𝐴 ∈ ∪ ∪ 𝑅 → 𝐴 𝑅 𝐴 ) ∧ ( ( 𝐴 𝑅 𝐴 ∧ 𝐴 𝑅 𝐴 ) → 𝐴 = 𝐴 ) ) )
7 6 simp2d ⊢ ( 𝑅 ∈ PosetRel → ( 𝐴 ∈ ∪ ∪ 𝑅 → 𝐴 𝑅 𝐴 ) )
8 5 7 sylbid ⊢ ( 𝑅 ∈ PosetRel → ( 𝐴 ∈ 𝑋 → 𝐴 𝑅 𝐴 ) )
9 8 imp ⊢ ( ( 𝑅 ∈ PosetRel ∧ 𝐴 ∈ 𝑋 ) → 𝐴 𝑅 𝐴 )