Metamath Proof Explorer


Theorem frrlem11

Description: Lemma for well-founded recursion. For the next several theorems we will be aiming to prove that dom F = A . To do this, we set up a function C that supposedly contains an element of A that is not in dom F and we show that the element must be in dom F . Our choice of what to restrict F to depends on if we assume partial orders or the axiom of infinity. To begin with, we establish the functionality of C . (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
Assertion frrlem11 φzAdomFCFnSdomFz

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 1 2 3 frrlem9 φFunF
6 5 funresd φFunFS
7 dmres domFS=SdomF
8 df-fn FSFnSdomFFunFSdomFS=SdomF
9 7 8 mpbiran2 FSFnSdomFFunFS
10 6 9 sylibr φFSFnSdomF
11 vex zV
12 ovex zGFPredRAzV
13 11 12 fnsn zzGFPredRAzFnz
14 10 13 jctir φFSFnSdomFzzGFPredRAzFnz
15 eldifn zAdomF¬zdomF
16 elinel2 zSdomFzdomF
17 15 16 nsyl zAdomF¬zSdomF
18 disjsn SdomFz=¬zSdomF
19 17 18 sylibr zAdomFSdomFz=
20 fnun FSFnSdomFzzGFPredRAzFnzSdomFz=FSzzGFPredRAzFnSdomFz
21 14 19 20 syl2an φzAdomFFSzzGFPredRAzFnSdomFz
22 4 fneq1i CFnSdomFzFSzzGFPredRAzFnSdomFz
23 21 22 sylibr φzAdomFCFnSdomFz