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 | |
|
frrlem5.2 | |
||
Assertion | frrlem7 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | frrlem5.1 | |
|
2 | frrlem5.2 | |
|
3 | 1 2 | frrlem5 | |
4 | 3 | dmeqi | |
5 | dmuni | |
|
6 | 4 5 | eqtri | |
7 | 6 | sseq1i | |
8 | iunss | |
|
9 | 7 8 | bitri | |
10 | 1 | frrlem3 | |
11 | 9 10 | mprgbir | |