Metamath Proof Explorer

Theorem dirtr

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

Ref Expression
Assertion dirtr ( ( ( 𝑅 ∈ DirRel ∧ 𝐶 ∈ 𝑉 ) ∧ ( 𝐴 𝑅 𝐵 ∧ 𝐵 𝑅 𝐶 ) ) → 𝐴 𝑅 𝐶 )

Proof

Step Hyp Ref Expression
1 reldir ⊢ ( 𝑅 ∈ DirRel → Rel 𝑅 )
2 brrelex1 ⊢ ( ( Rel 𝑅 ∧ 𝐴 𝑅 𝐵 ) → 𝐴 ∈ V )
3 2 ex ⊢ ( Rel 𝑅 → ( 𝐴 𝑅 𝐵 → 𝐴 ∈ V ) )
4 brrelex1 ⊢ ( ( Rel 𝑅 ∧ 𝐵 𝑅 𝐶 ) → 𝐵 ∈ V )
5 4 ex ⊢ ( Rel 𝑅 → ( 𝐵 𝑅 𝐶 → 𝐵 ∈ V ) )
6 3 5 anim12d ⊢ ( Rel 𝑅 → ( ( 𝐴 𝑅 𝐵 ∧ 𝐵 𝑅 𝐶 ) → ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ) )
7 1 6 syl ⊢ ( 𝑅 ∈ DirRel → ( ( 𝐴 𝑅 𝐵 ∧ 𝐵 𝑅 𝐶 ) → ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ) )
8 eqid ⊢ ∪ ∪ 𝑅 = ∪ ∪ 𝑅
9 8 isdir ⊢ ( 𝑅 ∈ DirRel → ( 𝑅 ∈ DirRel ↔ ( ( Rel 𝑅 ∧ ( I ↾ ∪ ∪ 𝑅 ) ⊆ 𝑅 ) ∧ ( ( 𝑅 ∘ 𝑅 ) ⊆ 𝑅 ∧ ( ∪ ∪ 𝑅 × ∪ ∪ 𝑅 ) ⊆ ( ◡ 𝑅 ∘ 𝑅 ) ) ) ) )
10 9 ibi ⊢ ( 𝑅 ∈ DirRel → ( ( Rel 𝑅 ∧ ( I ↾ ∪ ∪ 𝑅 ) ⊆ 𝑅 ) ∧ ( ( 𝑅 ∘ 𝑅 ) ⊆ 𝑅 ∧ ( ∪ ∪ 𝑅 × ∪ ∪ 𝑅 ) ⊆ ( ◡ 𝑅 ∘ 𝑅 ) ) ) )
11 10 simprld ⊢ ( 𝑅 ∈ DirRel → ( 𝑅 ∘ 𝑅 ) ⊆ 𝑅 )
12 cotr ⊢ ( ( 𝑅 ∘ 𝑅 ) ⊆ 𝑅 ↔ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) )
13 11 12 sylib ⊢ ( 𝑅 ∈ DirRel → ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) )
14 breq12 ⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( 𝑥 𝑅 𝑦 ↔ 𝐴 𝑅 𝐵 ) )
15 14 3adant3 ⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶 ) → ( 𝑥 𝑅 𝑦 ↔ 𝐴 𝑅 𝐵 ) )
16 breq12 ⊢ ( ( 𝑦 = 𝐵 ∧ 𝑧 = 𝐶 ) → ( 𝑦 𝑅 𝑧 ↔ 𝐵 𝑅 𝐶 ) )
17 16 3adant1 ⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶 ) → ( 𝑦 𝑅 𝑧 ↔ 𝐵 𝑅 𝐶 ) )
18 15 17 anbi12d ⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶 ) → ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) ↔ ( 𝐴 𝑅 𝐵 ∧ 𝐵 𝑅 𝐶 ) ) )
19 breq12 ⊢ ( ( 𝑥 = 𝐴 ∧ 𝑧 = 𝐶 ) → ( 𝑥 𝑅 𝑧 ↔ 𝐴 𝑅 𝐶 ) )
20 19 3adant2 ⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶 ) → ( 𝑥 𝑅 𝑧 ↔ 𝐴 𝑅 𝐶 ) )
21 18 20 imbi12d ⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶 ) → ( ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) ↔ ( ( 𝐴 𝑅 𝐵 ∧ 𝐵 𝑅 𝐶 ) → 𝐴 𝑅 𝐶 ) ) )
22 21 spc3gv ⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐶 ∈ 𝑉 ) → ( ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) → ( ( 𝐴 𝑅 𝐵 ∧ 𝐵 𝑅 𝐶 ) → 𝐴 𝑅 𝐶 ) ) )
23 13 22 syl5 ⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐶 ∈ 𝑉 ) → ( 𝑅 ∈ DirRel → ( ( 𝐴 𝑅 𝐵 ∧ 𝐵 𝑅 𝐶 ) → 𝐴 𝑅 𝐶 ) ) )
24 23 3expia ⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ( 𝐶 ∈ 𝑉 → ( 𝑅 ∈ DirRel → ( ( 𝐴 𝑅 𝐵 ∧ 𝐵 𝑅 𝐶 ) → 𝐴 𝑅 𝐶 ) ) ) )
25 24 com4t ⊢ ( 𝑅 ∈ DirRel → ( ( 𝐴 𝑅 𝐵 ∧ 𝐵 𝑅 𝐶 ) → ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ( 𝐶 ∈ 𝑉 → 𝐴 𝑅 𝐶 ) ) ) )
26 7 25 mpdd ⊢ ( 𝑅 ∈ DirRel → ( ( 𝐴 𝑅 𝐵 ∧ 𝐵 𝑅 𝐶 ) → ( 𝐶 ∈ 𝑉 → 𝐴 𝑅 𝐶 ) ) )
27 26 imp31 ⊢ ( ( ( 𝑅 ∈ DirRel ∧ ( 𝐴 𝑅 𝐵 ∧ 𝐵 𝑅 𝐶 ) ) ∧ 𝐶 ∈ 𝑉 ) → 𝐴 𝑅 𝐶 )
28 27 an32s ⊢ ( ( ( 𝑅 ∈ DirRel ∧ 𝐶 ∈ 𝑉 ) ∧ ( 𝐴 𝑅 𝐵 ∧ 𝐵 𝑅 𝐶 ) ) → 𝐴 𝑅 𝐶 )