Metamath Proof Explorer

Theorem tfrlem9

Description: Lemma for transfinite recursion. Here we compute the value of recs (the union of all acceptable functions). (Contributed by NM, 17-Aug-1994)

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

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 eldm2g 
 |-  ( B e. dom recs ( F ) -> ( B e. dom recs ( F ) <-> E. z <. B , z >. e. recs ( F ) ) )
3 2 ibi 
 |-  ( B e. dom recs ( F ) -> E. z <. B , z >. e. recs ( F ) )
4 dfrecs3 
 |-  recs ( F ) = U. { f | E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) ) }
5 4 eleq2i 
 |-  ( <. B , z >. e. recs ( F ) <-> <. B , z >. e. U. { f | E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) ) } )
6 eluniab 
 |-  ( <. B , z >. e. U. { f | E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) ) } <-> E. f ( <. B , z >. e. f /\ E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) ) ) )
7 5 6 bitri 
 |-  ( <. B , z >. e. recs ( F ) <-> E. f ( <. B , z >. e. f /\ E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) ) ) )
8 fnop 
 |-  ( ( f Fn x /\ <. B , z >. e. f ) -> B e. x )
9 rspe 
 |-  ( ( x e. On /\ ( f Fn x /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) ) ) -> E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) ) )
10 1 abeq2i 
 |-  ( f e. A <-> E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) ) )
11 elssuni 
 |-  ( f e. A -> f C_ U. A )
12 1 recsfval 
 |-  recs ( F ) = U. A
13 11 12 sseqtrrdi 
 |-  ( f e. A -> f C_ recs ( F ) )
14 10 13 sylbir 
 |-  ( E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) ) -> f C_ recs ( F ) )
15 9 14 syl 
 |-  ( ( x e. On /\ ( f Fn x /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) ) ) -> f C_ recs ( F ) )
16 fveq2 
 |-  ( y = B -> ( f ` y ) = ( f ` B ) )
17 reseq2 
 |-  ( y = B -> ( f |` y ) = ( f |` B ) )
18 17 fveq2d 
 |-  ( y = B -> ( F ` ( f |` y ) ) = ( F ` ( f |` B ) ) )
19 16 18 eqeq12d 
 |-  ( y = B -> ( ( f ` y ) = ( F ` ( f |` y ) ) <-> ( f ` B ) = ( F ` ( f |` B ) ) ) )
20 19 rspcv 
 |-  ( B e. x -> ( A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) -> ( f ` B ) = ( F ` ( f |` B ) ) ) )
21 fndm 
 |-  ( f Fn x -> dom f = x )
22 21 eleq2d 
 |-  ( f Fn x -> ( B e. dom f <-> B e. x ) )
23 1 tfrlem7 
 |-  Fun recs ( F )
24 funssfv 
 |-  ( ( Fun recs ( F ) /\ f C_ recs ( F ) /\ B e. dom f ) -> ( recs ( F ) ` B ) = ( f ` B ) )
25 23 24 mp3an1 
 |-  ( ( f C_ recs ( F ) /\ B e. dom f ) -> ( recs ( F ) ` B ) = ( f ` B ) )
26 25 adantrl 
 |-  ( ( f C_ recs ( F ) /\ ( ( f Fn x /\ x e. On ) /\ B e. dom f ) ) -> ( recs ( F ) ` B ) = ( f ` B ) )
27 21 eleq1d 
 |-  ( f Fn x -> ( dom f e. On <-> x e. On ) )
28 onelss 
 |-  ( dom f e. On -> ( B e. dom f -> B C_ dom f ) )
29 27 28 syl6bir 
 |-  ( f Fn x -> ( x e. On -> ( B e. dom f -> B C_ dom f ) ) )
30 29 imp31 
 |-  ( ( ( f Fn x /\ x e. On ) /\ B e. dom f ) -> B C_ dom f )
31 fun2ssres 
 |-  ( ( Fun recs ( F ) /\ f C_ recs ( F ) /\ B C_ dom f ) -> ( recs ( F ) |` B ) = ( f |` B ) )
32 31 fveq2d 
 |-  ( ( Fun recs ( F ) /\ f C_ recs ( F ) /\ B C_ dom f ) -> ( F ` ( recs ( F ) |` B ) ) = ( F ` ( f |` B ) ) )
33 23 32 mp3an1 
 |-  ( ( f C_ recs ( F ) /\ B C_ dom f ) -> ( F ` ( recs ( F ) |` B ) ) = ( F ` ( f |` B ) ) )
34 30 33 sylan2 
 |-  ( ( f C_ recs ( F ) /\ ( ( f Fn x /\ x e. On ) /\ B e. dom f ) ) -> ( F ` ( recs ( F ) |` B ) ) = ( F ` ( f |` B ) ) )
35 26 34 eqeq12d 
 |-  ( ( f C_ recs ( F ) /\ ( ( f Fn x /\ x e. On ) /\ B e. dom f ) ) -> ( ( recs ( F ) ` B ) = ( F ` ( recs ( F ) |` B ) ) <-> ( f ` B ) = ( F ` ( f |` B ) ) ) )
36 35 exbiri 
 |-  ( f C_ recs ( F ) -> ( ( ( f Fn x /\ x e. On ) /\ B e. dom f ) -> ( ( f ` B ) = ( F ` ( f |` B ) ) -> ( recs ( F ) ` B ) = ( F ` ( recs ( F ) |` B ) ) ) ) )
37 36 com3l 
 |-  ( ( ( f Fn x /\ x e. On ) /\ B e. dom f ) -> ( ( f ` B ) = ( F ` ( f |` B ) ) -> ( f C_ recs ( F ) -> ( recs ( F ) ` B ) = ( F ` ( recs ( F ) |` B ) ) ) ) )
38 37 exp31 
 |-  ( f Fn x -> ( x e. On -> ( B e. dom f -> ( ( f ` B ) = ( F ` ( f |` B ) ) -> ( f C_ recs ( F ) -> ( recs ( F ) ` B ) = ( F ` ( recs ( F ) |` B ) ) ) ) ) ) )
39 38 com34 
 |-  ( f Fn x -> ( x e. On -> ( ( f ` B ) = ( F ` ( f |` B ) ) -> ( B e. dom f -> ( f C_ recs ( F ) -> ( recs ( F ) ` B ) = ( F ` ( recs ( F ) |` B ) ) ) ) ) ) )
40 39 com24 
 |-  ( f Fn x -> ( B e. dom f -> ( ( f ` B ) = ( F ` ( f |` B ) ) -> ( x e. On -> ( f C_ recs ( F ) -> ( recs ( F ) ` B ) = ( F ` ( recs ( F ) |` B ) ) ) ) ) ) )
41 22 40 sylbird 
 |-  ( f Fn x -> ( B e. x -> ( ( f ` B ) = ( F ` ( f |` B ) ) -> ( x e. On -> ( f C_ recs ( F ) -> ( recs ( F ) ` B ) = ( F ` ( recs ( F ) |` B ) ) ) ) ) ) )
42 41 com3l 
 |-  ( B e. x -> ( ( f ` B ) = ( F ` ( f |` B ) ) -> ( f Fn x -> ( x e. On -> ( f C_ recs ( F ) -> ( recs ( F ) ` B ) = ( F ` ( recs ( F ) |` B ) ) ) ) ) ) )
43 20 42 syld 
 |-  ( B e. x -> ( A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) -> ( f Fn x -> ( x e. On -> ( f C_ recs ( F ) -> ( recs ( F ) ` B ) = ( F ` ( recs ( F ) |` B ) ) ) ) ) ) )
44 43 com24 
 |-  ( B e. x -> ( x e. On -> ( f Fn x -> ( A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) -> ( f C_ recs ( F ) -> ( recs ( F ) ` B ) = ( F ` ( recs ( F ) |` B ) ) ) ) ) ) )
45 44 imp4d 
 |-  ( B e. x -> ( ( x e. On /\ ( f Fn x /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) ) ) -> ( f C_ recs ( F ) -> ( recs ( F ) ` B ) = ( F ` ( recs ( F ) |` B ) ) ) ) )
46 15 45 mpdi 
 |-  ( B e. x -> ( ( x e. On /\ ( f Fn x /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) ) ) -> ( recs ( F ) ` B ) = ( F ` ( recs ( F ) |` B ) ) ) )
47 8 46 syl 
 |-  ( ( f Fn x /\ <. B , z >. e. f ) -> ( ( x e. On /\ ( f Fn x /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) ) ) -> ( recs ( F ) ` B ) = ( F ` ( recs ( F ) |` B ) ) ) )
48 47 exp4d 
 |-  ( ( f Fn x /\ <. B , z >. e. f ) -> ( x e. On -> ( f Fn x -> ( A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) -> ( recs ( F ) ` B ) = ( F ` ( recs ( F ) |` B ) ) ) ) ) )
49 48 ex 
 |-  ( f Fn x -> ( <. B , z >. e. f -> ( x e. On -> ( f Fn x -> ( A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) -> ( recs ( F ) ` B ) = ( F ` ( recs ( F ) |` B ) ) ) ) ) ) )
50 49 com4r 
 |-  ( f Fn x -> ( f Fn x -> ( <. B , z >. e. f -> ( x e. On -> ( A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) -> ( recs ( F ) ` B ) = ( F ` ( recs ( F ) |` B ) ) ) ) ) ) )
51 50 pm2.43i 
 |-  ( f Fn x -> ( <. B , z >. e. f -> ( x e. On -> ( A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) -> ( recs ( F ) ` B ) = ( F ` ( recs ( F ) |` B ) ) ) ) ) )
52 51 com3l 
 |-  ( <. B , z >. e. f -> ( x e. On -> ( f Fn x -> ( A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) -> ( recs ( F ) ` B ) = ( F ` ( recs ( F ) |` B ) ) ) ) ) )
53 52 imp4a 
 |-  ( <. B , z >. e. f -> ( x e. On -> ( ( f Fn x /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) ) -> ( recs ( F ) ` B ) = ( F ` ( recs ( F ) |` B ) ) ) ) )
54 53 rexlimdv 
 |-  ( <. B , z >. e. f -> ( E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) ) -> ( recs ( F ) ` B ) = ( F ` ( recs ( F ) |` B ) ) ) )
55 54 imp 
 |-  ( ( <. B , z >. e. f /\ E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) ) ) -> ( recs ( F ) ` B ) = ( F ` ( recs ( F ) |` B ) ) )
56 55 exlimiv 
 |-  ( E. f ( <. B , z >. e. f /\ E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) ) ) -> ( recs ( F ) ` B ) = ( F ` ( recs ( F ) |` B ) ) )
57 7 56 sylbi 
 |-  ( <. B , z >. e. recs ( F ) -> ( recs ( F ) ` B ) = ( F ` ( recs ( F ) |` B ) ) )
58 57 exlimiv 
 |-  ( E. z <. B , z >. e. recs ( F ) -> ( recs ( F ) ` B ) = ( F ` ( recs ( F ) |` B ) ) )
59 3 58 syl 
 |-  ( B e. dom recs ( F ) -> ( recs ( F ) ` B ) = ( F ` ( recs ( F ) |` B ) ) )