Theorem rnttrcl

Description: The range of a transitive closure is the same as the range of the original class. (Contributed by Scott Fenton, 26-Oct-2024)

	Ref	Expression
Assertion	rnttrcl	Could not format assertion : No typesetting found for |- ran t++ R = ran R with typecode |-

Proof

Step	Hyp	Ref	Expression
1		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 |-
2	1	rneqi	Could not format ran t++ R = ran { <. 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 |- ran t++ R = ran { <. 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 |-
3		rnopab	$$⊢\mathrm{ran}\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\}=\left\{y|\exists x\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\}$$
4	2 3	eqtri	Could not format ran t++ R = { y | E. x 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 |- ran t++ R = { y | E. x 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 |-
5		fveq2	$$⊢a=\bigcup n\to f\left(a\right)=f\left(\bigcup n\right)$$
6		suceq	$$⊢a=\bigcup n\to \mathrm{suc}a=\mathrm{suc}\bigcup n$$
7	6	fveq2d	$$⊢a=\bigcup n\to f\left(\mathrm{suc}a\right)=f\left(\mathrm{suc}\bigcup n\right)$$
8	5 7	breq12d	$$⊢a=\bigcup n\to \left(f\left(a\right)Rf\left(\mathrm{suc}a\right)\leftrightarrow f\left(\bigcup n\right)Rf\left(\mathrm{suc}\bigcup n\right)\right)$$
9		simpr3	$$⊢\left(n\in \left(\mathrm{\omega }\setminus 1_{𝑜}\right)\wedge \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)\to \forall a\in nf\left(a\right)Rf\left(\mathrm{suc}a\right)$$
10		df-1o	$$⊢1_{𝑜}=\mathrm{suc}\varnothing$$
11	10	difeq2i	$$⊢\mathrm{\omega }\setminus 1_{𝑜}=\mathrm{\omega }\setminus \mathrm{suc}\varnothing$$
12	11	eleq2i	$$⊢n\in \left(\mathrm{\omega }\setminus 1_{𝑜}\right)\leftrightarrow n\in \left(\mathrm{\omega }\setminus \mathrm{suc}\varnothing \right)$$
13		peano1	$$⊢\varnothing \in \mathrm{\omega }$$
14		eldifsucnn	$$⊢\varnothing \in \mathrm{\omega }\to \left(n\in \left(\mathrm{\omega }\setminus \mathrm{suc}\varnothing \right)\leftrightarrow \exists x\in \left(\mathrm{\omega }\setminus \varnothing \right)n=\mathrm{suc}x\right)$$
15	13 14	ax-mp	$$⊢n\in \left(\mathrm{\omega }\setminus \mathrm{suc}\varnothing \right)\leftrightarrow \exists x\in \left(\mathrm{\omega }\setminus \varnothing \right)n=\mathrm{suc}x$$
16		dif0	$$⊢\mathrm{\omega }\setminus \varnothing =\mathrm{\omega }$$
17	16	rexeqi	$$⊢\exists x\in \left(\mathrm{\omega }\setminus \varnothing \right)n=\mathrm{suc}x\leftrightarrow \exists x\in \mathrm{\omega }n=\mathrm{suc}x$$
18	12 15 17	3bitri	$$⊢n\in \left(\mathrm{\omega }\setminus 1_{𝑜}\right)\leftrightarrow \exists x\in \mathrm{\omega }n=\mathrm{suc}x$$
19		nnord	$$⊢x\in \mathrm{\omega }\to \mathrm{Ord}x$$
20		ordunisuc	$$⊢\mathrm{Ord}x\to \bigcup \mathrm{suc}x=x$$
21	19 20	syl	$$⊢x\in \mathrm{\omega }\to \bigcup \mathrm{suc}x=x$$
22		vex	$$⊢x\in \mathrm{V}$$
23	22	sucid	$$⊢x\in \mathrm{suc}x$$
24	21 23	eqeltrdi	$$⊢x\in \mathrm{\omega }\to \bigcup \mathrm{suc}x\in \mathrm{suc}x$$
25		unieq	$$⊢n=\mathrm{suc}x\to \bigcup n=\bigcup \mathrm{suc}x$$
26		id	$$⊢n=\mathrm{suc}x\to n=\mathrm{suc}x$$
27	25 26	eleq12d	$$⊢n=\mathrm{suc}x\to \left(\bigcup n\in n\leftrightarrow \bigcup \mathrm{suc}x\in \mathrm{suc}x\right)$$
28	24 27	syl5ibrcom	$$⊢x\in \mathrm{\omega }\to \left(n=\mathrm{suc}x\to \bigcup n\in n\right)$$
29	28	rexlimiv	$$⊢\exists x\in \mathrm{\omega }n=\mathrm{suc}x\to \bigcup n\in n$$
30	18 29	sylbi	$$⊢n\in \left(\mathrm{\omega }\setminus 1_{𝑜}\right)\to \bigcup n\in n$$
31	30	adantr	$$⊢\left(n\in \left(\mathrm{\omega }\setminus 1_{𝑜}\right)\wedge \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)\to \bigcup n\in n$$
32	8 9 31	rspcdva	$$⊢\left(n\in \left(\mathrm{\omega }\setminus 1_{𝑜}\right)\wedge \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)\to f\left(\bigcup n\right)Rf\left(\mathrm{suc}\bigcup n\right)$$
33		suceq	$$⊢\bigcup \mathrm{suc}x=x\to \mathrm{suc}\bigcup \mathrm{suc}x=\mathrm{suc}x$$
34	21 33	syl	$$⊢x\in \mathrm{\omega }\to \mathrm{suc}\bigcup \mathrm{suc}x=\mathrm{suc}x$$
35		suceq	$$⊢\bigcup n=\bigcup \mathrm{suc}x\to \mathrm{suc}\bigcup n=\mathrm{suc}\bigcup \mathrm{suc}x$$
36	25 35	syl	$$⊢n=\mathrm{suc}x\to \mathrm{suc}\bigcup n=\mathrm{suc}\bigcup \mathrm{suc}x$$
37	36 26	eqeq12d	$$⊢n=\mathrm{suc}x\to \left(\mathrm{suc}\bigcup n=n\leftrightarrow \mathrm{suc}\bigcup \mathrm{suc}x=\mathrm{suc}x\right)$$
38	34 37	syl5ibrcom	$$⊢x\in \mathrm{\omega }\to \left(n=\mathrm{suc}x\to \mathrm{suc}\bigcup n=n\right)$$
39	38	rexlimiv	$$⊢\exists x\in \mathrm{\omega }n=\mathrm{suc}x\to \mathrm{suc}\bigcup n=n$$
40	18 39	sylbi	$$⊢n\in \left(\mathrm{\omega }\setminus 1_{𝑜}\right)\to \mathrm{suc}\bigcup n=n$$
41	40	fveq2d	$$⊢n\in \left(\mathrm{\omega }\setminus 1_{𝑜}\right)\to f\left(\mathrm{suc}\bigcup n\right)=f\left(n\right)$$
42	41	adantr	$$⊢\left(n\in \left(\mathrm{\omega }\setminus 1_{𝑜}\right)\wedge \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)\to f\left(\mathrm{suc}\bigcup n\right)=f\left(n\right)$$
43		simpr2r	$$⊢\left(n\in \left(\mathrm{\omega }\setminus 1_{𝑜}\right)\wedge \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)\to f\left(n\right)=y$$
44	42 43	eqtrd	$$⊢\left(n\in \left(\mathrm{\omega }\setminus 1_{𝑜}\right)\wedge \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)\to f\left(\mathrm{suc}\bigcup n\right)=y$$
45	32 44	breqtrd	$$⊢\left(n\in \left(\mathrm{\omega }\setminus 1_{𝑜}\right)\wedge \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)\to f\left(\bigcup n\right)Ry$$
46		fvex	$$⊢f\left(\bigcup n\right)\in \mathrm{V}$$
47		vex	$$⊢y\in \mathrm{V}$$
48	46 47	brelrn	$$⊢f\left(\bigcup n\right)Ry\to y\in \mathrm{ran}R$$
49	45 48	syl	$$⊢\left(n\in \left(\mathrm{\omega }\setminus 1_{𝑜}\right)\wedge \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)\to y\in \mathrm{ran}R$$
50	49	ex	$$⊢n\in \left(\mathrm{\omega }\setminus 1_{𝑜}\right)\to \left(\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)\to y\in \mathrm{ran}R\right)$$
51	50	exlimdv	$$⊢n\in \left(\mathrm{\omega }\setminus 1_{𝑜}\right)\to \left(\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)\to y\in \mathrm{ran}R\right)$$
52	51	rexlimiv	$$⊢\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)\to y\in \mathrm{ran}R$$
53	52	exlimiv	$$⊢\exists x\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)\to y\in \mathrm{ran}R$$
54	53	abssi	$$⊢\left\{y|\exists x\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\}\subseteq \mathrm{ran}R$$
55	4 54	eqsstri	Could not format ran t++ R C_ ran R : No typesetting found for |- ran t++ R C_ ran R with typecode |-
56		rnresv	$$⊢\mathrm{ran}\left({R\upharpoonright }_{\mathrm{V}}\right)=\mathrm{ran}R$$
57		relres	$$⊢\mathrm{Rel}\left({R\upharpoonright }_{\mathrm{V}}\right)$$
58		ssttrcl	Could not format ( Rel ( R |` _V ) -> ( R |` _V ) C_ t++ ( R |` _V ) ) : No typesetting found for |- ( Rel ( R |` _V ) -> ( R |` _V ) C_ t++ ( R |` _V ) ) with typecode |-
59	57 58	ax-mp	Could not format ( R |` _V ) C_ t++ ( R |` _V ) : No typesetting found for |- ( R |` _V ) C_ t++ ( R |` _V ) with typecode |-
60		ttrclresv	Could not format t++ ( R |` _V ) = t++ R : No typesetting found for |- t++ ( R |` _V ) = t++ R with typecode |-
61	59 60	sseqtri	Could not format ( R |` _V ) C_ t++ R : No typesetting found for |- ( R |` _V ) C_ t++ R with typecode |-
62	61	rnssi	Could not format ran ( R |` _V ) C_ ran t++ R : No typesetting found for |- ran ( R |` _V ) C_ ran t++ R with typecode |-
63	56 62	eqsstrri	Could not format ran R C_ ran t++ R : No typesetting found for |- ran R C_ ran t++ R with typecode |-
64	55 63	eqssi	Could not format ran t++ R = ran R : No typesetting found for |- ran t++ R = ran R with typecode |-