Metamath Proof Explorer

Theorem trclfvcotr

Description: The transitive closure of a relation is a transitive relation. (Contributed by RP, 29-Apr-2020)

Ref Expression
Assertion trclfvcotr ( 𝑅 ∈ 𝑉 → ( ( t+ ‘ 𝑅 ) ∘ ( t+ ‘ 𝑅 ) ) ⊆ ( t+ ‘ 𝑅 ) )

Proof

Step Hyp Ref Expression
1 cotr ⊢ ( ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ↔ ∀ 𝑎 ∀ 𝑏 ∀ 𝑐 ( ( 𝑎 𝑟 𝑏 ∧ 𝑏 𝑟 𝑐 ) → 𝑎 𝑟 𝑐 ) )
2 sp ⊢ ( ∀ 𝑎 ∀ 𝑏 ∀ 𝑐 ( ( 𝑎 𝑟 𝑏 ∧ 𝑏 𝑟 𝑐 ) → 𝑎 𝑟 𝑐 ) → ∀ 𝑏 ∀ 𝑐 ( ( 𝑎 𝑟 𝑏 ∧ 𝑏 𝑟 𝑐 ) → 𝑎 𝑟 𝑐 ) )
3 2 19.21bbi ⊢ ( ∀ 𝑎 ∀ 𝑏 ∀ 𝑐 ( ( 𝑎 𝑟 𝑏 ∧ 𝑏 𝑟 𝑐 ) → 𝑎 𝑟 𝑐 ) → ( ( 𝑎 𝑟 𝑏 ∧ 𝑏 𝑟 𝑐 ) → 𝑎 𝑟 𝑐 ) )
4 1 3 sylbi ⊢ ( ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 → ( ( 𝑎 𝑟 𝑏 ∧ 𝑏 𝑟 𝑐 ) → 𝑎 𝑟 𝑐 ) )
5 4 adantl ⊢ ( ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) → ( ( 𝑎 𝑟 𝑏 ∧ 𝑏 𝑟 𝑐 ) → 𝑎 𝑟 𝑐 ) )
6 5 a2i ⊢ ( ( ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) → ( 𝑎 𝑟 𝑏 ∧ 𝑏 𝑟 𝑐 ) ) → ( ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) → 𝑎 𝑟 𝑐 ) )
7 6 alimi ⊢ ( ∀ 𝑟 ( ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) → ( 𝑎 𝑟 𝑏 ∧ 𝑏 𝑟 𝑐 ) ) → ∀ 𝑟 ( ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) → 𝑎 𝑟 𝑐 ) )
8 7 ax-gen ⊢ ∀ 𝑐 ( ∀ 𝑟 ( ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) → ( 𝑎 𝑟 𝑏 ∧ 𝑏 𝑟 𝑐 ) ) → ∀ 𝑟 ( ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) → 𝑎 𝑟 𝑐 ) )
9 8 ax-gen ⊢ ∀ 𝑏 ∀ 𝑐 ( ∀ 𝑟 ( ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) → ( 𝑎 𝑟 𝑏 ∧ 𝑏 𝑟 𝑐 ) ) → ∀ 𝑟 ( ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) → 𝑎 𝑟 𝑐 ) )
10 9 ax-gen ⊢ ∀ 𝑎 ∀ 𝑏 ∀ 𝑐 ( ∀ 𝑟 ( ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) → ( 𝑎 𝑟 𝑏 ∧ 𝑏 𝑟 𝑐 ) ) → ∀ 𝑟 ( ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) → 𝑎 𝑟 𝑐 ) )
11 brtrclfv ⊢ ( 𝑅 ∈ 𝑉 → ( 𝑎 ( t+ ‘ 𝑅 ) 𝑏 ↔ ∀ 𝑟 ( ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) → 𝑎 𝑟 𝑏 ) ) )
12 brtrclfv ⊢ ( 𝑅 ∈ 𝑉 → ( 𝑏 ( t+ ‘ 𝑅 ) 𝑐 ↔ ∀ 𝑟 ( ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) → 𝑏 𝑟 𝑐 ) ) )
13 11 12 anbi12d ⊢ ( 𝑅 ∈ 𝑉 → ( ( 𝑎 ( t+ ‘ 𝑅 ) 𝑏 ∧ 𝑏 ( t+ ‘ 𝑅 ) 𝑐 ) ↔ ( ∀ 𝑟 ( ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) → 𝑎 𝑟 𝑏 ) ∧ ∀ 𝑟 ( ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) → 𝑏 𝑟 𝑐 ) ) ) )
14 jcab ⊢ ( ( ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) → ( 𝑎 𝑟 𝑏 ∧ 𝑏 𝑟 𝑐 ) ) ↔ ( ( ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) → 𝑎 𝑟 𝑏 ) ∧ ( ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) → 𝑏 𝑟 𝑐 ) ) )
15 14 albii ⊢ ( ∀ 𝑟 ( ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) → ( 𝑎 𝑟 𝑏 ∧ 𝑏 𝑟 𝑐 ) ) ↔ ∀ 𝑟 ( ( ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) → 𝑎 𝑟 𝑏 ) ∧ ( ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) → 𝑏 𝑟 𝑐 ) ) )
16 19.26 ⊢ ( ∀ 𝑟 ( ( ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) → 𝑎 𝑟 𝑏 ) ∧ ( ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) → 𝑏 𝑟 𝑐 ) ) ↔ ( ∀ 𝑟 ( ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) → 𝑎 𝑟 𝑏 ) ∧ ∀ 𝑟 ( ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) → 𝑏 𝑟 𝑐 ) ) )
17 15 16 bitri ⊢ ( ∀ 𝑟 ( ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) → ( 𝑎 𝑟 𝑏 ∧ 𝑏 𝑟 𝑐 ) ) ↔ ( ∀ 𝑟 ( ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) → 𝑎 𝑟 𝑏 ) ∧ ∀ 𝑟 ( ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) → 𝑏 𝑟 𝑐 ) ) )
18 13 17 bitr4di ⊢ ( 𝑅 ∈ 𝑉 → ( ( 𝑎 ( t+ ‘ 𝑅 ) 𝑏 ∧ 𝑏 ( t+ ‘ 𝑅 ) 𝑐 ) ↔ ∀ 𝑟 ( ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) → ( 𝑎 𝑟 𝑏 ∧ 𝑏 𝑟 𝑐 ) ) ) )
19 brtrclfv ⊢ ( 𝑅 ∈ 𝑉 → ( 𝑎 ( t+ ‘ 𝑅 ) 𝑐 ↔ ∀ 𝑟 ( ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) → 𝑎 𝑟 𝑐 ) ) )
20 18 19 imbi12d ⊢ ( 𝑅 ∈ 𝑉 → ( ( ( 𝑎 ( t+ ‘ 𝑅 ) 𝑏 ∧ 𝑏 ( t+ ‘ 𝑅 ) 𝑐 ) → 𝑎 ( t+ ‘ 𝑅 ) 𝑐 ) ↔ ( ∀ 𝑟 ( ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) → ( 𝑎 𝑟 𝑏 ∧ 𝑏 𝑟 𝑐 ) ) → ∀ 𝑟 ( ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) → 𝑎 𝑟 𝑐 ) ) ) )
21 20 albidv ⊢ ( 𝑅 ∈ 𝑉 → ( ∀ 𝑐 ( ( 𝑎 ( t+ ‘ 𝑅 ) 𝑏 ∧ 𝑏 ( t+ ‘ 𝑅 ) 𝑐 ) → 𝑎 ( t+ ‘ 𝑅 ) 𝑐 ) ↔ ∀ 𝑐 ( ∀ 𝑟 ( ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) → ( 𝑎 𝑟 𝑏 ∧ 𝑏 𝑟 𝑐 ) ) → ∀ 𝑟 ( ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) → 𝑎 𝑟 𝑐 ) ) ) )
22 21 2albidv ⊢ ( 𝑅 ∈ 𝑉 → ( ∀ 𝑎 ∀ 𝑏 ∀ 𝑐 ( ( 𝑎 ( t+ ‘ 𝑅 ) 𝑏 ∧ 𝑏 ( t+ ‘ 𝑅 ) 𝑐 ) → 𝑎 ( t+ ‘ 𝑅 ) 𝑐 ) ↔ ∀ 𝑎 ∀ 𝑏 ∀ 𝑐 ( ∀ 𝑟 ( ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) → ( 𝑎 𝑟 𝑏 ∧ 𝑏 𝑟 𝑐 ) ) → ∀ 𝑟 ( ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) → 𝑎 𝑟 𝑐 ) ) ) )
23 10 22 mpbiri ⊢ ( 𝑅 ∈ 𝑉 → ∀ 𝑎 ∀ 𝑏 ∀ 𝑐 ( ( 𝑎 ( t+ ‘ 𝑅 ) 𝑏 ∧ 𝑏 ( t+ ‘ 𝑅 ) 𝑐 ) → 𝑎 ( t+ ‘ 𝑅 ) 𝑐 ) )
24 cotr ⊢ ( ( ( t+ ‘ 𝑅 ) ∘ ( t+ ‘ 𝑅 ) ) ⊆ ( t+ ‘ 𝑅 ) ↔ ∀ 𝑎 ∀ 𝑏 ∀ 𝑐 ( ( 𝑎 ( t+ ‘ 𝑅 ) 𝑏 ∧ 𝑏 ( t+ ‘ 𝑅 ) 𝑐 ) → 𝑎 ( t+ ‘ 𝑅 ) 𝑐 ) )
25 23 24 sylibr ⊢ ( 𝑅 ∈ 𝑉 → ( ( t+ ‘ 𝑅 ) ∘ ( t+ ‘ 𝑅 ) ) ⊆ ( t+ ‘ 𝑅 ) )