Step | Hyp | Ref
| Expression |
1 | | df-fmla 33020 |
. . 3
⊢ Fmla =
(𝑛 ∈ suc ω
↦ dom ((∅ Sat ∅)‘𝑛)) |
2 | | fveq2 6717 |
. . . 4
⊢ (𝑛 = suc 𝑁 → ((∅ Sat ∅)‘𝑛) = ((∅ Sat
∅)‘suc 𝑁)) |
3 | 2 | dmeqd 5774 |
. . 3
⊢ (𝑛 = suc 𝑁 → dom ((∅ Sat
∅)‘𝑛) = dom
((∅ Sat ∅)‘suc 𝑁)) |
4 | | omsucelsucb 8194 |
. . . 4
⊢ (𝑁 ∈ ω ↔ suc 𝑁 ∈ suc
ω) |
5 | 4 | biimpi 219 |
. . 3
⊢ (𝑁 ∈ ω → suc 𝑁 ∈ suc
ω) |
6 | | fvex 6730 |
. . . . 5
⊢ ((∅
Sat ∅)‘suc 𝑁)
∈ V |
7 | 6 | dmex 7689 |
. . . 4
⊢ dom
((∅ Sat ∅)‘suc 𝑁) ∈ V |
8 | 7 | a1i 11 |
. . 3
⊢ (𝑁 ∈ ω → dom
((∅ Sat ∅)‘suc 𝑁) ∈ V) |
9 | 1, 3, 5, 8 | fvmptd3 6841 |
. 2
⊢ (𝑁 ∈ ω →
(Fmla‘suc 𝑁) = dom
((∅ Sat ∅)‘suc 𝑁)) |
10 | | satf0sucom 33048 |
. . . . 5
⊢ (suc
𝑁 ∈ suc ω →
((∅ Sat ∅)‘suc 𝑁) = (rec((𝑓 ∈ V ↦ (𝑓 ∪ {〈𝑥, 𝑦〉 ∣ (𝑦 = ∅ ∧ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))})), {〈𝑥, 𝑦〉 ∣ (𝑦 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗))})‘suc 𝑁)) |
11 | 5, 10 | syl 17 |
. . . 4
⊢ (𝑁 ∈ ω → ((∅
Sat ∅)‘suc 𝑁) =
(rec((𝑓 ∈ V ↦
(𝑓 ∪ {〈𝑥, 𝑦〉 ∣ (𝑦 = ∅ ∧ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))})), {〈𝑥, 𝑦〉 ∣ (𝑦 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗))})‘suc 𝑁)) |
12 | | nnon 7650 |
. . . . 5
⊢ (𝑁 ∈ ω → 𝑁 ∈ On) |
13 | | rdgsuc 8160 |
. . . . 5
⊢ (𝑁 ∈ On → (rec((𝑓 ∈ V ↦ (𝑓 ∪ {〈𝑥, 𝑦〉 ∣ (𝑦 = ∅ ∧ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))})), {〈𝑥, 𝑦〉 ∣ (𝑦 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗))})‘suc 𝑁) = ((𝑓 ∈ V ↦ (𝑓 ∪ {〈𝑥, 𝑦〉 ∣ (𝑦 = ∅ ∧ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))}))‘(rec((𝑓 ∈ V ↦ (𝑓 ∪ {〈𝑥, 𝑦〉 ∣ (𝑦 = ∅ ∧ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))})), {〈𝑥, 𝑦〉 ∣ (𝑦 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗))})‘𝑁))) |
14 | 12, 13 | syl 17 |
. . . 4
⊢ (𝑁 ∈ ω →
(rec((𝑓 ∈ V ↦
(𝑓 ∪ {〈𝑥, 𝑦〉 ∣ (𝑦 = ∅ ∧ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))})), {〈𝑥, 𝑦〉 ∣ (𝑦 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗))})‘suc 𝑁) = ((𝑓 ∈ V ↦ (𝑓 ∪ {〈𝑥, 𝑦〉 ∣ (𝑦 = ∅ ∧ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))}))‘(rec((𝑓 ∈ V ↦ (𝑓 ∪ {〈𝑥, 𝑦〉 ∣ (𝑦 = ∅ ∧ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))})), {〈𝑥, 𝑦〉 ∣ (𝑦 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗))})‘𝑁))) |
15 | 11, 14 | eqtrd 2777 |
. . 3
⊢ (𝑁 ∈ ω → ((∅
Sat ∅)‘suc 𝑁) =
((𝑓 ∈ V ↦ (𝑓 ∪ {〈𝑥, 𝑦〉 ∣ (𝑦 = ∅ ∧ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))}))‘(rec((𝑓 ∈ V ↦ (𝑓 ∪ {〈𝑥, 𝑦〉 ∣ (𝑦 = ∅ ∧ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))})), {〈𝑥, 𝑦〉 ∣ (𝑦 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗))})‘𝑁))) |
16 | 15 | dmeqd 5774 |
. 2
⊢ (𝑁 ∈ ω → dom
((∅ Sat ∅)‘suc 𝑁) = dom ((𝑓 ∈ V ↦ (𝑓 ∪ {〈𝑥, 𝑦〉 ∣ (𝑦 = ∅ ∧ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))}))‘(rec((𝑓 ∈ V ↦ (𝑓 ∪ {〈𝑥, 𝑦〉 ∣ (𝑦 = ∅ ∧ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))})), {〈𝑥, 𝑦〉 ∣ (𝑦 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗))})‘𝑁))) |
17 | | elelsuc 6285 |
. . . . . . . 8
⊢ (𝑁 ∈ ω → 𝑁 ∈ suc
ω) |
18 | | satf0sucom 33048 |
. . . . . . . . 9
⊢ (𝑁 ∈ suc ω →
((∅ Sat ∅)‘𝑁) = (rec((𝑓 ∈ V ↦ (𝑓 ∪ {〈𝑥, 𝑦〉 ∣ (𝑦 = ∅ ∧ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))})), {〈𝑥, 𝑦〉 ∣ (𝑦 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗))})‘𝑁)) |
19 | 18 | eqcomd 2743 |
. . . . . . . 8
⊢ (𝑁 ∈ suc ω →
(rec((𝑓 ∈ V ↦
(𝑓 ∪ {〈𝑥, 𝑦〉 ∣ (𝑦 = ∅ ∧ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))})), {〈𝑥, 𝑦〉 ∣ (𝑦 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗))})‘𝑁) = ((∅ Sat ∅)‘𝑁)) |
20 | 17, 19 | syl 17 |
. . . . . . 7
⊢ (𝑁 ∈ ω →
(rec((𝑓 ∈ V ↦
(𝑓 ∪ {〈𝑥, 𝑦〉 ∣ (𝑦 = ∅ ∧ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))})), {〈𝑥, 𝑦〉 ∣ (𝑦 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗))})‘𝑁) = ((∅ Sat ∅)‘𝑁)) |
21 | 20 | fveq2d 6721 |
. . . . . 6
⊢ (𝑁 ∈ ω → ((𝑓 ∈ V ↦ (𝑓 ∪ {〈𝑥, 𝑦〉 ∣ (𝑦 = ∅ ∧ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))}))‘(rec((𝑓 ∈ V ↦ (𝑓 ∪ {〈𝑥, 𝑦〉 ∣ (𝑦 = ∅ ∧ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))})), {〈𝑥, 𝑦〉 ∣ (𝑦 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗))})‘𝑁)) = ((𝑓 ∈ V ↦ (𝑓 ∪ {〈𝑥, 𝑦〉 ∣ (𝑦 = ∅ ∧ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))}))‘((∅ Sat
∅)‘𝑁))) |
22 | | eqidd 2738 |
. . . . . . 7
⊢ (𝑁 ∈ ω → (𝑓 ∈ V ↦ (𝑓 ∪ {〈𝑥, 𝑦〉 ∣ (𝑦 = ∅ ∧ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))})) = (𝑓 ∈ V ↦ (𝑓 ∪ {〈𝑥, 𝑦〉 ∣ (𝑦 = ∅ ∧ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))}))) |
23 | | id 22 |
. . . . . . . . 9
⊢ (𝑓 = ((∅ Sat
∅)‘𝑁) →
𝑓 = ((∅ Sat
∅)‘𝑁)) |
24 | | rexeq 3320 |
. . . . . . . . . . . . 13
⊢ (𝑓 = ((∅ Sat
∅)‘𝑁) →
(∃𝑣 ∈ 𝑓 𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ↔
∃𝑣 ∈ ((∅
Sat ∅)‘𝑁)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)))) |
25 | 24 | orbi1d 917 |
. . . . . . . . . . . 12
⊢ (𝑓 = ((∅ Sat
∅)‘𝑁) →
((∃𝑣 ∈ 𝑓 𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)) ↔ (∃𝑣 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))) |
26 | 25 | rexeqbi1dv 3318 |
. . . . . . . . . . 11
⊢ (𝑓 = ((∅ Sat
∅)‘𝑁) →
(∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)) ↔ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑁)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))) |
27 | 26 | anbi2d 632 |
. . . . . . . . . 10
⊢ (𝑓 = ((∅ Sat
∅)‘𝑁) →
((𝑦 = ∅ ∧
∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢))) ↔ (𝑦 = ∅ ∧ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑁)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢))))) |
28 | 27 | opabbidv 5119 |
. . . . . . . . 9
⊢ (𝑓 = ((∅ Sat
∅)‘𝑁) →
{〈𝑥, 𝑦〉 ∣ (𝑦 = ∅ ∧ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))} = {〈𝑥, 𝑦〉 ∣ (𝑦 = ∅ ∧ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑁)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))}) |
29 | 23, 28 | uneq12d 4078 |
. . . . . . . 8
⊢ (𝑓 = ((∅ Sat
∅)‘𝑁) →
(𝑓 ∪ {〈𝑥, 𝑦〉 ∣ (𝑦 = ∅ ∧ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))}) = (((∅ Sat ∅)‘𝑁) ∪ {〈𝑥, 𝑦〉 ∣ (𝑦 = ∅ ∧ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑁)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))})) |
30 | 29 | adantl 485 |
. . . . . . 7
⊢ ((𝑁 ∈ ω ∧ 𝑓 = ((∅ Sat
∅)‘𝑁)) →
(𝑓 ∪ {〈𝑥, 𝑦〉 ∣ (𝑦 = ∅ ∧ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))}) = (((∅ Sat ∅)‘𝑁) ∪ {〈𝑥, 𝑦〉 ∣ (𝑦 = ∅ ∧ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑁)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))})) |
31 | | fvex 6730 |
. . . . . . . 8
⊢ ((∅
Sat ∅)‘𝑁)
∈ V |
32 | 31 | a1i 11 |
. . . . . . 7
⊢ (𝑁 ∈ ω → ((∅
Sat ∅)‘𝑁)
∈ V) |
33 | | peano1 7667 |
. . . . . . . . . . . . 13
⊢ ∅
∈ ω |
34 | | eleq1 2825 |
. . . . . . . . . . . . 13
⊢ (𝑦 = ∅ → (𝑦 ∈ ω ↔ ∅
∈ ω)) |
35 | 33, 34 | mpbiri 261 |
. . . . . . . . . . . 12
⊢ (𝑦 = ∅ → 𝑦 ∈
ω) |
36 | 35 | adantr 484 |
. . . . . . . . . . 11
⊢ ((𝑦 = ∅ ∧ ∃𝑢 ∈ ((∅ Sat
∅)‘𝑁)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢))) → 𝑦 ∈ ω) |
37 | 36 | pm4.71ri 564 |
. . . . . . . . . 10
⊢ ((𝑦 = ∅ ∧ ∃𝑢 ∈ ((∅ Sat
∅)‘𝑁)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢))) ↔ (𝑦 ∈ ω ∧ (𝑦 = ∅ ∧ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑁)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢))))) |
38 | 37 | opabbii 5120 |
. . . . . . . . 9
⊢
{〈𝑥, 𝑦〉 ∣ (𝑦 = ∅ ∧ ∃𝑢 ∈ ((∅ Sat
∅)‘𝑁)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))} = {〈𝑥, 𝑦〉 ∣ (𝑦 ∈ ω ∧ (𝑦 = ∅ ∧ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑁)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢))))} |
39 | | omex 9258 |
. . . . . . . . . . . 12
⊢ ω
∈ V |
40 | | id 22 |
. . . . . . . . . . . . 13
⊢ (ω
∈ V → ω ∈ V) |
41 | | unab 4213 |
. . . . . . . . . . . . . . . . 17
⊢ ({𝑥 ∣ ∃𝑣 ∈ ((∅ Sat
∅)‘𝑁)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣))} ∪ {𝑥 ∣ ∃𝑖 ∈ ω 𝑥 =
∀𝑔𝑖(1st ‘𝑢)}) = {𝑥 ∣ (∃𝑣 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢))} |
42 | 31 | abrexex 7735 |
. . . . . . . . . . . . . . . . . 18
⊢ {𝑥 ∣ ∃𝑣 ∈ ((∅ Sat
∅)‘𝑁)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣))} ∈
V |
43 | 39 | abrexex 7735 |
. . . . . . . . . . . . . . . . . 18
⊢ {𝑥 ∣ ∃𝑖 ∈ ω 𝑥 =
∀𝑔𝑖(1st ‘𝑢)} ∈ V |
44 | 42, 43 | unex 7531 |
. . . . . . . . . . . . . . . . 17
⊢ ({𝑥 ∣ ∃𝑣 ∈ ((∅ Sat
∅)‘𝑁)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣))} ∪ {𝑥 ∣ ∃𝑖 ∈ ω 𝑥 =
∀𝑔𝑖(1st ‘𝑢)}) ∈ V |
45 | 41, 44 | eqeltrri 2835 |
. . . . . . . . . . . . . . . 16
⊢ {𝑥 ∣ (∃𝑣 ∈ ((∅ Sat
∅)‘𝑁)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢))} ∈ V |
46 | 45 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢
(((ω ∈ V ∧ 𝑦 ∈ ω) ∧ 𝑢 ∈ ((∅ Sat ∅)‘𝑁)) → {𝑥 ∣ (∃𝑣 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢))} ∈ V) |
47 | 46 | ralrimiva 3105 |
. . . . . . . . . . . . . 14
⊢ ((ω
∈ V ∧ 𝑦 ∈
ω) → ∀𝑢
∈ ((∅ Sat ∅)‘𝑁){𝑥 ∣ (∃𝑣 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢))} ∈ V) |
48 | | abrexex2g 7737 |
. . . . . . . . . . . . . 14
⊢
((((∅ Sat ∅)‘𝑁) ∈ V ∧ ∀𝑢 ∈ ((∅ Sat ∅)‘𝑁){𝑥 ∣ (∃𝑣 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢))} ∈ V) → {𝑥 ∣ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑁)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢))} ∈ V) |
49 | 31, 47, 48 | sylancr 590 |
. . . . . . . . . . . . 13
⊢ ((ω
∈ V ∧ 𝑦 ∈
ω) → {𝑥 ∣
∃𝑢 ∈ ((∅
Sat ∅)‘𝑁)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢))} ∈ V) |
50 | 40, 49 | opabex3rd 7739 |
. . . . . . . . . . . 12
⊢ (ω
∈ V → {〈𝑥,
𝑦〉 ∣ (𝑦 ∈ ω ∧
∃𝑢 ∈ ((∅
Sat ∅)‘𝑁)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))} ∈ V) |
51 | 39, 50 | ax-mp 5 |
. . . . . . . . . . 11
⊢
{〈𝑥, 𝑦〉 ∣ (𝑦 ∈ ω ∧
∃𝑢 ∈ ((∅
Sat ∅)‘𝑁)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))} ∈ V |
52 | | simpr 488 |
. . . . . . . . . . . . 13
⊢ ((𝑦 = ∅ ∧ ∃𝑢 ∈ ((∅ Sat
∅)‘𝑁)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢))) → ∃𝑢 ∈ ((∅ Sat ∅)‘𝑁)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢))) |
53 | 52 | anim2i 620 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ ω ∧ (𝑦 = ∅ ∧ ∃𝑢 ∈ ((∅ Sat
∅)‘𝑁)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))) → (𝑦 ∈ ω ∧ ∃𝑢 ∈ ((∅ Sat
∅)‘𝑁)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))) |
54 | 53 | ssopab2i 5431 |
. . . . . . . . . . 11
⊢
{〈𝑥, 𝑦〉 ∣ (𝑦 ∈ ω ∧ (𝑦 = ∅ ∧ ∃𝑢 ∈ ((∅ Sat
∅)‘𝑁)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢))))} ⊆ {〈𝑥, 𝑦〉 ∣ (𝑦 ∈ ω ∧ ∃𝑢 ∈ ((∅ Sat
∅)‘𝑁)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))} |
55 | 51, 54 | ssexi 5215 |
. . . . . . . . . 10
⊢
{〈𝑥, 𝑦〉 ∣ (𝑦 ∈ ω ∧ (𝑦 = ∅ ∧ ∃𝑢 ∈ ((∅ Sat
∅)‘𝑁)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢))))} ∈ V |
56 | 55 | a1i 11 |
. . . . . . . . 9
⊢ (𝑁 ∈ ω →
{〈𝑥, 𝑦〉 ∣ (𝑦 ∈ ω ∧ (𝑦 = ∅ ∧ ∃𝑢 ∈ ((∅ Sat
∅)‘𝑁)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢))))} ∈ V) |
57 | 38, 56 | eqeltrid 2842 |
. . . . . . . 8
⊢ (𝑁 ∈ ω →
{〈𝑥, 𝑦〉 ∣ (𝑦 = ∅ ∧ ∃𝑢 ∈ ((∅ Sat
∅)‘𝑁)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))} ∈ V) |
58 | | unexg 7534 |
. . . . . . . 8
⊢
((((∅ Sat ∅)‘𝑁) ∈ V ∧ {〈𝑥, 𝑦〉 ∣ (𝑦 = ∅ ∧ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑁)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))} ∈ V) → (((∅ Sat
∅)‘𝑁) ∪
{〈𝑥, 𝑦〉 ∣ (𝑦 = ∅ ∧ ∃𝑢 ∈ ((∅ Sat
∅)‘𝑁)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))}) ∈ V) |
59 | 31, 57, 58 | sylancr 590 |
. . . . . . 7
⊢ (𝑁 ∈ ω →
(((∅ Sat ∅)‘𝑁) ∪ {〈𝑥, 𝑦〉 ∣ (𝑦 = ∅ ∧ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑁)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))}) ∈ V) |
60 | 22, 30, 32, 59 | fvmptd 6825 |
. . . . . 6
⊢ (𝑁 ∈ ω → ((𝑓 ∈ V ↦ (𝑓 ∪ {〈𝑥, 𝑦〉 ∣ (𝑦 = ∅ ∧ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))}))‘((∅ Sat
∅)‘𝑁)) =
(((∅ Sat ∅)‘𝑁) ∪ {〈𝑥, 𝑦〉 ∣ (𝑦 = ∅ ∧ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑁)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))})) |
61 | 21, 60 | eqtrd 2777 |
. . . . 5
⊢ (𝑁 ∈ ω → ((𝑓 ∈ V ↦ (𝑓 ∪ {〈𝑥, 𝑦〉 ∣ (𝑦 = ∅ ∧ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))}))‘(rec((𝑓 ∈ V ↦ (𝑓 ∪ {〈𝑥, 𝑦〉 ∣ (𝑦 = ∅ ∧ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))})), {〈𝑥, 𝑦〉 ∣ (𝑦 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗))})‘𝑁)) = (((∅ Sat ∅)‘𝑁) ∪ {〈𝑥, 𝑦〉 ∣ (𝑦 = ∅ ∧ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑁)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))})) |
62 | 61 | dmeqd 5774 |
. . . 4
⊢ (𝑁 ∈ ω → dom
((𝑓 ∈ V ↦ (𝑓 ∪ {〈𝑥, 𝑦〉 ∣ (𝑦 = ∅ ∧ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))}))‘(rec((𝑓 ∈ V ↦ (𝑓 ∪ {〈𝑥, 𝑦〉 ∣ (𝑦 = ∅ ∧ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))})), {〈𝑥, 𝑦〉 ∣ (𝑦 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗))})‘𝑁)) = dom (((∅ Sat ∅)‘𝑁) ∪ {〈𝑥, 𝑦〉 ∣ (𝑦 = ∅ ∧ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑁)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))})) |
63 | | dmun 5779 |
. . . 4
⊢ dom
(((∅ Sat ∅)‘𝑁) ∪ {〈𝑥, 𝑦〉 ∣ (𝑦 = ∅ ∧ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑁)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))}) = (dom ((∅ Sat
∅)‘𝑁) ∪ dom
{〈𝑥, 𝑦〉 ∣ (𝑦 = ∅ ∧ ∃𝑢 ∈ ((∅ Sat
∅)‘𝑁)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))}) |
64 | 62, 63 | eqtrdi 2794 |
. . 3
⊢ (𝑁 ∈ ω → dom
((𝑓 ∈ V ↦ (𝑓 ∪ {〈𝑥, 𝑦〉 ∣ (𝑦 = ∅ ∧ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))}))‘(rec((𝑓 ∈ V ↦ (𝑓 ∪ {〈𝑥, 𝑦〉 ∣ (𝑦 = ∅ ∧ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))})), {〈𝑥, 𝑦〉 ∣ (𝑦 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗))})‘𝑁)) = (dom ((∅ Sat ∅)‘𝑁) ∪ dom {〈𝑥, 𝑦〉 ∣ (𝑦 = ∅ ∧ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑁)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))})) |
65 | | fmlafv 33055 |
. . . . . 6
⊢ (𝑁 ∈ suc ω →
(Fmla‘𝑁) = dom
((∅ Sat ∅)‘𝑁)) |
66 | 17, 65 | syl 17 |
. . . . 5
⊢ (𝑁 ∈ ω →
(Fmla‘𝑁) = dom
((∅ Sat ∅)‘𝑁)) |
67 | 66 | eqcomd 2743 |
. . . 4
⊢ (𝑁 ∈ ω → dom
((∅ Sat ∅)‘𝑁) = (Fmla‘𝑁)) |
68 | | dmopab 5784 |
. . . . . 6
⊢ dom
{〈𝑥, 𝑦〉 ∣ (𝑦 = ∅ ∧ ∃𝑢 ∈ ((∅ Sat
∅)‘𝑁)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))} = {𝑥 ∣ ∃𝑦(𝑦 = ∅ ∧ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑁)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))} |
69 | 68 | a1i 11 |
. . . . 5
⊢ (𝑁 ∈ ω → dom
{〈𝑥, 𝑦〉 ∣ (𝑦 = ∅ ∧ ∃𝑢 ∈ ((∅ Sat
∅)‘𝑁)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))} = {𝑥 ∣ ∃𝑦(𝑦 = ∅ ∧ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑁)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))}) |
70 | | 0ex 5200 |
. . . . . . . 8
⊢ ∅
∈ V |
71 | 70 | isseti 3423 |
. . . . . . 7
⊢
∃𝑦 𝑦 = ∅ |
72 | | 19.41v 1958 |
. . . . . . 7
⊢
(∃𝑦(𝑦 = ∅ ∧ ∃𝑢 ∈ ((∅ Sat
∅)‘𝑁)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢))) ↔ (∃𝑦 𝑦 = ∅ ∧ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑁)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))) |
73 | 71, 72 | mpbiran 709 |
. . . . . 6
⊢
(∃𝑦(𝑦 = ∅ ∧ ∃𝑢 ∈ ((∅ Sat
∅)‘𝑁)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢))) ↔ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑁)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢))) |
74 | 73 | abbii 2808 |
. . . . 5
⊢ {𝑥 ∣ ∃𝑦(𝑦 = ∅ ∧ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑁)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))} = {𝑥 ∣ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑁)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢))} |
75 | 69, 74 | eqtrdi 2794 |
. . . 4
⊢ (𝑁 ∈ ω → dom
{〈𝑥, 𝑦〉 ∣ (𝑦 = ∅ ∧ ∃𝑢 ∈ ((∅ Sat
∅)‘𝑁)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))} = {𝑥 ∣ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑁)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢))}) |
76 | 67, 75 | uneq12d 4078 |
. . 3
⊢ (𝑁 ∈ ω → (dom
((∅ Sat ∅)‘𝑁) ∪ dom {〈𝑥, 𝑦〉 ∣ (𝑦 = ∅ ∧ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑁)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))}) = ((Fmla‘𝑁) ∪ {𝑥 ∣ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑁)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢))})) |
77 | 64, 76 | eqtrd 2777 |
. 2
⊢ (𝑁 ∈ ω → dom
((𝑓 ∈ V ↦ (𝑓 ∪ {〈𝑥, 𝑦〉 ∣ (𝑦 = ∅ ∧ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))}))‘(rec((𝑓 ∈ V ↦ (𝑓 ∪ {〈𝑥, 𝑦〉 ∣ (𝑦 = ∅ ∧ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))})), {〈𝑥, 𝑦〉 ∣ (𝑦 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗))})‘𝑁)) = ((Fmla‘𝑁) ∪ {𝑥 ∣ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑁)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢))})) |
78 | 9, 16, 77 | 3eqtrd 2781 |
1
⊢ (𝑁 ∈ ω →
(Fmla‘suc 𝑁) =
((Fmla‘𝑁) ∪
{𝑥 ∣ ∃𝑢 ∈ ((∅ Sat
∅)‘𝑁)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢))})) |