Metamath Proof Explorer

Theorem wfr3g

Description: Functions defined by well-founded recursion are identical up to relation, domain, and characteristic function. (Contributed by Scott Fenton, 11-Feb-2011)

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

Proof

Step Hyp Ref Expression
1 r19.26 
 |-  ( A. y e. A ( ( F ` y ) = ( H ` ( F |` Pred ( R , A , y ) ) ) /\ ( G ` y ) = ( H ` ( G |` Pred ( R , A , y ) ) ) ) <-> ( A. y e. A ( F ` y ) = ( H ` ( F |` Pred ( R , A , y ) ) ) /\ A. y e. A ( G ` y ) = ( H ` ( G |` Pred ( R , A , y ) ) ) ) )
2 fveq2 
 |-  ( z = w -> ( F ` z ) = ( F ` w ) )
3 fveq2 
 |-  ( z = w -> ( G ` z ) = ( G ` w ) )
4 2 3 eqeq12d 
 |-  ( z = w -> ( ( F ` z ) = ( G ` z ) <-> ( F ` w ) = ( G ` w ) ) )
5 4 imbi2d 
 |-  ( z = w -> ( ( ( ( F Fn A /\ G Fn A ) /\ A. y e. A ( ( F ` y ) = ( H ` ( F |` Pred ( R , A , y ) ) ) /\ ( G ` y ) = ( H ` ( G |` Pred ( R , A , y ) ) ) ) ) -> ( F ` z ) = ( G ` z ) ) <-> ( ( ( F Fn A /\ G Fn A ) /\ A. y e. A ( ( F ` y ) = ( H ` ( F |` Pred ( R , A , y ) ) ) /\ ( G ` y ) = ( H ` ( G |` Pred ( R , A , y ) ) ) ) ) -> ( F ` w ) = ( G ` w ) ) ) )
6 ra4v 
 |-  ( A. w e. Pred ( R , A , z ) ( ( ( F Fn A /\ G Fn A ) /\ A. y e. A ( ( F ` y ) = ( H ` ( F |` Pred ( R , A , y ) ) ) /\ ( G ` y ) = ( H ` ( G |` Pred ( R , A , y ) ) ) ) ) -> ( F ` w ) = ( G ` w ) ) -> ( ( ( F Fn A /\ G Fn A ) /\ A. y e. A ( ( F ` y ) = ( H ` ( F |` Pred ( R , A , y ) ) ) /\ ( G ` y ) = ( H ` ( G |` Pred ( R , A , y ) ) ) ) ) -> A. w e. Pred ( R , A , z ) ( F ` w ) = ( G ` w ) ) )
7 fveq2 
 |-  ( y = z -> ( F ` y ) = ( F ` z ) )
8 predeq3 
 |-  ( y = z -> Pred ( R , A , y ) = Pred ( R , A , z ) )
9 8 reseq2d 
 |-  ( y = z -> ( F |` Pred ( R , A , y ) ) = ( F |` Pred ( R , A , z ) ) )
10 9 fveq2d 
 |-  ( y = z -> ( H ` ( F |` Pred ( R , A , y ) ) ) = ( H ` ( F |` Pred ( R , A , z ) ) ) )
11 7 10 eqeq12d 
 |-  ( y = z -> ( ( F ` y ) = ( H ` ( F |` Pred ( R , A , y ) ) ) <-> ( F ` z ) = ( H ` ( F |` Pred ( R , A , z ) ) ) ) )
12 fveq2 
 |-  ( y = z -> ( G ` y ) = ( G ` z ) )
13 8 reseq2d 
 |-  ( y = z -> ( G |` Pred ( R , A , y ) ) = ( G |` Pred ( R , A , z ) ) )
14 13 fveq2d 
 |-  ( y = z -> ( H ` ( G |` Pred ( R , A , y ) ) ) = ( H ` ( G |` Pred ( R , A , z ) ) ) )
15 12 14 eqeq12d 
 |-  ( y = z -> ( ( G ` y ) = ( H ` ( G |` Pred ( R , A , y ) ) ) <-> ( G ` z ) = ( H ` ( G |` Pred ( R , A , z ) ) ) ) )
16 11 15 anbi12d 
 |-  ( y = z -> ( ( ( F ` y ) = ( H ` ( F |` Pred ( R , A , y ) ) ) /\ ( G ` y ) = ( H ` ( G |` Pred ( R , A , y ) ) ) ) <-> ( ( F ` z ) = ( H ` ( F |` Pred ( R , A , z ) ) ) /\ ( G ` z ) = ( H ` ( G |` Pred ( R , A , z ) ) ) ) ) )
17 16 rspcva 
 |-  ( ( z e. A /\ A. y e. A ( ( F ` y ) = ( H ` ( F |` Pred ( R , A , y ) ) ) /\ ( G ` y ) = ( H ` ( G |` Pred ( R , A , y ) ) ) ) ) -> ( ( F ` z ) = ( H ` ( F |` Pred ( R , A , z ) ) ) /\ ( G ` z ) = ( H ` ( G |` Pred ( R , A , z ) ) ) ) )
18 eqtr3 
 |-  ( ( ( F ` z ) = ( H ` ( F |` Pred ( R , A , z ) ) ) /\ ( H ` ( G |` Pred ( R , A , z ) ) ) = ( H ` ( F |` Pred ( R , A , z ) ) ) ) -> ( F ` z ) = ( H ` ( G |` Pred ( R , A , z ) ) ) )
19 18 ancoms 
 |-  ( ( ( H ` ( G |` Pred ( R , A , z ) ) ) = ( H ` ( F |` Pred ( R , A , z ) ) ) /\ ( F ` z ) = ( H ` ( F |` Pred ( R , A , z ) ) ) ) -> ( F ` z ) = ( H ` ( G |` Pred ( R , A , z ) ) ) )
20 eqtr3 
 |-  ( ( ( F ` z ) = ( H ` ( G |` Pred ( R , A , z ) ) ) /\ ( G ` z ) = ( H ` ( G |` Pred ( R , A , z ) ) ) ) -> ( F ` z ) = ( G ` z ) )
21 20 ex 
 |-  ( ( F ` z ) = ( H ` ( G |` Pred ( R , A , z ) ) ) -> ( ( G ` z ) = ( H ` ( G |` Pred ( R , A , z ) ) ) -> ( F ` z ) = ( G ` z ) ) )
22 19 21 syl 
 |-  ( ( ( H ` ( G |` Pred ( R , A , z ) ) ) = ( H ` ( F |` Pred ( R , A , z ) ) ) /\ ( F ` z ) = ( H ` ( F |` Pred ( R , A , z ) ) ) ) -> ( ( G ` z ) = ( H ` ( G |` Pred ( R , A , z ) ) ) -> ( F ` z ) = ( G ` z ) ) )
23 22 expimpd 
 |-  ( ( H ` ( G |` Pred ( R , A , z ) ) ) = ( H ` ( F |` Pred ( R , A , z ) ) ) -> ( ( ( F ` z ) = ( H ` ( F |` Pred ( R , A , z ) ) ) /\ ( G ` z ) = ( H ` ( G |` Pred ( R , A , z ) ) ) ) -> ( F ` z ) = ( G ` z ) ) )
24 predss 
 |-  Pred ( R , A , z ) C_ A
25 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 ) ) )
26 24 25 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 ) ) )
27 26 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 ) ) )
28 27 eqcomd 
 |-  ( ( ( F Fn A /\ G Fn A ) /\ A. w e. Pred ( R , A , z ) ( F ` w ) = ( G ` w ) ) -> ( G |` Pred ( R , A , z ) ) = ( F |` Pred ( R , A , z ) ) )
29 28 fveq2d 
 |-  ( ( ( F Fn A /\ G Fn A ) /\ A. w e. Pred ( R , A , z ) ( F ` w ) = ( G ` w ) ) -> ( H ` ( G |` Pred ( R , A , z ) ) ) = ( H ` ( F |` Pred ( R , A , z ) ) ) )
30 23 29 syl11 
 |-  ( ( ( F ` z ) = ( H ` ( F |` Pred ( R , A , z ) ) ) /\ ( G ` 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 ) ) )
31 30 expd 
 |-  ( ( ( F ` z ) = ( H ` ( F |` Pred ( R , A , z ) ) ) /\ ( G ` 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 ) ) ) )
32 17 31 syl 
 |-  ( ( z e. A /\ A. y e. A ( ( F ` y ) = ( H ` ( F |` Pred ( R , A , y ) ) ) /\ ( G ` 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 ) ) ) )
33 32 ex 
 |-  ( z e. A -> ( A. y e. A ( ( F ` y ) = ( H ` ( F |` Pred ( R , A , y ) ) ) /\ ( G ` 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 ) ) ) ) )
34 33 impcomd 
 |-  ( z e. A -> ( ( ( F Fn A /\ G Fn A ) /\ A. y e. A ( ( F ` y ) = ( H ` ( F |` Pred ( R , A , y ) ) ) /\ ( G ` 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 ) = ( H ` ( F |` Pred ( R , A , y ) ) ) /\ ( G ` 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 ) = ( H ` ( F |` Pred ( R , A , y ) ) ) /\ ( G ` y ) = ( H ` ( G |` Pred ( R , A , y ) ) ) ) ) -> ( F ` z ) = ( G ` z ) ) ) )
36 6 35 syl5 
 |-  ( z e. A -> ( A. w e. Pred ( R , A , z ) ( ( ( F Fn A /\ G Fn A ) /\ A. y e. A ( ( F ` y ) = ( H ` ( F |` Pred ( R , A , y ) ) ) /\ ( G ` y ) = ( H ` ( G |` Pred ( R , A , y ) ) ) ) ) -> ( F ` w ) = ( G ` w ) ) -> ( ( ( F Fn A /\ G Fn A ) /\ A. y e. A ( ( F ` y ) = ( H ` ( F |` Pred ( R , A , y ) ) ) /\ ( G ` y ) = ( H ` ( G |` Pred ( R , A , y ) ) ) ) ) -> ( F ` z ) = ( G ` z ) ) ) )
37 5 36 wfis2g 
 |-  ( ( R We A /\ R Se A ) -> A. z e. A ( ( ( F Fn A /\ G Fn A ) /\ A. y e. A ( ( F ` y ) = ( H ` ( F |` Pred ( R , A , y ) ) ) /\ ( G ` y ) = ( H ` ( G |` Pred ( R , A , y ) ) ) ) ) -> ( F ` z ) = ( G ` z ) ) )
38 r19.21v 
 |-  ( A. z e. A ( ( ( F Fn A /\ G Fn A ) /\ A. y e. A ( ( F ` y ) = ( H ` ( F |` Pred ( R , A , y ) ) ) /\ ( G ` y ) = ( H ` ( G |` Pred ( R , A , y ) ) ) ) ) -> ( F ` z ) = ( G ` z ) ) <-> ( ( ( F Fn A /\ G Fn A ) /\ A. y e. A ( ( F ` y ) = ( H ` ( F |` Pred ( R , A , y ) ) ) /\ ( G ` y ) = ( H ` ( G |` Pred ( R , A , y ) ) ) ) ) -> A. z e. A ( F ` z ) = ( G ` z ) ) )
39 37 38 sylib 
 |-  ( ( R We A /\ R Se A ) -> ( ( ( F Fn A /\ G Fn A ) /\ A. y e. A ( ( F ` y ) = ( H ` ( F |` Pred ( R , A , y ) ) ) /\ ( G ` y ) = ( H ` ( G |` Pred ( R , A , y ) ) ) ) ) -> A. z e. A ( F ` z ) = ( G ` z ) ) )
40 39 com12 
 |-  ( ( ( F Fn A /\ G Fn A ) /\ A. y e. A ( ( F ` y ) = ( H ` ( F |` Pred ( R , A , y ) ) ) /\ ( G ` y ) = ( H ` ( G |` Pred ( R , A , y ) ) ) ) ) -> ( ( R We A /\ R Se A ) -> A. z e. A ( F ` z ) = ( G ` z ) ) )
41 1 40 sylan2br 
 |-  ( ( ( F Fn A /\ G Fn A ) /\ ( A. y e. A ( F ` y ) = ( H ` ( F |` Pred ( R , A , y ) ) ) /\ A. y e. A ( G ` y ) = ( H ` ( G |` Pred ( R , A , y ) ) ) ) ) -> ( ( R We A /\ R Se A ) -> A. z e. A ( F ` z ) = ( G ` z ) ) )
42 41 an4s 
 |-  ( ( ( F Fn A /\ A. y e. A ( F ` y ) = ( H ` ( F |` Pred ( R , A , y ) ) ) ) /\ ( G Fn A /\ A. y e. A ( G ` y ) = ( H ` ( G |` Pred ( R , A , y ) ) ) ) ) -> ( ( R We A /\ R Se A ) -> A. z e. A ( F ` z ) = ( G ` z ) ) )
43 42 com12 
 |-  ( ( R We A /\ R Se A ) -> ( ( ( F Fn A /\ A. y e. A ( F ` y ) = ( H ` ( F |` Pred ( R , A , y ) ) ) ) /\ ( G Fn A /\ A. y e. A ( G ` y ) = ( H ` ( G |` Pred ( R , A , y ) ) ) ) ) -> A. z e. A ( F ` z ) = ( G ` z ) ) )
44 43 3impib 
 |-  ( ( ( R We A /\ R Se A ) /\ ( F Fn A /\ A. y e. A ( F ` y ) = ( H ` ( F |` Pred ( R , A , y ) ) ) ) /\ ( G Fn A /\ A. y e. A ( G ` y ) = ( H ` ( G |` Pred ( R , A , y ) ) ) ) ) -> A. z e. A ( F ` z ) = ( G ` z ) )
45 eqid 
 |-  A = A
46 44 45 jctil 
 |-  ( ( ( R We A /\ R Se A ) /\ ( F Fn A /\ A. y e. A ( F ` y ) = ( H ` ( F |` Pred ( R , A , y ) ) ) ) /\ ( G Fn A /\ A. y e. A ( G ` y ) = ( H ` ( G |` Pred ( R , A , y ) ) ) ) ) -> ( A = A /\ A. z e. A ( F ` z ) = ( G ` z ) ) )
47 eqfnfv2 
 |-  ( ( F Fn A /\ G Fn A ) -> ( F = G <-> ( A = A /\ A. z e. A ( F ` z ) = ( G ` z ) ) ) )
48 47 ad2ant2r 
 |-  ( ( ( F Fn A /\ A. y e. A ( F ` y ) = ( H ` ( F |` Pred ( R , A , y ) ) ) ) /\ ( G Fn A /\ A. y e. A ( G ` y ) = ( H ` ( G |` Pred ( R , A , y ) ) ) ) ) -> ( F = G <-> ( A = A /\ A. z e. A ( F ` z ) = ( G ` z ) ) ) )
49 48 3adant1 
 |-  ( ( ( R We A /\ R Se A ) /\ ( F Fn A /\ A. y e. A ( F ` y ) = ( H ` ( F |` Pred ( R , A , y ) ) ) ) /\ ( G Fn A /\ A. y e. A ( G ` y ) = ( H ` ( G |` Pred ( R , A , y ) ) ) ) ) -> ( F = G <-> ( A = A /\ A. z e. A ( F ` z ) = ( G ` z ) ) ) )
50 46 49 mpbird 
 |-  ( ( ( R We A /\ R Se A ) /\ ( F Fn A /\ A. y e. A ( F ` y ) = ( H ` ( F |` Pred ( R , A , y ) ) ) ) /\ ( G Fn A /\ A. y e. A ( G ` y ) = ( H ` ( G |` Pred ( R , A , y ) ) ) ) ) -> F = G )