cnvpsb

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

		Ref	Expression
	Assertion	cnvpsb	$⊢ Rel R \to (R \in PosetRel \leftrightarrow R^{-1} \in PosetRel)$

Step	Hyp	Ref	Expression
1		cnvps	$⊢ R \in PosetRel \to R^{-1} \in PosetRel$
2		cnvps	$⊢ R^{-1} \in PosetRel \to {R^{-1}}^{-1} \in PosetRel$
3		dfrel2	$⊢ Rel R \leftrightarrow {R^{-1}}^{-1} = R$
4		eleq1	$⊢ {R^{-1}}^{-1} = R \to ({R^{-1}}^{-1} \in PosetRel \leftrightarrow R \in PosetRel)$
5	4	biimpd	$⊢ {R^{-1}}^{-1} = R \to ({R^{-1}}^{-1} \in PosetRel \to R \in PosetRel)$
6	3 5	sylbi	$⊢ Rel R \to ({R^{-1}}^{-1} \in PosetRel \to R \in PosetRel)$
7	2 6	syl5	$⊢ Rel R \to (R^{-1} \in PosetRel \to R \in PosetRel)$
8	1 7	impbid2	$⊢ Rel R \to (R \in PosetRel \leftrightarrow R^{-1} \in PosetRel)$

Metamath Proof Explorer