Description: Lemma for well-founded recursion. Finally, we tie all these threads together and show that dom F = A when given the right S . Specifically, we prove that there can be no R -minimal element of ( A \ dom F ) . (Contributed by Scott Fenton, 7-Dec-2022)
Ref | Expression | ||
---|---|---|---|
Hypotheses | frrlem11.1 | |
|
frrlem11.2 | |
||
frrlem11.3 | |
||
frrlem11.4 | |
||
frrlem12.5 | |
||
frrlem12.6 | |
||
frrlem12.7 | |
||
frrlem13.8 | |
||
frrlem13.9 | |
||
frrlem14.10 | |
||
Assertion | frrlem14 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | frrlem11.1 | |
|
2 | frrlem11.2 | |
|
3 | frrlem11.3 | |
|
4 | frrlem11.4 | |
|
5 | frrlem12.5 | |
|
6 | frrlem12.6 | |
|
7 | frrlem12.7 | |
|
8 | frrlem13.8 | |
|
9 | frrlem13.9 | |
|
10 | frrlem14.10 | |
|
11 | 1 2 | frrlem7 | |
12 | 11 | a1i | |
13 | eldifn | |
|
14 | 13 | adantl | |
15 | 1 2 3 4 5 6 7 8 9 | frrlem13 | |
16 | elssuni | |
|
17 | 15 16 | syl | |
18 | 1 2 | frrlem5 | |
19 | 17 18 | sseqtrrdi | |
20 | dmss | |
|
21 | 19 20 | syl | |
22 | ssun2 | |
|
23 | vsnid | |
|
24 | 22 23 | sselii | |
25 | 4 | dmeqi | |
26 | dmun | |
|
27 | ovex | |
|
28 | 27 | dmsnop | |
29 | 28 | uneq2i | |
30 | 25 26 29 | 3eqtri | |
31 | 24 30 | eleqtrri | |
32 | 31 | a1i | |
33 | 21 32 | sseldd | |
34 | 33 | expr | |
35 | 14 34 | mtod | |
36 | 35 | nrexdv | |
37 | df-ne | |
|
38 | 37 10 | sylan2br | |
39 | 38 | ex | |
40 | 36 39 | mt3d | |
41 | ssdif0 | |
|
42 | 40 41 | sylibr | |
43 | 12 42 | eqssd | |