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 ) ) )