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 )