Metamath Proof Explorer

Theorem bnj882

Description: Definition (using hypotheses for readability) of the function giving the transitive closure of X in A by R . (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

Ref Expression
Hypotheses bnj882.1 
|- ( ph <-> ( f ` (/) ) = _pred ( X , A , R ) )
bnj882.2 
|- ( ps <-> A. i e. _om ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) )
bnj882.3 
|- D = ( _om \ { (/) } )
bnj882.4 
|- B = { f | E. n e. D ( f Fn n /\ ph /\ ps ) }
Assertion bnj882 
|- _trCl ( X , A , R ) = U_ f e. B U_ i e. dom f ( f ` i )

Proof

Step Hyp Ref Expression
1 bnj882.1 
 |-  ( ph <-> ( f ` (/) ) = _pred ( X , A , R ) )
2 bnj882.2 
 |-  ( ps <-> A. i e. _om ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) )
3 bnj882.3 
 |-  D = ( _om \ { (/) } )
4 bnj882.4 
 |-  B = { f | E. n e. D ( f Fn n /\ ph /\ ps ) }
5 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 )
6 df-iun 
 |-  U_ f e. B U_ i e. dom f ( f ` i ) = { w | E. f e. B w e. U_ i e. dom f ( f ` i ) }
7 df-iun 
 |-  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 ) = { w | E. 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 ) ) ) } w e. U_ i e. dom f ( f ` i ) }
8 1 2 anbi12i 
 |-  ( ( ph /\ ps ) <-> ( ( 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 ) ) ) )
9 8 anbi2i 
 |-  ( ( f Fn n /\ ( ph /\ ps ) ) <-> ( 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 ) ) ) ) )
10 3anass 
 |-  ( ( f Fn n /\ ph /\ ps ) <-> ( f Fn n /\ ( ph /\ ps ) ) )
11 3anass 
 |-  ( ( 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 ) ) ) <-> ( 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 ) ) ) ) )
12 9 10 11 3bitr4i 
 |-  ( ( f Fn n /\ ph /\ ps ) <-> ( 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 ) ) ) )
13 3 12 rexeqbii 
 |-  ( E. n e. D ( f Fn n /\ ph /\ ps ) <-> 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 ) ) ) )
14 13 abbii 
 |-  { f | E. n e. D ( f Fn n /\ ph /\ ps ) } = { 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 ) ) ) }
15 4 14 eqtri 
 |-  B = { 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 ) ) ) }
16 15 eleq2i 
 |-  ( f e. B <-> 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 ) ) ) } )
17 16 anbi1i 
 |-  ( ( f e. B /\ w e. U_ i e. dom f ( f ` i ) ) <-> ( 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 ) ) ) } /\ w e. U_ i e. dom f ( f ` i ) ) )
18 17 rexbii2 
 |-  ( E. f e. B w e. U_ i e. dom f ( f ` i ) <-> E. 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 ) ) ) } w e. U_ i e. dom f ( f ` i ) )
19 18 abbii 
 |-  { w | E. f e. B w e. U_ i e. dom f ( f ` i ) } = { w | E. 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 ) ) ) } w e. U_ i e. dom f ( f ` i ) }
20 7 19 eqtr4i 
 |-  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 ) = { w | E. f e. B w e. U_ i e. dom f ( f ` i ) }
21 6 20 eqtr4i 
 |-  U_ f e. B U_ i e. dom f ( f ` i ) = 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 )
22 5 21 eqtr4i 
 |-  _trCl ( X , A , R ) = U_ f e. B U_ i e. dom f ( f ` i )