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	syl5bi	|- ( 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 )