Metamath Proof Explorer

Theorem psasym

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

		Ref	Expression
	Assertion	psasym	\|- ( ( R e. PosetRel /\ A R B /\ B R A ) -> A = B )

Step	Hyp	Ref	Expression
1		pslem	\|- ( R e. PosetRel -> ( ( ( A R B /\ B R A ) -> A R A ) /\ ( A e. U. U. R -> A R A ) /\ ( ( A R B /\ B R A ) -> A = B ) ) )
2	1	simp3d	\|- ( R e. PosetRel -> ( ( A R B /\ B R A ) -> A = B ) )
3	2	3impib	\|- ( ( R e. PosetRel /\ A R B /\ B R A ) -> A = B )

Step

Hyp

Ref

Expression

 |-  ( R e. PosetRel -> ( ( ( A R B /\ B R A ) -> A R A ) /\ ( A e. U. U. R -> A R A ) /\ ( ( A R B /\ B R A ) -> A = B ) ) )

 |-  ( R e. PosetRel -> ( ( A R B /\ B R A ) -> A = B ) )

 |-  ( ( R e. PosetRel /\ A R B /\ B R A ) -> A = B )