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

Metamath Proof Explorer

Theorem poirr2

Description: A partial order is irreflexive. (Contributed by Mario Carneiro, 2-Nov-2015) (Proof shortened by Peter Mazsa, 2-Oct-2022)

Ref Expression
Assertion poirr2 
|- ( R Po A -> ( R i^i ( _I |` A ) ) = (/) )

Proof

Step Hyp Ref Expression
1 relres 
 |-  Rel ( _I |` A )
2 relin2 
 |-  ( Rel ( _I |` A ) -> Rel ( R i^i ( _I |` A ) ) )
3 1 2 mp1i 
 |-  ( R Po A -> Rel ( R i^i ( _I |` A ) ) )
4 df-br 
 |-  ( x ( R i^i ( _I |` A ) ) y <-> <. x , y >. e. ( R i^i ( _I |` A ) ) )
5 brin 
 |-  ( x ( R i^i ( _I |` A ) ) y <-> ( x R y /\ x ( _I |` A ) y ) )
6 4 5 bitr3i 
 |-  ( <. x , y >. e. ( R i^i ( _I |` A ) ) <-> ( x R y /\ x ( _I |` A ) y ) )
7 vex 
 |-  y e. _V
8 7 brresi 
 |-  ( x ( _I |` A ) y <-> ( x e. A /\ x _I y ) )
9 poirr 
 |-  ( ( R Po A /\ x e. A ) -> -. x R x )
10 7 ideq 
 |-  ( x _I y <-> x = y )
11 breq2 
 |-  ( x = y -> ( x R x <-> x R y ) )
12 10 11 sylbi 
 |-  ( x _I y -> ( x R x <-> x R y ) )
13 12 notbid 
 |-  ( x _I y -> ( -. x R x <-> -. x R y ) )
14 9 13 syl5ibcom 
 |-  ( ( R Po A /\ x e. A ) -> ( x _I y -> -. x R y ) )
15 14 expimpd 
 |-  ( R Po A -> ( ( x e. A /\ x _I y ) -> -. x R y ) )
16 8 15 biimtrid 
 |-  ( R Po A -> ( x ( _I |` A ) y -> -. x R y ) )
17 16 con2d 
 |-  ( R Po A -> ( x R y -> -. x ( _I |` A ) y ) )
18 imnan 
 |-  ( ( x R y -> -. x ( _I |` A ) y ) <-> -. ( x R y /\ x ( _I |` A ) y ) )
19 17 18 sylib 
 |-  ( R Po A -> -. ( x R y /\ x ( _I |` A ) y ) )
20 19 pm2.21d 
 |-  ( R Po A -> ( ( x R y /\ x ( _I |` A ) y ) -> <. x , y >. e. (/) ) )
21 6 20 biimtrid 
 |-  ( R Po A -> ( <. x , y >. e. ( R i^i ( _I |` A ) ) -> <. x , y >. e. (/) ) )
22 3 21 relssdv 
 |-  ( R Po A -> ( R i^i ( _I |` A ) ) C_ (/) )
23 ss0 
 |-  ( ( R i^i ( _I |` A ) ) C_ (/) -> ( R i^i ( _I |` A ) ) = (/) )
24 22 23 syl 
 |-  ( R Po A -> ( R i^i ( _I |` A ) ) = (/) )