Theorem dirref

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

	Ref	Expression
Hypothesis	dirref.1	⊢ 𝑋 = dom 𝑅
Assertion	dirref	⊢ ( ( 𝑅 ∈ DirRel ∧ 𝐴 ∈ 𝑋 ) → 𝐴 𝑅 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		dirref.1	⊢ 𝑋 = dom 𝑅
2		dirdm	⊢ ( 𝑅 ∈ DirRel → dom 𝑅 = ∪ ∪ 𝑅 )
3	1 2	syl5eq	⊢ ( 𝑅 ∈ DirRel → 𝑋 = ∪ ∪ 𝑅 )
4	3	reseq2d	⊢ ( 𝑅 ∈ DirRel → ( I ↾ 𝑋 ) = ( I ↾ ∪ ∪ 𝑅 ) )
5		eqid	⊢ ∪ ∪ 𝑅 = ∪ ∪ 𝑅
6	5	isdir	⊢ ( 𝑅 ∈ DirRel → ( 𝑅 ∈ DirRel ↔ ( ( Rel 𝑅 ∧ ( I ↾ ∪ ∪ 𝑅 ) ⊆ 𝑅 ) ∧ ( ( 𝑅 ∘ 𝑅 ) ⊆ 𝑅 ∧ ( ∪ ∪ 𝑅 × ∪ ∪ 𝑅 ) ⊆ ( ◡ 𝑅 ∘ 𝑅 ) ) ) ) )
7	6	ibi	⊢ ( 𝑅 ∈ DirRel → ( ( Rel 𝑅 ∧ ( I ↾ ∪ ∪ 𝑅 ) ⊆ 𝑅 ) ∧ ( ( 𝑅 ∘ 𝑅 ) ⊆ 𝑅 ∧ ( ∪ ∪ 𝑅 × ∪ ∪ 𝑅 ) ⊆ ( ◡ 𝑅 ∘ 𝑅 ) ) ) )
8	7	simplrd	⊢ ( 𝑅 ∈ DirRel → ( I ↾ ∪ ∪ 𝑅 ) ⊆ 𝑅 )
9	4 8	eqsstrd	⊢ ( 𝑅 ∈ DirRel → ( I ↾ 𝑋 ) ⊆ 𝑅 )
10	9	ssbrd	⊢ ( 𝑅 ∈ DirRel → ( 𝐴 ( I ↾ 𝑋 ) 𝐴 → 𝐴 𝑅 𝐴 ) )
11		eqid	⊢ 𝐴 = 𝐴
12		resieq	⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) → ( 𝐴 ( I ↾ 𝑋 ) 𝐴 ↔ 𝐴 = 𝐴 ) )
13	12	anidms	⊢ ( 𝐴 ∈ 𝑋 → ( 𝐴 ( I ↾ 𝑋 ) 𝐴 ↔ 𝐴 = 𝐴 ) )
14	11 13	mpbiri	⊢ ( 𝐴 ∈ 𝑋 → 𝐴 ( I ↾ 𝑋 ) 𝐴 )
15	10 14	impel	⊢ ( ( 𝑅 ∈ DirRel ∧ 𝐴 ∈ 𝑋 ) → 𝐴 𝑅 𝐴 )