Metamath Proof Explorer


Theorem satfsucom

Description: The satisfaction predicate for wff codes in the model M and the binary relation E on M at an element of the successor of _om . (Contributed by AV, 22-Sep-2023)

Ref Expression
Assertion satfsucom MVEWNsucωMSatEN=recfVfxy|ufvfx=1stu𝑔1stvy=Mω2ndu2ndviωx=𝑔i1stuy=aMω|zMizaωi2nduxy|iωjωx=i𝑔jy=aMω|aiEajN

Proof

Step Hyp Ref Expression
1 satf MVEWMSatE=recfVfxy|ufvfx=1stu𝑔1stvy=Mω2ndu2ndviωx=𝑔i1stuy=aMω|zMizaωi2nduxy|iωjωx=i𝑔jy=aMω|aiEajsucω
2 1 fveq1d MVEWMSatEN=recfVfxy|ufvfx=1stu𝑔1stvy=Mω2ndu2ndviωx=𝑔i1stuy=aMω|zMizaωi2nduxy|iωjωx=i𝑔jy=aMω|aiEajsucωN
3 2 3adant3 MVEWNsucωMSatEN=recfVfxy|ufvfx=1stu𝑔1stvy=Mω2ndu2ndviωx=𝑔i1stuy=aMω|zMizaωi2nduxy|iωjωx=i𝑔jy=aMω|aiEajsucωN
4 fvres NsucωrecfVfxy|ufvfx=1stu𝑔1stvy=Mω2ndu2ndviωx=𝑔i1stuy=aMω|zMizaωi2nduxy|iωjωx=i𝑔jy=aMω|aiEajsucωN=recfVfxy|ufvfx=1stu𝑔1stvy=Mω2ndu2ndviωx=𝑔i1stuy=aMω|zMizaωi2nduxy|iωjωx=i𝑔jy=aMω|aiEajN
5 4 3ad2ant3 MVEWNsucωrecfVfxy|ufvfx=1stu𝑔1stvy=Mω2ndu2ndviωx=𝑔i1stuy=aMω|zMizaωi2nduxy|iωjωx=i𝑔jy=aMω|aiEajsucωN=recfVfxy|ufvfx=1stu𝑔1stvy=Mω2ndu2ndviωx=𝑔i1stuy=aMω|zMizaωi2nduxy|iωjωx=i𝑔jy=aMω|aiEajN
6 3 5 eqtrd MVEWNsucωMSatEN=recfVfxy|ufvfx=1stu𝑔1stvy=Mω2ndu2ndviωx=𝑔i1stuy=aMω|zMizaωi2nduxy|iωjωx=i𝑔jy=aMω|aiEajN