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 ∈ PosetRel ∧ A ∈ X → A R A

Proof

Step Hyp Ref Expression
1 psref.1 ⊢ X = dom ⁡ R
2 psdmrn ⊢ R ∈ PosetRel → dom ⁡ R = ⋃ ⋃ R ∧ ran ⁡ R = ⋃ ⋃ R
3 2 simpld ⊢ R ∈ PosetRel → dom ⁡ R = ⋃ ⋃ R
4 1 3 eqtrid ⊢ R ∈ PosetRel → X = ⋃ ⋃ R
5 4 eleq2d ⊢ R ∈ PosetRel → A ∈ X ↔ A ∈ ⋃ ⋃ R
6 pslem ⊢ R ∈ PosetRel → A R A ∧ A R A → A R A ∧ A ∈ ⋃ ⋃ R → A R A ∧ A R A ∧ A R A → A = A
7 6 simp2d ⊢ R ∈ PosetRel → A ∈ ⋃ ⋃ R → A R A
8 5 7 sylbid ⊢ R ∈ PosetRel → A ∈ X → A R A
9 8 imp ⊢ R ∈ PosetRel ∧ A ∈ X → A R A