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 ( ( 𝑀𝑉𝐸𝑊 ) → ( 𝑀 Sat 𝐸 ) Fn suc ω )

Proof

Step Hyp Ref Expression
1 rdgfnon rec ( ( 𝑓 ∈ V ↦ ( 𝑓 ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢𝑓 ( ∃ 𝑣𝑓 ( 𝑥 = ( ( 1st𝑢 ) ⊼𝑔 ( 1st𝑣 ) ) ∧ 𝑦 = ( ( 𝑀m ω ) ∖ ( ( 2nd𝑢 ) ∩ ( 2nd𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀m ω ) ∣ ∀ 𝑧𝑀 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd𝑢 ) } ) ) } ) ) , { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑥 = ( 𝑖𝑔 𝑗 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀m ω ) ∣ ( 𝑎𝑖 ) 𝐸 ( 𝑎𝑗 ) } ) } ) Fn On
2 1 a1i ( ( 𝑀𝑉𝐸𝑊 ) → rec ( ( 𝑓 ∈ V ↦ ( 𝑓 ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢𝑓 ( ∃ 𝑣𝑓 ( 𝑥 = ( ( 1st𝑢 ) ⊼𝑔 ( 1st𝑣 ) ) ∧ 𝑦 = ( ( 𝑀m ω ) ∖ ( ( 2nd𝑢 ) ∩ ( 2nd𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀m ω ) ∣ ∀ 𝑧𝑀 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd𝑢 ) } ) ) } ) ) , { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑥 = ( 𝑖𝑔 𝑗 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀m ω ) ∣ ( 𝑎𝑖 ) 𝐸 ( 𝑎𝑗 ) } ) } ) 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 ( ( 𝑀𝑉𝐸𝑊 ) → suc ω ⊆ On )
8 2 7 fnssresd ( ( 𝑀𝑉𝐸𝑊 ) → ( rec ( ( 𝑓 ∈ V ↦ ( 𝑓 ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢𝑓 ( ∃ 𝑣𝑓 ( 𝑥 = ( ( 1st𝑢 ) ⊼𝑔 ( 1st𝑣 ) ) ∧ 𝑦 = ( ( 𝑀m ω ) ∖ ( ( 2nd𝑢 ) ∩ ( 2nd𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀m ω ) ∣ ∀ 𝑧𝑀 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd𝑢 ) } ) ) } ) ) , { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑥 = ( 𝑖𝑔 𝑗 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀m ω ) ∣ ( 𝑎𝑖 ) 𝐸 ( 𝑎𝑗 ) } ) } ) ↾ suc ω ) Fn suc ω )
9 satf ( ( 𝑀𝑉𝐸𝑊 ) → ( 𝑀 Sat 𝐸 ) = ( rec ( ( 𝑓 ∈ V ↦ ( 𝑓 ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢𝑓 ( ∃ 𝑣𝑓 ( 𝑥 = ( ( 1st𝑢 ) ⊼𝑔 ( 1st𝑣 ) ) ∧ 𝑦 = ( ( 𝑀m ω ) ∖ ( ( 2nd𝑢 ) ∩ ( 2nd𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀m ω ) ∣ ∀ 𝑧𝑀 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd𝑢 ) } ) ) } ) ) , { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑥 = ( 𝑖𝑔 𝑗 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀m ω ) ∣ ( 𝑎𝑖 ) 𝐸 ( 𝑎𝑗 ) } ) } ) ↾ suc ω ) )
10 9 fneq1d ( ( 𝑀𝑉𝐸𝑊 ) → ( ( 𝑀 Sat 𝐸 ) Fn suc ω ↔ ( rec ( ( 𝑓 ∈ V ↦ ( 𝑓 ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢𝑓 ( ∃ 𝑣𝑓 ( 𝑥 = ( ( 1st𝑢 ) ⊼𝑔 ( 1st𝑣 ) ) ∧ 𝑦 = ( ( 𝑀m ω ) ∖ ( ( 2nd𝑢 ) ∩ ( 2nd𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀m ω ) ∣ ∀ 𝑧𝑀 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd𝑢 ) } ) ) } ) ) , { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑥 = ( 𝑖𝑔 𝑗 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀m ω ) ∣ ( 𝑎𝑖 ) 𝐸 ( 𝑎𝑗 ) } ) } ) ↾ suc ω ) Fn suc ω ) )
11 8 10 mpbird ( ( 𝑀𝑉𝐸𝑊 ) → ( 𝑀 Sat 𝐸 ) Fn suc ω )