Metamath Proof Explorer

Theorem frr1

Description: Law of general well-founded recursion, part one. This theorem and the following two drop the partial order requirement from fpr1 , fpr2 , and fpr3 , which requires using the axiom of infinity (Contributed by Scott Fenton, 11-Sep-2023)

Ref Expression
Hypothesis frr.1 
|- F = frecs ( R , A , G )
Assertion frr1 
|- ( ( R Fr A /\ R Se A ) -> F Fn A )

Proof

Step Hyp Ref Expression
1 frr.1 
 |-  F = frecs ( R , A , G )
2 eqid 
 |-  { a | E. b ( a Fn b /\ ( b C_ A /\ A. c e. b Pred ( R , A , c ) C_ b ) /\ A. c e. b ( a ` c ) = ( c G ( a |` Pred ( R , A , c ) ) ) ) } = { a | E. b ( a Fn b /\ ( b C_ A /\ A. c e. b Pred ( R , A , c ) C_ b ) /\ A. c e. b ( a ` c ) = ( c G ( a |` Pred ( R , A , c ) ) ) ) }
3 2 frrlem1 
 |-  { a | E. b ( a Fn b /\ ( b C_ A /\ A. c e. b Pred ( R , A , c ) C_ b ) /\ A. c e. b ( a ` c ) = ( c G ( a |` Pred ( R , A , c ) ) ) ) } = { 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 ) ) ) ) }
4 3 1 frrlem15 
 |-  ( ( ( R Fr A /\ R Se A ) /\ ( g e. { a | E. b ( a Fn b /\ ( b C_ A /\ A. c e. b Pred ( R , A , c ) C_ b ) /\ A. c e. b ( a ` c ) = ( c G ( a |` Pred ( R , A , c ) ) ) ) } /\ h e. { a | E. b ( a Fn b /\ ( b C_ A /\ A. c e. b Pred ( R , A , c ) C_ b ) /\ A. c e. b ( a ` c ) = ( c G ( a |` Pred ( R , A , c ) ) ) ) } ) ) -> ( ( x g u /\ x h v ) -> u = v ) )
5 3 1 4 frrlem9 
 |-  ( ( R Fr A /\ R Se A ) -> Fun F )
6 eqid 
 |-  ( ( F |` Pred ( t++ ( R |` A ) , A , z ) ) u. { <. z , ( z G ( F |` Pred ( R , A , z ) ) ) >. } ) = ( ( F |` Pred ( t++ ( R |` A ) , A , z ) ) u. { <. z , ( z G ( F |` Pred ( R , A , z ) ) ) >. } )
7 simpl 
 |-  ( ( R Fr A /\ R Se A ) -> R Fr A )
8 predres 
 |-  Pred ( R , A , z ) = Pred ( ( R |` A ) , A , z )
9 relres 
 |-  Rel ( R |` A )
10 ssttrcl 
 |-  ( Rel ( R |` A ) -> ( R |` A ) C_ t++ ( R |` A ) )
11 predrelss 
 |-  ( ( R |` A ) C_ t++ ( R |` A ) -> Pred ( ( R |` A ) , A , z ) C_ Pred ( t++ ( R |` A ) , A , z ) )
12 9 10 11 mp2b 
 |-  Pred ( ( R |` A ) , A , z ) C_ Pred ( t++ ( R |` A ) , A , z )
13 8 12 eqsstri 
 |-  Pred ( R , A , z ) C_ Pred ( t++ ( R |` A ) , A , z )
14 13 a1i 
 |-  ( ( ( R Fr A /\ R Se A ) /\ z e. A ) -> Pred ( R , A , z ) C_ Pred ( t++ ( R |` A ) , A , z ) )
15 frrlem16 
 |-  ( ( ( R Fr A /\ R Se A ) /\ z e. A ) -> A. a e. Pred ( t++ ( R |` A ) , A , z ) Pred ( R , A , a ) C_ Pred ( t++ ( R |` A ) , A , z ) )
16 ttrclse 
 |-  ( R Se A -> t++ ( R |` A ) Se A )
17 setlikespec 
 |-  ( ( z e. A /\ t++ ( R |` A ) Se A ) -> Pred ( t++ ( R |` A ) , A , z ) e. _V )
18 17 ancoms 
 |-  ( ( t++ ( R |` A ) Se A /\ z e. A ) -> Pred ( t++ ( R |` A ) , A , z ) e. _V )
19 16 18 sylan 
 |-  ( ( R Se A /\ z e. A ) -> Pred ( t++ ( R |` A ) , A , z ) e. _V )
20 19 adantll 
 |-  ( ( ( R Fr A /\ R Se A ) /\ z e. A ) -> Pred ( t++ ( R |` A ) , A , z ) e. _V )
21 predss 
 |-  Pred ( t++ ( R |` A ) , A , z ) C_ A
22 21 a1i 
 |-  ( ( ( R Fr A /\ R Se A ) /\ z e. A ) -> Pred ( t++ ( R |` A ) , A , z ) C_ A )
23 difss 
 |-  ( A \ dom F ) C_ A
24 frmin 
 |-  ( ( ( R Fr A /\ R Se A ) /\ ( ( A \ dom F ) C_ A /\ ( A \ dom F ) =/= (/) ) ) -> E. z e. ( A \ dom F ) Pred ( R , ( A \ dom F ) , z ) = (/) )
25 23 24 mpanr1 
 |-  ( ( ( R Fr A /\ R Se A ) /\ ( A \ dom F ) =/= (/) ) -> E. z e. ( A \ dom F ) Pred ( R , ( A \ dom F ) , z ) = (/) )
26 3 1 4 6 7 14 15 20 22 25 frrlem14 
 |-  ( ( R Fr A /\ R Se A ) -> dom F = A )
27 df-fn 
 |-  ( F Fn A <-> ( Fun F /\ dom F = A ) )
28 5 26 27 sylanbrc 
 |-  ( ( R Fr A /\ R Se A ) -> F Fn A )