This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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