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	Could not format assertion : No typesetting found for |- t++ ( R |` _V ) = t++ R with typecode |-

Proof

Step	Hyp	Ref	Expression
1		fvex	$$⊢f\left(a\right)\in \mathrm{V}$$
2		fvex	$$⊢f\left(\mathrm{suc}a\right)\in \mathrm{V}$$
3	2	brresi	$$⊢f\left(a\right)\left({R\upharpoonright }_{\mathrm{V}}\right)f\left(\mathrm{suc}a\right)\leftrightarrow \left(f\left(a\right)\in \mathrm{V}\wedge f\left(a\right)Rf\left(\mathrm{suc}a\right)\right)$$
4	1 3	mpbiran	$$⊢f\left(a\right)\left({R\upharpoonright }_{\mathrm{V}}\right)f\left(\mathrm{suc}a\right)\leftrightarrow f\left(a\right)Rf\left(\mathrm{suc}a\right)$$
5	4	ralbii	$$⊢\forall a\in nf\left(a\right)\left({R\upharpoonright }_{\mathrm{V}}\right)f\left(\mathrm{suc}a\right)\leftrightarrow \forall a\in nf\left(a\right)Rf\left(\mathrm{suc}a\right)$$
6	5	3anbi3i	$$⊢\left(fFn\mathrm{suc}n\wedge \left(f\left(\varnothing \right)=x\wedge f\left(n\right)=y\right)\wedge \forall a\in nf\left(a\right)\left({R\upharpoonright }_{\mathrm{V}}\right)f\left(\mathrm{suc}a\right)\right)\leftrightarrow \left(fFn\mathrm{suc}n\wedge \left(f\left(\varnothing \right)=x\wedge f\left(n\right)=y\right)\wedge \forall a\in nf\left(a\right)Rf\left(\mathrm{suc}a\right)\right)$$
7	6	exbii	$$⊢\exists f\left(fFn\mathrm{suc}n\wedge \left(f\left(\varnothing \right)=x\wedge f\left(n\right)=y\right)\wedge \forall a\in nf\left(a\right)\left({R\upharpoonright }_{\mathrm{V}}\right)f\left(\mathrm{suc}a\right)\right)\leftrightarrow \exists f\left(fFn\mathrm{suc}n\wedge \left(f\left(\varnothing \right)=x\wedge f\left(n\right)=y\right)\wedge \forall a\in nf\left(a\right)Rf\left(\mathrm{suc}a\right)\right)$$
8	7	rexbii	$$⊢\exists n\in \left(\mathrm{\omega }\setminus 1_{𝑜}\right)\exists f\left(fFn\mathrm{suc}n\wedge \left(f\left(\varnothing \right)=x\wedge f\left(n\right)=y\right)\wedge \forall a\in nf\left(a\right)\left({R\upharpoonright }_{\mathrm{V}}\right)f\left(\mathrm{suc}a\right)\right)\leftrightarrow \exists n\in \left(\mathrm{\omega }\setminus 1_{𝑜}\right)\exists f\left(fFn\mathrm{suc}n\wedge \left(f\left(\varnothing \right)=x\wedge f\left(n\right)=y\right)\wedge \forall a\in nf\left(a\right)Rf\left(\mathrm{suc}a\right)\right)$$
9	8	opabbii	$$⊢\left\{⟨x,y⟩|\exists n\in \left(\mathrm{\omega }\setminus 1_{𝑜}\right)\exists f\left(fFn\mathrm{suc}n\wedge \left(f\left(\varnothing \right)=x\wedge f\left(n\right)=y\right)\wedge \forall a\in nf\left(a\right)\left({R\upharpoonright }_{\mathrm{V}}\right)f\left(\mathrm{suc}a\right)\right)\right\}=\left\{⟨x,y⟩|\exists n\in \left(\mathrm{\omega }\setminus 1_{𝑜}\right)\exists f\left(fFn\mathrm{suc}n\wedge \left(f\left(\varnothing \right)=x\wedge f\left(n\right)=y\right)\wedge \forall a\in nf\left(a\right)Rf\left(\mathrm{suc}a\right)\right)\right\}$$
10		df-ttrcl	Could not format 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 ) ) } : No typesetting found for |- 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 ) ) } with typecode |-
11		df-ttrcl	Could not format 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 ) ) } : No typesetting found for |- 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 ) ) } with typecode |-
12	9 10 11	3eqtr4i	Could not format t++ ( R |` _V ) = t++ R : No typesetting found for |- t++ ( R |` _V ) = t++ R with typecode |-