Theorem isdir

Description: A condition for a relation to be a direction. (Contributed by Jeff Hankins, 25-Nov-2009) (Revised by Mario Carneiro, 22-Nov-2013)

	Ref	Expression
Hypothesis	isdir.1	|- A = U. U. R
Assertion	isdir	|- ( R e. V -> ( R e. DirRel <-> ( ( Rel R /\ ( _I |` A ) C_ R ) /\ ( ( R o. R ) C_ R /\ ( A X. A ) C_ ( `' R o. R ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		isdir.1	|- A = U. U. R
2		releq	|- ( r = R -> ( Rel r <-> Rel R ) )
3		unieq	|- ( r = R -> U. r = U. R )
4	3	unieqd	|- ( r = R -> U. U. r = U. U. R )
5	4 1	eqtr4di	|- ( r = R -> U. U. r = A )
6	5	reseq2d	|- ( r = R -> ( _I |` U. U. r ) = ( _I |` A ) )
7		id	|- ( r = R -> r = R )
8	6 7	sseq12d	|- ( r = R -> ( ( _I |` U. U. r ) C_ r <-> ( _I |` A ) C_ R ) )
9	2 8	anbi12d	|- ( r = R -> ( ( Rel r /\ ( _I |` U. U. r ) C_ r ) <-> ( Rel R /\ ( _I |` A ) C_ R ) ) )
10	7 7	coeq12d	|- ( r = R -> ( r o. r ) = ( R o. R ) )
11	10 7	sseq12d	|- ( r = R -> ( ( r o. r ) C_ r <-> ( R o. R ) C_ R ) )
12	5	sqxpeqd	|- ( r = R -> ( U. U. r X. U. U. r ) = ( A X. A ) )
13		cnveq	|- ( r = R -> `' r = `' R )
14	13 7	coeq12d	|- ( r = R -> ( `' r o. r ) = ( `' R o. R ) )
15	12 14	sseq12d	|- ( r = R -> ( ( U. U. r X. U. U. r ) C_ ( `' r o. r ) <-> ( A X. A ) C_ ( `' R o. R ) ) )
16	11 15	anbi12d	|- ( r = R -> ( ( ( r o. r ) C_ r /\ ( U. U. r X. U. U. r ) C_ ( `' r o. r ) ) <-> ( ( R o. R ) C_ R /\ ( A X. A ) C_ ( `' R o. R ) ) ) )
17	9 16	anbi12d	|- ( r = R -> ( ( ( Rel r /\ ( _I |` U. U. r ) C_ r ) /\ ( ( r o. r ) C_ r /\ ( U. U. r X. U. U. r ) C_ ( `' r o. r ) ) ) <-> ( ( Rel R /\ ( _I |` A ) C_ R ) /\ ( ( R o. R ) C_ R /\ ( A X. A ) C_ ( `' R o. R ) ) ) ) )
18		df-dir	|- DirRel = { r | ( ( Rel r /\ ( _I |` U. U. r ) C_ r ) /\ ( ( r o. r ) C_ r /\ ( U. U. r X. U. U. r ) C_ ( `' r o. r ) ) ) }
19	17 18	elab2g	|- ( R e. V -> ( R e. DirRel <-> ( ( Rel R /\ ( _I |` A ) C_ R ) /\ ( ( R o. R ) C_ R /\ ( A X. A ) C_ ( `' R o. R ) ) ) ) )