Metamath Proof Explorer

Theorem frrlem13

Description: Lemma for well-founded recursion. Assuming that S is a subset of A and that z is R -minimal, then C is an acceptable function. (Contributed by Scott Fenton, 7-Dec-2022)

Ref Expression
Hypotheses frrlem11.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 ) ) ) ) }
frrlem11.2 
|- F = frecs ( R , A , G )
frrlem11.3 
|- ( ( ph /\ ( g e. B /\ h e. B ) ) -> ( ( x g u /\ x h v ) -> u = v ) )
frrlem11.4 
|- C = ( ( F |` S ) u. { <. z , ( z G ( F |` Pred ( R , A , z ) ) ) >. } )
frrlem12.5 
|- ( ph -> R Fr A )
frrlem12.6 
|- ( ( ph /\ z e. A ) -> Pred ( R , A , z ) C_ S )
frrlem12.7 
|- ( ( ph /\ z e. A ) -> A. w e. S Pred ( R , A , w ) C_ S )
frrlem13.8 
|- ( ( ph /\ z e. A ) -> S e. _V )
frrlem13.9 
|- ( ( ph /\ z e. A ) -> S C_ A )
Assertion frrlem13 
|- ( ( ph /\ ( z e. ( A \ dom F ) /\ Pred ( R , ( A \ dom F ) , z ) = (/) ) ) -> C e. B )

Proof

Step Hyp Ref Expression
1 frrlem11.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 frrlem11.2 
 |-  F = frecs ( R , A , G )
3 frrlem11.3 
 |-  ( ( ph /\ ( g e. B /\ h e. B ) ) -> ( ( x g u /\ x h v ) -> u = v ) )
4 frrlem11.4 
 |-  C = ( ( F |` S ) u. { <. z , ( z G ( F |` Pred ( R , A , z ) ) ) >. } )
5 frrlem12.5 
 |-  ( ph -> R Fr A )
6 frrlem12.6 
 |-  ( ( ph /\ z e. A ) -> Pred ( R , A , z ) C_ S )
7 frrlem12.7 
 |-  ( ( ph /\ z e. A ) -> A. w e. S Pred ( R , A , w ) C_ S )
8 frrlem13.8 
 |-  ( ( ph /\ z e. A ) -> S e. _V )
9 frrlem13.9 
 |-  ( ( ph /\ z e. A ) -> S C_ A )
10 eldifi 
 |-  ( z e. ( A \ dom F ) -> z e. A )
11 10 8 sylan2 
 |-  ( ( ph /\ z e. ( A \ dom F ) ) -> S e. _V )
12 11 adantrr 
 |-  ( ( ph /\ ( z e. ( A \ dom F ) /\ Pred ( R , ( A \ dom F ) , z ) = (/) ) ) -> S e. _V )
13 inex1g 
 |-  ( S e. _V -> ( S i^i dom F ) e. _V )
14 snex 
 |-  { z } e. _V
15 unexg 
 |-  ( ( ( S i^i dom F ) e. _V /\ { z } e. _V ) -> ( ( S i^i dom F ) u. { z } ) e. _V )
16 13 14 15 sylancl 
 |-  ( S e. _V -> ( ( S i^i dom F ) u. { z } ) e. _V )
17 12 16 syl 
 |-  ( ( ph /\ ( z e. ( A \ dom F ) /\ Pred ( R , ( A \ dom F ) , z ) = (/) ) ) -> ( ( S i^i dom F ) u. { z } ) e. _V )
18 1 2 3 4 frrlem11 
 |-  ( ( ph /\ z e. ( A \ dom F ) ) -> C Fn ( ( S i^i dom F ) u. { z } ) )
19 18 adantrr 
 |-  ( ( ph /\ ( z e. ( A \ dom F ) /\ Pred ( R , ( A \ dom F ) , z ) = (/) ) ) -> C Fn ( ( S i^i dom F ) u. { z } ) )
20 inss1 
 |-  ( S i^i dom F ) C_ S
21 10 9 sylan2 
 |-  ( ( ph /\ z e. ( A \ dom F ) ) -> S C_ A )
22 21 adantrr 
 |-  ( ( ph /\ ( z e. ( A \ dom F ) /\ Pred ( R , ( A \ dom F ) , z ) = (/) ) ) -> S C_ A )
23 20 22 sstrid 
 |-  ( ( ph /\ ( z e. ( A \ dom F ) /\ Pred ( R , ( A \ dom F ) , z ) = (/) ) ) -> ( S i^i dom F ) C_ A )
24 10 adantl 
 |-  ( ( ph /\ z e. ( A \ dom F ) ) -> z e. A )
25 24 adantrr 
 |-  ( ( ph /\ ( z e. ( A \ dom F ) /\ Pred ( R , ( A \ dom F ) , z ) = (/) ) ) -> z e. A )
26 25 snssd 
 |-  ( ( ph /\ ( z e. ( A \ dom F ) /\ Pred ( R , ( A \ dom F ) , z ) = (/) ) ) -> { z } C_ A )
27 23 26 unssd 
 |-  ( ( ph /\ ( z e. ( A \ dom F ) /\ Pred ( R , ( A \ dom F ) , z ) = (/) ) ) -> ( ( S i^i dom F ) u. { z } ) C_ A )
28 elun 
 |-  ( w e. ( ( S i^i dom F ) u. { z } ) <-> ( w e. ( S i^i dom F ) \/ w e. { z } ) )
29 elin 
 |-  ( w e. ( S i^i dom F ) <-> ( w e. S /\ w e. dom F ) )
30 velsn 
 |-  ( w e. { z } <-> w = z )
31 29 30 orbi12i 
 |-  ( ( w e. ( S i^i dom F ) \/ w e. { z } ) <-> ( ( w e. S /\ w e. dom F ) \/ w = z ) )
32 28 31 bitri 
 |-  ( w e. ( ( S i^i dom F ) u. { z } ) <-> ( ( w e. S /\ w e. dom F ) \/ w = z ) )
33 10 7 sylan2 
 |-  ( ( ph /\ z e. ( A \ dom F ) ) -> A. w e. S Pred ( R , A , w ) C_ S )
34 33 adantrr 
 |-  ( ( ph /\ ( z e. ( A \ dom F ) /\ Pred ( R , ( A \ dom F ) , z ) = (/) ) ) -> A. w e. S Pred ( R , A , w ) C_ S )
35 rsp 
 |-  ( A. w e. S Pred ( R , A , w ) C_ S -> ( w e. S -> Pred ( R , A , w ) C_ S ) )
36 34 35 syl 
 |-  ( ( ph /\ ( z e. ( A \ dom F ) /\ Pred ( R , ( A \ dom F ) , z ) = (/) ) ) -> ( w e. S -> Pred ( R , A , w ) C_ S ) )
37 1 2 frrlem8 
 |-  ( w e. dom F -> Pred ( R , A , w ) C_ dom F )
38 36 37 anim12d1 
 |-  ( ( ph /\ ( z e. ( A \ dom F ) /\ Pred ( R , ( A \ dom F ) , z ) = (/) ) ) -> ( ( w e. S /\ w e. dom F ) -> ( Pred ( R , A , w ) C_ S /\ Pred ( R , A , w ) C_ dom F ) ) )
39 ssin 
 |-  ( ( Pred ( R , A , w ) C_ S /\ Pred ( R , A , w ) C_ dom F ) <-> Pred ( R , A , w ) C_ ( S i^i dom F ) )
40 38 39 imbitrdi 
 |-  ( ( ph /\ ( z e. ( A \ dom F ) /\ Pred ( R , ( A \ dom F ) , z ) = (/) ) ) -> ( ( w e. S /\ w e. dom F ) -> Pred ( R , A , w ) C_ ( S i^i dom F ) ) )
41 10 6 sylan2 
 |-  ( ( ph /\ z e. ( A \ dom F ) ) -> Pred ( R , A , z ) C_ S )
42 41 adantrr 
 |-  ( ( ph /\ ( z e. ( A \ dom F ) /\ Pred ( R , ( A \ dom F ) , z ) = (/) ) ) -> Pred ( R , A , z ) C_ S )
43 preddif 
 |-  Pred ( R , ( A \ dom F ) , z ) = ( Pred ( R , A , z ) \ Pred ( R , dom F , z ) )
44 43 eqeq1i 
 |-  ( Pred ( R , ( A \ dom F ) , z ) = (/) <-> ( Pred ( R , A , z ) \ Pred ( R , dom F , z ) ) = (/) )
45 ssdif0 
 |-  ( Pred ( R , A , z ) C_ Pred ( R , dom F , z ) <-> ( Pred ( R , A , z ) \ Pred ( R , dom F , z ) ) = (/) )
46 44 45 sylbb2 
 |-  ( Pred ( R , ( A \ dom F ) , z ) = (/) -> Pred ( R , A , z ) C_ Pred ( R , dom F , z ) )
47 predss 
 |-  Pred ( R , dom F , z ) C_ dom F
48 46 47 sstrdi 
 |-  ( Pred ( R , ( A \ dom F ) , z ) = (/) -> Pred ( R , A , z ) C_ dom F )
49 48 adantl 
 |-  ( ( z e. ( A \ dom F ) /\ Pred ( R , ( A \ dom F ) , z ) = (/) ) -> Pred ( R , A , z ) C_ dom F )
50 49 adantl 
 |-  ( ( ph /\ ( z e. ( A \ dom F ) /\ Pred ( R , ( A \ dom F ) , z ) = (/) ) ) -> Pred ( R , A , z ) C_ dom F )
51 42 50 ssind 
 |-  ( ( ph /\ ( z e. ( A \ dom F ) /\ Pred ( R , ( A \ dom F ) , z ) = (/) ) ) -> Pred ( R , A , z ) C_ ( S i^i dom F ) )
52 predeq3 
 |-  ( w = z -> Pred ( R , A , w ) = Pred ( R , A , z ) )
53 52 sseq1d 
 |-  ( w = z -> ( Pred ( R , A , w ) C_ ( S i^i dom F ) <-> Pred ( R , A , z ) C_ ( S i^i dom F ) ) )
54 51 53 syl5ibrcom 
 |-  ( ( ph /\ ( z e. ( A \ dom F ) /\ Pred ( R , ( A \ dom F ) , z ) = (/) ) ) -> ( w = z -> Pred ( R , A , w ) C_ ( S i^i dom F ) ) )
55 40 54 jaod 
 |-  ( ( ph /\ ( z e. ( A \ dom F ) /\ Pred ( R , ( A \ dom F ) , z ) = (/) ) ) -> ( ( ( w e. S /\ w e. dom F ) \/ w = z ) -> Pred ( R , A , w ) C_ ( S i^i dom F ) ) )
56 32 55 biimtrid 
 |-  ( ( ph /\ ( z e. ( A \ dom F ) /\ Pred ( R , ( A \ dom F ) , z ) = (/) ) ) -> ( w e. ( ( S i^i dom F ) u. { z } ) -> Pred ( R , A , w ) C_ ( S i^i dom F ) ) )
57 56 imp 
 |-  ( ( ( ph /\ ( z e. ( A \ dom F ) /\ Pred ( R , ( A \ dom F ) , z ) = (/) ) ) /\ w e. ( ( S i^i dom F ) u. { z } ) ) -> Pred ( R , A , w ) C_ ( S i^i dom F ) )
58 ssun1 
 |-  ( S i^i dom F ) C_ ( ( S i^i dom F ) u. { z } )
59 57 58 sstrdi 
 |-  ( ( ( ph /\ ( z e. ( A \ dom F ) /\ Pred ( R , ( A \ dom F ) , z ) = (/) ) ) /\ w e. ( ( S i^i dom F ) u. { z } ) ) -> Pred ( R , A , w ) C_ ( ( S i^i dom F ) u. { z } ) )
60 59 ralrimiva 
 |-  ( ( ph /\ ( z e. ( A \ dom F ) /\ Pred ( R , ( A \ dom F ) , z ) = (/) ) ) -> A. w e. ( ( S i^i dom F ) u. { z } ) Pred ( R , A , w ) C_ ( ( S i^i dom F ) u. { z } ) )
61 27 60 jca 
 |-  ( ( ph /\ ( z e. ( A \ dom F ) /\ Pred ( R , ( A \ dom F ) , z ) = (/) ) ) -> ( ( ( S i^i dom F ) u. { z } ) C_ A /\ A. w e. ( ( S i^i dom F ) u. { z } ) Pred ( R , A , w ) C_ ( ( S i^i dom F ) u. { z } ) ) )
62 1 2 3 4 5 6 7 frrlem12 
 |-  ( ( ph /\ z e. ( A \ dom F ) /\ w e. ( ( S i^i dom F ) u. { z } ) ) -> ( C ` w ) = ( w G ( C |` Pred ( R , A , w ) ) ) )
63 62 3expa 
 |-  ( ( ( ph /\ z e. ( A \ dom F ) ) /\ w e. ( ( S i^i dom F ) u. { z } ) ) -> ( C ` w ) = ( w G ( C |` Pred ( R , A , w ) ) ) )
64 63 ralrimiva 
 |-  ( ( ph /\ z e. ( A \ dom F ) ) -> A. w e. ( ( S i^i dom F ) u. { z } ) ( C ` w ) = ( w G ( C |` Pred ( R , A , w ) ) ) )
65 64 adantrr 
 |-  ( ( ph /\ ( z e. ( A \ dom F ) /\ Pred ( R , ( A \ dom F ) , z ) = (/) ) ) -> A. w e. ( ( S i^i dom F ) u. { z } ) ( C ` w ) = ( w G ( C |` Pred ( R , A , w ) ) ) )
66 fneq2 
 |-  ( t = ( ( S i^i dom F ) u. { z } ) -> ( C Fn t <-> C Fn ( ( S i^i dom F ) u. { z } ) ) )
67 sseq1 
 |-  ( t = ( ( S i^i dom F ) u. { z } ) -> ( t C_ A <-> ( ( S i^i dom F ) u. { z } ) C_ A ) )
68 sseq2 
 |-  ( t = ( ( S i^i dom F ) u. { z } ) -> ( Pred ( R , A , w ) C_ t <-> Pred ( R , A , w ) C_ ( ( S i^i dom F ) u. { z } ) ) )
69 68 raleqbi1dv 
 |-  ( t = ( ( S i^i dom F ) u. { z } ) -> ( A. w e. t Pred ( R , A , w ) C_ t <-> A. w e. ( ( S i^i dom F ) u. { z } ) Pred ( R , A , w ) C_ ( ( S i^i dom F ) u. { z } ) ) )
70 67 69 anbi12d 
 |-  ( t = ( ( S i^i dom F ) u. { z } ) -> ( ( t C_ A /\ A. w e. t Pred ( R , A , w ) C_ t ) <-> ( ( ( S i^i dom F ) u. { z } ) C_ A /\ A. w e. ( ( S i^i dom F ) u. { z } ) Pred ( R , A , w ) C_ ( ( S i^i dom F ) u. { z } ) ) ) )
71 raleq 
 |-  ( t = ( ( S i^i dom F ) u. { z } ) -> ( A. w e. t ( C ` w ) = ( w G ( C |` Pred ( R , A , w ) ) ) <-> A. w e. ( ( S i^i dom F ) u. { z } ) ( C ` w ) = ( w G ( C |` Pred ( R , A , w ) ) ) ) )
72 66 70 71 3anbi123d 
 |-  ( t = ( ( S i^i dom F ) u. { z } ) -> ( ( C Fn t /\ ( t C_ A /\ A. w e. t Pred ( R , A , w ) C_ t ) /\ A. w e. t ( C ` w ) = ( w G ( C |` Pred ( R , A , w ) ) ) ) <-> ( C Fn ( ( S i^i dom F ) u. { z } ) /\ ( ( ( S i^i dom F ) u. { z } ) C_ A /\ A. w e. ( ( S i^i dom F ) u. { z } ) Pred ( R , A , w ) C_ ( ( S i^i dom F ) u. { z } ) ) /\ A. w e. ( ( S i^i dom F ) u. { z } ) ( C ` w ) = ( w G ( C |` Pred ( R , A , w ) ) ) ) ) )
73 72 spcegv 
 |-  ( ( ( S i^i dom F ) u. { z } ) e. _V -> ( ( C Fn ( ( S i^i dom F ) u. { z } ) /\ ( ( ( S i^i dom F ) u. { z } ) C_ A /\ A. w e. ( ( S i^i dom F ) u. { z } ) Pred ( R , A , w ) C_ ( ( S i^i dom F ) u. { z } ) ) /\ A. w e. ( ( S i^i dom F ) u. { z } ) ( C ` w ) = ( w G ( C |` Pred ( R , A , w ) ) ) ) -> E. t ( C Fn t /\ ( t C_ A /\ A. w e. t Pred ( R , A , w ) C_ t ) /\ A. w e. t ( C ` w ) = ( w G ( C |` Pred ( R , A , w ) ) ) ) ) )
74 73 imp 
 |-  ( ( ( ( S i^i dom F ) u. { z } ) e. _V /\ ( C Fn ( ( S i^i dom F ) u. { z } ) /\ ( ( ( S i^i dom F ) u. { z } ) C_ A /\ A. w e. ( ( S i^i dom F ) u. { z } ) Pred ( R , A , w ) C_ ( ( S i^i dom F ) u. { z } ) ) /\ A. w e. ( ( S i^i dom F ) u. { z } ) ( C ` w ) = ( w G ( C |` Pred ( R , A , w ) ) ) ) ) -> E. t ( C Fn t /\ ( t C_ A /\ A. w e. t Pred ( R , A , w ) C_ t ) /\ A. w e. t ( C ` w ) = ( w G ( C |` Pred ( R , A , w ) ) ) ) )
75 17 19 61 65 74 syl13anc 
 |-  ( ( ph /\ ( z e. ( A \ dom F ) /\ Pred ( R , ( A \ dom F ) , z ) = (/) ) ) -> E. t ( C Fn t /\ ( t C_ A /\ A. w e. t Pred ( R , A , w ) C_ t ) /\ A. w e. t ( C ` w ) = ( w G ( C |` Pred ( R , A , w ) ) ) ) )
76 1 2 3 frrlem9 
 |-  ( ph -> Fun F )
77 resfunexg 
 |-  ( ( Fun F /\ S e. _V ) -> ( F |` S ) e. _V )
78 76 12 77 syl2an2r 
 |-  ( ( ph /\ ( z e. ( A \ dom F ) /\ Pred ( R , ( A \ dom F ) , z ) = (/) ) ) -> ( F |` S ) e. _V )
79 snex 
 |-  { <. z , ( z G ( F |` Pred ( R , A , z ) ) ) >. } e. _V
80 unexg 
 |-  ( ( ( F |` S ) e. _V /\ { <. z , ( z G ( F |` Pred ( R , A , z ) ) ) >. } e. _V ) -> ( ( F |` S ) u. { <. z , ( z G ( F |` Pred ( R , A , z ) ) ) >. } ) e. _V )
81 78 79 80 sylancl 
 |-  ( ( ph /\ ( z e. ( A \ dom F ) /\ Pred ( R , ( A \ dom F ) , z ) = (/) ) ) -> ( ( F |` S ) u. { <. z , ( z G ( F |` Pred ( R , A , z ) ) ) >. } ) e. _V )
82 4 81 eqeltrid 
 |-  ( ( ph /\ ( z e. ( A \ dom F ) /\ Pred ( R , ( A \ dom F ) , z ) = (/) ) ) -> C e. _V )
83 fneq1 
 |-  ( c = C -> ( c Fn t <-> C Fn t ) )
84 fveq1 
 |-  ( c = C -> ( c ` w ) = ( C ` w ) )
85 reseq1 
 |-  ( c = C -> ( c |` Pred ( R , A , w ) ) = ( C |` Pred ( R , A , w ) ) )
86 85 oveq2d 
 |-  ( c = C -> ( w G ( c |` Pred ( R , A , w ) ) ) = ( w G ( C |` Pred ( R , A , w ) ) ) )
87 84 86 eqeq12d 
 |-  ( c = C -> ( ( c ` w ) = ( w G ( c |` Pred ( R , A , w ) ) ) <-> ( C ` w ) = ( w G ( C |` Pred ( R , A , w ) ) ) ) )
88 87 ralbidv 
 |-  ( c = C -> ( A. w e. t ( c ` w ) = ( w G ( c |` Pred ( R , A , w ) ) ) <-> A. w e. t ( C ` w ) = ( w G ( C |` Pred ( R , A , w ) ) ) ) )
89 83 88 3anbi13d 
 |-  ( c = C -> ( ( c Fn t /\ ( t C_ A /\ A. w e. t Pred ( R , A , w ) C_ t ) /\ A. w e. t ( c ` w ) = ( w G ( c |` Pred ( R , A , w ) ) ) ) <-> ( C Fn t /\ ( t C_ A /\ A. w e. t Pred ( R , A , w ) C_ t ) /\ A. w e. t ( C ` w ) = ( w G ( C |` Pred ( R , A , w ) ) ) ) ) )
90 89 exbidv 
 |-  ( c = C -> ( E. t ( c Fn t /\ ( t C_ A /\ A. w e. t Pred ( R , A , w ) C_ t ) /\ A. w e. t ( c ` w ) = ( w G ( c |` Pred ( R , A , w ) ) ) ) <-> E. t ( C Fn t /\ ( t C_ A /\ A. w e. t Pred ( R , A , w ) C_ t ) /\ A. w e. t ( C ` w ) = ( w G ( C |` Pred ( R , A , w ) ) ) ) ) )
91 1 frrlem1 
 |-  B = { c | E. t ( c Fn t /\ ( t C_ A /\ A. w e. t Pred ( R , A , w ) C_ t ) /\ A. w e. t ( c ` w ) = ( w G ( c |` Pred ( R , A , w ) ) ) ) }
92 90 91 elab2g 
 |-  ( C e. _V -> ( C e. B <-> E. t ( C Fn t /\ ( t C_ A /\ A. w e. t Pred ( R , A , w ) C_ t ) /\ A. w e. t ( C ` w ) = ( w G ( C |` Pred ( R , A , w ) ) ) ) ) )
93 82 92 syl 
 |-  ( ( ph /\ ( z e. ( A \ dom F ) /\ Pred ( R , ( A \ dom F ) , z ) = (/) ) ) -> ( C e. B <-> E. t ( C Fn t /\ ( t C_ A /\ A. w e. t Pred ( R , A , w ) C_ t ) /\ A. w e. t ( C ` w ) = ( w G ( C |` Pred ( R , A , w ) ) ) ) ) )
94 75 93 mpbird 
 |-  ( ( ph /\ ( z e. ( A \ dom F ) /\ Pred ( R , ( A \ dom F ) , z ) = (/) ) ) -> C e. B )