Metamath Proof Explorer

Theorem tfrlem11

Description: Lemma for transfinite recursion. Compute the value of C . (Contributed by NM, 18-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 tfrlem11 
|- ( dom recs ( F ) e. On -> ( B e. suc dom recs ( F ) -> ( C ` B ) = ( F ` ( C |` 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 tfrlem.3 
 |-  C = ( recs ( F ) u. { <. dom recs ( F ) , ( F ` recs ( F ) ) >. } )
3 elsuci 
 |-  ( B e. suc dom recs ( F ) -> ( B e. dom recs ( F ) \/ B = dom recs ( F ) ) )
4 1 2 tfrlem10 
 |-  ( dom recs ( F ) e. On -> C Fn suc dom recs ( F ) )
5 fnfun 
 |-  ( C Fn suc dom recs ( F ) -> Fun C )
6 4 5 syl 
 |-  ( dom recs ( F ) e. On -> Fun C )
7 ssun1 
 |-  recs ( F ) C_ ( recs ( F ) u. { <. dom recs ( F ) , ( F ` recs ( F ) ) >. } )
8 7 2 sseqtrri 
 |-  recs ( F ) C_ C
9 1 tfrlem9 
 |-  ( B e. dom recs ( F ) -> ( recs ( F ) ` B ) = ( F ` ( recs ( F ) |` B ) ) )
10 funssfv 
 |-  ( ( Fun C /\ recs ( F ) C_ C /\ B e. dom recs ( F ) ) -> ( C ` B ) = ( recs ( F ) ` B ) )
11 10 3expa 
 |-  ( ( ( Fun C /\ recs ( F ) C_ C ) /\ B e. dom recs ( F ) ) -> ( C ` B ) = ( recs ( F ) ` B ) )
12 11 adantrl 
 |-  ( ( ( Fun C /\ recs ( F ) C_ C ) /\ ( dom recs ( F ) e. On /\ B e. dom recs ( F ) ) ) -> ( C ` B ) = ( recs ( F ) ` B ) )
13 onelss 
 |-  ( dom recs ( F ) e. On -> ( B e. dom recs ( F ) -> B C_ dom recs ( F ) ) )
14 13 imp 
 |-  ( ( dom recs ( F ) e. On /\ B e. dom recs ( F ) ) -> B C_ dom recs ( F ) )
15 fun2ssres 
 |-  ( ( Fun C /\ recs ( F ) C_ C /\ B C_ dom recs ( F ) ) -> ( C |` B ) = ( recs ( F ) |` B ) )
16 15 3expa 
 |-  ( ( ( Fun C /\ recs ( F ) C_ C ) /\ B C_ dom recs ( F ) ) -> ( C |` B ) = ( recs ( F ) |` B ) )
17 16 fveq2d 
 |-  ( ( ( Fun C /\ recs ( F ) C_ C ) /\ B C_ dom recs ( F ) ) -> ( F ` ( C |` B ) ) = ( F ` ( recs ( F ) |` B ) ) )
18 14 17 sylan2 
 |-  ( ( ( Fun C /\ recs ( F ) C_ C ) /\ ( dom recs ( F ) e. On /\ B e. dom recs ( F ) ) ) -> ( F ` ( C |` B ) ) = ( F ` ( recs ( F ) |` B ) ) )
19 12 18 eqeq12d 
 |-  ( ( ( Fun C /\ recs ( F ) C_ C ) /\ ( dom recs ( F ) e. On /\ B e. dom recs ( F ) ) ) -> ( ( C ` B ) = ( F ` ( C |` B ) ) <-> ( recs ( F ) ` B ) = ( F ` ( recs ( F ) |` B ) ) ) )
20 9 19 imbitrrid 
 |-  ( ( ( Fun C /\ recs ( F ) C_ C ) /\ ( dom recs ( F ) e. On /\ B e. dom recs ( F ) ) ) -> ( B e. dom recs ( F ) -> ( C ` B ) = ( F ` ( C |` B ) ) ) )
21 8 20 mpanl2 
 |-  ( ( Fun C /\ ( dom recs ( F ) e. On /\ B e. dom recs ( F ) ) ) -> ( B e. dom recs ( F ) -> ( C ` B ) = ( F ` ( C |` B ) ) ) )
22 6 21 sylan 
 |-  ( ( dom recs ( F ) e. On /\ ( dom recs ( F ) e. On /\ B e. dom recs ( F ) ) ) -> ( B e. dom recs ( F ) -> ( C ` B ) = ( F ` ( C |` B ) ) ) )
23 22 exp32 
 |-  ( dom recs ( F ) e. On -> ( dom recs ( F ) e. On -> ( B e. dom recs ( F ) -> ( B e. dom recs ( F ) -> ( C ` B ) = ( F ` ( C |` B ) ) ) ) ) )
24 23 pm2.43i 
 |-  ( dom recs ( F ) e. On -> ( B e. dom recs ( F ) -> ( B e. dom recs ( F ) -> ( C ` B ) = ( F ` ( C |` B ) ) ) ) )
25 24 pm2.43d 
 |-  ( dom recs ( F ) e. On -> ( B e. dom recs ( F ) -> ( C ` B ) = ( F ` ( C |` B ) ) ) )
26 opex 
 |-  <. B , ( F ` ( C |` B ) ) >. e. _V
27 26 snid 
 |-  <. B , ( F ` ( C |` B ) ) >. e. { <. B , ( F ` ( C |` B ) ) >. }
28 opeq1 
 |-  ( B = dom recs ( F ) -> <. B , ( F ` ( C |` B ) ) >. = <. dom recs ( F ) , ( F ` ( C |` B ) ) >. )
29 28 adantl 
 |-  ( ( dom recs ( F ) e. On /\ B = dom recs ( F ) ) -> <. B , ( F ` ( C |` B ) ) >. = <. dom recs ( F ) , ( F ` ( C |` B ) ) >. )
30 eqimss 
 |-  ( B = dom recs ( F ) -> B C_ dom recs ( F ) )
31 8 15 mp3an2 
 |-  ( ( Fun C /\ B C_ dom recs ( F ) ) -> ( C |` B ) = ( recs ( F ) |` B ) )
32 6 30 31 syl2an 
 |-  ( ( dom recs ( F ) e. On /\ B = dom recs ( F ) ) -> ( C |` B ) = ( recs ( F ) |` B ) )
33 reseq2 
 |-  ( B = dom recs ( F ) -> ( recs ( F ) |` B ) = ( recs ( F ) |` dom recs ( F ) ) )
34 1 tfrlem6 
 |-  Rel recs ( F )
35 resdm 
 |-  ( Rel recs ( F ) -> ( recs ( F ) |` dom recs ( F ) ) = recs ( F ) )
36 34 35 ax-mp 
 |-  ( recs ( F ) |` dom recs ( F ) ) = recs ( F )
37 33 36 eqtrdi 
 |-  ( B = dom recs ( F ) -> ( recs ( F ) |` B ) = recs ( F ) )
38 37 adantl 
 |-  ( ( dom recs ( F ) e. On /\ B = dom recs ( F ) ) -> ( recs ( F ) |` B ) = recs ( F ) )
39 32 38 eqtrd 
 |-  ( ( dom recs ( F ) e. On /\ B = dom recs ( F ) ) -> ( C |` B ) = recs ( F ) )
40 39 fveq2d 
 |-  ( ( dom recs ( F ) e. On /\ B = dom recs ( F ) ) -> ( F ` ( C |` B ) ) = ( F ` recs ( F ) ) )
41 40 opeq2d 
 |-  ( ( dom recs ( F ) e. On /\ B = dom recs ( F ) ) -> <. dom recs ( F ) , ( F ` ( C |` B ) ) >. = <. dom recs ( F ) , ( F ` recs ( F ) ) >. )
42 29 41 eqtrd 
 |-  ( ( dom recs ( F ) e. On /\ B = dom recs ( F ) ) -> <. B , ( F ` ( C |` B ) ) >. = <. dom recs ( F ) , ( F ` recs ( F ) ) >. )
43 42 sneqd 
 |-  ( ( dom recs ( F ) e. On /\ B = dom recs ( F ) ) -> { <. B , ( F ` ( C |` B ) ) >. } = { <. dom recs ( F ) , ( F ` recs ( F ) ) >. } )
44 27 43 eleqtrid 
 |-  ( ( dom recs ( F ) e. On /\ B = dom recs ( F ) ) -> <. B , ( F ` ( C |` B ) ) >. e. { <. dom recs ( F ) , ( F ` recs ( F ) ) >. } )
45 elun2 
 |-  ( <. B , ( F ` ( C |` B ) ) >. e. { <. dom recs ( F ) , ( F ` recs ( F ) ) >. } -> <. B , ( F ` ( C |` B ) ) >. e. ( recs ( F ) u. { <. dom recs ( F ) , ( F ` recs ( F ) ) >. } ) )
46 44 45 syl 
 |-  ( ( dom recs ( F ) e. On /\ B = dom recs ( F ) ) -> <. B , ( F ` ( C |` B ) ) >. e. ( recs ( F ) u. { <. dom recs ( F ) , ( F ` recs ( F ) ) >. } ) )
47 46 2 eleqtrrdi 
 |-  ( ( dom recs ( F ) e. On /\ B = dom recs ( F ) ) -> <. B , ( F ` ( C |` B ) ) >. e. C )
48 simpr 
 |-  ( ( dom recs ( F ) e. On /\ B = dom recs ( F ) ) -> B = dom recs ( F ) )
49 sucidg 
 |-  ( dom recs ( F ) e. On -> dom recs ( F ) e. suc dom recs ( F ) )
50 49 adantr 
 |-  ( ( dom recs ( F ) e. On /\ B = dom recs ( F ) ) -> dom recs ( F ) e. suc dom recs ( F ) )
51 48 50 eqeltrd 
 |-  ( ( dom recs ( F ) e. On /\ B = dom recs ( F ) ) -> B e. suc dom recs ( F ) )
52 fnopfvb 
 |-  ( ( C Fn suc dom recs ( F ) /\ B e. suc dom recs ( F ) ) -> ( ( C ` B ) = ( F ` ( C |` B ) ) <-> <. B , ( F ` ( C |` B ) ) >. e. C ) )
53 4 51 52 syl2an2r 
 |-  ( ( dom recs ( F ) e. On /\ B = dom recs ( F ) ) -> ( ( C ` B ) = ( F ` ( C |` B ) ) <-> <. B , ( F ` ( C |` B ) ) >. e. C ) )
54 47 53 mpbird 
 |-  ( ( dom recs ( F ) e. On /\ B = dom recs ( F ) ) -> ( C ` B ) = ( F ` ( C |` B ) ) )
55 54 ex 
 |-  ( dom recs ( F ) e. On -> ( B = dom recs ( F ) -> ( C ` B ) = ( F ` ( C |` B ) ) ) )
56 25 55 jaod 
 |-  ( dom recs ( F ) e. On -> ( ( B e. dom recs ( F ) \/ B = dom recs ( F ) ) -> ( C ` B ) = ( F ` ( C |` B ) ) ) )
57 3 56 syl5 
 |-  ( dom recs ( F ) e. On -> ( B e. suc dom recs ( F ) -> ( C ` B ) = ( F ` ( C |` B ) ) ) )