Metamath Proof Explorer

Theorem bnj893

Description: Property of _trCl . Under certain conditions, the transitive closure of X in A by R is a set. (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

Ref Expression
Assertion bnj893 
|- ( ( R _FrSe A /\ X e. A ) -> _trCl ( X , A , R ) e. _V )

Proof

Step Hyp Ref Expression
1 biid 
 |-  ( ( f ` (/) ) = _pred ( X , A , R ) <-> ( f ` (/) ) = _pred ( X , A , R ) )
2 biid 
 |-  ( A. i e. _om ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) <-> A. i e. _om ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) )
3 eqid 
 |-  ( _om \ { (/) } ) = ( _om \ { (/) } )
4 eqid 
 |-  { 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 ) ) ) } = { 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 ) ) ) }
5 1 2 3 4 bnj882 
 |-  _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 vex 
 |-  g e. _V
7 fveq1 
 |-  ( f = g -> ( f ` (/) ) = ( g ` (/) ) )
8 7 eqeq1d 
 |-  ( f = g -> ( ( f ` (/) ) = _pred ( X , A , R ) <-> ( g ` (/) ) = _pred ( X , A , R ) ) )
9 6 8 sbcie 
 |-  ( [. g / f ]. ( f ` (/) ) = _pred ( X , A , R ) <-> ( g ` (/) ) = _pred ( X , A , R ) )
10 9 bicomi 
 |-  ( ( g ` (/) ) = _pred ( X , A , R ) <-> [. g / f ]. ( f ` (/) ) = _pred ( X , A , R ) )
11 fveq1 
 |-  ( f = g -> ( f ` suc i ) = ( g ` suc i ) )
12 fveq1 
 |-  ( f = g -> ( f ` i ) = ( g ` i ) )
13 12 iuneq1d 
 |-  ( f = g -> U_ y e. ( f ` i ) _pred ( y , A , R ) = U_ y e. ( g ` i ) _pred ( y , A , R ) )
14 11 13 eqeq12d 
 |-  ( f = g -> ( ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) <-> ( g ` suc i ) = U_ y e. ( g ` i ) _pred ( y , A , R ) ) )
15 14 imbi2d 
 |-  ( f = g -> ( ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) <-> ( suc i e. n -> ( g ` suc i ) = U_ y e. ( g ` i ) _pred ( y , A , R ) ) ) )
16 15 ralbidv 
 |-  ( f = g -> ( A. i e. _om ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) <-> A. i e. _om ( suc i e. n -> ( g ` suc i ) = U_ y e. ( g ` i ) _pred ( y , A , R ) ) ) )
17 6 16 sbcie 
 |-  ( [. g / f ]. A. i e. _om ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) <-> A. i e. _om ( suc i e. n -> ( g ` suc i ) = U_ y e. ( g ` i ) _pred ( y , A , R ) ) )
18 17 bicomi 
 |-  ( A. i e. _om ( suc i e. n -> ( g ` suc i ) = U_ y e. ( g ` i ) _pred ( y , A , R ) ) <-> [. g / f ]. A. i e. _om ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) )
19 4 10 18 bnj873 
 |-  { 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 ) ) ) } = { g | E. n e. ( _om \ { (/) } ) ( g Fn n /\ ( g ` (/) ) = _pred ( X , A , R ) /\ A. i e. _om ( suc i e. n -> ( g ` suc i ) = U_ y e. ( g ` i ) _pred ( y , A , R ) ) ) }
20 19 eleq2i 
 |-  ( 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 ) ) ) } <-> f e. { g | E. n e. ( _om \ { (/) } ) ( g Fn n /\ ( g ` (/) ) = _pred ( X , A , R ) /\ A. i e. _om ( suc i e. n -> ( g ` suc i ) = U_ y e. ( g ` i ) _pred ( y , A , R ) ) ) } )
21 20 anbi1i 
 |-  ( ( 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 ) ) <-> ( f e. { g | E. n e. ( _om \ { (/) } ) ( g Fn n /\ ( g ` (/) ) = _pred ( X , A , R ) /\ A. i e. _om ( suc i e. n -> ( g ` suc i ) = U_ y e. ( g ` i ) _pred ( y , A , R ) ) ) } /\ w e. U_ i e. dom f ( f ` i ) ) )
22 21 rexbii2 
 |-  ( 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 ) <-> E. f e. { g | E. n e. ( _om \ { (/) } ) ( g Fn n /\ ( g ` (/) ) = _pred ( X , A , R ) /\ A. i e. _om ( suc i e. n -> ( g ` suc i ) = U_ y e. ( g ` i ) _pred ( y , A , R ) ) ) } w e. U_ i e. dom f ( f ` i ) )
23 22 abbii 
 |-  { 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 ) } = { w | E. f e. { g | E. n e. ( _om \ { (/) } ) ( g Fn n /\ ( g ` (/) ) = _pred ( X , A , R ) /\ A. i e. _om ( suc i e. n -> ( g ` suc i ) = U_ y e. ( g ` i ) _pred ( y , A , R ) ) ) } w e. U_ i e. dom f ( f ` i ) }
24 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 ) }
25 df-iun 
 |-  U_ f e. { g | E. n e. ( _om \ { (/) } ) ( g Fn n /\ ( g ` (/) ) = _pred ( X , A , R ) /\ A. i e. _om ( suc i e. n -> ( g ` suc i ) = U_ y e. ( g ` i ) _pred ( y , A , R ) ) ) } U_ i e. dom f ( f ` i ) = { w | E. f e. { g | E. n e. ( _om \ { (/) } ) ( g Fn n /\ ( g ` (/) ) = _pred ( X , A , R ) /\ A. i e. _om ( suc i e. n -> ( g ` suc i ) = U_ y e. ( g ` i ) _pred ( y , A , R ) ) ) } w e. U_ i e. dom f ( f ` i ) }
26 23 24 25 3eqtr4i 
 |-  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 ) = U_ f e. { g | E. n e. ( _om \ { (/) } ) ( g Fn n /\ ( g ` (/) ) = _pred ( X , A , R ) /\ A. i e. _om ( suc i e. n -> ( g ` suc i ) = U_ y e. ( g ` i ) _pred ( y , A , R ) ) ) } U_ i e. dom f ( f ` i )
27 biid 
 |-  ( ( g ` (/) ) = _pred ( X , A , R ) <-> ( g ` (/) ) = _pred ( X , A , R ) )
28 biid 
 |-  ( A. i e. _om ( suc i e. n -> ( g ` suc i ) = U_ y e. ( g ` i ) _pred ( y , A , R ) ) <-> A. i e. _om ( suc i e. n -> ( g ` suc i ) = U_ y e. ( g ` i ) _pred ( y , A , R ) ) )
29 eqid 
 |-  { g | E. n e. ( _om \ { (/) } ) ( g Fn n /\ ( g ` (/) ) = _pred ( X , A , R ) /\ A. i e. _om ( suc i e. n -> ( g ` suc i ) = U_ y e. ( g ` i ) _pred ( y , A , R ) ) ) } = { g | E. n e. ( _om \ { (/) } ) ( g Fn n /\ ( g ` (/) ) = _pred ( X , A , R ) /\ A. i e. _om ( suc i e. n -> ( g ` suc i ) = U_ y e. ( g ` i ) _pred ( y , A , R ) ) ) }
30 biid 
 |-  ( ( R _FrSe A /\ X e. A /\ n e. ( _om \ { (/) } ) ) <-> ( R _FrSe A /\ X e. A /\ n e. ( _om \ { (/) } ) ) )
31 biid 
 |-  ( ( g Fn n /\ ( g ` (/) ) = _pred ( X , A , R ) /\ A. i e. _om ( suc i e. n -> ( g ` suc i ) = U_ y e. ( g ` i ) _pred ( y , A , R ) ) ) <-> ( g Fn n /\ ( g ` (/) ) = _pred ( X , A , R ) /\ A. i e. _om ( suc i e. n -> ( g ` suc i ) = U_ y e. ( g ` i ) _pred ( y , A , R ) ) ) )
32 biid 
 |-  ( [. z / g ]. ( g ` (/) ) = _pred ( X , A , R ) <-> [. z / g ]. ( g ` (/) ) = _pred ( X , A , R ) )
33 biid 
 |-  ( [. z / g ]. A. i e. _om ( suc i e. n -> ( g ` suc i ) = U_ y e. ( g ` i ) _pred ( y , A , R ) ) <-> [. z / g ]. A. i e. _om ( suc i e. n -> ( g ` suc i ) = U_ y e. ( g ` i ) _pred ( y , A , R ) ) )
34 biid 
 |-  ( [. z / g ]. ( g Fn n /\ ( g ` (/) ) = _pred ( X , A , R ) /\ A. i e. _om ( suc i e. n -> ( g ` suc i ) = U_ y e. ( g ` i ) _pred ( y , A , R ) ) ) <-> [. z / g ]. ( g Fn n /\ ( g ` (/) ) = _pred ( X , A , R ) /\ A. i e. _om ( suc i e. n -> ( g ` suc i ) = U_ y e. ( g ` i ) _pred ( y , A , R ) ) ) )
35 biid 
 |-  ( ( R _FrSe A /\ X e. A ) <-> ( R _FrSe A /\ X e. A ) )
36 27 28 3 29 30 31 32 33 34 35 bnj849 
 |-  ( ( R _FrSe A /\ X e. A ) -> { g | E. n e. ( _om \ { (/) } ) ( g Fn n /\ ( g ` (/) ) = _pred ( X , A , R ) /\ A. i e. _om ( suc i e. n -> ( g ` suc i ) = U_ y e. ( g ` i ) _pred ( y , A , R ) ) ) } e. _V )
37 vex 
 |-  f e. _V
38 37 dmex 
 |-  dom f e. _V
39 fvex 
 |-  ( f ` i ) e. _V
40 38 39 iunex 
 |-  U_ i e. dom f ( f ` i ) e. _V
41 40 rgenw 
 |-  A. f e. { g | E. n e. ( _om \ { (/) } ) ( g Fn n /\ ( g ` (/) ) = _pred ( X , A , R ) /\ A. i e. _om ( suc i e. n -> ( g ` suc i ) = U_ y e. ( g ` i ) _pred ( y , A , R ) ) ) } U_ i e. dom f ( f ` i ) e. _V
42 iunexg 
 |-  ( ( { g | E. n e. ( _om \ { (/) } ) ( g Fn n /\ ( g ` (/) ) = _pred ( X , A , R ) /\ A. i e. _om ( suc i e. n -> ( g ` suc i ) = U_ y e. ( g ` i ) _pred ( y , A , R ) ) ) } e. _V /\ A. f e. { g | E. n e. ( _om \ { (/) } ) ( g Fn n /\ ( g ` (/) ) = _pred ( X , A , R ) /\ A. i e. _om ( suc i e. n -> ( g ` suc i ) = U_ y e. ( g ` i ) _pred ( y , A , R ) ) ) } U_ i e. dom f ( f ` i ) e. _V ) -> U_ f e. { g | E. n e. ( _om \ { (/) } ) ( g Fn n /\ ( g ` (/) ) = _pred ( X , A , R ) /\ A. i e. _om ( suc i e. n -> ( g ` suc i ) = U_ y e. ( g ` i ) _pred ( y , A , R ) ) ) } U_ i e. dom f ( f ` i ) e. _V )
43 36 41 42 sylancl 
 |-  ( ( R _FrSe A /\ X e. A ) -> U_ f e. { g | E. n e. ( _om \ { (/) } ) ( g Fn n /\ ( g ` (/) ) = _pred ( X , A , R ) /\ A. i e. _om ( suc i e. n -> ( g ` suc i ) = U_ y e. ( g ` i ) _pred ( y , A , R ) ) ) } U_ i e. dom f ( f ` i ) e. _V )
44 26 43 eqeltrid 
 |-  ( ( R _FrSe A /\ X e. A ) -> 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 ) e. _V )
45 5 44 eqeltrid 
 |-  ( ( R _FrSe A /\ X e. A ) -> _trCl ( X , A , R ) e. _V )