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