Metamath Proof Explorer


Theorem satom

Description: The satisfaction predicate for wff codes in the model M and the binary relation E on M at omega ( _om ). (Contributed by AV, 6-Oct-2023)

Ref Expression
Assertion satom M V E W M Sat E ω = n ω M Sat E 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 ω = 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 ω ω
3 omex ω V
4 3 sucid ω suc ω
5 fvres ω 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 ω ω = 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 ω
6 4 5 mp1i M V E W 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 ω ω = 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 ω
7 limom Lim ω
8 3 7 pm3.2i ω V Lim ω
9 rdglim2a ω V Lim ω 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 ω 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
10 8 9 mp1i M V E W 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 ω 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
11 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
12 11 adantr M V E W n ω 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
13 elelsuc n ω n suc ω
14 13 adantl M V E W n ω n suc ω
15 14 fvresd M V E W 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 = 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
16 12 15 eqtr2d M V E W 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 = M Sat E n
17 16 iuneq2dv M V E W 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 = n ω M Sat E n
18 10 17 eqtrd M V E W 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 ω M Sat E n
19 2 6 18 3eqtrd M V E W M Sat E ω = n ω M Sat E n