Metamath Proof Explorer

Theorem antisymrelres

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

Ref Expression
Assertion antisymrelres 
|- ( AntisymRel ( R |` A ) <-> A. x e. A A. y e. A ( ( x R y /\ y R x ) -> x = y ) )

Proof

Step Hyp Ref Expression
1 relres 
 |-  Rel ( R |` A )
2 dfantisymrel5 
 |-  ( AntisymRel ( R |` A ) <-> ( A. x A. y ( ( x ( R |` A ) y /\ y ( R |` A ) x ) -> x = y ) /\ Rel ( R |` A ) ) )
3 1 2 mpbiran2 
 |-  ( AntisymRel ( R |` A ) <-> A. x A. y ( ( x ( R |` A ) y /\ y ( R |` A ) x ) -> x = y ) )
4 brres 
 |-  ( y e. _V -> ( x ( R |` A ) y <-> ( x e. A /\ x R y ) ) )
5 4 elv 
 |-  ( x ( R |` A ) y <-> ( x e. A /\ x R y ) )
6 brres 
 |-  ( x e. _V -> ( y ( R |` A ) x <-> ( y e. A /\ y R x ) ) )
7 6 elv 
 |-  ( y ( R |` A ) x <-> ( y e. A /\ y R x ) )
8 5 7 anbi12i 
 |-  ( ( x ( R |` A ) y /\ y ( R |` A ) x ) <-> ( ( x e. A /\ x R y ) /\ ( y e. A /\ y R x ) ) )
9 an4 
 |-  ( ( ( x e. A /\ x R y ) /\ ( y e. A /\ y R x ) ) <-> ( ( x e. A /\ y e. A ) /\ ( x R y /\ y R x ) ) )
10 8 9 bitri 
 |-  ( ( x ( R |` A ) y /\ y ( R |` A ) x ) <-> ( ( x e. A /\ y e. A ) /\ ( x R y /\ y R x ) ) )
11 10 imbi1i 
 |-  ( ( ( x ( R |` A ) y /\ y ( R |` A ) x ) -> x = y ) <-> ( ( ( x e. A /\ y e. A ) /\ ( x R y /\ y R x ) ) -> x = y ) )
12 11 2albii 
 |-  ( A. x A. y ( ( x ( R |` A ) y /\ y ( R |` A ) x ) -> x = y ) <-> A. x A. y ( ( ( x e. A /\ y e. A ) /\ ( x R y /\ y R x ) ) -> x = y ) )
13 r2alan 
 |-  ( A. x A. y ( ( ( x e. A /\ y e. A ) /\ ( x R y /\ y R x ) ) -> x = y ) <-> A. x e. A A. y e. A ( ( x R y /\ y R x ) -> x = y ) )
14 3 12 13 3bitri 
 |-  ( AntisymRel ( R |` A ) <-> A. x e. A A. y e. A ( ( x R y /\ y R x ) -> x = y ) )