Metamath Proof Explorer

Definition df-ttrcl

Description: Define the transitive closure of a class. This is the smallest relation 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 
|- 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 ) ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 cR 
 |-  R
1 0 cttrcl 
 |-  t++ R
2 vx 
 |-  x
3 vy 
 |-  y
4 vn 
 |-  n
5 com 
 |-  _om
6 c1o 
 |-  1o
7 5 6 cdif 
 |-  ( _om \ 1o )
8 vf 
 |-  f
9 8 cv 
 |-  f
10 4 cv 
 |-  n
11 10 csuc 
 |-  suc n
12 9 11 wfn 
 |-  f Fn suc n
13 c0 
 |-  (/)
14 13 9 cfv 
 |-  ( f ` (/) )
15 2 cv 
 |-  x
16 14 15 wceq 
 |-  ( f ` (/) ) = x
17 10 9 cfv 
 |-  ( f ` n )
18 3 cv 
 |-  y
19 17 18 wceq 
 |-  ( f ` n ) = y
20 16 19 wa 
 |-  ( ( f ` (/) ) = x /\ ( f ` n ) = y )
21 vm 
 |-  m
22 21 cv 
 |-  m
23 22 9 cfv 
 |-  ( f ` m )
24 22 csuc 
 |-  suc m
25 24 9 cfv 
 |-  ( f ` suc m )
26 23 25 0 wbr 
 |-  ( f ` m ) R ( f ` suc m )
27 26 21 10 wral 
 |-  A. m e. n ( f ` m ) R ( f ` suc m )
28 12 20 27 w3a 
 |-  ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = y ) /\ A. m e. n ( f ` m ) R ( f ` suc m ) )
29 28 8 wex 
 |-  E. f ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = y ) /\ A. m e. n ( f ` m ) R ( f ` suc m ) )
30 29 4 7 wrex 
 |-  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 ) )
31 30 2 3 copab 
 |-  { <. 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 ) ) }
32 1 31 wceq 
 |-  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 ) ) }