Metamath Proof Explorer

Theorem psrel

Description: A poset is a relation. (Contributed by NM, 12-May-2008)

		Ref	Expression
	Assertion	psrel	\|- ( A e. PosetRel -> Rel A )

Step	Hyp	Ref	Expression
1		isps	\|- ( A e. PosetRel -> ( A e. PosetRel <-> ( Rel A /\ ( A o. A ) C_ A /\ ( A i^i `' A ) = ( _I \|` U. U. A ) ) ) )
2	1	ibi	\|- ( A e. PosetRel -> ( Rel A /\ ( A o. A ) C_ A /\ ( A i^i `' A ) = ( _I \|` U. U. A ) ) )
3	2	simp1d	\|- ( A e. PosetRel -> Rel A )

Step

Hyp

Ref

Expression

 |-  ( A e. PosetRel -> ( A e. PosetRel <-> ( Rel A /\ ( A o. A ) C_ A /\ ( A i^i `' A ) = ( _I |` U. U. A ) ) ) )

 |-  ( A e. PosetRel -> ( Rel A /\ ( A o. A ) C_ A /\ ( A i^i `' A ) = ( _I |` U. U. A ) ) )

 |-  ( A e. PosetRel -> Rel A )