Metamath Proof Explorer


Theorem ttrclresv

Description: The transitive closure of R restricted to _V is the same as the transitive closure of R itself. (Contributed by Scott Fenton, 20-Oct-2024)

Ref Expression
Assertion ttrclresv t++ R V = t++ R

Proof

Step Hyp Ref Expression
1 fvex f a V
2 fvex f suc a V
3 2 brresi f a R V f suc a f a V f a R f suc a
4 1 3 mpbiran f a R V f suc a f a R f suc a
5 4 ralbii a n f a R V f suc a a n f a R f suc a
6 5 3anbi3i f Fn suc n f = x f n = y a n f a R V f suc a f Fn suc n f = x f n = y a n f a R f suc a
7 6 exbii f f Fn suc n f = x f n = y a n f a R V f suc a f f Fn suc n f = x f n = y a n f a R f suc a
8 7 rexbii n ω 1 𝑜 f f Fn suc n f = x f n = y a n f a R V f suc a n ω 1 𝑜 f f Fn suc n f = x f n = y a n f a R f suc a
9 8 opabbii x y | n ω 1 𝑜 f f Fn suc n f = x f n = y a n f a R V f suc a = x y | n ω 1 𝑜 f f Fn suc n f = x f n = y a n f a R f suc a
10 df-ttrcl t++ R V = x y | n ω 1 𝑜 f f Fn suc n f = x f n = y a n f a R V f suc a
11 df-ttrcl t++ R = x y | n ω 1 𝑜 f f Fn suc n f = x f n = y a n f a R f suc a
12 9 10 11 3eqtr4i t++ R V = t++ R