Theorem reldir

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

	Ref	Expression
Assertion	reldir	⊢ ( 𝑅 ∈ DirRel → Rel 𝑅 )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ∪ ∪ 𝑅 = ∪ ∪ 𝑅
2	1	isdir	⊢ ( 𝑅 ∈ DirRel → ( 𝑅 ∈ DirRel ↔ ( ( Rel 𝑅 ∧ ( I ↾ ∪ ∪ 𝑅 ) ⊆ 𝑅 ) ∧ ( ( 𝑅 ∘ 𝑅 ) ⊆ 𝑅 ∧ ( ∪ ∪ 𝑅 × ∪ ∪ 𝑅 ) ⊆ ( ◡ 𝑅 ∘ 𝑅 ) ) ) ) )
3	2	ibi	⊢ ( 𝑅 ∈ DirRel → ( ( Rel 𝑅 ∧ ( I ↾ ∪ ∪ 𝑅 ) ⊆ 𝑅 ) ∧ ( ( 𝑅 ∘ 𝑅 ) ⊆ 𝑅 ∧ ( ∪ ∪ 𝑅 × ∪ ∪ 𝑅 ) ⊆ ( ◡ 𝑅 ∘ 𝑅 ) ) ) )
4	3	simplld	⊢ ( 𝑅 ∈ DirRel → Rel 𝑅 )