Theorem frrlem9

Description: Lemma for well-founded recursion. Show that the well-founded recursive generator produces a function. Hypothesis three will be eliminated using different induction rules depending on if we use partial orders or the axiom of infinity. (Contributed by Scott Fenton, 27-Aug-2022)

	Ref	Expression
Hypotheses	frrlem9.1	|- B = { f | E. x ( f Fn x /\ ( x C_ A /\ A. y e. x Pred ( R , A , y ) C_ x ) /\ A. y e. x ( f ` y ) = ( y G ( f |` Pred ( R , A , y ) ) ) ) }
	frrlem9.2	|- F = frecs ( R , A , G )
	frrlem9.3	|- ( ( ph /\ ( g e. B /\ h e. B ) ) -> ( ( x g u /\ x h v ) -> u = v ) )
Assertion	frrlem9	|- ( ph -> Fun F )

Proof

Step	Hyp	Ref	Expression
1		frrlem9.1	|- B = { f | E. x ( f Fn x /\ ( x C_ A /\ A. y e. x Pred ( R , A , y ) C_ x ) /\ A. y e. x ( f ` y ) = ( y G ( f |` Pred ( R , A , y ) ) ) ) }
2		frrlem9.2	|- F = frecs ( R , A , G )
3		frrlem9.3	|- ( ( ph /\ ( g e. B /\ h e. B ) ) -> ( ( x g u /\ x h v ) -> u = v ) )
4		eluni2	|- ( <. x , u >. e. U. B <-> E. g e. B <. x , u >. e. g )
5		df-br	|- ( x F u <-> <. x , u >. e. F )
6	1 2	frrlem5	|- F = U. B
7	6	eleq2i	|- ( <. x , u >. e. F <-> <. x , u >. e. U. B )
8	5 7	bitri	|- ( x F u <-> <. x , u >. e. U. B )
9		df-br	|- ( x g u <-> <. x , u >. e. g )
10	9	rexbii	|- ( E. g e. B x g u <-> E. g e. B <. x , u >. e. g )
11	4 8 10	3bitr4i	|- ( x F u <-> E. g e. B x g u )
12		eluni2	|- ( <. x , v >. e. U. B <-> E. h e. B <. x , v >. e. h )
13		df-br	|- ( x F v <-> <. x , v >. e. F )
14	6	eleq2i	|- ( <. x , v >. e. F <-> <. x , v >. e. U. B )
15	13 14	bitri	|- ( x F v <-> <. x , v >. e. U. B )
16		df-br	|- ( x h v <-> <. x , v >. e. h )
17	16	rexbii	|- ( E. h e. B x h v <-> E. h e. B <. x , v >. e. h )
18	12 15 17	3bitr4i	|- ( x F v <-> E. h e. B x h v )
19	11 18	anbi12i	|- ( ( x F u /\ x F v ) <-> ( E. g e. B x g u /\ E. h e. B x h v ) )
20		reeanv	|- ( E. g e. B E. h e. B ( x g u /\ x h v ) <-> ( E. g e. B x g u /\ E. h e. B x h v ) )
21	19 20	bitr4i	|- ( ( x F u /\ x F v ) <-> E. g e. B E. h e. B ( x g u /\ x h v ) )
22	3	rexlimdvva	|- ( ph -> ( E. g e. B E. h e. B ( x g u /\ x h v ) -> u = v ) )
23	21 22	syl5bi	|- ( ph -> ( ( x F u /\ x F v ) -> u = v ) )
24	23	alrimiv	|- ( ph -> A. v ( ( x F u /\ x F v ) -> u = v ) )
25	24	alrimivv	|- ( ph -> A. x A. u A. v ( ( x F u /\ x F v ) -> u = v ) )
26	1 2	frrlem6	|- Rel F
27		dffun2	|- ( Fun F <-> ( Rel F /\ A. x A. u A. v ( ( x F u /\ x F v ) -> u = v ) ) )
28	26 27	mpbiran	|- ( Fun F <-> A. x A. u A. v ( ( x F u /\ x F v ) -> u = v ) )
29	25 28	sylibr	|- ( ph -> Fun F )