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 | x f Fn x x A y x Pred R A y x y x f y = y G f Pred R A y
frrlem5.2 F = frecs R A G
Assertion frrlem7 dom F A

Proof

Step Hyp Ref Expression
1 frrlem5.1 B = 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
2 frrlem5.2 F = frecs R A G
3 1 2 frrlem5 F = B
4 3 dmeqi dom F = dom B
5 dmuni dom B = g B dom g
6 4 5 eqtri dom F = g B dom g
7 6 sseq1i dom F A g B dom g A
8 iunss g B dom g A g B dom g A
9 7 8 bitri dom F A g B dom g A
10 1 frrlem3 g B dom g A
11 9 10 mprgbir dom F A