Metamath Proof Explorer

Theorem intasym

Description: Two ways of saying a relation is antisymmetric. Definition of antisymmetry in Schechter p. 51. (Contributed by NM, 9-Sep-2004) (Proof shortened by Andrew Salmon, 27-Aug-2011)

Ref Expression
Assertion intasym 
|- ( ( R i^i `' R ) C_ _I <-> A. x A. y ( ( x R y /\ y R x ) -> x = y ) )

Proof

Step Hyp Ref Expression
1 relcnv 
 |-  Rel `' R
2 relin2 
 |-  ( Rel `' R -> Rel ( R i^i `' R ) )
3 ssrel 
 |-  ( Rel ( R i^i `' R ) -> ( ( R i^i `' R ) C_ _I <-> A. x A. y ( <. x , y >. e. ( R i^i `' R ) -> <. x , y >. e. _I ) ) )
4 1 2 3 mp2b 
 |-  ( ( R i^i `' R ) C_ _I <-> A. x A. y ( <. x , y >. e. ( R i^i `' R ) -> <. x , y >. e. _I ) )
5 elin 
 |-  ( <. x , y >. e. ( R i^i `' R ) <-> ( <. x , y >. e. R /\ <. x , y >. e. `' R ) )
6 df-br 
 |-  ( x R y <-> <. x , y >. e. R )
7 vex 
 |-  x e. _V
8 vex 
 |-  y e. _V
9 7 8 brcnv 
 |-  ( x `' R y <-> y R x )
10 df-br 
 |-  ( x `' R y <-> <. x , y >. e. `' R )
11 9 10 bitr3i 
 |-  ( y R x <-> <. x , y >. e. `' R )
12 6 11 anbi12i 
 |-  ( ( x R y /\ y R x ) <-> ( <. x , y >. e. R /\ <. x , y >. e. `' R ) )
13 5 12 bitr4i 
 |-  ( <. x , y >. e. ( R i^i `' R ) <-> ( x R y /\ y R x ) )
14 df-br 
 |-  ( x _I y <-> <. x , y >. e. _I )
15 8 ideq 
 |-  ( x _I y <-> x = y )
16 14 15 bitr3i 
 |-  ( <. x , y >. e. _I <-> x = y )
17 13 16 imbi12i 
 |-  ( ( <. x , y >. e. ( R i^i `' R ) -> <. x , y >. e. _I ) <-> ( ( x R y /\ y R x ) -> x = y ) )
18 17 2albii 
 |-  ( A. x A. y ( <. x , y >. e. ( R i^i `' R ) -> <. x , y >. e. _I ) <-> A. x A. y ( ( x R y /\ y R x ) -> x = y ) )
19 4 18 bitri 
 |-  ( ( R i^i `' R ) C_ _I <-> A. x A. y ( ( x R y /\ y R x ) -> x = y ) )