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 )