Theorem antisymrelres

Description: (Contributed by Peter Mazsa, 25-Jun-2024)

	Ref	Expression
Assertion	antisymrelres	⊢ ( AntisymRel ( 𝑅 ↾ 𝐴 ) ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑥 ) → 𝑥 = 𝑦 ) )

Proof

Step	Hyp	Ref	Expression
1		relres	⊢ Rel ( 𝑅 ↾ 𝐴 )
2		dfantisymrel5	⊢ ( AntisymRel ( 𝑅 ↾ 𝐴 ) ↔ ( ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 ( 𝑅 ↾ 𝐴 ) 𝑦 ∧ 𝑦 ( 𝑅 ↾ 𝐴 ) 𝑥 ) → 𝑥 = 𝑦 ) ∧ Rel ( 𝑅 ↾ 𝐴 ) ) )
3	1 2	mpbiran2	⊢ ( AntisymRel ( 𝑅 ↾ 𝐴 ) ↔ ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 ( 𝑅 ↾ 𝐴 ) 𝑦 ∧ 𝑦 ( 𝑅 ↾ 𝐴 ) 𝑥 ) → 𝑥 = 𝑦 ) )
4		brres	⊢ ( 𝑦 ∈ V → ( 𝑥 ( 𝑅 ↾ 𝐴 ) 𝑦 ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝑅 𝑦 ) ) )
5	4	elv	⊢ ( 𝑥 ( 𝑅 ↾ 𝐴 ) 𝑦 ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝑅 𝑦 ) )
6		brres	⊢ ( 𝑥 ∈ V → ( 𝑦 ( 𝑅 ↾ 𝐴 ) 𝑥 ↔ ( 𝑦 ∈ 𝐴 ∧ 𝑦 𝑅 𝑥 ) ) )
7	6	elv	⊢ ( 𝑦 ( 𝑅 ↾ 𝐴 ) 𝑥 ↔ ( 𝑦 ∈ 𝐴 ∧ 𝑦 𝑅 𝑥 ) )
8	5 7	anbi12i	⊢ ( ( 𝑥 ( 𝑅 ↾ 𝐴 ) 𝑦 ∧ 𝑦 ( 𝑅 ↾ 𝐴 ) 𝑥 ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝑅 𝑦 ) ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑦 𝑅 𝑥 ) ) )
9		an4	⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝑅 𝑦 ) ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑦 𝑅 𝑥 ) ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑥 ) ) )
10	8 9	bitri	⊢ ( ( 𝑥 ( 𝑅 ↾ 𝐴 ) 𝑦 ∧ 𝑦 ( 𝑅 ↾ 𝐴 ) 𝑥 ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑥 ) ) )
11	10	imbi1i	⊢ ( ( ( 𝑥 ( 𝑅 ↾ 𝐴 ) 𝑦 ∧ 𝑦 ( 𝑅 ↾ 𝐴 ) 𝑥 ) → 𝑥 = 𝑦 ) ↔ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑥 ) ) → 𝑥 = 𝑦 ) )
12	11	2albii	⊢ ( ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 ( 𝑅 ↾ 𝐴 ) 𝑦 ∧ 𝑦 ( 𝑅 ↾ 𝐴 ) 𝑥 ) → 𝑥 = 𝑦 ) ↔ ∀ 𝑥 ∀ 𝑦 ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑥 ) ) → 𝑥 = 𝑦 ) )
13		r2alan	⊢ ( ∀ 𝑥 ∀ 𝑦 ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑥 ) ) → 𝑥 = 𝑦 ) ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑥 ) → 𝑥 = 𝑦 ) )
14	3 12 13	3bitri	⊢ ( AntisymRel ( 𝑅 ↾ 𝐴 ) ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑥 ) → 𝑥 = 𝑦 ) )