Theorem dfantisymrel4

Description: Alternate definition of the antisymmetric relation predicate. (Contributed by Peter Mazsa, 24-Jun-2024)

	Ref	Expression
Assertion	dfantisymrel4	$$⊢AntisymRelR\leftrightarrow \left(R\cap R^{-1}\subseteq \mathrm{I}\wedge \mathrm{Rel}R\right)$$

Proof

Step	Hyp	Ref	Expression
1		df-antisymrel	$$⊢AntisymRelR\leftrightarrow \left(CnvRefRel\left(R\cap R^{-1}\right)\wedge \mathrm{Rel}R\right)$$
2		relcnv	$$⊢\mathrm{Rel}{R}^{-1}$$
3		relin2	$$⊢\mathrm{Rel}{R}^{-1}\to \mathrm{Rel}\left(R\cap R^{-1}\right)$$
4	2 3	ax-mp	$$⊢\mathrm{Rel}\left(R\cap R^{-1}\right)$$
5		dfcnvrefrel4	$$⊢CnvRefRel\left(R\cap R^{-1}\right)\leftrightarrow \left(R\cap R^{-1}\subseteq \mathrm{I}\wedge \mathrm{Rel}\left(R\cap R^{-1}\right)\right)$$
6	4 5	mpbiran2	$$⊢CnvRefRel\left(R\cap R^{-1}\right)\leftrightarrow R\cap R^{-1}\subseteq \mathrm{I}$$
7	1 6	bianbi	$$⊢AntisymRelR\leftrightarrow \left(R\cap R^{-1}\subseteq \mathrm{I}\wedge \mathrm{Rel}R\right)$$