Metamath Proof Explorer

Theorem tfr3

Description: Principle of Transfinite Recursion, part 3 of 3. Theorem 7.41(3) of TakeutiZaring p. 47. Finally, we show that F is unique. We do this by showing that any class B with the same properties of F that we showed in parts 1 and 2 is identical to F . (Contributed by NM, 18-Aug-1994) (Revised by Mario Carneiro, 9-May-2015)

Ref Expression
Hypothesis tfr.1 
|- F = recs ( G )
Assertion tfr3 
|- ( ( B Fn On /\ A. x e. On ( B ` x ) = ( G ` ( B |` x ) ) ) -> B = F )

Proof

Step Hyp Ref Expression
1 tfr.1 
 |-  F = recs ( G )
2 nfv 
 |-  F/ x B Fn On
3 nfra1 
 |-  F/ x A. x e. On ( B ` x ) = ( G ` ( B |` x ) )
4 2 3 nfan 
 |-  F/ x ( B Fn On /\ A. x e. On ( B ` x ) = ( G ` ( B |` x ) ) )
5 nfv 
 |-  F/ x ( B ` y ) = ( F ` y )
6 4 5 nfim 
 |-  F/ x ( ( B Fn On /\ A. x e. On ( B ` x ) = ( G ` ( B |` x ) ) ) -> ( B ` y ) = ( F ` y ) )
7 fveq2 
 |-  ( x = y -> ( B ` x ) = ( B ` y ) )
8 fveq2 
 |-  ( x = y -> ( F ` x ) = ( F ` y ) )
9 7 8 eqeq12d 
 |-  ( x = y -> ( ( B ` x ) = ( F ` x ) <-> ( B ` y ) = ( F ` y ) ) )
10 9 imbi2d 
 |-  ( x = y -> ( ( ( B Fn On /\ A. x e. On ( B ` x ) = ( G ` ( B |` x ) ) ) -> ( B ` x ) = ( F ` x ) ) <-> ( ( B Fn On /\ A. x e. On ( B ` x ) = ( G ` ( B |` x ) ) ) -> ( B ` y ) = ( F ` y ) ) ) )
11 r19.21v 
 |-  ( A. y e. x ( ( B Fn On /\ A. x e. On ( B ` x ) = ( G ` ( B |` x ) ) ) -> ( B ` y ) = ( F ` y ) ) <-> ( ( B Fn On /\ A. x e. On ( B ` x ) = ( G ` ( B |` x ) ) ) -> A. y e. x ( B ` y ) = ( F ` y ) ) )
12 rsp 
 |-  ( A. x e. On ( B ` x ) = ( G ` ( B |` x ) ) -> ( x e. On -> ( B ` x ) = ( G ` ( B |` x ) ) ) )
13 onss 
 |-  ( x e. On -> x C_ On )
14 1 tfr1 
 |-  F Fn On
15 fvreseq 
 |-  ( ( ( B Fn On /\ F Fn On ) /\ x C_ On ) -> ( ( B |` x ) = ( F |` x ) <-> A. y e. x ( B ` y ) = ( F ` y ) ) )
16 14 15 mpanl2 
 |-  ( ( B Fn On /\ x C_ On ) -> ( ( B |` x ) = ( F |` x ) <-> A. y e. x ( B ` y ) = ( F ` y ) ) )
17 fveq2 
 |-  ( ( B |` x ) = ( F |` x ) -> ( G ` ( B |` x ) ) = ( G ` ( F |` x ) ) )
18 16 17 biimtrrdi 
 |-  ( ( B Fn On /\ x C_ On ) -> ( A. y e. x ( B ` y ) = ( F ` y ) -> ( G ` ( B |` x ) ) = ( G ` ( F |` x ) ) ) )
19 13 18 sylan2 
 |-  ( ( B Fn On /\ x e. On ) -> ( A. y e. x ( B ` y ) = ( F ` y ) -> ( G ` ( B |` x ) ) = ( G ` ( F |` x ) ) ) )
20 19 ancoms 
 |-  ( ( x e. On /\ B Fn On ) -> ( A. y e. x ( B ` y ) = ( F ` y ) -> ( G ` ( B |` x ) ) = ( G ` ( F |` x ) ) ) )
21 20 imp 
 |-  ( ( ( x e. On /\ B Fn On ) /\ A. y e. x ( B ` y ) = ( F ` y ) ) -> ( G ` ( B |` x ) ) = ( G ` ( F |` x ) ) )
22 21 adantr 
 |-  ( ( ( ( x e. On /\ B Fn On ) /\ A. y e. x ( B ` y ) = ( F ` y ) ) /\ ( ( x e. On -> ( B ` x ) = ( G ` ( B |` x ) ) ) /\ x e. On ) ) -> ( G ` ( B |` x ) ) = ( G ` ( F |` x ) ) )
23 1 tfr2 
 |-  ( x e. On -> ( F ` x ) = ( G ` ( F |` x ) ) )
24 23 jctr 
 |-  ( ( x e. On -> ( B ` x ) = ( G ` ( B |` x ) ) ) -> ( ( x e. On -> ( B ` x ) = ( G ` ( B |` x ) ) ) /\ ( x e. On -> ( F ` x ) = ( G ` ( F |` x ) ) ) ) )
25 jcab 
 |-  ( ( x e. On -> ( ( B ` x ) = ( G ` ( B |` x ) ) /\ ( F ` x ) = ( G ` ( F |` x ) ) ) ) <-> ( ( x e. On -> ( B ` x ) = ( G ` ( B |` x ) ) ) /\ ( x e. On -> ( F ` x ) = ( G ` ( F |` x ) ) ) ) )
26 24 25 sylibr 
 |-  ( ( x e. On -> ( B ` x ) = ( G ` ( B |` x ) ) ) -> ( x e. On -> ( ( B ` x ) = ( G ` ( B |` x ) ) /\ ( F ` x ) = ( G ` ( F |` x ) ) ) ) )
27 eqeq12 
 |-  ( ( ( B ` x ) = ( G ` ( B |` x ) ) /\ ( F ` x ) = ( G ` ( F |` x ) ) ) -> ( ( B ` x ) = ( F ` x ) <-> ( G ` ( B |` x ) ) = ( G ` ( F |` x ) ) ) )
28 26 27 syl6 
 |-  ( ( x e. On -> ( B ` x ) = ( G ` ( B |` x ) ) ) -> ( x e. On -> ( ( B ` x ) = ( F ` x ) <-> ( G ` ( B |` x ) ) = ( G ` ( F |` x ) ) ) ) )
29 28 imp 
 |-  ( ( ( x e. On -> ( B ` x ) = ( G ` ( B |` x ) ) ) /\ x e. On ) -> ( ( B ` x ) = ( F ` x ) <-> ( G ` ( B |` x ) ) = ( G ` ( F |` x ) ) ) )
30 29 adantl 
 |-  ( ( ( ( x e. On /\ B Fn On ) /\ A. y e. x ( B ` y ) = ( F ` y ) ) /\ ( ( x e. On -> ( B ` x ) = ( G ` ( B |` x ) ) ) /\ x e. On ) ) -> ( ( B ` x ) = ( F ` x ) <-> ( G ` ( B |` x ) ) = ( G ` ( F |` x ) ) ) )
31 22 30 mpbird 
 |-  ( ( ( ( x e. On /\ B Fn On ) /\ A. y e. x ( B ` y ) = ( F ` y ) ) /\ ( ( x e. On -> ( B ` x ) = ( G ` ( B |` x ) ) ) /\ x e. On ) ) -> ( B ` x ) = ( F ` x ) )
32 31 exp43 
 |-  ( ( x e. On /\ B Fn On ) -> ( A. y e. x ( B ` y ) = ( F ` y ) -> ( ( x e. On -> ( B ` x ) = ( G ` ( B |` x ) ) ) -> ( x e. On -> ( B ` x ) = ( F ` x ) ) ) ) )
33 32 com4t 
 |-  ( ( x e. On -> ( B ` x ) = ( G ` ( B |` x ) ) ) -> ( x e. On -> ( ( x e. On /\ B Fn On ) -> ( A. y e. x ( B ` y ) = ( F ` y ) -> ( B ` x ) = ( F ` x ) ) ) ) )
34 33 exp4a 
 |-  ( ( x e. On -> ( B ` x ) = ( G ` ( B |` x ) ) ) -> ( x e. On -> ( x e. On -> ( B Fn On -> ( A. y e. x ( B ` y ) = ( F ` y ) -> ( B ` x ) = ( F ` x ) ) ) ) ) )
35 34 pm2.43d 
 |-  ( ( x e. On -> ( B ` x ) = ( G ` ( B |` x ) ) ) -> ( x e. On -> ( B Fn On -> ( A. y e. x ( B ` y ) = ( F ` y ) -> ( B ` x ) = ( F ` x ) ) ) ) )
36 12 35 syl 
 |-  ( A. x e. On ( B ` x ) = ( G ` ( B |` x ) ) -> ( x e. On -> ( B Fn On -> ( A. y e. x ( B ` y ) = ( F ` y ) -> ( B ` x ) = ( F ` x ) ) ) ) )
37 36 com3l 
 |-  ( x e. On -> ( B Fn On -> ( A. x e. On ( B ` x ) = ( G ` ( B |` x ) ) -> ( A. y e. x ( B ` y ) = ( F ` y ) -> ( B ` x ) = ( F ` x ) ) ) ) )
38 37 impd 
 |-  ( x e. On -> ( ( B Fn On /\ A. x e. On ( B ` x ) = ( G ` ( B |` x ) ) ) -> ( A. y e. x ( B ` y ) = ( F ` y ) -> ( B ` x ) = ( F ` x ) ) ) )
39 38 a2d 
 |-  ( x e. On -> ( ( ( B Fn On /\ A. x e. On ( B ` x ) = ( G ` ( B |` x ) ) ) -> A. y e. x ( B ` y ) = ( F ` y ) ) -> ( ( B Fn On /\ A. x e. On ( B ` x ) = ( G ` ( B |` x ) ) ) -> ( B ` x ) = ( F ` x ) ) ) )
40 11 39 biimtrid 
 |-  ( x e. On -> ( A. y e. x ( ( B Fn On /\ A. x e. On ( B ` x ) = ( G ` ( B |` x ) ) ) -> ( B ` y ) = ( F ` y ) ) -> ( ( B Fn On /\ A. x e. On ( B ` x ) = ( G ` ( B |` x ) ) ) -> ( B ` x ) = ( F ` x ) ) ) )
41 6 10 40 tfis2f 
 |-  ( x e. On -> ( ( B Fn On /\ A. x e. On ( B ` x ) = ( G ` ( B |` x ) ) ) -> ( B ` x ) = ( F ` x ) ) )
42 41 com12 
 |-  ( ( B Fn On /\ A. x e. On ( B ` x ) = ( G ` ( B |` x ) ) ) -> ( x e. On -> ( B ` x ) = ( F ` x ) ) )
43 4 42 ralrimi 
 |-  ( ( B Fn On /\ A. x e. On ( B ` x ) = ( G ` ( B |` x ) ) ) -> A. x e. On ( B ` x ) = ( F ` x ) )
44 eqfnfv 
 |-  ( ( B Fn On /\ F Fn On ) -> ( B = F <-> A. x e. On ( B ` x ) = ( F ` x ) ) )
45 14 44 mpan2 
 |-  ( B Fn On -> ( B = F <-> A. x e. On ( B ` x ) = ( F ` x ) ) )
46 45 biimpar 
 |-  ( ( B Fn On /\ A. x e. On ( B ` x ) = ( F ` x ) ) -> B = F )
47 43 46 syldan 
 |-  ( ( B Fn On /\ A. x e. On ( B ` x ) = ( G ` ( B |` x ) ) ) -> B = F )