Metamath Proof Explorer


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 ↾ 𝐴 ) ⊆ 𝑅 ) ∧ ( ( 𝑅𝑅 ) ⊆ 𝑅 ∧ ( 𝐴 × 𝐴 ) ⊆ ( 𝑅𝑅 ) ) ) ) )