Metamath Proof Explorer

Theorem tfrlem9a

Description: Lemma for transfinite recursion. Without using ax-rep , show that all the restrictions of recs are sets. (Contributed by Mario Carneiro, 16-Nov-2014)

Ref Expression
Hypothesis tfrlem.1 
|- A = { f | E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) ) }
Assertion tfrlem9a 
|- ( B e. dom recs ( F ) -> ( recs ( F ) |` B ) e. _V )

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 tfrlem7 
 |-  Fun recs ( F )
3 funfvop 
 |-  ( ( Fun recs ( F ) /\ B e. dom recs ( F ) ) -> <. B , ( recs ( F ) ` B ) >. e. recs ( F ) )
4 2 3 mpan 
 |-  ( B e. dom recs ( F ) -> <. B , ( recs ( F ) ` B ) >. e. recs ( F ) )
5 1 recsfval 
 |-  recs ( F ) = U. A
6 5 eleq2i 
 |-  ( <. B , ( recs ( F ) ` B ) >. e. recs ( F ) <-> <. B , ( recs ( F ) ` B ) >. e. U. A )
7 eluni 
 |-  ( <. B , ( recs ( F ) ` B ) >. e. U. A <-> E. g ( <. B , ( recs ( F ) ` B ) >. e. g /\ g e. A ) )
8 6 7 bitri 
 |-  ( <. B , ( recs ( F ) ` B ) >. e. recs ( F ) <-> E. g ( <. B , ( recs ( F ) ` B ) >. e. g /\ g e. A ) )
9 4 8 sylib 
 |-  ( B e. dom recs ( F ) -> E. g ( <. B , ( recs ( F ) ` B ) >. e. g /\ g e. A ) )
10 simprr 
 |-  ( ( B e. dom recs ( F ) /\ ( <. B , ( recs ( F ) ` B ) >. e. g /\ g e. A ) ) -> g e. A )
11 vex 
 |-  g e. _V
12 1 11 tfrlem3a 
 |-  ( g e. A <-> E. z e. On ( g Fn z /\ A. a e. z ( g ` a ) = ( F ` ( g |` a ) ) ) )
13 10 12 sylib 
 |-  ( ( B e. dom recs ( F ) /\ ( <. B , ( recs ( F ) ` B ) >. e. g /\ g e. A ) ) -> E. z e. On ( g Fn z /\ A. a e. z ( g ` a ) = ( F ` ( g |` a ) ) ) )
14 2 a1i 
 |-  ( ( ( B e. dom recs ( F ) /\ ( <. B , ( recs ( F ) ` B ) >. e. g /\ g e. A ) ) /\ ( z e. On /\ g Fn z ) ) -> Fun recs ( F ) )
15 simplrr 
 |-  ( ( ( B e. dom recs ( F ) /\ ( <. B , ( recs ( F ) ` B ) >. e. g /\ g e. A ) ) /\ ( z e. On /\ g Fn z ) ) -> g e. A )
16 elssuni 
 |-  ( g e. A -> g C_ U. A )
17 15 16 syl 
 |-  ( ( ( B e. dom recs ( F ) /\ ( <. B , ( recs ( F ) ` B ) >. e. g /\ g e. A ) ) /\ ( z e. On /\ g Fn z ) ) -> g C_ U. A )
18 17 5 sseqtrrdi 
 |-  ( ( ( B e. dom recs ( F ) /\ ( <. B , ( recs ( F ) ` B ) >. e. g /\ g e. A ) ) /\ ( z e. On /\ g Fn z ) ) -> g C_ recs ( F ) )
19 fndm 
 |-  ( g Fn z -> dom g = z )
20 19 ad2antll 
 |-  ( ( ( B e. dom recs ( F ) /\ ( <. B , ( recs ( F ) ` B ) >. e. g /\ g e. A ) ) /\ ( z e. On /\ g Fn z ) ) -> dom g = z )
21 simprl 
 |-  ( ( ( B e. dom recs ( F ) /\ ( <. B , ( recs ( F ) ` B ) >. e. g /\ g e. A ) ) /\ ( z e. On /\ g Fn z ) ) -> z e. On )
22 20 21 eqeltrd 
 |-  ( ( ( B e. dom recs ( F ) /\ ( <. B , ( recs ( F ) ` B ) >. e. g /\ g e. A ) ) /\ ( z e. On /\ g Fn z ) ) -> dom g e. On )
23 eloni 
 |-  ( dom g e. On -> Ord dom g )
24 22 23 syl 
 |-  ( ( ( B e. dom recs ( F ) /\ ( <. B , ( recs ( F ) ` B ) >. e. g /\ g e. A ) ) /\ ( z e. On /\ g Fn z ) ) -> Ord dom g )
25 simpll 
 |-  ( ( ( B e. dom recs ( F ) /\ ( <. B , ( recs ( F ) ` B ) >. e. g /\ g e. A ) ) /\ ( z e. On /\ g Fn z ) ) -> B e. dom recs ( F ) )
26 fvexd 
 |-  ( ( ( B e. dom recs ( F ) /\ ( <. B , ( recs ( F ) ` B ) >. e. g /\ g e. A ) ) /\ ( z e. On /\ g Fn z ) ) -> ( recs ( F ) ` B ) e. _V )
27 simplrl 
 |-  ( ( ( B e. dom recs ( F ) /\ ( <. B , ( recs ( F ) ` B ) >. e. g /\ g e. A ) ) /\ ( z e. On /\ g Fn z ) ) -> <. B , ( recs ( F ) ` B ) >. e. g )
28 df-br 
 |-  ( B g ( recs ( F ) ` B ) <-> <. B , ( recs ( F ) ` B ) >. e. g )
29 27 28 sylibr 
 |-  ( ( ( B e. dom recs ( F ) /\ ( <. B , ( recs ( F ) ` B ) >. e. g /\ g e. A ) ) /\ ( z e. On /\ g Fn z ) ) -> B g ( recs ( F ) ` B ) )
30 breldmg 
 |-  ( ( B e. dom recs ( F ) /\ ( recs ( F ) ` B ) e. _V /\ B g ( recs ( F ) ` B ) ) -> B e. dom g )
31 25 26 29 30 syl3anc 
 |-  ( ( ( B e. dom recs ( F ) /\ ( <. B , ( recs ( F ) ` B ) >. e. g /\ g e. A ) ) /\ ( z e. On /\ g Fn z ) ) -> B e. dom g )
32 ordelss 
 |-  ( ( Ord dom g /\ B e. dom g ) -> B C_ dom g )
33 24 31 32 syl2anc 
 |-  ( ( ( B e. dom recs ( F ) /\ ( <. B , ( recs ( F ) ` B ) >. e. g /\ g e. A ) ) /\ ( z e. On /\ g Fn z ) ) -> B C_ dom g )
34 fun2ssres 
 |-  ( ( Fun recs ( F ) /\ g C_ recs ( F ) /\ B C_ dom g ) -> ( recs ( F ) |` B ) = ( g |` B ) )
35 14 18 33 34 syl3anc 
 |-  ( ( ( B e. dom recs ( F ) /\ ( <. B , ( recs ( F ) ` B ) >. e. g /\ g e. A ) ) /\ ( z e. On /\ g Fn z ) ) -> ( recs ( F ) |` B ) = ( g |` B ) )
36 11 resex 
 |-  ( g |` B ) e. _V
37 36 a1i 
 |-  ( ( ( B e. dom recs ( F ) /\ ( <. B , ( recs ( F ) ` B ) >. e. g /\ g e. A ) ) /\ ( z e. On /\ g Fn z ) ) -> ( g |` B ) e. _V )
38 35 37 eqeltrd 
 |-  ( ( ( B e. dom recs ( F ) /\ ( <. B , ( recs ( F ) ` B ) >. e. g /\ g e. A ) ) /\ ( z e. On /\ g Fn z ) ) -> ( recs ( F ) |` B ) e. _V )
39 38 expr 
 |-  ( ( ( B e. dom recs ( F ) /\ ( <. B , ( recs ( F ) ` B ) >. e. g /\ g e. A ) ) /\ z e. On ) -> ( g Fn z -> ( recs ( F ) |` B ) e. _V ) )
40 39 adantrd 
 |-  ( ( ( B e. dom recs ( F ) /\ ( <. B , ( recs ( F ) ` B ) >. e. g /\ g e. A ) ) /\ z e. On ) -> ( ( g Fn z /\ A. a e. z ( g ` a ) = ( F ` ( g |` a ) ) ) -> ( recs ( F ) |` B ) e. _V ) )
41 40 rexlimdva 
 |-  ( ( B e. dom recs ( F ) /\ ( <. B , ( recs ( F ) ` B ) >. e. g /\ g e. A ) ) -> ( E. z e. On ( g Fn z /\ A. a e. z ( g ` a ) = ( F ` ( g |` a ) ) ) -> ( recs ( F ) |` B ) e. _V ) )
42 13 41 mpd 
 |-  ( ( B e. dom recs ( F ) /\ ( <. B , ( recs ( F ) ` B ) >. e. g /\ g e. A ) ) -> ( recs ( F ) |` B ) e. _V )
43 9 42 exlimddv 
 |-  ( B e. dom recs ( F ) -> ( recs ( F ) |` B ) e. _V )