Metamath Proof Explorer


Theorem frr2

Description: Law of general well-founded recursion, part two. Now we establish the value of F within A . (Contributed by Scott Fenton, 11-Sep-2023)

Ref Expression
Hypothesis frr.1 F = frecs R A G
Assertion frr2 R Fr A R Se A X A F X = X G F Pred R A X

Proof

Step Hyp Ref Expression
1 frr.1 F = frecs R A G
2 1 frr1 R Fr A R Se A F Fn A
3 2 fndmd R Fr A R Se A dom F = A
4 3 eleq2d R Fr A R Se A X dom F X A
5 4 pm5.32i R Fr A R Se A X dom F R Fr A R Se A X A
6 fveq2 y = X F y = F X
7 id y = X y = X
8 predeq3 y = X Pred R A y = Pred R A X
9 8 reseq2d y = X F Pred R A y = F Pred R A X
10 7 9 oveq12d y = X y G F Pred R A y = X G F Pred R A X
11 6 10 eqeq12d y = X F y = y G F Pred R A y F X = X G F Pred R A X
12 11 imbi2d y = X R Fr A R Se A F y = y G F Pred R A y R Fr A R Se A F X = X G F Pred R A X
13 eqid a | b a Fn b b A c b Pred R A c b c b a c = c G a Pred R A c = a | b a Fn b b A c b Pred R A c b c b a c = c G a Pred R A c
14 13 frrlem1 a | b a Fn b b A c b Pred R A c b c b a c = c G a Pred R A c = f | x f Fn x x A y x Pred R A y x y x f y = y G f Pred R A y
15 14 1 frrlem15 R Fr A R Se A g a | b a Fn b b A c b Pred R A c b c b a c = c G a Pred R A c h a | b a Fn b b A c b Pred R A c b c b a c = c G a Pred R A c x g u x h v u = v
16 14 1 15 frrlem10 R Fr A R Se A y dom F F y = y G F Pred R A y
17 16 expcom y dom F R Fr A R Se A F y = y G F Pred R A y
18 12 17 vtoclga X dom F R Fr A R Se A F X = X G F Pred R A X
19 18 impcom R Fr A R Se A X dom F F X = X G F Pred R A X
20 5 19 sylbir R Fr A R Se A X A F X = X G F Pred R A X