# 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 )`