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 syl6ib
 |-  ( ( 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 syl5bi
 |-  ( ( 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 )