Step | Hyp | Ref
| Expression |
1 | | fveq2 6892 |
. . . . 5
⊢ (𝑥 = ∅ → ((∅ Sat
∅)‘𝑥) =
((∅ Sat ∅)‘∅)) |
2 | 1 | eleq2d 2820 |
. . . 4
⊢ (𝑥 = ∅ → (∅
∈ ((∅ Sat ∅)‘𝑥) ↔ ∅ ∈ ((∅ Sat
∅)‘∅))) |
3 | 2 | notbid 318 |
. . 3
⊢ (𝑥 = ∅ → (¬ ∅
∈ ((∅ Sat ∅)‘𝑥) ↔ ¬ ∅ ∈ ((∅ Sat
∅)‘∅))) |
4 | | fveq2 6892 |
. . . . 5
⊢ (𝑥 = 𝑦 → ((∅ Sat ∅)‘𝑥) = ((∅ Sat
∅)‘𝑦)) |
5 | 4 | eleq2d 2820 |
. . . 4
⊢ (𝑥 = 𝑦 → (∅ ∈ ((∅ Sat
∅)‘𝑥) ↔
∅ ∈ ((∅ Sat ∅)‘𝑦))) |
6 | 5 | notbid 318 |
. . 3
⊢ (𝑥 = 𝑦 → (¬ ∅ ∈ ((∅ Sat
∅)‘𝑥) ↔
¬ ∅ ∈ ((∅ Sat ∅)‘𝑦))) |
7 | | fveq2 6892 |
. . . . 5
⊢ (𝑥 = suc 𝑦 → ((∅ Sat ∅)‘𝑥) = ((∅ Sat
∅)‘suc 𝑦)) |
8 | 7 | eleq2d 2820 |
. . . 4
⊢ (𝑥 = suc 𝑦 → (∅ ∈ ((∅ Sat
∅)‘𝑥) ↔
∅ ∈ ((∅ Sat ∅)‘suc 𝑦))) |
9 | 8 | notbid 318 |
. . 3
⊢ (𝑥 = suc 𝑦 → (¬ ∅ ∈ ((∅ Sat
∅)‘𝑥) ↔
¬ ∅ ∈ ((∅ Sat ∅)‘suc 𝑦))) |
10 | | fveq2 6892 |
. . . . 5
⊢ (𝑥 = 𝑁 → ((∅ Sat ∅)‘𝑥) = ((∅ Sat
∅)‘𝑁)) |
11 | 10 | eleq2d 2820 |
. . . 4
⊢ (𝑥 = 𝑁 → (∅ ∈ ((∅ Sat
∅)‘𝑥) ↔
∅ ∈ ((∅ Sat ∅)‘𝑁))) |
12 | 11 | notbid 318 |
. . 3
⊢ (𝑥 = 𝑁 → (¬ ∅ ∈ ((∅ Sat
∅)‘𝑥) ↔
¬ ∅ ∈ ((∅ Sat ∅)‘𝑁))) |
13 | | 0nelopab 5568 |
. . . 4
⊢ ¬
∅ ∈ {⟨𝑥,
𝑦⟩ ∣ (𝑦 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗))} |
14 | | satf00 34365 |
. . . . 5
⊢ ((∅
Sat ∅)‘∅) = {⟨𝑥, 𝑦⟩ ∣ (𝑦 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗))} |
15 | 14 | eleq2i 2826 |
. . . 4
⊢ (∅
∈ ((∅ Sat ∅)‘∅) ↔ ∅ ∈ {⟨𝑥, 𝑦⟩ ∣ (𝑦 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗))}) |
16 | 13, 15 | mtbir 323 |
. . 3
⊢ ¬
∅ ∈ ((∅ Sat ∅)‘∅) |
17 | | simpr 486 |
. . . . . 6
⊢ ((𝑦 ∈ ω ∧ ¬
∅ ∈ ((∅ Sat ∅)‘𝑦)) → ¬ ∅ ∈ ((∅ Sat
∅)‘𝑦)) |
18 | | 0nelopab 5568 |
. . . . . 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 591 |
. . . . 5
⊢ ((𝑦 ∈ ω ∧ ¬
∅ ∈ ((∅ Sat ∅)‘𝑦)) → ¬ (∅ ∈ ((∅ Sat
∅)‘𝑦) ∨
∅ ∈ {⟨𝑥,
𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ ((∅ Sat
∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))})) |
21 | | eqid 2733 |
. . . . . . . . 9
⊢ (∅
Sat ∅) = (∅ Sat ∅) |
22 | 21 | satf0suc 34367 |
. . . . . . . 8
⊢ (𝑦 ∈ ω → ((∅
Sat ∅)‘suc 𝑦) =
(((∅ Sat ∅)‘𝑦) ∪ {⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))})) |
23 | 22 | adantr 482 |
. . . . . . 7
⊢ ((𝑦 ∈ ω ∧ ¬
∅ ∈ ((∅ Sat ∅)‘𝑦)) → ((∅ Sat ∅)‘suc
𝑦) = (((∅ Sat
∅)‘𝑦) ∪
{⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ ((∅ Sat
∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))})) |
24 | 23 | eleq2d 2820 |
. . . . . 6
⊢ ((𝑦 ∈ ω ∧ ¬
∅ ∈ ((∅ Sat ∅)‘𝑦)) → (∅ ∈ ((∅ Sat
∅)‘suc 𝑦)
↔ ∅ ∈ (((∅ Sat ∅)‘𝑦) ∪ {⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))}))) |
25 | | elun 4149 |
. . . . . 6
⊢ (∅
∈ (((∅ Sat ∅)‘𝑦) ∪ {⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))}) ↔ (∅ ∈ ((∅ Sat
∅)‘𝑦) ∨
∅ ∈ {⟨𝑥,
𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ ((∅ Sat
∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))})) |
26 | 24, 25 | bitrdi 287 |
. . . . 5
⊢ ((𝑦 ∈ ω ∧ ¬
∅ ∈ ((∅ Sat ∅)‘𝑦)) → (∅ ∈ ((∅ Sat
∅)‘suc 𝑦)
↔ (∅ ∈ ((∅ Sat ∅)‘𝑦) ∨ ∅ ∈ {⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))}))) |
27 | 20, 26 | mtbird 325 |
. . . 4
⊢ ((𝑦 ∈ ω ∧ ¬
∅ ∈ ((∅ Sat ∅)‘𝑦)) → ¬ ∅ ∈ ((∅ Sat
∅)‘suc 𝑦)) |
28 | 27 | ex 414 |
. . 3
⊢ (𝑦 ∈ ω → (¬
∅ ∈ ((∅ Sat ∅)‘𝑦) → ¬ ∅ ∈ ((∅ Sat
∅)‘suc 𝑦))) |
29 | 3, 6, 9, 12, 16, 28 | finds 7889 |
. 2
⊢ (𝑁 ∈ ω → ¬
∅ ∈ ((∅ Sat ∅)‘𝑁)) |
30 | | df-nel 3048 |
. 2
⊢ (∅
∉ ((∅ Sat ∅)‘𝑁) ↔ ¬ ∅ ∈ ((∅ Sat
∅)‘𝑁)) |
31 | 29, 30 | sylibr 233 |
1
⊢ (𝑁 ∈ ω → ∅
∉ ((∅ Sat ∅)‘𝑁)) |