Metamath Proof Explorer


Theorem satffunlem1

Description: Lemma 1 for satffun : induction basis. (Contributed by AV, 28-Oct-2023)

Ref Expression
Assertion satffunlem1 MVEWFunMSatEsuc

Proof

Step Hyp Ref Expression
1 satfv0fun MVEWFunMSatE
2 satffunlem1lem1 FunMSatEFunxy|uMSatEvMSatEx=1stu𝑔1stvy=Mω2ndu2ndviωx=𝑔i1stuy=fMω|jMijfωi2ndu
3 1 2 syl MVEWFunxy|uMSatEvMSatEx=1stu𝑔1stvy=Mω2ndu2ndviωx=𝑔i1stuy=fMω|jMijfωi2ndu
4 satffunlem1lem2 MVEWdomMSatEdomxy|uMSatEvMSatEx=1stu𝑔1stvy=Mω2ndu2ndviωx=𝑔i1stuy=fMω|jMijfωi2ndu=
5 funun FunMSatEFunxy|uMSatEvMSatEx=1stu𝑔1stvy=Mω2ndu2ndviωx=𝑔i1stuy=fMω|jMijfωi2ndudomMSatEdomxy|uMSatEvMSatEx=1stu𝑔1stvy=Mω2ndu2ndviωx=𝑔i1stuy=fMω|jMijfωi2ndu=FunMSatExy|uMSatEvMSatEx=1stu𝑔1stvy=Mω2ndu2ndviωx=𝑔i1stuy=fMω|jMijfωi2ndu
6 1 3 4 5 syl21anc MVEWFunMSatExy|uMSatEvMSatEx=1stu𝑔1stvy=Mω2ndu2ndviωx=𝑔i1stuy=fMω|jMijfωi2ndu
7 peano1 ω
8 eqid MSatE=MSatE
9 8 satfvsuc MVEWωMSatEsuc=MSatExy|uMSatEvMSatEx=1stu𝑔1stvy=Mω2ndu2ndviωx=𝑔i1stuy=fMω|jMijfωi2ndu
10 7 9 mp3an3 MVEWMSatEsuc=MSatExy|uMSatEvMSatEx=1stu𝑔1stvy=Mω2ndu2ndviωx=𝑔i1stuy=fMω|jMijfωi2ndu
11 10 funeqd MVEWFunMSatEsucFunMSatExy|uMSatEvMSatEx=1stu𝑔1stvy=Mω2ndu2ndviωx=𝑔i1stuy=fMω|jMijfωi2ndu
12 6 11 mpbird MVEWFunMSatEsuc