Metamath Proof Explorer

Theorem tfrlem12

Description: Lemma for transfinite recursion. Show C is an acceptable function. (Contributed by NM, 15-Aug-1994) (Revised by Mario Carneiro, 9-May-2015)

Ref Expression
Hypotheses tfrlem.1 
|- A = { f | E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) ) }
tfrlem.3 
|- C = ( recs ( F ) u. { <. dom recs ( F ) , ( F ` recs ( F ) ) >. } )
Assertion tfrlem12 
|- ( recs ( F ) e. _V -> C e. A )

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 tfrlem.3 
 |-  C = ( recs ( F ) u. { <. dom recs ( F ) , ( F ` recs ( F ) ) >. } )
3 1 tfrlem8 
 |-  Ord dom recs ( F )
4 3 a1i 
 |-  ( recs ( F ) e. _V -> Ord dom recs ( F ) )
5 dmexg 
 |-  ( recs ( F ) e. _V -> dom recs ( F ) e. _V )
6 elon2 
 |-  ( dom recs ( F ) e. On <-> ( Ord dom recs ( F ) /\ dom recs ( F ) e. _V ) )
7 4 5 6 sylanbrc 
 |-  ( recs ( F ) e. _V -> dom recs ( F ) e. On )
8 suceloni 
 |-  ( dom recs ( F ) e. On -> suc dom recs ( F ) e. On )
9 1 2 tfrlem10 
 |-  ( dom recs ( F ) e. On -> C Fn suc dom recs ( F ) )
10 1 2 tfrlem11 
 |-  ( dom recs ( F ) e. On -> ( z e. suc dom recs ( F ) -> ( C ` z ) = ( F ` ( C |` z ) ) ) )
11 10 ralrimiv 
 |-  ( dom recs ( F ) e. On -> A. z e. suc dom recs ( F ) ( C ` z ) = ( F ` ( C |` z ) ) )
12 fveq2 
 |-  ( z = y -> ( C ` z ) = ( C ` y ) )
13 reseq2 
 |-  ( z = y -> ( C |` z ) = ( C |` y ) )
14 13 fveq2d 
 |-  ( z = y -> ( F ` ( C |` z ) ) = ( F ` ( C |` y ) ) )
15 12 14 eqeq12d 
 |-  ( z = y -> ( ( C ` z ) = ( F ` ( C |` z ) ) <-> ( C ` y ) = ( F ` ( C |` y ) ) ) )
16 15 cbvralvw 
 |-  ( A. z e. suc dom recs ( F ) ( C ` z ) = ( F ` ( C |` z ) ) <-> A. y e. suc dom recs ( F ) ( C ` y ) = ( F ` ( C |` y ) ) )
17 11 16 sylib 
 |-  ( dom recs ( F ) e. On -> A. y e. suc dom recs ( F ) ( C ` y ) = ( F ` ( C |` y ) ) )
18 fneq2 
 |-  ( x = suc dom recs ( F ) -> ( C Fn x <-> C Fn suc dom recs ( F ) ) )
19 raleq 
 |-  ( x = suc dom recs ( F ) -> ( A. y e. x ( C ` y ) = ( F ` ( C |` y ) ) <-> A. y e. suc dom recs ( F ) ( C ` y ) = ( F ` ( C |` y ) ) ) )
20 18 19 anbi12d 
 |-  ( x = suc dom recs ( F ) -> ( ( C Fn x /\ A. y e. x ( C ` y ) = ( F ` ( C |` y ) ) ) <-> ( C Fn suc dom recs ( F ) /\ A. y e. suc dom recs ( F ) ( C ` y ) = ( F ` ( C |` y ) ) ) ) )
21 20 rspcev 
 |-  ( ( suc dom recs ( F ) e. On /\ ( C Fn suc dom recs ( F ) /\ A. y e. suc dom recs ( F ) ( C ` y ) = ( F ` ( C |` y ) ) ) ) -> E. x e. On ( C Fn x /\ A. y e. x ( C ` y ) = ( F ` ( C |` y ) ) ) )
22 8 9 17 21 syl12anc 
 |-  ( dom recs ( F ) e. On -> E. x e. On ( C Fn x /\ A. y e. x ( C ` y ) = ( F ` ( C |` y ) ) ) )
23 7 22 syl 
 |-  ( recs ( F ) e. _V -> E. x e. On ( C Fn x /\ A. y e. x ( C ` y ) = ( F ` ( C |` y ) ) ) )
24 snex 
 |-  { <. dom recs ( F ) , ( F ` recs ( F ) ) >. } e. _V
25 unexg 
 |-  ( ( recs ( F ) e. _V /\ { <. dom recs ( F ) , ( F ` recs ( F ) ) >. } e. _V ) -> ( recs ( F ) u. { <. dom recs ( F ) , ( F ` recs ( F ) ) >. } ) e. _V )
26 24 25 mpan2 
 |-  ( recs ( F ) e. _V -> ( recs ( F ) u. { <. dom recs ( F ) , ( F ` recs ( F ) ) >. } ) e. _V )
27 2 26 eqeltrid 
 |-  ( recs ( F ) e. _V -> C e. _V )
28 fneq1 
 |-  ( f = C -> ( f Fn x <-> C Fn x ) )
29 fveq1 
 |-  ( f = C -> ( f ` y ) = ( C ` y ) )
30 reseq1 
 |-  ( f = C -> ( f |` y ) = ( C |` y ) )
31 30 fveq2d 
 |-  ( f = C -> ( F ` ( f |` y ) ) = ( F ` ( C |` y ) ) )
32 29 31 eqeq12d 
 |-  ( f = C -> ( ( f ` y ) = ( F ` ( f |` y ) ) <-> ( C ` y ) = ( F ` ( C |` y ) ) ) )
33 32 ralbidv 
 |-  ( f = C -> ( A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) <-> A. y e. x ( C ` y ) = ( F ` ( C |` y ) ) ) )
34 28 33 anbi12d 
 |-  ( f = C -> ( ( f Fn x /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) ) <-> ( C Fn x /\ A. y e. x ( C ` y ) = ( F ` ( C |` y ) ) ) ) )
35 34 rexbidv 
 |-  ( f = C -> ( E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) ) <-> E. x e. On ( C Fn x /\ A. y e. x ( C ` y ) = ( F ` ( C |` y ) ) ) ) )
36 35 1 elab2g 
 |-  ( C e. _V -> ( C e. A <-> E. x e. On ( C Fn x /\ A. y e. x ( C ` y ) = ( F ` ( C |` y ) ) ) ) )
37 27 36 syl 
 |-  ( recs ( F ) e. _V -> ( C e. A <-> E. x e. On ( C Fn x /\ A. y e. x ( C ` y ) = ( F ` ( C |` y ) ) ) ) )
38 23 37 mpbird 
 |-  ( recs ( F ) e. _V -> C e. A )