Theorem dfantisymrel5

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

	Ref	Expression
Assertion	dfantisymrel5	⊢ ( AntisymRel 𝑅 ↔ ( ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑥 ) → 𝑥 = 𝑦 ) ∧ 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		dfcnvrefrel5	⊢ ( CnvRefRel ( 𝑅 ∩ ◡ 𝑅 ) ↔ ( ∀ 𝑥 ∀ 𝑦 ( 𝑥 ( 𝑅 ∩ ◡ 𝑅 ) 𝑦 → 𝑥 = 𝑦 ) ∧ Rel ( 𝑅 ∩ ◡ 𝑅 ) ) )
6	4 5	mpbiran2	⊢ ( CnvRefRel ( 𝑅 ∩ ◡ 𝑅 ) ↔ ∀ 𝑥 ∀ 𝑦 ( 𝑥 ( 𝑅 ∩ ◡ 𝑅 ) 𝑦 → 𝑥 = 𝑦 ) )
7		brcnvin	⊢ ( ( 𝑥 ∈ V ∧ 𝑦 ∈ V ) → ( 𝑥 ( 𝑅 ∩ ◡ 𝑅 ) 𝑦 ↔ ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑥 ) ) )
8	7	el2v	⊢ ( 𝑥 ( 𝑅 ∩ ◡ 𝑅 ) 𝑦 ↔ ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑥 ) )
9	8	imbi1i	⊢ ( ( 𝑥 ( 𝑅 ∩ ◡ 𝑅 ) 𝑦 → 𝑥 = 𝑦 ) ↔ ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑥 ) → 𝑥 = 𝑦 ) )
10	9	2albii	⊢ ( ∀ 𝑥 ∀ 𝑦 ( 𝑥 ( 𝑅 ∩ ◡ 𝑅 ) 𝑦 → 𝑥 = 𝑦 ) ↔ ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑥 ) → 𝑥 = 𝑦 ) )
11	6 10	bitri	⊢ ( CnvRefRel ( 𝑅 ∩ ◡ 𝑅 ) ↔ ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑥 ) → 𝑥 = 𝑦 ) )
12	1 11	bianbi	⊢ ( AntisymRel 𝑅 ↔ ( ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑥 ) → 𝑥 = 𝑦 ) ∧ Rel 𝑅 ) )