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	syl5bi	|- ( 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	syl5bi	|- ( 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 ) ) = (/) )