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 ω ) |