Theorem dirdm

Description: A direction's domain is equal to its field. (Contributed by Jeff Hankins, 25-Nov-2009) (Revised by Mario Carneiro, 22-Nov-2013)

	Ref	Expression
Assertion	dirdm	⊢ ( 𝑅 ∈ DirRel → dom 𝑅 = ∪ ∪ 𝑅 )

Proof

Step	Hyp	Ref	Expression
1		ssun1	⊢ dom 𝑅 ⊆ ( dom 𝑅 ∪ ran 𝑅 )
2		dmrnssfld	⊢ ( dom 𝑅 ∪ ran 𝑅 ) ⊆ ∪ ∪ 𝑅
3	1 2	sstri	⊢ dom 𝑅 ⊆ ∪ ∪ 𝑅
4	3	a1i	⊢ ( 𝑅 ∈ DirRel → dom 𝑅 ⊆ ∪ ∪ 𝑅 )
5		dmresi	⊢ dom ( I ↾ ∪ ∪ 𝑅 ) = ∪ ∪ 𝑅
6		eqid	⊢ ∪ ∪ 𝑅 = ∪ ∪ 𝑅
7	6	isdir	⊢ ( 𝑅 ∈ DirRel → ( 𝑅 ∈ DirRel ↔ ( ( Rel 𝑅 ∧ ( I ↾ ∪ ∪ 𝑅 ) ⊆ 𝑅 ) ∧ ( ( 𝑅 ∘ 𝑅 ) ⊆ 𝑅 ∧ ( ∪ ∪ 𝑅 × ∪ ∪ 𝑅 ) ⊆ ( ◡ 𝑅 ∘ 𝑅 ) ) ) ) )
8	7	ibi	⊢ ( 𝑅 ∈ DirRel → ( ( Rel 𝑅 ∧ ( I ↾ ∪ ∪ 𝑅 ) ⊆ 𝑅 ) ∧ ( ( 𝑅 ∘ 𝑅 ) ⊆ 𝑅 ∧ ( ∪ ∪ 𝑅 × ∪ ∪ 𝑅 ) ⊆ ( ◡ 𝑅 ∘ 𝑅 ) ) ) )
9	8	simplrd	⊢ ( 𝑅 ∈ DirRel → ( I ↾ ∪ ∪ 𝑅 ) ⊆ 𝑅 )
10		dmss	⊢ ( ( I ↾ ∪ ∪ 𝑅 ) ⊆ 𝑅 → dom ( I ↾ ∪ ∪ 𝑅 ) ⊆ dom 𝑅 )
11	9 10	syl	⊢ ( 𝑅 ∈ DirRel → dom ( I ↾ ∪ ∪ 𝑅 ) ⊆ dom 𝑅 )
12	5 11	eqsstrrid	⊢ ( 𝑅 ∈ DirRel → ∪ ∪ 𝑅 ⊆ dom 𝑅 )
13	4 12	eqssd	⊢ ( 𝑅 ∈ DirRel → dom 𝑅 = ∪ ∪ 𝑅 )