Metamath Proof Explorer

Definition df-bnj18

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 . (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

Ref Expression
Assertion 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 )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cX 
 |-  X
1 cA 
 |-  A
2 cR 
 |-  R
3 1 2 0 c-bnj18 
 |-  _trCl ( X , A , R )
4 vf 
 |-  f
5 vn 
 |-  n
6 com 
 |-  _om
7 c0 
 |-  (/)
8 7 csn 
 |-  { (/) }
9 6 8 cdif 
 |-  ( _om \ { (/) } )
10 4 cv 
 |-  f
11 5 cv 
 |-  n
12 10 11 wfn 
 |-  f Fn n
13 7 10 cfv 
 |-  ( f ` (/) )
14 1 2 0 c-bnj14 
 |-  _pred ( X , A , R )
15 13 14 wceq 
 |-  ( f ` (/) ) = _pred ( X , A , R )
16 vi 
 |-  i
17 16 cv 
 |-  i
18 17 csuc 
 |-  suc i
19 18 11 wcel 
 |-  suc i e. n
20 18 10 cfv 
 |-  ( f ` suc i )
21 vy 
 |-  y
22 17 10 cfv 
 |-  ( f ` i )
23 21 cv 
 |-  y
24 1 2 23 c-bnj14 
 |-  _pred ( y , A , R )
25 21 22 24 ciun 
 |-  U_ y e. ( f ` i ) _pred ( y , A , R )
26 20 25 wceq 
 |-  ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R )
27 19 26 wi 
 |-  ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) )
28 27 16 6 wral 
 |-  A. i e. _om ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) )
29 12 15 28 w3a 
 |-  ( 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 ) ) )
30 29 5 9 wrex 
 |-  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 ) ) )
31 30 4 cab 
 |-  { 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 ) ) ) }
32 10 cdm 
 |-  dom f
33 16 32 22 ciun 
 |-  U_ i e. dom f ( f ` i )
34 4 31 33 ciun 
 |-  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 )
35 3 34 wceq 
 |-  _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 )