Metamath Proof Explorer


Theorem frrlem14

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 B=f|xfFnxxAyxPredRAyxyxfy=yGfPredRAy
frrlem11.2 F=frecsRAG
frrlem11.3 φgBhBxguxhvu=v
frrlem11.4 C=FSzzGFPredRAz
frrlem12.5 φRFrA
frrlem12.6 φzAPredRAzS
frrlem12.7 φzAwSPredRAwS
frrlem13.8 φzASV
frrlem13.9 φzASA
frrlem14.10 φAdomFzAdomFPredRAdomFz=
Assertion frrlem14 φdomF=A

Proof

Step Hyp Ref Expression
1 frrlem11.1 B=f|xfFnxxAyxPredRAyxyxfy=yGfPredRAy
2 frrlem11.2 F=frecsRAG
3 frrlem11.3 φgBhBxguxhvu=v
4 frrlem11.4 C=FSzzGFPredRAz
5 frrlem12.5 φRFrA
6 frrlem12.6 φzAPredRAzS
7 frrlem12.7 φzAwSPredRAwS
8 frrlem13.8 φzASV
9 frrlem13.9 φzASA
10 frrlem14.10 φAdomFzAdomFPredRAdomFz=
11 1 2 frrlem7 domFA
12 11 a1i φdomFA
13 eldifn zAdomF¬zdomF
14 13 adantl φzAdomF¬zdomF
15 1 2 3 4 5 6 7 8 9 frrlem13 φzAdomFPredRAdomFz=CB
16 elssuni CBCB
17 15 16 syl φzAdomFPredRAdomFz=CB
18 1 2 frrlem5 F=B
19 17 18 sseqtrrdi φzAdomFPredRAdomFz=CF
20 dmss CFdomCdomF
21 19 20 syl φzAdomFPredRAdomFz=domCdomF
22 ssun2 zdomFSz
23 vsnid zz
24 22 23 sselii zdomFSz
25 4 dmeqi domC=domFSzzGFPredRAz
26 dmun domFSzzGFPredRAz=domFSdomzzGFPredRAz
27 ovex zGFPredRAzV
28 27 dmsnop domzzGFPredRAz=z
29 28 uneq2i domFSdomzzGFPredRAz=domFSz
30 25 26 29 3eqtri domC=domFSz
31 24 30 eleqtrri zdomC
32 31 a1i φzAdomFPredRAdomFz=zdomC
33 21 32 sseldd φzAdomFPredRAdomFz=zdomF
34 33 expr φzAdomFPredRAdomFz=zdomF
35 14 34 mtod φzAdomF¬PredRAdomFz=
36 35 nrexdv φ¬zAdomFPredRAdomFz=
37 df-ne AdomF¬AdomF=
38 37 10 sylan2br φ¬AdomF=zAdomFPredRAdomFz=
39 38 ex φ¬AdomF=zAdomFPredRAdomFz=
40 36 39 mt3d φAdomF=
41 ssdif0 AdomFAdomF=
42 40 41 sylibr φAdomF
43 12 42 eqssd φdomF=A