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 ) e. _V
2		fvex	|- ( f ` suc a ) e. _V
3	2	brresi	|- ( ( f ` a ) ( R |` _V ) ( f ` suc a ) <-> ( ( f ` a ) e. _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. a e. n ( f ` a ) ( R |` _V ) ( f ` suc a ) <-> A. a e. n ( f ` a ) R ( f ` suc a ) )
6	5	3anbi3i	|- ( ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = y ) /\ A. a e. n ( f ` a ) ( R |` _V ) ( f ` suc a ) ) <-> ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = y ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) )
7	6	exbii	|- ( E. f ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = y ) /\ A. a e. n ( f ` a ) ( R |` _V ) ( f ` suc a ) ) <-> E. f ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = y ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) )
8	7	rexbii	|- ( E. n e. ( _om \ 1o ) E. f ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = y ) /\ A. a e. n ( f ` a ) ( R |` _V ) ( f ` suc a ) ) <-> E. n e. ( _om \ 1o ) E. f ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = y ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) )
9	8	opabbii	|- { <. x , y >. | E. n e. ( _om \ 1o ) E. f ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = y ) /\ A. a e. n ( f ` a ) ( R |` _V ) ( f ` suc a ) ) } = { <. x , y >. | E. n e. ( _om \ 1o ) E. f ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = y ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) }
10		df-ttrcl	|- t++ ( R |` _V ) = { <. x , y >. | E. n e. ( _om \ 1o ) E. f ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = y ) /\ A. a e. n ( f ` a ) ( R |` _V ) ( f ` suc a ) ) }
11		df-ttrcl	|- t++ R = { <. x , y >. | E. n e. ( _om \ 1o ) E. f ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = y ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) }
12	9 10 11	3eqtr4i	|- t++ ( R |` _V ) = t++ R