Step |
Hyp |
Ref |
Expression |
1 |
|
satf0 |
⊢ ( ∅ Sat ∅ ) = ( rec ( ( 𝑓 ∈ V ↦ ( 𝑓 ∪ { 〈 𝑥 , 𝑦 〉 ∣ ( 𝑦 = ∅ ∧ ∃ 𝑢 ∈ 𝑓 ( ∃ 𝑣 ∈ 𝑓 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ) ) } ) ) , { 〈 𝑥 , 𝑦 〉 ∣ ( 𝑦 = ∅ ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖 ∈𝑔 𝑗 ) ) } ) ↾ suc ω ) |
2 |
1
|
fveq1i |
⊢ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) = ( ( rec ( ( 𝑓 ∈ V ↦ ( 𝑓 ∪ { 〈 𝑥 , 𝑦 〉 ∣ ( 𝑦 = ∅ ∧ ∃ 𝑢 ∈ 𝑓 ( ∃ 𝑣 ∈ 𝑓 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ) ) } ) ) , { 〈 𝑥 , 𝑦 〉 ∣ ( 𝑦 = ∅ ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖 ∈𝑔 𝑗 ) ) } ) ↾ suc ω ) ‘ 𝑁 ) |
3 |
|
fvres |
⊢ ( 𝑁 ∈ suc ω → ( ( rec ( ( 𝑓 ∈ V ↦ ( 𝑓 ∪ { 〈 𝑥 , 𝑦 〉 ∣ ( 𝑦 = ∅ ∧ ∃ 𝑢 ∈ 𝑓 ( ∃ 𝑣 ∈ 𝑓 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ) ) } ) ) , { 〈 𝑥 , 𝑦 〉 ∣ ( 𝑦 = ∅ ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖 ∈𝑔 𝑗 ) ) } ) ↾ suc ω ) ‘ 𝑁 ) = ( rec ( ( 𝑓 ∈ V ↦ ( 𝑓 ∪ { 〈 𝑥 , 𝑦 〉 ∣ ( 𝑦 = ∅ ∧ ∃ 𝑢 ∈ 𝑓 ( ∃ 𝑣 ∈ 𝑓 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ) ) } ) ) , { 〈 𝑥 , 𝑦 〉 ∣ ( 𝑦 = ∅ ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖 ∈𝑔 𝑗 ) ) } ) ‘ 𝑁 ) ) |
4 |
2 3
|
syl5eq |
⊢ ( 𝑁 ∈ suc ω → ( ( ∅ Sat ∅ ) ‘ 𝑁 ) = ( rec ( ( 𝑓 ∈ V ↦ ( 𝑓 ∪ { 〈 𝑥 , 𝑦 〉 ∣ ( 𝑦 = ∅ ∧ ∃ 𝑢 ∈ 𝑓 ( ∃ 𝑣 ∈ 𝑓 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ) ) } ) ) , { 〈 𝑥 , 𝑦 〉 ∣ ( 𝑦 = ∅ ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖 ∈𝑔 𝑗 ) ) } ) ‘ 𝑁 ) ) |