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 𝐸 ) ‘ 𝑛 ) ) |