Metamath Proof Explorer

Theorem fpr3g

Description: Functions defined by well-founded recursion over a partial order are identical up to relation, domain, and characteristic function. This version of frr3g does not require infinity. (Contributed by Scott Fenton, 24-Aug-2022)

Ref Expression
Assertion fpr3g 
|- ( ( ( R Fr A /\ R Po 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 eqidd 
 |-  ( ( ( R Fr A /\ R Po 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 )
2 r19.21v 
 |-  ( A. w e. Pred ( R , A , z ) ( ( ( 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 ` w ) = ( G ` w ) ) <-> ( ( ( 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. w e. Pred ( R , A , z ) ( F ` w ) = ( G ` w ) ) )
3 simprll 
 |-  ( ( z e. 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 Fn A )
4 simprrl 
 |-  ( ( z e. 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 ) ) ) ) ) ) -> G Fn A )
5 predss 
 |-  Pred ( R , A , z ) C_ A
6 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 ) ) )
7 5 6 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 ) ) )
8 3 4 7 syl2anc 
 |-  ( ( z e. 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 |` Pred ( R , A , z ) ) = ( G |` Pred ( R , A , z ) ) <-> A. w e. Pred ( R , A , z ) ( F ` w ) = ( G ` w ) ) )
9 8 biimp3ar 
 |-  ( ( z e. 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. w e. Pred ( R , A , z ) ( F ` w ) = ( G ` w ) ) -> ( F |` Pred ( R , A , z ) ) = ( G |` Pred ( R , A , z ) ) )
10 9 oveq2d 
 |-  ( ( z e. 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. w e. Pred ( R , A , z ) ( F ` w ) = ( G ` w ) ) -> ( z H ( F |` Pred ( R , A , z ) ) ) = ( z H ( G |` Pred ( R , A , z ) ) ) )
11 fveq2 
 |-  ( y = z -> ( F ` y ) = ( F ` z ) )
12 id 
 |-  ( y = z -> y = z )
13 predeq3 
 |-  ( y = z -> Pred ( R , A , y ) = Pred ( R , A , z ) )
14 13 reseq2d 
 |-  ( y = z -> ( F |` Pred ( R , A , y ) ) = ( F |` Pred ( R , A , z ) ) )
15 12 14 oveq12d 
 |-  ( y = z -> ( y H ( F |` Pred ( R , A , y ) ) ) = ( z H ( F |` Pred ( R , A , z ) ) ) )
16 11 15 eqeq12d 
 |-  ( y = z -> ( ( F ` y ) = ( y H ( F |` Pred ( R , A , y ) ) ) <-> ( F ` z ) = ( z H ( F |` Pred ( R , A , z ) ) ) ) )
17 simp2lr 
 |-  ( ( z e. 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. w e. Pred ( R , A , z ) ( F ` w ) = ( G ` w ) ) -> A. y e. A ( F ` y ) = ( y H ( F |` Pred ( R , A , y ) ) ) )
18 simp1 
 |-  ( ( z e. 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. w e. Pred ( R , A , z ) ( F ` w ) = ( G ` w ) ) -> z e. A )
19 16 17 18 rspcdva 
 |-  ( ( z e. 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. w e. Pred ( R , A , z ) ( F ` w ) = ( G ` w ) ) -> ( F ` z ) = ( z H ( F |` Pred ( R , A , z ) ) ) )
20 fveq2 
 |-  ( y = z -> ( G ` y ) = ( G ` z ) )
21 13 reseq2d 
 |-  ( y = z -> ( G |` Pred ( R , A , y ) ) = ( G |` Pred ( R , A , z ) ) )
22 12 21 oveq12d 
 |-  ( y = z -> ( y H ( G |` Pred ( R , A , y ) ) ) = ( z H ( G |` Pred ( R , A , z ) ) ) )
23 20 22 eqeq12d 
 |-  ( y = z -> ( ( G ` y ) = ( y H ( G |` Pred ( R , A , y ) ) ) <-> ( G ` z ) = ( z H ( G |` Pred ( R , A , z ) ) ) ) )
24 simp2rr 
 |-  ( ( z e. 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. w e. Pred ( R , A , z ) ( F ` w ) = ( G ` w ) ) -> A. y e. A ( G ` y ) = ( y H ( G |` Pred ( R , A , y ) ) ) )
25 23 24 18 rspcdva 
 |-  ( ( z e. 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. w e. Pred ( R , A , z ) ( F ` w ) = ( G ` w ) ) -> ( G ` z ) = ( z H ( G |` Pred ( R , A , z ) ) ) )
26 10 19 25 3eqtr4d 
 |-  ( ( z e. 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. w e. Pred ( R , A , z ) ( F ` w ) = ( G ` w ) ) -> ( F ` z ) = ( G ` z ) )
27 26 3exp 
 |-  ( z e. 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. w e. Pred ( R , A , z ) ( F ` w ) = ( G ` w ) -> ( F ` z ) = ( G ` z ) ) ) )
28 27 a2d 
 |-  ( z e. 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. w e. Pred ( R , A , z ) ( F ` w ) = ( G ` w ) ) -> ( ( ( 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 ` z ) = ( G ` z ) ) ) )
29 2 28 biimtrid 
 |-  ( z e. A -> ( A. w e. Pred ( R , A , z ) ( ( ( 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 ` w ) = ( G ` w ) ) -> ( ( ( 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 ` z ) = ( G ` z ) ) ) )
30 fveq2 
 |-  ( z = w -> ( F ` z ) = ( F ` w ) )
31 fveq2 
 |-  ( z = w -> ( G ` z ) = ( G ` w ) )
32 30 31 eqeq12d 
 |-  ( z = w -> ( ( F ` z ) = ( G ` z ) <-> ( F ` w ) = ( G ` w ) ) )
33 32 imbi2d 
 |-  ( z = w -> ( ( ( ( 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 ` z ) = ( G ` z ) ) <-> ( ( ( 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 ` w ) = ( G ` w ) ) ) )
34 29 33 frpoins2g 
 |-  ( ( R Fr A /\ R Po A /\ R Se A ) -> A. z e. 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 ` z ) = ( G ` z ) ) )
35 r19.21v 
 |-  ( A. z e. 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 ` z ) = ( G ` z ) ) <-> ( ( ( 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 ) ) )
36 34 35 sylib 
 |-  ( ( R Fr A /\ R Po 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 ) ) )
37 36 3impib 
 |-  ( ( ( R Fr A /\ R Po 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 ) )
38 simp2l 
 |-  ( ( ( R Fr A /\ R Po 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 Fn A )
39 simp3l 
 |-  ( ( ( R Fr A /\ R Po 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 ) ) ) ) ) -> G Fn A )
40 eqfnfv2 
 |-  ( ( F Fn A /\ G Fn A ) -> ( F = G <-> ( A = A /\ A. z e. A ( F ` z ) = ( G ` z ) ) ) )
41 38 39 40 syl2anc 
 |-  ( ( ( R Fr A /\ R Po 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 ) ) ) )
42 1 37 41 mpbir2and 
 |-  ( ( ( R Fr A /\ R Po 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 )