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 M V E W N suc ω M Sat E N = rec f V f x y | u f v f x = 1 st u 𝑔 1 st v y = M ω 2 nd u 2 nd v i ω x = 𝑔 i 1 st u y = a M ω | z M i z a ω i 2 nd u x y | i ω j ω x = i 𝑔 j y = a M ω | a i E a j N

Proof

Step Hyp Ref Expression
1 satf M V E W M Sat E = rec f V f x y | u f v f x = 1 st u 𝑔 1 st v y = M ω 2 nd u 2 nd v i ω x = 𝑔 i 1 st u y = a M ω | z M i z a ω i 2 nd u x y | i ω j ω x = i 𝑔 j y = a M ω | a i E a j suc ω
2 1 fveq1d M V E W M Sat E N = rec f V f x y | u f v f x = 1 st u 𝑔 1 st v y = M ω 2 nd u 2 nd v i ω x = 𝑔 i 1 st u y = a M ω | z M i z a ω i 2 nd u x y | i ω j ω x = i 𝑔 j y = a M ω | a i E a j suc ω N
3 2 3adant3 M V E W N suc ω M Sat E N = rec f V f x y | u f v f x = 1 st u 𝑔 1 st v y = M ω 2 nd u 2 nd v i ω x = 𝑔 i 1 st u y = a M ω | z M i z a ω i 2 nd u x y | i ω j ω x = i 𝑔 j y = a M ω | a i E a j suc ω N
4 fvres N suc ω rec f V f x y | u f v f x = 1 st u 𝑔 1 st v y = M ω 2 nd u 2 nd v i ω x = 𝑔 i 1 st u y = a M ω | z M i z a ω i 2 nd u x y | i ω j ω x = i 𝑔 j y = a M ω | a i E a j suc ω N = rec f V f x y | u f v f x = 1 st u 𝑔 1 st v y = M ω 2 nd u 2 nd v i ω x = 𝑔 i 1 st u y = a M ω | z M i z a ω i 2 nd u x y | i ω j ω x = i 𝑔 j y = a M ω | a i E a j N
5 4 3ad2ant3 M V E W N suc ω rec f V f x y | u f v f x = 1 st u 𝑔 1 st v y = M ω 2 nd u 2 nd v i ω x = 𝑔 i 1 st u y = a M ω | z M i z a ω i 2 nd u x y | i ω j ω x = i 𝑔 j y = a M ω | a i E a j suc ω N = rec f V f x y | u f v f x = 1 st u 𝑔 1 st v y = M ω 2 nd u 2 nd v i ω x = 𝑔 i 1 st u y = a M ω | z M i z a ω i 2 nd u x y | i ω j ω x = i 𝑔 j y = a M ω | a i E a j N
6 3 5 eqtrd M V E W N suc ω M Sat E N = rec f V f x y | u f v f x = 1 st u 𝑔 1 st v y = M ω 2 nd u 2 nd v i ω x = 𝑔 i 1 st u y = a M ω | z M i z a ω i 2 nd u x y | i ω j ω x = i 𝑔 j y = a M ω | a i E a j N