Metamath Proof Explorer


Theorem frrlem9

Description: Lemma for founded recursion. Show that the founded recursive generator produces a function. Hypothesis three will be eliminated using different induction rules depending on if we use partial ordering or 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 )