Metamath Proof Explorer

Theorem frr3g

Description: Functions defined by well-founded recursion are identical up to relation, domain, and characteristic function. General version of frr3 . (Contributed by Scott Fenton, 10-Feb-2011) (Revised by Mario Carneiro, 26-Jun-2015)

Ref Expression
Assertion frr3g 
|- ( ( ( R Fr A /\ R Se A ) /\ ( F Fn A /\ A. y e. A ( F ` y ) = ( y H ( F |` Pred ( R , A , y ) ) ) ) /\ ( G Fn A /\ A. y e. A ( G ` y ) = ( y H ( G |` Pred ( R , A , y ) ) ) ) ) -> F = G )

Proof

Step Hyp Ref Expression
1 ra4v 
 |-  ( A. w e. Pred ( R , A , z ) ( ( ( F Fn A /\ G Fn A ) /\ ( A. y e. A ( F ` y ) = ( y H ( F |` Pred ( R , A , y ) ) ) /\ A. y e. A ( G ` y ) = ( y H ( G |` Pred ( R , A , y ) ) ) ) ) -> ( F ` w ) = ( G ` w ) ) -> ( ( ( F Fn A /\ G Fn A ) /\ ( A. y e. A ( F ` y ) = ( y H ( F |` Pred ( R , A , y ) ) ) /\ A. y e. A ( G ` y ) = ( y H ( G |` Pred ( R , A , y ) ) ) ) ) -> A. w e. Pred ( R , A , z ) ( F ` w ) = ( G ` w ) ) )
2 r19.26 
 |-  ( A. y e. A ( ( F ` y ) = ( y H ( F |` Pred ( R , A , y ) ) ) /\ ( G ` y ) = ( y H ( G |` Pred ( R , A , y ) ) ) ) <-> ( A. y e. A ( F ` y ) = ( y H ( F |` Pred ( R , A , y ) ) ) /\ A. y e. A ( G ` y ) = ( y H ( G |` Pred ( R , A , y ) ) ) ) )
3 2 anbi2i 
 |-  ( ( ( F Fn A /\ G Fn A ) /\ A. y e. A ( ( F ` y ) = ( y H ( F |` Pred ( R , A , y ) ) ) /\ ( G ` y ) = ( y H ( G |` Pred ( R , A , y ) ) ) ) ) <-> ( ( F Fn A /\ G Fn A ) /\ ( A. y e. A ( F ` y ) = ( y H ( F |` Pred ( R , A , y ) ) ) /\ A. y e. A ( G ` y ) = ( y H ( G |` Pred ( R , A , y ) ) ) ) ) )
4 fveq2 
 |-  ( y = z -> ( F ` y ) = ( F ` z ) )
5 id 
 |-  ( y = z -> y = z )
6 predeq3 
 |-  ( y = z -> Pred ( R , A , y ) = Pred ( R , A , z ) )
7 6 reseq2d 
 |-  ( y = z -> ( F |` Pred ( R , A , y ) ) = ( F |` Pred ( R , A , z ) ) )
8 5 7 oveq12d 
 |-  ( y = z -> ( y H ( F |` Pred ( R , A , y ) ) ) = ( z H ( F |` Pred ( R , A , z ) ) ) )
9 4 8 eqeq12d 
 |-  ( y = z -> ( ( F ` y ) = ( y H ( F |` Pred ( R , A , y ) ) ) <-> ( F ` z ) = ( z H ( F |` Pred ( R , A , z ) ) ) ) )
10 fveq2 
 |-  ( y = z -> ( G ` y ) = ( G ` z ) )
11 6 reseq2d 
 |-  ( y = z -> ( G |` Pred ( R , A , y ) ) = ( G |` Pred ( R , A , z ) ) )
12 5 11 oveq12d 
 |-  ( y = z -> ( y H ( G |` Pred ( R , A , y ) ) ) = ( z H ( G |` Pred ( R , A , z ) ) ) )
13 10 12 eqeq12d 
 |-  ( y = z -> ( ( G ` y ) = ( y H ( G |` Pred ( R , A , y ) ) ) <-> ( G ` z ) = ( z H ( G |` Pred ( R , A , z ) ) ) ) )
14 9 13 anbi12d 
 |-  ( y = z -> ( ( ( F ` y ) = ( y H ( F |` Pred ( R , A , y ) ) ) /\ ( G ` y ) = ( y H ( G |` Pred ( R , A , y ) ) ) ) <-> ( ( F ` z ) = ( z H ( F |` Pred ( R , A , z ) ) ) /\ ( G ` z ) = ( z H ( G |` Pred ( R , A , z ) ) ) ) ) )
15 14 rspcva 
 |-  ( ( z e. A /\ A. y e. A ( ( F ` y ) = ( y H ( F |` Pred ( R , A , y ) ) ) /\ ( G ` y ) = ( y H ( G |` Pred ( R , A , y ) ) ) ) ) -> ( ( F ` z ) = ( z H ( F |` Pred ( R , A , z ) ) ) /\ ( G ` z ) = ( z H ( G |` Pred ( R , A , z ) ) ) ) )
16 eqtr3 
 |-  ( ( ( z H ( G |` Pred ( R , A , z ) ) ) = ( z H ( F |` Pred ( R , A , z ) ) ) /\ ( F ` z ) = ( z H ( F |` Pred ( R , A , z ) ) ) ) -> ( z H ( G |` Pred ( R , A , z ) ) ) = ( F ` z ) )
17 16 eqcomd 
 |-  ( ( ( z H ( G |` Pred ( R , A , z ) ) ) = ( z H ( F |` Pred ( R , A , z ) ) ) /\ ( F ` z ) = ( z H ( F |` Pred ( R , A , z ) ) ) ) -> ( F ` z ) = ( z H ( G |` Pred ( R , A , z ) ) ) )
18 eqtr3 
 |-  ( ( ( F ` z ) = ( z H ( G |` Pred ( R , A , z ) ) ) /\ ( G ` z ) = ( z H ( G |` Pred ( R , A , z ) ) ) ) -> ( F ` z ) = ( G ` z ) )
19 18 ex 
 |-  ( ( F ` z ) = ( z H ( G |` Pred ( R , A , z ) ) ) -> ( ( G ` z ) = ( z H ( G |` Pred ( R , A , z ) ) ) -> ( F ` z ) = ( G ` z ) ) )
20 17 19 syl 
 |-  ( ( ( z H ( G |` Pred ( R , A , z ) ) ) = ( z H ( F |` Pred ( R , A , z ) ) ) /\ ( F ` z ) = ( z H ( F |` Pred ( R , A , z ) ) ) ) -> ( ( G ` z ) = ( z H ( G |` Pred ( R , A , z ) ) ) -> ( F ` z ) = ( G ` z ) ) )
21 20 expimpd 
 |-  ( ( z H ( G |` Pred ( R , A , z ) ) ) = ( z H ( F |` Pred ( R , A , z ) ) ) -> ( ( ( F ` z ) = ( z H ( F |` Pred ( R , A , z ) ) ) /\ ( G ` z ) = ( z H ( G |` Pred ( R , A , z ) ) ) ) -> ( F ` z ) = ( G ` z ) ) )
22 predss 
 |-  Pred ( R , A , z ) C_ A
23 fvreseq 
 |-  ( ( ( F Fn A /\ G Fn A ) /\ Pred ( R , A , z ) C_ A ) -> ( ( F |` Pred ( R , A , z ) ) = ( G |` Pred ( R , A , z ) ) <-> A. w e. Pred ( R , A , z ) ( F ` w ) = ( G ` w ) ) )
24 22 23 mpan2 
 |-  ( ( F Fn A /\ G Fn A ) -> ( ( F |` Pred ( R , A , z ) ) = ( G |` Pred ( R , A , z ) ) <-> A. w e. Pred ( R , A , z ) ( F ` w ) = ( G ` w ) ) )
25 24 biimpar 
 |-  ( ( ( F Fn A /\ G Fn A ) /\ A. w e. Pred ( R , A , z ) ( F ` w ) = ( G ` w ) ) -> ( F |` Pred ( R , A , z ) ) = ( G |` Pred ( R , A , z ) ) )
26 25 oveq2d 
 |-  ( ( ( F Fn A /\ G Fn A ) /\ A. w e. Pred ( R , A , z ) ( F ` w ) = ( G ` w ) ) -> ( z H ( F |` Pred ( R , A , z ) ) ) = ( z H ( G |` Pred ( R , A , z ) ) ) )
27 26 eqcomd 
 |-  ( ( ( F Fn A /\ G Fn A ) /\ A. w e. Pred ( R , A , z ) ( F ` w ) = ( G ` w ) ) -> ( z H ( G |` Pred ( R , A , z ) ) ) = ( z H ( F |` Pred ( R , A , z ) ) ) )
28 21 27 syl11 
 |-  ( ( ( F ` z ) = ( z H ( F |` Pred ( R , A , z ) ) ) /\ ( G ` z ) = ( z H ( G |` Pred ( R , A , z ) ) ) ) -> ( ( ( F Fn A /\ G Fn A ) /\ A. w e. Pred ( R , A , z ) ( F ` w ) = ( G ` w ) ) -> ( F ` z ) = ( G ` z ) ) )
29 28 expd 
 |-  ( ( ( F ` z ) = ( z H ( F |` Pred ( R , A , z ) ) ) /\ ( G ` z ) = ( z H ( G |` Pred ( R , A , z ) ) ) ) -> ( ( F Fn A /\ G Fn A ) -> ( A. w e. Pred ( R , A , z ) ( F ` w ) = ( G ` w ) -> ( F ` z ) = ( G ` z ) ) ) )
30 15 29 syl 
 |-  ( ( z e. A /\ A. y e. A ( ( F ` y ) = ( y H ( F |` Pred ( R , A , y ) ) ) /\ ( G ` y ) = ( y H ( G |` Pred ( R , A , y ) ) ) ) ) -> ( ( F Fn A /\ G Fn A ) -> ( A. w e. Pred ( R , A , z ) ( F ` w ) = ( G ` w ) -> ( F ` z ) = ( G ` z ) ) ) )
31 30 ex 
 |-  ( z e. A -> ( A. y e. A ( ( F ` y ) = ( y H ( F |` Pred ( R , A , y ) ) ) /\ ( G ` y ) = ( y H ( G |` Pred ( R , A , y ) ) ) ) -> ( ( F Fn A /\ G Fn A ) -> ( A. w e. Pred ( R , A , z ) ( F ` w ) = ( G ` w ) -> ( F ` z ) = ( G ` z ) ) ) ) )
32 31 com23 
 |-  ( z e. A -> ( ( F Fn A /\ G Fn A ) -> ( A. y e. A ( ( F ` y ) = ( y H ( F |` Pred ( R , A , y ) ) ) /\ ( G ` y ) = ( y H ( G |` Pred ( R , A , y ) ) ) ) -> ( A. w e. Pred ( R , A , z ) ( F ` w ) = ( G ` w ) -> ( F ` z ) = ( G ` z ) ) ) ) )
33 32 impd 
 |-  ( z e. A -> ( ( ( F Fn A /\ G Fn A ) /\ A. y e. A ( ( F ` y ) = ( y H ( F |` Pred ( R , A , y ) ) ) /\ ( G ` y ) = ( y H ( G |` Pred ( R , A , y ) ) ) ) ) -> ( A. w e. Pred ( R , A , z ) ( F ` w ) = ( G ` w ) -> ( F ` z ) = ( G ` z ) ) ) )
34 3 33 syl5bir 
 |-  ( z e. A -> ( ( ( F Fn A /\ G Fn A ) /\ ( A. y e. A ( F ` y ) = ( y H ( F |` Pred ( R , A , y ) ) ) /\ A. y e. A ( G ` y ) = ( y H ( G |` Pred ( R , A , y ) ) ) ) ) -> ( A. w e. Pred ( R , A , z ) ( F ` w ) = ( G ` w ) -> ( F ` z ) = ( G ` z ) ) ) )
35 34 a2d 
 |-  ( z e. A -> ( ( ( ( F Fn A /\ G Fn A ) /\ ( A. y e. A ( F ` y ) = ( y H ( F |` Pred ( R , A , y ) ) ) /\ A. y e. A ( G ` y ) = ( y H ( G |` Pred ( R , A , y ) ) ) ) ) -> A. w e. Pred ( R , A , z ) ( F ` w ) = ( G ` w ) ) -> ( ( ( F Fn A /\ G Fn A ) /\ ( A. y e. A ( F ` y ) = ( y H ( F |` Pred ( R , A , y ) ) ) /\ A. y e. A ( G ` y ) = ( y H ( G |` Pred ( R , A , y ) ) ) ) ) -> ( F ` z ) = ( G ` z ) ) ) )
36 1 35 syl5 
 |-  ( z e. A -> ( A. w e. Pred ( R , A , z ) ( ( ( F Fn A /\ G Fn A ) /\ ( A. y e. A ( F ` y ) = ( y H ( F |` Pred ( R , A , y ) ) ) /\ A. y e. A ( G ` y ) = ( y H ( G |` Pred ( R , A , y ) ) ) ) ) -> ( F ` w ) = ( G ` w ) ) -> ( ( ( F Fn A /\ G Fn A ) /\ ( A. y e. A ( F ` y ) = ( y H ( F |` Pred ( R , A , y ) ) ) /\ A. y e. A ( G ` y ) = ( y H ( G |` Pred ( R , A , y ) ) ) ) ) -> ( F ` z ) = ( G ` z ) ) ) )
37 fveq2 
 |-  ( z = w -> ( F ` z ) = ( F ` w ) )
38 fveq2 
 |-  ( z = w -> ( G ` z ) = ( G ` w ) )
39 37 38 eqeq12d 
 |-  ( z = w -> ( ( F ` z ) = ( G ` z ) <-> ( F ` w ) = ( G ` w ) ) )
40 39 imbi2d 
 |-  ( z = w -> ( ( ( ( F Fn A /\ G Fn A ) /\ ( A. y e. A ( F ` y ) = ( y H ( F |` Pred ( R , A , y ) ) ) /\ A. y e. A ( G ` y ) = ( y H ( G |` Pred ( R , A , y ) ) ) ) ) -> ( F ` z ) = ( G ` z ) ) <-> ( ( ( F Fn A /\ G Fn A ) /\ ( A. y e. A ( F ` y ) = ( y H ( F |` Pred ( R , A , y ) ) ) /\ A. y e. A ( G ` y ) = ( y H ( G |` Pred ( R , A , y ) ) ) ) ) -> ( F ` w ) = ( G ` w ) ) ) )
41 36 40 frins2 
 |-  ( ( R Fr A /\ R Se A ) -> A. z e. A ( ( ( F Fn A /\ G Fn A ) /\ ( A. y e. A ( F ` y ) = ( y H ( F |` Pred ( R , A , y ) ) ) /\ A. y e. A ( G ` y ) = ( y H ( G |` Pred ( R , A , y ) ) ) ) ) -> ( F ` z ) = ( G ` z ) ) )
42 rsp 
 |-  ( A. z e. A ( ( ( F Fn A /\ G Fn A ) /\ ( A. y e. A ( F ` y ) = ( y H ( F |` Pred ( R , A , y ) ) ) /\ A. y e. A ( G ` y ) = ( y H ( G |` Pred ( R , A , y ) ) ) ) ) -> ( F ` z ) = ( G ` z ) ) -> ( z e. A -> ( ( ( F Fn A /\ G Fn A ) /\ ( A. y e. A ( F ` y ) = ( y H ( F |` Pred ( R , A , y ) ) ) /\ A. y e. A ( G ` y ) = ( y H ( G |` Pred ( R , A , y ) ) ) ) ) -> ( F ` z ) = ( G ` z ) ) ) )
43 41 42 syl 
 |-  ( ( R Fr A /\ R Se A ) -> ( z e. A -> ( ( ( F Fn A /\ G Fn A ) /\ ( A. y e. A ( F ` y ) = ( y H ( F |` Pred ( R , A , y ) ) ) /\ A. y e. A ( G ` y ) = ( y H ( G |` Pred ( R , A , y ) ) ) ) ) -> ( F ` z ) = ( G ` z ) ) ) )
44 43 com3r 
 |-  ( ( ( F Fn A /\ G Fn A ) /\ ( A. y e. A ( F ` y ) = ( y H ( F |` Pred ( R , A , y ) ) ) /\ A. y e. A ( G ` y ) = ( y H ( G |` Pred ( R , A , y ) ) ) ) ) -> ( ( R Fr A /\ R Se A ) -> ( z e. A -> ( F ` z ) = ( G ` z ) ) ) )
45 44 an4s 
 |-  ( ( ( F Fn A /\ A. y e. A ( F ` y ) = ( y H ( F |` Pred ( R , A , y ) ) ) ) /\ ( G Fn A /\ A. y e. A ( G ` y ) = ( y H ( G |` Pred ( R , A , y ) ) ) ) ) -> ( ( R Fr A /\ R Se A ) -> ( z e. A -> ( F ` z ) = ( G ` z ) ) ) )
46 45 com12 
 |-  ( ( R Fr A /\ R Se A ) -> ( ( ( F Fn A /\ A. y e. A ( F ` y ) = ( y H ( F |` Pred ( R , A , y ) ) ) ) /\ ( G Fn A /\ A. y e. A ( G ` y ) = ( y H ( G |` Pred ( R , A , y ) ) ) ) ) -> ( z e. A -> ( F ` z ) = ( G ` z ) ) ) )
47 46 3impib 
 |-  ( ( ( R Fr A /\ R Se A ) /\ ( F Fn A /\ A. y e. A ( F ` y ) = ( y H ( F |` Pred ( R , A , y ) ) ) ) /\ ( G Fn A /\ A. y e. A ( G ` y ) = ( y H ( G |` Pred ( R , A , y ) ) ) ) ) -> ( z e. A -> ( F ` z ) = ( G ` z ) ) )
48 47 ralrimiv 
 |-  ( ( ( R Fr A /\ R Se A ) /\ ( F Fn A /\ A. y e. A ( F ` y ) = ( y H ( F |` Pred ( R , A , y ) ) ) ) /\ ( G Fn A /\ A. y e. A ( G ` y ) = ( y H ( G |` Pred ( R , A , y ) ) ) ) ) -> A. z e. A ( F ` z ) = ( G ` z ) )
49 eqid 
 |-  A = A
50 48 49 jctil 
 |-  ( ( ( R Fr A /\ R Se A ) /\ ( F Fn A /\ A. y e. A ( F ` y ) = ( y H ( F |` Pred ( R , A , y ) ) ) ) /\ ( G Fn A /\ A. y e. A ( G ` y ) = ( y H ( G |` Pred ( R , A , y ) ) ) ) ) -> ( A = A /\ A. z e. A ( F ` z ) = ( G ` z ) ) )
51 eqfnfv2 
 |-  ( ( F Fn A /\ G Fn A ) -> ( F = G <-> ( A = A /\ A. z e. A ( F ` z ) = ( G ` z ) ) ) )
52 51 ad2ant2r 
 |-  ( ( ( F Fn A /\ A. y e. A ( F ` y ) = ( y H ( F |` Pred ( R , A , y ) ) ) ) /\ ( G Fn A /\ A. y e. A ( G ` y ) = ( y H ( G |` Pred ( R , A , y ) ) ) ) ) -> ( F = G <-> ( A = A /\ A. z e. A ( F ` z ) = ( G ` z ) ) ) )
53 52 3adant1 
 |-  ( ( ( R Fr A /\ R Se A ) /\ ( F Fn A /\ A. y e. A ( F ` y ) = ( y H ( F |` Pred ( R , A , y ) ) ) ) /\ ( G Fn A /\ A. y e. A ( G ` y ) = ( y H ( G |` Pred ( R , A , y ) ) ) ) ) -> ( F = G <-> ( A = A /\ A. z e. A ( F ` z ) = ( G ` z ) ) ) )
54 50 53 mpbird 
 |-  ( ( ( R Fr A /\ R Se A ) /\ ( F Fn A /\ A. y e. A ( F ` y ) = ( y H ( F |` Pred ( R , A , y ) ) ) ) /\ ( G Fn A /\ A. y e. A ( G ` y ) = ( y H ( G |` Pred ( R , A , y ) ) ) ) ) -> F = G )