Metamath Proof Explorer


Theorem satffunlem2

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

Ref Expression
Assertion satffunlem2 NωMVEWFunMSatEsucNFunMSatEsucsucN

Proof

Step Hyp Ref Expression
1 simpr NωMVEWFunMSatEsucNFunMSatEsucN
2 simpr NωMVEWMVEW
3 peano2 NωsucNω
4 3 ancri NωsucNωNω
5 4 adantr NωMVEWsucNωNω
6 sssucid NsucN
7 6 a1i NωMVEWNsucN
8 eqid MSatE=MSatE
9 8 satfsschain MVEWsucNωNωNsucNMSatENMSatEsucN
10 9 imp MVEWsucNωNωNsucNMSatENMSatEsucN
11 2 5 7 10 syl21anc NωMVEWMSatENMSatEsucN
12 eqid Mω2ndu2ndv=Mω2ndu2ndv
13 eqid fMω|jMijfωi2ndu=fMω|jMijfωi2ndu
14 8 12 13 satffunlem2lem1 FunMSatEsucNMSatENMSatEsucNFunxy|uMSatEsucNMSatENvMSatEsucNx=1stu𝑔1stvy=Mω2ndu2ndviωx=𝑔i1stuy=fMω|jMijfωi2nduuMSatENvMSatEsucNMSatENx=1stu𝑔1stvy=Mω2ndu2ndv
15 14 expcom MSatENMSatEsucNFunMSatEsucNFunxy|uMSatEsucNMSatENvMSatEsucNx=1stu𝑔1stvy=Mω2ndu2ndviωx=𝑔i1stuy=fMω|jMijfωi2nduuMSatENvMSatEsucNMSatENx=1stu𝑔1stvy=Mω2ndu2ndv
16 11 15 syl NωMVEWFunMSatEsucNFunxy|uMSatEsucNMSatENvMSatEsucNx=1stu𝑔1stvy=Mω2ndu2ndviωx=𝑔i1stuy=fMω|jMijfωi2nduuMSatENvMSatEsucNMSatENx=1stu𝑔1stvy=Mω2ndu2ndv
17 16 imp NωMVEWFunMSatEsucNFunxy|uMSatEsucNMSatENvMSatEsucNx=1stu𝑔1stvy=Mω2ndu2ndviωx=𝑔i1stuy=fMω|jMijfωi2nduuMSatENvMSatEsucNMSatENx=1stu𝑔1stvy=Mω2ndu2ndv
18 8 12 13 satffunlem2lem2 NωMVEWFunMSatEsucNdomMSatEsucNdomxy|uMSatEsucNMSatENvMSatEsucNx=1stu𝑔1stvy=Mω2ndu2ndviωx=𝑔i1stuy=fMω|jMijfωi2nduuMSatENvMSatEsucNMSatENx=1stu𝑔1stvy=Mω2ndu2ndv=
19 funun FunMSatEsucNFunxy|uMSatEsucNMSatENvMSatEsucNx=1stu𝑔1stvy=Mω2ndu2ndviωx=𝑔i1stuy=fMω|jMijfωi2nduuMSatENvMSatEsucNMSatENx=1stu𝑔1stvy=Mω2ndu2ndvdomMSatEsucNdomxy|uMSatEsucNMSatENvMSatEsucNx=1stu𝑔1stvy=Mω2ndu2ndviωx=𝑔i1stuy=fMω|jMijfωi2nduuMSatENvMSatEsucNMSatENx=1stu𝑔1stvy=Mω2ndu2ndv=FunMSatEsucNxy|uMSatEsucNMSatENvMSatEsucNx=1stu𝑔1stvy=Mω2ndu2ndviωx=𝑔i1stuy=fMω|jMijfωi2nduuMSatENvMSatEsucNMSatENx=1stu𝑔1stvy=Mω2ndu2ndv
20 1 17 18 19 syl21anc NωMVEWFunMSatEsucNFunMSatEsucNxy|uMSatEsucNMSatENvMSatEsucNx=1stu𝑔1stvy=Mω2ndu2ndviωx=𝑔i1stuy=fMω|jMijfωi2nduuMSatENvMSatEsucNMSatENx=1stu𝑔1stvy=Mω2ndu2ndv
21 simpl MVEWMV
22 simpr MVEWEW
23 simpl NωMVEWNω
24 8 12 13 satfvsucsuc MVEWNωMSatEsucsucN=MSatEsucNxy|uMSatEsucNMSatENvMSatEsucNx=1stu𝑔1stvy=Mω2ndu2ndviωx=𝑔i1stuy=fMω|jMijfωi2nduuMSatENvMSatEsucNMSatENx=1stu𝑔1stvy=Mω2ndu2ndv
25 21 22 23 24 syl2an23an NωMVEWMSatEsucsucN=MSatEsucNxy|uMSatEsucNMSatENvMSatEsucNx=1stu𝑔1stvy=Mω2ndu2ndviωx=𝑔i1stuy=fMω|jMijfωi2nduuMSatENvMSatEsucNMSatENx=1stu𝑔1stvy=Mω2ndu2ndv
26 25 funeqd NωMVEWFunMSatEsucsucNFunMSatEsucNxy|uMSatEsucNMSatENvMSatEsucNx=1stu𝑔1stvy=Mω2ndu2ndviωx=𝑔i1stuy=fMω|jMijfωi2nduuMSatENvMSatEsucNMSatENx=1stu𝑔1stvy=Mω2ndu2ndv
27 26 adantr NωMVEWFunMSatEsucNFunMSatEsucsucNFunMSatEsucNxy|uMSatEsucNMSatENvMSatEsucNx=1stu𝑔1stvy=Mω2ndu2ndviωx=𝑔i1stuy=fMω|jMijfωi2nduuMSatENvMSatEsucNMSatENx=1stu𝑔1stvy=Mω2ndu2ndv
28 20 27 mpbird NωMVEWFunMSatEsucNFunMSatEsucsucN
29 28 ex NωMVEWFunMSatEsucNFunMSatEsucsucN