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	⊢ 𝐴 = ∪ ∪ 𝑅
Assertion	isdir	⊢ ( 𝑅 ∈ 𝑉 → ( 𝑅 ∈ DirRel ↔ ( ( Rel 𝑅 ∧ ( I ↾ 𝐴 ) ⊆ 𝑅 ) ∧ ( ( 𝑅 ∘ 𝑅 ) ⊆ 𝑅 ∧ ( 𝐴 × 𝐴 ) ⊆ ( ◡ 𝑅 ∘ 𝑅 ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		isdir.1	⊢ 𝐴 = ∪ ∪ 𝑅
2		releq	⊢ ( 𝑟 = 𝑅 → ( Rel 𝑟 ↔ Rel 𝑅 ) )
3		unieq	⊢ ( 𝑟 = 𝑅 → ∪ 𝑟 = ∪ 𝑅 )
4	3	unieqd	⊢ ( 𝑟 = 𝑅 → ∪ ∪ 𝑟 = ∪ ∪ 𝑅 )
5	4 1	eqtr4di	⊢ ( 𝑟 = 𝑅 → ∪ ∪ 𝑟 = 𝐴 )
6	5	reseq2d	⊢ ( 𝑟 = 𝑅 → ( I ↾ ∪ ∪ 𝑟 ) = ( I ↾ 𝐴 ) )
7		id	⊢ ( 𝑟 = 𝑅 → 𝑟 = 𝑅 )
8	6 7	sseq12d	⊢ ( 𝑟 = 𝑅 → ( ( I ↾ ∪ ∪ 𝑟 ) ⊆ 𝑟 ↔ ( I ↾ 𝐴 ) ⊆ 𝑅 ) )
9	2 8	anbi12d	⊢ ( 𝑟 = 𝑅 → ( ( Rel 𝑟 ∧ ( I ↾ ∪ ∪ 𝑟 ) ⊆ 𝑟 ) ↔ ( Rel 𝑅 ∧ ( I ↾ 𝐴 ) ⊆ 𝑅 ) ) )
10	7 7	coeq12d	⊢ ( 𝑟 = 𝑅 → ( 𝑟 ∘ 𝑟 ) = ( 𝑅 ∘ 𝑅 ) )
11	10 7	sseq12d	⊢ ( 𝑟 = 𝑅 → ( ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ↔ ( 𝑅 ∘ 𝑅 ) ⊆ 𝑅 ) )
12	5	sqxpeqd	⊢ ( 𝑟 = 𝑅 → ( ∪ ∪ 𝑟 × ∪ ∪ 𝑟 ) = ( 𝐴 × 𝐴 ) )
13		cnveq	⊢ ( 𝑟 = 𝑅 → ◡ 𝑟 = ◡ 𝑅 )
14	13 7	coeq12d	⊢ ( 𝑟 = 𝑅 → ( ◡ 𝑟 ∘ 𝑟 ) = ( ◡ 𝑅 ∘ 𝑅 ) )
15	12 14	sseq12d	⊢ ( 𝑟 = 𝑅 → ( ( ∪ ∪ 𝑟 × ∪ ∪ 𝑟 ) ⊆ ( ◡ 𝑟 ∘ 𝑟 ) ↔ ( 𝐴 × 𝐴 ) ⊆ ( ◡ 𝑅 ∘ 𝑅 ) ) )
16	11 15	anbi12d	⊢ ( 𝑟 = 𝑅 → ( ( ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ∧ ( ∪ ∪ 𝑟 × ∪ ∪ 𝑟 ) ⊆ ( ◡ 𝑟 ∘ 𝑟 ) ) ↔ ( ( 𝑅 ∘ 𝑅 ) ⊆ 𝑅 ∧ ( 𝐴 × 𝐴 ) ⊆ ( ◡ 𝑅 ∘ 𝑅 ) ) ) )
17	9 16	anbi12d	⊢ ( 𝑟 = 𝑅 → ( ( ( Rel 𝑟 ∧ ( I ↾ ∪ ∪ 𝑟 ) ⊆ 𝑟 ) ∧ ( ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ∧ ( ∪ ∪ 𝑟 × ∪ ∪ 𝑟 ) ⊆ ( ◡ 𝑟 ∘ 𝑟 ) ) ) ↔ ( ( Rel 𝑅 ∧ ( I ↾ 𝐴 ) ⊆ 𝑅 ) ∧ ( ( 𝑅 ∘ 𝑅 ) ⊆ 𝑅 ∧ ( 𝐴 × 𝐴 ) ⊆ ( ◡ 𝑅 ∘ 𝑅 ) ) ) ) )
18		df-dir	⊢ DirRel = { 𝑟 ∣ ( ( Rel 𝑟 ∧ ( I ↾ ∪ ∪ 𝑟 ) ⊆ 𝑟 ) ∧ ( ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ∧ ( ∪ ∪ 𝑟 × ∪ ∪ 𝑟 ) ⊆ ( ◡ 𝑟 ∘ 𝑟 ) ) ) }
19	17 18	elab2g	⊢ ( 𝑅 ∈ 𝑉 → ( 𝑅 ∈ DirRel ↔ ( ( Rel 𝑅 ∧ ( I ↾ 𝐴 ) ⊆ 𝑅 ) ∧ ( ( 𝑅 ∘ 𝑅 ) ⊆ 𝑅 ∧ ( 𝐴 × 𝐴 ) ⊆ ( ◡ 𝑅 ∘ 𝑅 ) ) ) ) )