Metamath Proof Explorer


Theorem frrlem7

Description: Lemma for well-founded recursion. The well-founded recursion generator's domain is a subclass of A . (Contributed by Scott Fenton, 27-Aug-2022)

Ref Expression
Hypotheses frrlem5.1 B=f|xfFnxxAyxPredRAyxyxfy=yGfPredRAy
frrlem5.2 F=frecsRAG
Assertion frrlem7 domFA

Proof

Step Hyp Ref Expression
1 frrlem5.1 B=f|xfFnxxAyxPredRAyxyxfy=yGfPredRAy
2 frrlem5.2 F=frecsRAG
3 1 2 frrlem5 F=B
4 3 dmeqi domF=domB
5 dmuni domB=gBdomg
6 4 5 eqtri domF=gBdomg
7 6 sseq1i domFAgBdomgA
8 iunss gBdomgAgBdomgA
9 7 8 bitri domFAgBdomgA
10 1 frrlem3 gBdomgA
11 9 10 mprgbir domFA