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 |` TrPred ( R , A , z ) ) u. { <. z , ( z G ( F |` Pred ( R , A , z ) ) ) >. } ) = ( ( F |` TrPred ( R , A , z ) ) u. { <. z , ( z G ( F |` Pred ( R , A , z ) ) ) >. } )
7 simpl 
 |-  ( ( R Fr A /\ R Se A ) -> R Fr A )
8 setlikespec 
 |-  ( ( z e. A /\ R Se A ) -> Pred ( R , A , z ) e. _V )
9 8 ancoms 
 |-  ( ( R Se A /\ z e. A ) -> Pred ( R , A , z ) e. _V )
10 9 adantll 
 |-  ( ( ( R Fr A /\ R Se A ) /\ z e. A ) -> Pred ( R , A , z ) e. _V )
11 trpredpred 
 |-  ( Pred ( R , A , z ) e. _V -> Pred ( R , A , z ) C_ TrPred ( R , A , z ) )
12 10 11 syl 
 |-  ( ( ( R Fr A /\ R Se A ) /\ z e. A ) -> Pred ( R , A , z ) C_ TrPred ( R , A , z ) )
13 frrlem16 
 |-  ( ( ( R Fr A /\ R Se A ) /\ z e. A ) -> A. a e. TrPred ( R , A , z ) Pred ( R , A , a ) C_ TrPred ( R , A , z ) )
14 trpredex 
 |-  TrPred ( R , A , z ) e. _V
15 14 a1i 
 |-  ( ( ( R Fr A /\ R Se A ) /\ z e. A ) -> TrPred ( R , A , z ) e. _V )
16 trpredss 
 |-  ( Pred ( R , A , z ) e. _V -> TrPred ( R , A , z ) C_ A )
17 10 16 syl 
 |-  ( ( ( R Fr A /\ R Se A ) /\ z e. A ) -> TrPred ( R , A , z ) C_ A )
18 difss 
 |-  ( A \ dom F ) C_ A
19 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 ) = (/) )
20 18 19 mpanr1 
 |-  ( ( ( R Fr A /\ R Se A ) /\ ( A \ dom F ) =/= (/) ) -> E. z e. ( A \ dom F ) Pred ( R , ( A \ dom F ) , z ) = (/) )
21 3 1 4 6 7 12 13 15 17 20 frrlem14 
 |-  ( ( R Fr A /\ R Se A ) -> dom F = A )
22 df-fn 
 |-  ( F Fn A <-> ( Fun F /\ dom F = A ) )
23 5 21 22 sylanbrc 
 |-  ( ( R Fr A /\ R Se A ) -> F Fn A )