Step | Hyp | Ref
| Expression |
1 | | fveq2 6668 |
. . . . 5
⊢ (𝑥 = ∅ → ((∅ Sat
∅)‘𝑥) =
((∅ Sat ∅)‘∅)) |
2 | 1 | eleq2d 2818 |
. . . 4
⊢ (𝑥 = ∅ → (∅
∈ ((∅ Sat ∅)‘𝑥) ↔ ∅ ∈ ((∅ Sat
∅)‘∅))) |
3 | 2 | notbid 321 |
. . 3
⊢ (𝑥 = ∅ → (¬ ∅
∈ ((∅ Sat ∅)‘𝑥) ↔ ¬ ∅ ∈ ((∅ Sat
∅)‘∅))) |
4 | | fveq2 6668 |
. . . . 5
⊢ (𝑥 = 𝑦 → ((∅ Sat ∅)‘𝑥) = ((∅ Sat
∅)‘𝑦)) |
5 | 4 | eleq2d 2818 |
. . . 4
⊢ (𝑥 = 𝑦 → (∅ ∈ ((∅ Sat
∅)‘𝑥) ↔
∅ ∈ ((∅ Sat ∅)‘𝑦))) |
6 | 5 | notbid 321 |
. . 3
⊢ (𝑥 = 𝑦 → (¬ ∅ ∈ ((∅ Sat
∅)‘𝑥) ↔
¬ ∅ ∈ ((∅ Sat ∅)‘𝑦))) |
7 | | fveq2 6668 |
. . . . 5
⊢ (𝑥 = suc 𝑦 → ((∅ Sat ∅)‘𝑥) = ((∅ Sat
∅)‘suc 𝑦)) |
8 | 7 | eleq2d 2818 |
. . . 4
⊢ (𝑥 = suc 𝑦 → (∅ ∈ ((∅ Sat
∅)‘𝑥) ↔
∅ ∈ ((∅ Sat ∅)‘suc 𝑦))) |
9 | 8 | notbid 321 |
. . 3
⊢ (𝑥 = suc 𝑦 → (¬ ∅ ∈ ((∅ Sat
∅)‘𝑥) ↔
¬ ∅ ∈ ((∅ Sat ∅)‘suc 𝑦))) |
10 | | fveq2 6668 |
. . . . 5
⊢ (𝑥 = 𝑁 → ((∅ Sat ∅)‘𝑥) = ((∅ Sat
∅)‘𝑁)) |
11 | 10 | eleq2d 2818 |
. . . 4
⊢ (𝑥 = 𝑁 → (∅ ∈ ((∅ Sat
∅)‘𝑥) ↔
∅ ∈ ((∅ Sat ∅)‘𝑁))) |
12 | 11 | notbid 321 |
. . 3
⊢ (𝑥 = 𝑁 → (¬ ∅ ∈ ((∅ Sat
∅)‘𝑥) ↔
¬ ∅ ∈ ((∅ Sat ∅)‘𝑁))) |
13 | | 0nelopab 5417 |
. . . 4
⊢ ¬
∅ ∈ {〈𝑥,
𝑦〉 ∣ (𝑦 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗))} |
14 | | satf00 32899 |
. . . . 5
⊢ ((∅
Sat ∅)‘∅) = {〈𝑥, 𝑦〉 ∣ (𝑦 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗))} |
15 | 14 | eleq2i 2824 |
. . . 4
⊢ (∅
∈ ((∅ Sat ∅)‘∅) ↔ ∅ ∈ {〈𝑥, 𝑦〉 ∣ (𝑦 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗))}) |
16 | 13, 15 | mtbir 326 |
. . 3
⊢ ¬
∅ ∈ ((∅ Sat ∅)‘∅) |
17 | | simpr 488 |
. . . . . 6
⊢ ((𝑦 ∈ ω ∧ ¬
∅ ∈ ((∅ Sat ∅)‘𝑦)) → ¬ ∅ ∈ ((∅ Sat
∅)‘𝑦)) |
18 | | 0nelopab 5417 |
. . . . . 6
⊢ ¬
∅ ∈ {〈𝑥,
𝑧〉 ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ ((∅ Sat
∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))} |
19 | | ioran 983 |
. . . . . 6
⊢ (¬
(∅ ∈ ((∅ Sat ∅)‘𝑦) ∨ ∅ ∈ {〈𝑥, 𝑧〉 ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))}) ↔ (¬ ∅ ∈ ((∅
Sat ∅)‘𝑦) ∧
¬ ∅ ∈ {〈𝑥, 𝑧〉 ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))})) |
20 | 17, 18, 19 | sylanblrc 593 |
. . . . 5
⊢ ((𝑦 ∈ ω ∧ ¬
∅ ∈ ((∅ Sat ∅)‘𝑦)) → ¬ (∅ ∈ ((∅ Sat
∅)‘𝑦) ∨
∅ ∈ {〈𝑥,
𝑧〉 ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ ((∅ Sat
∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))})) |
21 | | eqid 2738 |
. . . . . . . . 9
⊢ (∅
Sat ∅) = (∅ Sat ∅) |
22 | 21 | satf0suc 32901 |
. . . . . . . 8
⊢ (𝑦 ∈ ω → ((∅
Sat ∅)‘suc 𝑦) =
(((∅ Sat ∅)‘𝑦) ∪ {〈𝑥, 𝑧〉 ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))})) |
23 | 22 | adantr 484 |
. . . . . . 7
⊢ ((𝑦 ∈ ω ∧ ¬
∅ ∈ ((∅ Sat ∅)‘𝑦)) → ((∅ Sat ∅)‘suc
𝑦) = (((∅ Sat
∅)‘𝑦) ∪
{〈𝑥, 𝑧〉 ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ ((∅ Sat
∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))})) |
24 | 23 | eleq2d 2818 |
. . . . . 6
⊢ ((𝑦 ∈ ω ∧ ¬
∅ ∈ ((∅ Sat ∅)‘𝑦)) → (∅ ∈ ((∅ Sat
∅)‘suc 𝑦)
↔ ∅ ∈ (((∅ Sat ∅)‘𝑦) ∪ {〈𝑥, 𝑧〉 ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))}))) |
25 | | elun 4037 |
. . . . . 6
⊢ (∅
∈ (((∅ Sat ∅)‘𝑦) ∪ {〈𝑥, 𝑧〉 ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))}) ↔ (∅ ∈ ((∅ Sat
∅)‘𝑦) ∨
∅ ∈ {〈𝑥,
𝑧〉 ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ ((∅ Sat
∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))})) |
26 | 24, 25 | bitrdi 290 |
. . . . 5
⊢ ((𝑦 ∈ ω ∧ ¬
∅ ∈ ((∅ Sat ∅)‘𝑦)) → (∅ ∈ ((∅ Sat
∅)‘suc 𝑦)
↔ (∅ ∈ ((∅ Sat ∅)‘𝑦) ∨ ∅ ∈ {〈𝑥, 𝑧〉 ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))}))) |
27 | 20, 26 | mtbird 328 |
. . . 4
⊢ ((𝑦 ∈ ω ∧ ¬
∅ ∈ ((∅ Sat ∅)‘𝑦)) → ¬ ∅ ∈ ((∅ Sat
∅)‘suc 𝑦)) |
28 | 27 | ex 416 |
. . 3
⊢ (𝑦 ∈ ω → (¬
∅ ∈ ((∅ Sat ∅)‘𝑦) → ¬ ∅ ∈ ((∅ Sat
∅)‘suc 𝑦))) |
29 | 3, 6, 9, 12, 16, 28 | finds 7622 |
. 2
⊢ (𝑁 ∈ ω → ¬
∅ ∈ ((∅ Sat ∅)‘𝑁)) |
30 | | df-nel 3039 |
. 2
⊢ (∅
∉ ((∅ Sat ∅)‘𝑁) ↔ ¬ ∅ ∈ ((∅ Sat
∅)‘𝑁)) |
31 | 29, 30 | sylibr 237 |
1
⊢ (𝑁 ∈ ω → ∅
∉ ((∅ Sat ∅)‘𝑁)) |