Definition df-ttrcl

Description: Define the transitive closure of a class. This is the smallest relationship containing R (or more precisely, the relation ` ( R |`_V ) induced by R ) and having the transitive property. Definition from Levy p. 59, who denotes it as R * and calls it the "ancestral" of R . (Contributed by Scott Fenton, 17-Oct-2024)

	Ref	Expression
Assertion	df-ttrcl	Could not format assertion : 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. m e. n ( f ` m ) R ( f ` suc m ) ) } with typecode |-

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cR	$$classR$$
1	0	cttrcl	Could not format t++ R : No typesetting found for class t++ R with typecode class
2		vx	$$setvarx$$
3		vy	$$setvary$$
4		vn	$$setvarn$$
5		com	$$class\mathrm{\omega }$$
6		c1o	$$class{1}_{𝑜}$$
7	5 6	cdif	$$class\left(\mathrm{\omega }\setminus 1_{𝑜}\right)$$
8		vf	$$setvarf$$
9	8	cv	$$setvarf$$
10	4	cv	$$setvarn$$
11	10	csuc	$$class\mathrm{suc}n$$
12	9 11	wfn	$$wfffFn\mathrm{suc}n$$
13		c0	$$class\varnothing$$
14	13 9	cfv	$$classf\left(\varnothing \right)$$
15	2	cv	$$setvarx$$
16	14 15	wceq	$$wfff\left(\varnothing \right)=x$$
17	10 9	cfv	$$classf\left(n\right)$$
18	3	cv	$$setvary$$
19	17 18	wceq	$$wfff\left(n\right)=y$$
20	16 19	wa	$$wff\left(f\left(\varnothing \right)=x\wedge f\left(n\right)=y\right)$$
21		vm	$$setvarm$$
22	21	cv	$$setvarm$$
23	22 9	cfv	$$classf\left(m\right)$$
24	22	csuc	$$class\mathrm{suc}m$$
25	24 9	cfv	$$classf\left(\mathrm{suc}m\right)$$
26	23 25 0	wbr	$$wfff\left(m\right)Rf\left(\mathrm{suc}m\right)$$
27	26 21 10	wral	$$wff\forall m\in nf\left(m\right)Rf\left(\mathrm{suc}m\right)$$
28	12 20 27	w3a	$$wff\left(fFn\mathrm{suc}n\wedge \left(f\left(\varnothing \right)=x\wedge f\left(n\right)=y\right)\wedge \forall m\in nf\left(m\right)Rf\left(\mathrm{suc}m\right)\right)$$
29	28 8	wex	$$wff\exists f\left(fFn\mathrm{suc}n\wedge \left(f\left(\varnothing \right)=x\wedge f\left(n\right)=y\right)\wedge \forall m\in nf\left(m\right)Rf\left(\mathrm{suc}m\right)\right)$$
30	29 4 7	wrex	$$wff\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 m\in nf\left(m\right)Rf\left(\mathrm{suc}m\right)\right)$$
31	30 2 3	copab	$$class\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 m\in nf\left(m\right)Rf\left(\mathrm{suc}m\right)\right)\right\}$$
32	1 31	wceq	Could not format t++ R = { <. x , y >. | E. n e. ( _om \ 1o ) E. f ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = y ) /\ A. m e. n ( f ` m ) R ( f ` suc m ) ) } : No typesetting found for wff t++ R = { <. x , y >. | E. n e. ( _om \ 1o ) E. f ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = y ) /\ A. m e. n ( f ` m ) R ( f ` suc m ) ) } with typecode wff