# Metamath Proof Explorer

## Theorem tfrlem7

Description: Lemma for transfinite recursion. The union of all acceptable functions is a function. (Contributed by NM, 9-Aug-1994) (Revised by Mario Carneiro, 24-May-2019)

Ref Expression
Hypothesis tfrlem.1
`|- A = { f | E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) ) }`
Assertion tfrlem7
`|- Fun recs ( F )`

### Proof

Step Hyp Ref Expression
1 tfrlem.1
` |-  A = { f | E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) ) }`
2 1 tfrlem6
` |-  Rel recs ( F )`
3 1 recsfval
` |-  recs ( F ) = U. A`
4 3 eleq2i
` |-  ( <. x , u >. e. recs ( F ) <-> <. x , u >. e. U. A )`
5 eluni
` |-  ( <. x , u >. e. U. A <-> E. g ( <. x , u >. e. g /\ g e. A ) )`
6 4 5 bitri
` |-  ( <. x , u >. e. recs ( F ) <-> E. g ( <. x , u >. e. g /\ g e. A ) )`
7 3 eleq2i
` |-  ( <. x , v >. e. recs ( F ) <-> <. x , v >. e. U. A )`
8 eluni
` |-  ( <. x , v >. e. U. A <-> E. h ( <. x , v >. e. h /\ h e. A ) )`
9 7 8 bitri
` |-  ( <. x , v >. e. recs ( F ) <-> E. h ( <. x , v >. e. h /\ h e. A ) )`
10 6 9 anbi12i
` |-  ( ( <. x , u >. e. recs ( F ) /\ <. x , v >. e. recs ( F ) ) <-> ( E. g ( <. x , u >. e. g /\ g e. A ) /\ E. h ( <. x , v >. e. h /\ h e. A ) ) )`
11 exdistrv
` |-  ( E. g E. h ( ( <. x , u >. e. g /\ g e. A ) /\ ( <. x , v >. e. h /\ h e. A ) ) <-> ( E. g ( <. x , u >. e. g /\ g e. A ) /\ E. h ( <. x , v >. e. h /\ h e. A ) ) )`
12 10 11 bitr4i
` |-  ( ( <. x , u >. e. recs ( F ) /\ <. x , v >. e. recs ( F ) ) <-> E. g E. h ( ( <. x , u >. e. g /\ g e. A ) /\ ( <. x , v >. e. h /\ h e. A ) ) )`
13 df-br
` |-  ( x g u <-> <. x , u >. e. g )`
14 df-br
` |-  ( x h v <-> <. x , v >. e. h )`
15 13 14 anbi12i
` |-  ( ( x g u /\ x h v ) <-> ( <. x , u >. e. g /\ <. x , v >. e. h ) )`
16 1 tfrlem5
` |-  ( ( g e. A /\ h e. A ) -> ( ( x g u /\ x h v ) -> u = v ) )`
17 16 impcom
` |-  ( ( ( x g u /\ x h v ) /\ ( g e. A /\ h e. A ) ) -> u = v )`
18 15 17 sylanbr
` |-  ( ( ( <. x , u >. e. g /\ <. x , v >. e. h ) /\ ( g e. A /\ h e. A ) ) -> u = v )`
19 18 an4s
` |-  ( ( ( <. x , u >. e. g /\ g e. A ) /\ ( <. x , v >. e. h /\ h e. A ) ) -> u = v )`
20 19 exlimivv
` |-  ( E. g E. h ( ( <. x , u >. e. g /\ g e. A ) /\ ( <. x , v >. e. h /\ h e. A ) ) -> u = v )`
21 12 20 sylbi
` |-  ( ( <. x , u >. e. recs ( F ) /\ <. x , v >. e. recs ( F ) ) -> u = v )`
22 21 ax-gen
` |-  A. v ( ( <. x , u >. e. recs ( F ) /\ <. x , v >. e. recs ( F ) ) -> u = v )`
23 22 gen2
` |-  A. x A. u A. v ( ( <. x , u >. e. recs ( F ) /\ <. x , v >. e. recs ( F ) ) -> u = v )`
24 dffun4
` |-  ( Fun recs ( F ) <-> ( Rel recs ( F ) /\ A. x A. u A. v ( ( <. x , u >. e. recs ( F ) /\ <. x , v >. e. recs ( F ) ) -> u = v ) ) )`
25 2 23 24 mpbir2an
` |-  Fun recs ( F )`