Users' Mathboxes Mathbox for Jonathan Ben-Naim < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-bnj18 Unicode version

Definition df-bnj18 28720
Description: Define the function giving: the transitive closure of 
X in  A by  R. This definition has been designed for facilitating verification that it is eliminable and that the $d restrictions are sound and complete. For a more readable definition see bnj882 28958. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
Assertion
Ref Expression
df-bnj18  |-  trCl ( X ,  A ,  R )  =  U_ f  e.  { f  |  E. n  e.  ( om  \  { (/) } ) ( f  Fn  n  /\  ( f `
 (/) )  =  pred ( X ,  A ,  R )  /\  A. i  e.  om  ( suc  i  e.  n  ->  ( f `  suc  i )  =  U_ y  e.  ( f `  i )  pred (
y ,  A ,  R ) ) ) } U_ i  e. 
dom  f ( f `
 i )
Distinct variable groups:    f, X, n, i, y    A, f, n, i, y    R, f, n, i, y

Detailed syntax breakdown of Definition df-bnj18
StepHypRef Expression
1 cA . . 3  class  A
2 cR . . 3  class  R
3 cX . . 3  class  X
41, 2, 3c-bnj18 28719 . 2  class  trCl ( X ,  A ,  R )
5 vf . . 3  set  f
65cv 1622 . . . . . . 7  class  f
7 vn . . . . . . . 8  set  n
87cv 1622 . . . . . . 7  class  n
96, 8wfn 5250 . . . . . 6  wff  f  Fn  n
10 c0 3455 . . . . . . . 8  class  (/)
1110, 6cfv 5255 . . . . . . 7  class  ( f `
 (/) )
121, 2, 3c-bnj14 28713 . . . . . . 7  class  pred ( X ,  A ,  R )
1311, 12wceq 1623 . . . . . 6  wff  ( f `
 (/) )  =  pred ( X ,  A ,  R )
14 vi . . . . . . . . . . 11  set  i
1514cv 1622 . . . . . . . . . 10  class  i
1615csuc 4394 . . . . . . . . 9  class  suc  i
1716, 8wcel 1684 . . . . . . . 8  wff  suc  i  e.  n
1816, 6cfv 5255 . . . . . . . . 9  class  ( f `
 suc  i )
19 vy . . . . . . . . . 10  set  y
2015, 6cfv 5255 . . . . . . . . . 10  class  ( f `
 i )
2119cv 1622 . . . . . . . . . . 11  class  y
221, 2, 21c-bnj14 28713 . . . . . . . . . 10  class  pred (
y ,  A ,  R )
2319, 20, 22ciun 3905 . . . . . . . . 9  class  U_ y  e.  ( f `  i
)  pred ( y ,  A ,  R )
2418, 23wceq 1623 . . . . . . . 8  wff  ( f `
 suc  i )  =  U_ y  e.  ( f `  i ) 
pred ( y ,  A ,  R )
2517, 24wi 4 . . . . . . 7  wff  ( suc  i  e.  n  -> 
( f `  suc  i )  =  U_ y  e.  ( f `  i )  pred (
y ,  A ,  R ) )
26 com 4656 . . . . . . 7  class  om
2725, 14, 26wral 2543 . . . . . 6  wff  A. i  e.  om  ( suc  i  e.  n  ->  ( f `
 suc  i )  =  U_ y  e.  ( f `  i ) 
pred ( y ,  A ,  R ) )
289, 13, 27w3a 934 . . . . 5  wff  ( f  Fn  n  /\  (
f `  (/) )  = 
pred ( X ,  A ,  R )  /\  A. i  e.  om  ( suc  i  e.  n  ->  ( f `  suc  i )  =  U_ y  e.  ( f `  i )  pred (
y ,  A ,  R ) ) )
2910csn 3640 . . . . . 6  class  { (/) }
3026, 29cdif 3149 . . . . 5  class  ( om 
\  { (/) } )
3128, 7, 30wrex 2544 . . . 4  wff  E. n  e.  ( om  \  { (/)
} ) ( f  Fn  n  /\  (
f `  (/) )  = 
pred ( X ,  A ,  R )  /\  A. i  e.  om  ( suc  i  e.  n  ->  ( f `  suc  i )  =  U_ y  e.  ( f `  i )  pred (
y ,  A ,  R ) ) )
3231, 5cab 2269 . . 3  class  { f  |  E. n  e.  ( om  \  { (/)
} ) ( f  Fn  n  /\  (
f `  (/) )  = 
pred ( X ,  A ,  R )  /\  A. i  e.  om  ( suc  i  e.  n  ->  ( f `  suc  i )  =  U_ y  e.  ( f `  i )  pred (
y ,  A ,  R ) ) ) }
336cdm 4689 . . . 4  class  dom  f
3414, 33, 20ciun 3905 . . 3  class  U_ i  e.  dom  f ( f `
 i )
355, 32, 34ciun 3905 . 2  class  U_ f  e.  { f  |  E. n  e.  ( om  \  { (/) } ) ( f  Fn  n  /\  ( f `  (/) )  = 
pred ( X ,  A ,  R )  /\  A. i  e.  om  ( suc  i  e.  n  ->  ( f `  suc  i )  =  U_ y  e.  ( f `  i )  pred (
y ,  A ,  R ) ) ) } U_ i  e. 
dom  f ( f `
 i )
364, 35wceq 1623 1  wff  trCl ( X ,  A ,  R )  =  U_ f  e.  { f  |  E. n  e.  ( om  \  { (/) } ) ( f  Fn  n  /\  ( f `
 (/) )  =  pred ( X ,  A ,  R )  /\  A. i  e.  om  ( suc  i  e.  n  ->  ( f `  suc  i )  =  U_ y  e.  ( f `  i )  pred (
y ,  A ,  R ) ) ) } U_ i  e. 
dom  f ( f `
 i )
Colors of variables: wff set class
This definition is referenced by:  bnj882  28958  bnj18eq1  28959
  Copyright terms: Public domain W3C validator