This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem asymref

Description: Two ways of saying a relation is antisymmetric and reflexive. U. U. R is the field of a relation by relfld . (Contributed by NM, 6-May-2008) (Proof shortened by Andrew Salmon, 27-Aug-2011)

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

Proof

Step Hyp Ref Expression
1 df-br 
 |-  ( x R y <-> <. x , y >. e. R )
2 vex 
 |-  x e. _V
3 vex 
 |-  y e. _V
4 2 3 opeluu 
 |-  ( <. x , y >. e. R -> ( x e. U. U. R /\ y e. U. U. R ) )
5 1 4 sylbi 
 |-  ( x R y -> ( x e. U. U. R /\ y e. U. U. R ) )
6 5 simpld 
 |-  ( x R y -> x e. U. U. R )
7 6 adantr 
 |-  ( ( x R y /\ y R x ) -> x e. U. U. R )
8 7 pm4.71ri 
 |-  ( ( x R y /\ y R x ) <-> ( x e. U. U. R /\ ( x R y /\ y R x ) ) )
9 8 bibi1i 
 |-  ( ( ( x R y /\ y R x ) <-> ( x e. U. U. R /\ x = y ) ) <-> ( ( x e. U. U. R /\ ( x R y /\ y R x ) ) <-> ( x e. U. U. R /\ x = y ) ) )
10 elin 
 |-  ( <. x , y >. e. ( R i^i `' R ) <-> ( <. x , y >. e. R /\ <. x , y >. e. `' R ) )
11 2 3 brcnv 
 |-  ( x `' R y <-> y R x )
12 df-br 
 |-  ( x `' R y <-> <. x , y >. e. `' R )
13 11 12 bitr3i 
 |-  ( y R x <-> <. x , y >. e. `' R )
14 1 13 anbi12i 
 |-  ( ( x R y /\ y R x ) <-> ( <. x , y >. e. R /\ <. x , y >. e. `' R ) )
15 10 14 bitr4i 
 |-  ( <. x , y >. e. ( R i^i `' R ) <-> ( x R y /\ y R x ) )
16 3 opelresi 
 |-  ( <. x , y >. e. ( _I |` U. U. R ) <-> ( x e. U. U. R /\ <. x , y >. e. _I ) )
17 df-br 
 |-  ( x _I y <-> <. x , y >. e. _I )
18 3 ideq 
 |-  ( x _I y <-> x = y )
19 17 18 bitr3i 
 |-  ( <. x , y >. e. _I <-> x = y )
20 19 anbi2i 
 |-  ( ( x e. U. U. R /\ <. x , y >. e. _I ) <-> ( x e. U. U. R /\ x = y ) )
21 16 20 bitri 
 |-  ( <. x , y >. e. ( _I |` U. U. R ) <-> ( x e. U. U. R /\ x = y ) )
22 15 21 bibi12i 
 |-  ( ( <. x , y >. e. ( R i^i `' R ) <-> <. x , y >. e. ( _I |` U. U. R ) ) <-> ( ( x R y /\ y R x ) <-> ( x e. U. U. R /\ x = y ) ) )
23 pm5.32 
 |-  ( ( x e. U. U. R -> ( ( x R y /\ y R x ) <-> x = y ) ) <-> ( ( x e. U. U. R /\ ( x R y /\ y R x ) ) <-> ( x e. U. U. R /\ x = y ) ) )
24 9 22 23 3bitr4i 
 |-  ( ( <. x , y >. e. ( R i^i `' R ) <-> <. x , y >. e. ( _I |` U. U. R ) ) <-> ( x e. U. U. R -> ( ( x R y /\ y R x ) <-> x = y ) ) )
25 24 albii 
 |-  ( A. y ( <. x , y >. e. ( R i^i `' R ) <-> <. x , y >. e. ( _I |` U. U. R ) ) <-> A. y ( x e. U. U. R -> ( ( x R y /\ y R x ) <-> x = y ) ) )
26 19.21v 
 |-  ( A. y ( x e. U. U. R -> ( ( x R y /\ y R x ) <-> x = y ) ) <-> ( x e. U. U. R -> A. y ( ( x R y /\ y R x ) <-> x = y ) ) )
27 25 26 bitri 
 |-  ( A. y ( <. x , y >. e. ( R i^i `' R ) <-> <. x , y >. e. ( _I |` U. U. R ) ) <-> ( x e. U. U. R -> A. y ( ( x R y /\ y R x ) <-> x = y ) ) )
28 27 albii 
 |-  ( A. x A. y ( <. x , y >. e. ( R i^i `' R ) <-> <. x , y >. e. ( _I |` U. U. R ) ) <-> A. x ( x e. U. U. R -> A. y ( ( x R y /\ y R x ) <-> x = y ) ) )
29 relcnv 
 |-  Rel `' R
30 relin2 
 |-  ( Rel `' R -> Rel ( R i^i `' R ) )
31 29 30 ax-mp 
 |-  Rel ( R i^i `' R )
32 relres 
 |-  Rel ( _I |` U. U. R )
33 eqrel 
 |-  ( ( Rel ( R i^i `' R ) /\ Rel ( _I |` U. U. R ) ) -> ( ( R i^i `' R ) = ( _I |` U. U. R ) <-> A. x A. y ( <. x , y >. e. ( R i^i `' R ) <-> <. x , y >. e. ( _I |` U. U. R ) ) ) )
34 31 32 33 mp2an 
 |-  ( ( R i^i `' R ) = ( _I |` U. U. R ) <-> A. x A. y ( <. x , y >. e. ( R i^i `' R ) <-> <. x , y >. e. ( _I |` U. U. R ) ) )
35 df-ral 
 |-  ( A. x e. U. U. R A. y ( ( x R y /\ y R x ) <-> x = y ) <-> A. x ( x e. U. U. R -> A. y ( ( x R y /\ y R x ) <-> x = y ) ) )
36 28 34 35 3bitr4i 
 |-  ( ( R i^i `' R ) = ( _I |` U. U. R ) <-> A. x e. U. U. R A. y ( ( x R y /\ y R x ) <-> x = y ) )