Metamath Proof Explorer

Theorem pstr2

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

		Ref	Expression
	Assertion	pstr2	\|- ( R e. PosetRel -> ( R o. R ) C_ R )

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

Step

Hyp

Ref

Expression

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

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

 |-  ( R e. PosetRel -> ( R o. R ) C_ R )