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

Metamath Proof Explorer

Theorem intirr

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

Ref Expression
Assertion intirr 
|- ( ( R i^i _I ) = (/) <-> A. x -. x R x )

Proof

Step Hyp Ref Expression
1 incom 
 |-  ( R i^i _I ) = ( _I i^i R )
2 1 eqeq1i 
 |-  ( ( R i^i _I ) = (/) <-> ( _I i^i R ) = (/) )
3 disj2 
 |-  ( ( _I i^i R ) = (/) <-> _I C_ ( _V \ R ) )
4 reli 
 |-  Rel _I
5 ssrel 
 |-  ( Rel _I -> ( _I C_ ( _V \ R ) <-> A. x A. y ( <. x , y >. e. _I -> <. x , y >. e. ( _V \ R ) ) ) )
6 4 5 ax-mp 
 |-  ( _I C_ ( _V \ R ) <-> A. x A. y ( <. x , y >. e. _I -> <. x , y >. e. ( _V \ R ) ) )
7 2 3 6 3bitri 
 |-  ( ( R i^i _I ) = (/) <-> A. x A. y ( <. x , y >. e. _I -> <. x , y >. e. ( _V \ R ) ) )
8 equcom 
 |-  ( y = x <-> x = y )
9 vex 
 |-  y e. _V
10 9 ideq 
 |-  ( x _I y <-> x = y )
11 df-br 
 |-  ( x _I y <-> <. x , y >. e. _I )
12 8 10 11 3bitr2i 
 |-  ( y = x <-> <. x , y >. e. _I )
13 opex 
 |-  <. x , y >. e. _V
14 13 biantrur 
 |-  ( -. <. x , y >. e. R <-> ( <. x , y >. e. _V /\ -. <. x , y >. e. R ) )
15 eldif 
 |-  ( <. x , y >. e. ( _V \ R ) <-> ( <. x , y >. e. _V /\ -. <. x , y >. e. R ) )
16 14 15 bitr4i 
 |-  ( -. <. x , y >. e. R <-> <. x , y >. e. ( _V \ R ) )
17 df-br 
 |-  ( x R y <-> <. x , y >. e. R )
18 16 17 xchnxbir 
 |-  ( -. x R y <-> <. x , y >. e. ( _V \ R ) )
19 12 18 imbi12i 
 |-  ( ( y = x -> -. x R y ) <-> ( <. x , y >. e. _I -> <. x , y >. e. ( _V \ R ) ) )
20 19 2albii 
 |-  ( A. x A. y ( y = x -> -. x R y ) <-> A. x A. y ( <. x , y >. e. _I -> <. x , y >. e. ( _V \ R ) ) )
21 breq2 
 |-  ( y = x -> ( x R y <-> x R x ) )
22 21 notbid 
 |-  ( y = x -> ( -. x R y <-> -. x R x ) )
23 22 equsalvw 
 |-  ( A. y ( y = x -> -. x R y ) <-> -. x R x )
24 23 albii 
 |-  ( A. x A. y ( y = x -> -. x R y ) <-> A. x -. x R x )
25 7 20 24 3bitr2i 
 |-  ( ( R i^i _I ) = (/) <-> A. x -. x R x )