Theorem dfantisymrel4

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

	Ref	Expression
Assertion	dfantisymrel4	⊢ ( AntisymRel 𝑅 ↔ ( ( 𝑅 ∩ ◡ 𝑅 ) ⊆ I ∧ Rel 𝑅 ) )

Proof

Step	Hyp	Ref	Expression
1		df-antisymrel	⊢ ( AntisymRel 𝑅 ↔ ( CnvRefRel ( 𝑅 ∩ ◡ 𝑅 ) ∧ Rel 𝑅 ) )
2		relcnv	⊢ Rel ◡ 𝑅
3		relin2	⊢ ( Rel ◡ 𝑅 → Rel ( 𝑅 ∩ ◡ 𝑅 ) )
4	2 3	ax-mp	⊢ Rel ( 𝑅 ∩ ◡ 𝑅 )
5		dfcnvrefrel4	⊢ ( CnvRefRel ( 𝑅 ∩ ◡ 𝑅 ) ↔ ( ( 𝑅 ∩ ◡ 𝑅 ) ⊆ I ∧ Rel ( 𝑅 ∩ ◡ 𝑅 ) ) )
6	4 5	mpbiran2	⊢ ( CnvRefRel ( 𝑅 ∩ ◡ 𝑅 ) ↔ ( 𝑅 ∩ ◡ 𝑅 ) ⊆ I )
7	1 6	bianbi	⊢ ( AntisymRel 𝑅 ↔ ( ( 𝑅 ∩ ◡ 𝑅 ) ⊆ I ∧ Rel 𝑅 ) )