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 ( ( 𝑀𝑉𝐸𝑊 ) → ( ( 𝑀 Sat 𝐸 ) ‘ ω ) = 𝑛 ∈ ω ( ( 𝑀 Sat 𝐸 ) ‘ 𝑛 ) )

Proof

Step Hyp Ref Expression
1 satf ( ( 𝑀𝑉𝐸𝑊 ) → ( 𝑀 Sat 𝐸 ) = ( rec ( ( 𝑓 ∈ V ↦ ( 𝑓 ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢𝑓 ( ∃ 𝑣𝑓 ( 𝑥 = ( ( 1st𝑢 ) ⊼𝑔 ( 1st𝑣 ) ) ∧ 𝑦 = ( ( 𝑀m ω ) ∖ ( ( 2nd𝑢 ) ∩ ( 2nd𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀m ω ) ∣ ∀ 𝑧𝑀 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd𝑢 ) } ) ) } ) ) , { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑥 = ( 𝑖𝑔 𝑗 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀m ω ) ∣ ( 𝑎𝑖 ) 𝐸 ( 𝑎𝑗 ) } ) } ) ↾ suc ω ) )
2 1 fveq1d ( ( 𝑀𝑉𝐸𝑊 ) → ( ( 𝑀 Sat 𝐸 ) ‘ ω ) = ( ( rec ( ( 𝑓 ∈ V ↦ ( 𝑓 ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢𝑓 ( ∃ 𝑣𝑓 ( 𝑥 = ( ( 1st𝑢 ) ⊼𝑔 ( 1st𝑣 ) ) ∧ 𝑦 = ( ( 𝑀m ω ) ∖ ( ( 2nd𝑢 ) ∩ ( 2nd𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀m ω ) ∣ ∀ 𝑧𝑀 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd𝑢 ) } ) ) } ) ) , { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑥 = ( 𝑖𝑔 𝑗 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀m ω ) ∣ ( 𝑎𝑖 ) 𝐸 ( 𝑎𝑗 ) } ) } ) ↾ suc ω ) ‘ ω ) )
3 omex ω ∈ V
4 3 sucid ω ∈ suc ω
5 fvres ( ω ∈ suc ω → ( ( rec ( ( 𝑓 ∈ V ↦ ( 𝑓 ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢𝑓 ( ∃ 𝑣𝑓 ( 𝑥 = ( ( 1st𝑢 ) ⊼𝑔 ( 1st𝑣 ) ) ∧ 𝑦 = ( ( 𝑀m ω ) ∖ ( ( 2nd𝑢 ) ∩ ( 2nd𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀m ω ) ∣ ∀ 𝑧𝑀 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd𝑢 ) } ) ) } ) ) , { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑥 = ( 𝑖𝑔 𝑗 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀m ω ) ∣ ( 𝑎𝑖 ) 𝐸 ( 𝑎𝑗 ) } ) } ) ↾ suc ω ) ‘ ω ) = ( rec ( ( 𝑓 ∈ V ↦ ( 𝑓 ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢𝑓 ( ∃ 𝑣𝑓 ( 𝑥 = ( ( 1st𝑢 ) ⊼𝑔 ( 1st𝑣 ) ) ∧ 𝑦 = ( ( 𝑀m ω ) ∖ ( ( 2nd𝑢 ) ∩ ( 2nd𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀m ω ) ∣ ∀ 𝑧𝑀 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd𝑢 ) } ) ) } ) ) , { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑥 = ( 𝑖𝑔 𝑗 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀m ω ) ∣ ( 𝑎𝑖 ) 𝐸 ( 𝑎𝑗 ) } ) } ) ‘ ω ) )
6 4 5 mp1i ( ( 𝑀𝑉𝐸𝑊 ) → ( ( rec ( ( 𝑓 ∈ V ↦ ( 𝑓 ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢𝑓 ( ∃ 𝑣𝑓 ( 𝑥 = ( ( 1st𝑢 ) ⊼𝑔 ( 1st𝑣 ) ) ∧ 𝑦 = ( ( 𝑀m ω ) ∖ ( ( 2nd𝑢 ) ∩ ( 2nd𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀m ω ) ∣ ∀ 𝑧𝑀 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd𝑢 ) } ) ) } ) ) , { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑥 = ( 𝑖𝑔 𝑗 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀m ω ) ∣ ( 𝑎𝑖 ) 𝐸 ( 𝑎𝑗 ) } ) } ) ↾ suc ω ) ‘ ω ) = ( rec ( ( 𝑓 ∈ V ↦ ( 𝑓 ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢𝑓 ( ∃ 𝑣𝑓 ( 𝑥 = ( ( 1st𝑢 ) ⊼𝑔 ( 1st𝑣 ) ) ∧ 𝑦 = ( ( 𝑀m ω ) ∖ ( ( 2nd𝑢 ) ∩ ( 2nd𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀m ω ) ∣ ∀ 𝑧𝑀 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd𝑢 ) } ) ) } ) ) , { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑥 = ( 𝑖𝑔 𝑗 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀m ω ) ∣ ( 𝑎𝑖 ) 𝐸 ( 𝑎𝑗 ) } ) } ) ‘ ω ) )
7 limom Lim ω
8 3 7 pm3.2i ( ω ∈ V ∧ Lim ω )
9 rdglim2a ( ( ω ∈ V ∧ Lim ω ) → ( rec ( ( 𝑓 ∈ V ↦ ( 𝑓 ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢𝑓 ( ∃ 𝑣𝑓 ( 𝑥 = ( ( 1st𝑢 ) ⊼𝑔 ( 1st𝑣 ) ) ∧ 𝑦 = ( ( 𝑀m ω ) ∖ ( ( 2nd𝑢 ) ∩ ( 2nd𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀m ω ) ∣ ∀ 𝑧𝑀 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd𝑢 ) } ) ) } ) ) , { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑥 = ( 𝑖𝑔 𝑗 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀m ω ) ∣ ( 𝑎𝑖 ) 𝐸 ( 𝑎𝑗 ) } ) } ) ‘ ω ) = 𝑛 ∈ ω ( rec ( ( 𝑓 ∈ V ↦ ( 𝑓 ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢𝑓 ( ∃ 𝑣𝑓 ( 𝑥 = ( ( 1st𝑢 ) ⊼𝑔 ( 1st𝑣 ) ) ∧ 𝑦 = ( ( 𝑀m ω ) ∖ ( ( 2nd𝑢 ) ∩ ( 2nd𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀m ω ) ∣ ∀ 𝑧𝑀 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd𝑢 ) } ) ) } ) ) , { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑥 = ( 𝑖𝑔 𝑗 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀m ω ) ∣ ( 𝑎𝑖 ) 𝐸 ( 𝑎𝑗 ) } ) } ) ‘ 𝑛 ) )
10 8 9 mp1i ( ( 𝑀𝑉𝐸𝑊 ) → ( rec ( ( 𝑓 ∈ V ↦ ( 𝑓 ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢𝑓 ( ∃ 𝑣𝑓 ( 𝑥 = ( ( 1st𝑢 ) ⊼𝑔 ( 1st𝑣 ) ) ∧ 𝑦 = ( ( 𝑀m ω ) ∖ ( ( 2nd𝑢 ) ∩ ( 2nd𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀m ω ) ∣ ∀ 𝑧𝑀 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd𝑢 ) } ) ) } ) ) , { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑥 = ( 𝑖𝑔 𝑗 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀m ω ) ∣ ( 𝑎𝑖 ) 𝐸 ( 𝑎𝑗 ) } ) } ) ‘ ω ) = 𝑛 ∈ ω ( rec ( ( 𝑓 ∈ V ↦ ( 𝑓 ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢𝑓 ( ∃ 𝑣𝑓 ( 𝑥 = ( ( 1st𝑢 ) ⊼𝑔 ( 1st𝑣 ) ) ∧ 𝑦 = ( ( 𝑀m ω ) ∖ ( ( 2nd𝑢 ) ∩ ( 2nd𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀m ω ) ∣ ∀ 𝑧𝑀 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd𝑢 ) } ) ) } ) ) , { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑥 = ( 𝑖𝑔 𝑗 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀m ω ) ∣ ( 𝑎𝑖 ) 𝐸 ( 𝑎𝑗 ) } ) } ) ‘ 𝑛 ) )
11 1 fveq1d ( ( 𝑀𝑉𝐸𝑊 ) → ( ( 𝑀 Sat 𝐸 ) ‘ 𝑛 ) = ( ( rec ( ( 𝑓 ∈ V ↦ ( 𝑓 ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢𝑓 ( ∃ 𝑣𝑓 ( 𝑥 = ( ( 1st𝑢 ) ⊼𝑔 ( 1st𝑣 ) ) ∧ 𝑦 = ( ( 𝑀m ω ) ∖ ( ( 2nd𝑢 ) ∩ ( 2nd𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀m ω ) ∣ ∀ 𝑧𝑀 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd𝑢 ) } ) ) } ) ) , { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑥 = ( 𝑖𝑔 𝑗 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀m ω ) ∣ ( 𝑎𝑖 ) 𝐸 ( 𝑎𝑗 ) } ) } ) ↾ suc ω ) ‘ 𝑛 ) )
12 11 adantr ( ( ( 𝑀𝑉𝐸𝑊 ) ∧ 𝑛 ∈ ω ) → ( ( 𝑀 Sat 𝐸 ) ‘ 𝑛 ) = ( ( rec ( ( 𝑓 ∈ V ↦ ( 𝑓 ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢𝑓 ( ∃ 𝑣𝑓 ( 𝑥 = ( ( 1st𝑢 ) ⊼𝑔 ( 1st𝑣 ) ) ∧ 𝑦 = ( ( 𝑀m ω ) ∖ ( ( 2nd𝑢 ) ∩ ( 2nd𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀m ω ) ∣ ∀ 𝑧𝑀 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd𝑢 ) } ) ) } ) ) , { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑥 = ( 𝑖𝑔 𝑗 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀m ω ) ∣ ( 𝑎𝑖 ) 𝐸 ( 𝑎𝑗 ) } ) } ) ↾ suc ω ) ‘ 𝑛 ) )
13 elelsuc ( 𝑛 ∈ ω → 𝑛 ∈ suc ω )
14 13 adantl ( ( ( 𝑀𝑉𝐸𝑊 ) ∧ 𝑛 ∈ ω ) → 𝑛 ∈ suc ω )
15 14 fvresd ( ( ( 𝑀𝑉𝐸𝑊 ) ∧ 𝑛 ∈ ω ) → ( ( rec ( ( 𝑓 ∈ V ↦ ( 𝑓 ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢𝑓 ( ∃ 𝑣𝑓 ( 𝑥 = ( ( 1st𝑢 ) ⊼𝑔 ( 1st𝑣 ) ) ∧ 𝑦 = ( ( 𝑀m ω ) ∖ ( ( 2nd𝑢 ) ∩ ( 2nd𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀m ω ) ∣ ∀ 𝑧𝑀 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd𝑢 ) } ) ) } ) ) , { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑥 = ( 𝑖𝑔 𝑗 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀m ω ) ∣ ( 𝑎𝑖 ) 𝐸 ( 𝑎𝑗 ) } ) } ) ↾ suc ω ) ‘ 𝑛 ) = ( rec ( ( 𝑓 ∈ V ↦ ( 𝑓 ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢𝑓 ( ∃ 𝑣𝑓 ( 𝑥 = ( ( 1st𝑢 ) ⊼𝑔 ( 1st𝑣 ) ) ∧ 𝑦 = ( ( 𝑀m ω ) ∖ ( ( 2nd𝑢 ) ∩ ( 2nd𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀m ω ) ∣ ∀ 𝑧𝑀 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd𝑢 ) } ) ) } ) ) , { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑥 = ( 𝑖𝑔 𝑗 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀m ω ) ∣ ( 𝑎𝑖 ) 𝐸 ( 𝑎𝑗 ) } ) } ) ‘ 𝑛 ) )
16 12 15 eqtr2d ( ( ( 𝑀𝑉𝐸𝑊 ) ∧ 𝑛 ∈ ω ) → ( rec ( ( 𝑓 ∈ V ↦ ( 𝑓 ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢𝑓 ( ∃ 𝑣𝑓 ( 𝑥 = ( ( 1st𝑢 ) ⊼𝑔 ( 1st𝑣 ) ) ∧ 𝑦 = ( ( 𝑀m ω ) ∖ ( ( 2nd𝑢 ) ∩ ( 2nd𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀m ω ) ∣ ∀ 𝑧𝑀 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd𝑢 ) } ) ) } ) ) , { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑥 = ( 𝑖𝑔 𝑗 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀m ω ) ∣ ( 𝑎𝑖 ) 𝐸 ( 𝑎𝑗 ) } ) } ) ‘ 𝑛 ) = ( ( 𝑀 Sat 𝐸 ) ‘ 𝑛 ) )
17 16 iuneq2dv ( ( 𝑀𝑉𝐸𝑊 ) → 𝑛 ∈ ω ( rec ( ( 𝑓 ∈ V ↦ ( 𝑓 ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢𝑓 ( ∃ 𝑣𝑓 ( 𝑥 = ( ( 1st𝑢 ) ⊼𝑔 ( 1st𝑣 ) ) ∧ 𝑦 = ( ( 𝑀m ω ) ∖ ( ( 2nd𝑢 ) ∩ ( 2nd𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀m ω ) ∣ ∀ 𝑧𝑀 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd𝑢 ) } ) ) } ) ) , { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑥 = ( 𝑖𝑔 𝑗 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀m ω ) ∣ ( 𝑎𝑖 ) 𝐸 ( 𝑎𝑗 ) } ) } ) ‘ 𝑛 ) = 𝑛 ∈ ω ( ( 𝑀 Sat 𝐸 ) ‘ 𝑛 ) )
18 10 17 eqtrd ( ( 𝑀𝑉𝐸𝑊 ) → ( rec ( ( 𝑓 ∈ V ↦ ( 𝑓 ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢𝑓 ( ∃ 𝑣𝑓 ( 𝑥 = ( ( 1st𝑢 ) ⊼𝑔 ( 1st𝑣 ) ) ∧ 𝑦 = ( ( 𝑀m ω ) ∖ ( ( 2nd𝑢 ) ∩ ( 2nd𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀m ω ) ∣ ∀ 𝑧𝑀 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd𝑢 ) } ) ) } ) ) , { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑥 = ( 𝑖𝑔 𝑗 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀m ω ) ∣ ( 𝑎𝑖 ) 𝐸 ( 𝑎𝑗 ) } ) } ) ‘ ω ) = 𝑛 ∈ ω ( ( 𝑀 Sat 𝐸 ) ‘ 𝑛 ) )
19 2 6 18 3eqtrd ( ( 𝑀𝑉𝐸𝑊 ) → ( ( 𝑀 Sat 𝐸 ) ‘ ω ) = 𝑛 ∈ ω ( ( 𝑀 Sat 𝐸 ) ‘ 𝑛 ) )