Metamath Proof Explorer


Theorem satfn

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

Ref Expression
Assertion satfn M V E W M Sat E Fn suc ω

Proof

Step Hyp Ref Expression
1 rdgfnon 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 Fn On
2 1 a1i 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 Fn On
3 ordom Ord ω
4 ordsuc Ord ω Ord suc ω
5 3 4 mpbi Ord suc ω
6 ordsson Ord suc ω suc ω On
7 5 6 mp1i M V E W suc ω On
8 2 7 fnssresd 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 ω Fn suc ω
9 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 ω
10 9 fneq1d M V E W M Sat E Fn 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 ω Fn suc ω
11 8 10 mpbird M V E W M Sat E Fn suc ω