Metamath Proof Explorer

Theorem tfrlem5

Description: Lemma for transfinite recursion. The values of two acceptable functions are the same within their domains. (Contributed by NM, 9-Apr-1995) (Revised by Mario Carneiro, 24-May-2019)

Ref Expression
Hypothesis tfrlem.1 
|- A = { f | E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) ) }
Assertion tfrlem5 
|- ( ( g e. A /\ h e. A ) -> ( ( x g u /\ x h v ) -> u = v ) )

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 vex 
 |-  g e. _V
3 1 2 tfrlem3a 
 |-  ( g e. A <-> E. z e. On ( g Fn z /\ A. a e. z ( g ` a ) = ( F ` ( g |` a ) ) ) )
4 vex 
 |-  h e. _V
5 1 4 tfrlem3a 
 |-  ( h e. A <-> E. w e. On ( h Fn w /\ A. a e. w ( h ` a ) = ( F ` ( h |` a ) ) ) )
6 reeanv 
 |-  ( E. z e. On E. w e. On ( ( g Fn z /\ A. a e. z ( g ` a ) = ( F ` ( g |` a ) ) ) /\ ( h Fn w /\ A. a e. w ( h ` a ) = ( F ` ( h |` a ) ) ) ) <-> ( E. z e. On ( g Fn z /\ A. a e. z ( g ` a ) = ( F ` ( g |` a ) ) ) /\ E. w e. On ( h Fn w /\ A. a e. w ( h ` a ) = ( F ` ( h |` a ) ) ) ) )
7 fveq2 
 |-  ( a = x -> ( g ` a ) = ( g ` x ) )
8 fveq2 
 |-  ( a = x -> ( h ` a ) = ( h ` x ) )
9 7 8 eqeq12d 
 |-  ( a = x -> ( ( g ` a ) = ( h ` a ) <-> ( g ` x ) = ( h ` x ) ) )
10 onin 
 |-  ( ( z e. On /\ w e. On ) -> ( z i^i w ) e. On )
11 10 3ad2ant1 
 |-  ( ( ( z e. On /\ w e. On ) /\ ( ( g Fn z /\ A. a e. z ( g ` a ) = ( F ` ( g |` a ) ) ) /\ ( h Fn w /\ A. a e. w ( h ` a ) = ( F ` ( h |` a ) ) ) ) /\ ( x g u /\ x h v ) ) -> ( z i^i w ) e. On )
12 simp2ll 
 |-  ( ( ( z e. On /\ w e. On ) /\ ( ( g Fn z /\ A. a e. z ( g ` a ) = ( F ` ( g |` a ) ) ) /\ ( h Fn w /\ A. a e. w ( h ` a ) = ( F ` ( h |` a ) ) ) ) /\ ( x g u /\ x h v ) ) -> g Fn z )
13 fnfun 
 |-  ( g Fn z -> Fun g )
14 12 13 syl 
 |-  ( ( ( z e. On /\ w e. On ) /\ ( ( g Fn z /\ A. a e. z ( g ` a ) = ( F ` ( g |` a ) ) ) /\ ( h Fn w /\ A. a e. w ( h ` a ) = ( F ` ( h |` a ) ) ) ) /\ ( x g u /\ x h v ) ) -> Fun g )
15 inss1 
 |-  ( z i^i w ) C_ z
16 12 fndmd 
 |-  ( ( ( z e. On /\ w e. On ) /\ ( ( g Fn z /\ A. a e. z ( g ` a ) = ( F ` ( g |` a ) ) ) /\ ( h Fn w /\ A. a e. w ( h ` a ) = ( F ` ( h |` a ) ) ) ) /\ ( x g u /\ x h v ) ) -> dom g = z )
17 15 16 sseqtrrid 
 |-  ( ( ( z e. On /\ w e. On ) /\ ( ( g Fn z /\ A. a e. z ( g ` a ) = ( F ` ( g |` a ) ) ) /\ ( h Fn w /\ A. a e. w ( h ` a ) = ( F ` ( h |` a ) ) ) ) /\ ( x g u /\ x h v ) ) -> ( z i^i w ) C_ dom g )
18 14 17 jca 
 |-  ( ( ( z e. On /\ w e. On ) /\ ( ( g Fn z /\ A. a e. z ( g ` a ) = ( F ` ( g |` a ) ) ) /\ ( h Fn w /\ A. a e. w ( h ` a ) = ( F ` ( h |` a ) ) ) ) /\ ( x g u /\ x h v ) ) -> ( Fun g /\ ( z i^i w ) C_ dom g ) )
19 simp2rl 
 |-  ( ( ( z e. On /\ w e. On ) /\ ( ( g Fn z /\ A. a e. z ( g ` a ) = ( F ` ( g |` a ) ) ) /\ ( h Fn w /\ A. a e. w ( h ` a ) = ( F ` ( h |` a ) ) ) ) /\ ( x g u /\ x h v ) ) -> h Fn w )
20 fnfun 
 |-  ( h Fn w -> Fun h )
21 19 20 syl 
 |-  ( ( ( z e. On /\ w e. On ) /\ ( ( g Fn z /\ A. a e. z ( g ` a ) = ( F ` ( g |` a ) ) ) /\ ( h Fn w /\ A. a e. w ( h ` a ) = ( F ` ( h |` a ) ) ) ) /\ ( x g u /\ x h v ) ) -> Fun h )
22 inss2 
 |-  ( z i^i w ) C_ w
23 19 fndmd 
 |-  ( ( ( z e. On /\ w e. On ) /\ ( ( g Fn z /\ A. a e. z ( g ` a ) = ( F ` ( g |` a ) ) ) /\ ( h Fn w /\ A. a e. w ( h ` a ) = ( F ` ( h |` a ) ) ) ) /\ ( x g u /\ x h v ) ) -> dom h = w )
24 22 23 sseqtrrid 
 |-  ( ( ( z e. On /\ w e. On ) /\ ( ( g Fn z /\ A. a e. z ( g ` a ) = ( F ` ( g |` a ) ) ) /\ ( h Fn w /\ A. a e. w ( h ` a ) = ( F ` ( h |` a ) ) ) ) /\ ( x g u /\ x h v ) ) -> ( z i^i w ) C_ dom h )
25 21 24 jca 
 |-  ( ( ( z e. On /\ w e. On ) /\ ( ( g Fn z /\ A. a e. z ( g ` a ) = ( F ` ( g |` a ) ) ) /\ ( h Fn w /\ A. a e. w ( h ` a ) = ( F ` ( h |` a ) ) ) ) /\ ( x g u /\ x h v ) ) -> ( Fun h /\ ( z i^i w ) C_ dom h ) )
26 simp2lr 
 |-  ( ( ( z e. On /\ w e. On ) /\ ( ( g Fn z /\ A. a e. z ( g ` a ) = ( F ` ( g |` a ) ) ) /\ ( h Fn w /\ A. a e. w ( h ` a ) = ( F ` ( h |` a ) ) ) ) /\ ( x g u /\ x h v ) ) -> A. a e. z ( g ` a ) = ( F ` ( g |` a ) ) )
27 ssralv 
 |-  ( ( z i^i w ) C_ z -> ( A. a e. z ( g ` a ) = ( F ` ( g |` a ) ) -> A. a e. ( z i^i w ) ( g ` a ) = ( F ` ( g |` a ) ) ) )
28 15 26 27 mpsyl 
 |-  ( ( ( z e. On /\ w e. On ) /\ ( ( g Fn z /\ A. a e. z ( g ` a ) = ( F ` ( g |` a ) ) ) /\ ( h Fn w /\ A. a e. w ( h ` a ) = ( F ` ( h |` a ) ) ) ) /\ ( x g u /\ x h v ) ) -> A. a e. ( z i^i w ) ( g ` a ) = ( F ` ( g |` a ) ) )
29 simp2rr 
 |-  ( ( ( z e. On /\ w e. On ) /\ ( ( g Fn z /\ A. a e. z ( g ` a ) = ( F ` ( g |` a ) ) ) /\ ( h Fn w /\ A. a e. w ( h ` a ) = ( F ` ( h |` a ) ) ) ) /\ ( x g u /\ x h v ) ) -> A. a e. w ( h ` a ) = ( F ` ( h |` a ) ) )
30 ssralv 
 |-  ( ( z i^i w ) C_ w -> ( A. a e. w ( h ` a ) = ( F ` ( h |` a ) ) -> A. a e. ( z i^i w ) ( h ` a ) = ( F ` ( h |` a ) ) ) )
31 22 29 30 mpsyl 
 |-  ( ( ( z e. On /\ w e. On ) /\ ( ( g Fn z /\ A. a e. z ( g ` a ) = ( F ` ( g |` a ) ) ) /\ ( h Fn w /\ A. a e. w ( h ` a ) = ( F ` ( h |` a ) ) ) ) /\ ( x g u /\ x h v ) ) -> A. a e. ( z i^i w ) ( h ` a ) = ( F ` ( h |` a ) ) )
32 11 18 25 28 31 tfrlem1 
 |-  ( ( ( z e. On /\ w e. On ) /\ ( ( g Fn z /\ A. a e. z ( g ` a ) = ( F ` ( g |` a ) ) ) /\ ( h Fn w /\ A. a e. w ( h ` a ) = ( F ` ( h |` a ) ) ) ) /\ ( x g u /\ x h v ) ) -> A. a e. ( z i^i w ) ( g ` a ) = ( h ` a ) )
33 simp3l 
 |-  ( ( ( z e. On /\ w e. On ) /\ ( ( g Fn z /\ A. a e. z ( g ` a ) = ( F ` ( g |` a ) ) ) /\ ( h Fn w /\ A. a e. w ( h ` a ) = ( F ` ( h |` a ) ) ) ) /\ ( x g u /\ x h v ) ) -> x g u )
34 fnbr 
 |-  ( ( g Fn z /\ x g u ) -> x e. z )
35 12 33 34 syl2anc 
 |-  ( ( ( z e. On /\ w e. On ) /\ ( ( g Fn z /\ A. a e. z ( g ` a ) = ( F ` ( g |` a ) ) ) /\ ( h Fn w /\ A. a e. w ( h ` a ) = ( F ` ( h |` a ) ) ) ) /\ ( x g u /\ x h v ) ) -> x e. z )
36 simp3r 
 |-  ( ( ( z e. On /\ w e. On ) /\ ( ( g Fn z /\ A. a e. z ( g ` a ) = ( F ` ( g |` a ) ) ) /\ ( h Fn w /\ A. a e. w ( h ` a ) = ( F ` ( h |` a ) ) ) ) /\ ( x g u /\ x h v ) ) -> x h v )
37 fnbr 
 |-  ( ( h Fn w /\ x h v ) -> x e. w )
38 19 36 37 syl2anc 
 |-  ( ( ( z e. On /\ w e. On ) /\ ( ( g Fn z /\ A. a e. z ( g ` a ) = ( F ` ( g |` a ) ) ) /\ ( h Fn w /\ A. a e. w ( h ` a ) = ( F ` ( h |` a ) ) ) ) /\ ( x g u /\ x h v ) ) -> x e. w )
39 35 38 elind 
 |-  ( ( ( z e. On /\ w e. On ) /\ ( ( g Fn z /\ A. a e. z ( g ` a ) = ( F ` ( g |` a ) ) ) /\ ( h Fn w /\ A. a e. w ( h ` a ) = ( F ` ( h |` a ) ) ) ) /\ ( x g u /\ x h v ) ) -> x e. ( z i^i w ) )
40 9 32 39 rspcdva 
 |-  ( ( ( z e. On /\ w e. On ) /\ ( ( g Fn z /\ A. a e. z ( g ` a ) = ( F ` ( g |` a ) ) ) /\ ( h Fn w /\ A. a e. w ( h ` a ) = ( F ` ( h |` a ) ) ) ) /\ ( x g u /\ x h v ) ) -> ( g ` x ) = ( h ` x ) )
41 funbrfv 
 |-  ( Fun g -> ( x g u -> ( g ` x ) = u ) )
42 14 33 41 sylc 
 |-  ( ( ( z e. On /\ w e. On ) /\ ( ( g Fn z /\ A. a e. z ( g ` a ) = ( F ` ( g |` a ) ) ) /\ ( h Fn w /\ A. a e. w ( h ` a ) = ( F ` ( h |` a ) ) ) ) /\ ( x g u /\ x h v ) ) -> ( g ` x ) = u )
43 funbrfv 
 |-  ( Fun h -> ( x h v -> ( h ` x ) = v ) )
44 21 36 43 sylc 
 |-  ( ( ( z e. On /\ w e. On ) /\ ( ( g Fn z /\ A. a e. z ( g ` a ) = ( F ` ( g |` a ) ) ) /\ ( h Fn w /\ A. a e. w ( h ` a ) = ( F ` ( h |` a ) ) ) ) /\ ( x g u /\ x h v ) ) -> ( h ` x ) = v )
45 40 42 44 3eqtr3d 
 |-  ( ( ( z e. On /\ w e. On ) /\ ( ( g Fn z /\ A. a e. z ( g ` a ) = ( F ` ( g |` a ) ) ) /\ ( h Fn w /\ A. a e. w ( h ` a ) = ( F ` ( h |` a ) ) ) ) /\ ( x g u /\ x h v ) ) -> u = v )
46 45 3exp 
 |-  ( ( z e. On /\ w e. On ) -> ( ( ( g Fn z /\ A. a e. z ( g ` a ) = ( F ` ( g |` a ) ) ) /\ ( h Fn w /\ A. a e. w ( h ` a ) = ( F ` ( h |` a ) ) ) ) -> ( ( x g u /\ x h v ) -> u = v ) ) )
47 46 rexlimivv 
 |-  ( E. z e. On E. w e. On ( ( g Fn z /\ A. a e. z ( g ` a ) = ( F ` ( g |` a ) ) ) /\ ( h Fn w /\ A. a e. w ( h ` a ) = ( F ` ( h |` a ) ) ) ) -> ( ( x g u /\ x h v ) -> u = v ) )
48 6 47 sylbir 
 |-  ( ( E. z e. On ( g Fn z /\ A. a e. z ( g ` a ) = ( F ` ( g |` a ) ) ) /\ E. w e. On ( h Fn w /\ A. a e. w ( h ` a ) = ( F ` ( h |` a ) ) ) ) -> ( ( x g u /\ x h v ) -> u = v ) )
49 3 5 48 syl2anb 
 |-  ( ( g e. A /\ h e. A ) -> ( ( x g u /\ x h v ) -> u = v ) )