Theorem cnvpsb

Description: The converse of a poset is a poset. (Contributed by FL, 5-Jan-2009)

	Ref	Expression
Assertion	cnvpsb	⊢ ( Rel 𝑅 → ( 𝑅 ∈ PosetRel ↔ ◡ 𝑅 ∈ PosetRel ) )

Proof

Step	Hyp	Ref	Expression
1		cnvps	⊢ ( 𝑅 ∈ PosetRel → ◡ 𝑅 ∈ PosetRel )
2		cnvps	⊢ ( ◡ 𝑅 ∈ PosetRel → ◡ ◡ 𝑅 ∈ PosetRel )
3		dfrel2	⊢ ( Rel 𝑅 ↔ ◡ ◡ 𝑅 = 𝑅 )
4		eleq1	⊢ ( ◡ ◡ 𝑅 = 𝑅 → ( ◡ ◡ 𝑅 ∈ PosetRel ↔ 𝑅 ∈ PosetRel ) )
5	4	biimpd	⊢ ( ◡ ◡ 𝑅 = 𝑅 → ( ◡ ◡ 𝑅 ∈ PosetRel → 𝑅 ∈ PosetRel ) )
6	3 5	sylbi	⊢ ( Rel 𝑅 → ( ◡ ◡ 𝑅 ∈ PosetRel → 𝑅 ∈ PosetRel ) )
7	2 6	syl5	⊢ ( Rel 𝑅 → ( ◡ 𝑅 ∈ PosetRel → 𝑅 ∈ PosetRel ) )
8	1 7	impbid2	⊢ ( Rel 𝑅 → ( 𝑅 ∈ PosetRel ↔ ◡ 𝑅 ∈ PosetRel ) )