Theorem psref2

Description: A poset is antisymmetric and reflexive. (Contributed by FL, 3-Aug-2009)

	Ref	Expression
Assertion	psref2	⊢ ( 𝑅 ∈ PosetRel → ( 𝑅 ∩ ◡ 𝑅 ) = ( I ↾ ∪ ∪ 𝑅 ) )

Proof

Step	Hyp	Ref	Expression
1		isps	⊢ ( 𝑅 ∈ PosetRel → ( 𝑅 ∈ PosetRel ↔ ( Rel 𝑅 ∧ ( 𝑅 ∘ 𝑅 ) ⊆ 𝑅 ∧ ( 𝑅 ∩ ◡ 𝑅 ) = ( I ↾ ∪ ∪ 𝑅 ) ) ) )
2	1	ibi	⊢ ( 𝑅 ∈ PosetRel → ( Rel 𝑅 ∧ ( 𝑅 ∘ 𝑅 ) ⊆ 𝑅 ∧ ( 𝑅 ∩ ◡ 𝑅 ) = ( I ↾ ∪ ∪ 𝑅 ) ) )
3	2	simp3d	⊢ ( 𝑅 ∈ PosetRel → ( 𝑅 ∩ ◡ 𝑅 ) = ( I ↾ ∪ ∪ 𝑅 ) )