| Step | Hyp | Ref
| Expression |
| 1 | | fmlasuc0 35389 |
. 2
⊢ (𝑁 ∈ ω →
(Fmla‘suc 𝑁) =
((Fmla‘𝑁) ∪
{𝑥 ∣ ∃𝑦 ∈ ((∅ Sat
∅)‘𝑁)(∃𝑧 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = ((1st ‘𝑦)⊼𝑔(1st
‘𝑧)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑦))})) |
| 2 | | eqid 2737 |
. . . . . . . 8
⊢ (∅
Sat ∅) = (∅ Sat ∅) |
| 3 | 2 | satf0op 35382 |
. . . . . . 7
⊢ (𝑁 ∈ ω → (𝑦 ∈ ((∅ Sat
∅)‘𝑁) ↔
∃𝑧(𝑦 = 〈𝑧, ∅〉 ∧ 〈𝑧, ∅〉 ∈ ((∅
Sat ∅)‘𝑁)))) |
| 4 | | fveq2 6906 |
. . . . . . . . . . . 12
⊢ (𝑧 = 𝑤 → (1st ‘𝑧) = (1st ‘𝑤)) |
| 5 | 4 | oveq2d 7447 |
. . . . . . . . . . 11
⊢ (𝑧 = 𝑤 → ((1st ‘𝑦)⊼𝑔(1st
‘𝑧)) =
((1st ‘𝑦)⊼𝑔(1st
‘𝑤))) |
| 6 | 5 | eqeq2d 2748 |
. . . . . . . . . 10
⊢ (𝑧 = 𝑤 → (𝑥 = ((1st ‘𝑦)⊼𝑔(1st
‘𝑧)) ↔ 𝑥 = ((1st ‘𝑦)⊼𝑔(1st
‘𝑤)))) |
| 7 | 6 | cbvrexvw 3238 |
. . . . . . . . 9
⊢
(∃𝑧 ∈
((∅ Sat ∅)‘𝑁)𝑥 = ((1st ‘𝑦)⊼𝑔(1st
‘𝑧)) ↔
∃𝑤 ∈ ((∅
Sat ∅)‘𝑁)𝑥 = ((1st ‘𝑦)⊼𝑔(1st
‘𝑤))) |
| 8 | 7 | orbi1i 914 |
. . . . . . . 8
⊢
((∃𝑧 ∈
((∅ Sat ∅)‘𝑁)𝑥 = ((1st ‘𝑦)⊼𝑔(1st
‘𝑧)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑦)) ↔ (∃𝑤 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = ((1st ‘𝑦)⊼𝑔(1st
‘𝑤)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑦))) |
| 9 | | fmlafvel 35390 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈ ω → (𝑧 ∈ (Fmla‘𝑁) ↔ 〈𝑧, ∅〉 ∈ ((∅
Sat ∅)‘𝑁))) |
| 10 | 9 | biimprd 248 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈ ω →
(〈𝑧, ∅〉
∈ ((∅ Sat ∅)‘𝑁) → 𝑧 ∈ (Fmla‘𝑁))) |
| 11 | 10 | adantld 490 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈ ω → ((𝑦 = 〈𝑧, ∅〉 ∧ 〈𝑧, ∅〉 ∈ ((∅
Sat ∅)‘𝑁))
→ 𝑧 ∈
(Fmla‘𝑁))) |
| 12 | 11 | imp 406 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ω ∧ (𝑦 = 〈𝑧, ∅〉 ∧ 〈𝑧, ∅〉 ∈ ((∅
Sat ∅)‘𝑁)))
→ 𝑧 ∈
(Fmla‘𝑁)) |
| 13 | | vex 3484 |
. . . . . . . . . . . . . . . 16
⊢ 𝑧 ∈ V |
| 14 | | 0ex 5307 |
. . . . . . . . . . . . . . . 16
⊢ ∅
∈ V |
| 15 | 13, 14 | op1std 8024 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = 〈𝑧, ∅〉 → (1st
‘𝑦) = 𝑧) |
| 16 | 15 | eleq1d 2826 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = 〈𝑧, ∅〉 → ((1st
‘𝑦) ∈
(Fmla‘𝑁) ↔ 𝑧 ∈ (Fmla‘𝑁))) |
| 17 | 16 | ad2antrl 728 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ω ∧ (𝑦 = 〈𝑧, ∅〉 ∧ 〈𝑧, ∅〉 ∈ ((∅
Sat ∅)‘𝑁)))
→ ((1st ‘𝑦) ∈ (Fmla‘𝑁) ↔ 𝑧 ∈ (Fmla‘𝑁))) |
| 18 | 12, 17 | mpbird 257 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ω ∧ (𝑦 = 〈𝑧, ∅〉 ∧ 〈𝑧, ∅〉 ∈ ((∅
Sat ∅)‘𝑁)))
→ (1st ‘𝑦) ∈ (Fmla‘𝑁)) |
| 19 | 18 | 3adant3 1133 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ω ∧ (𝑦 = 〈𝑧, ∅〉 ∧ 〈𝑧, ∅〉 ∈ ((∅
Sat ∅)‘𝑁))
∧ (∃𝑤 ∈
((∅ Sat ∅)‘𝑁)𝑥 = ((1st ‘𝑦)⊼𝑔(1st
‘𝑤)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑦))) → (1st ‘𝑦) ∈ (Fmla‘𝑁)) |
| 20 | | oveq1 7438 |
. . . . . . . . . . . . . . 15
⊢ (𝑢 = (1st ‘𝑦) → (𝑢⊼𝑔𝑣) = ((1st ‘𝑦)⊼𝑔𝑣)) |
| 21 | 20 | eqeq2d 2748 |
. . . . . . . . . . . . . 14
⊢ (𝑢 = (1st ‘𝑦) → (𝑥 = (𝑢⊼𝑔𝑣) ↔ 𝑥 = ((1st ‘𝑦)⊼𝑔𝑣))) |
| 22 | 21 | rexbidv 3179 |
. . . . . . . . . . . . 13
⊢ (𝑢 = (1st ‘𝑦) → (∃𝑣 ∈ (Fmla‘𝑁)𝑥 = (𝑢⊼𝑔𝑣) ↔ ∃𝑣 ∈ (Fmla‘𝑁)𝑥 = ((1st ‘𝑦)⊼𝑔𝑣))) |
| 23 | | eqidd 2738 |
. . . . . . . . . . . . . . . 16
⊢ (𝑢 = (1st ‘𝑦) → 𝑖 = 𝑖) |
| 24 | | id 22 |
. . . . . . . . . . . . . . . 16
⊢ (𝑢 = (1st ‘𝑦) → 𝑢 = (1st ‘𝑦)) |
| 25 | 23, 24 | goaleq12d 35356 |
. . . . . . . . . . . . . . 15
⊢ (𝑢 = (1st ‘𝑦) →
∀𝑔𝑖𝑢 = ∀𝑔𝑖(1st ‘𝑦)) |
| 26 | 25 | eqeq2d 2748 |
. . . . . . . . . . . . . 14
⊢ (𝑢 = (1st ‘𝑦) → (𝑥 = ∀𝑔𝑖𝑢 ↔ 𝑥 = ∀𝑔𝑖(1st ‘𝑦))) |
| 27 | 26 | rexbidv 3179 |
. . . . . . . . . . . . 13
⊢ (𝑢 = (1st ‘𝑦) → (∃𝑖 ∈ ω 𝑥 =
∀𝑔𝑖𝑢 ↔ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st ‘𝑦))) |
| 28 | 22, 27 | orbi12d 919 |
. . . . . . . . . . . 12
⊢ (𝑢 = (1st ‘𝑦) → ((∃𝑣 ∈ (Fmla‘𝑁)𝑥 = (𝑢⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢) ↔ (∃𝑣 ∈ (Fmla‘𝑁)𝑥 = ((1st ‘𝑦)⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st ‘𝑦)))) |
| 29 | 28 | adantl 481 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ω ∧ (𝑦 = 〈𝑧, ∅〉 ∧ 〈𝑧, ∅〉 ∈ ((∅
Sat ∅)‘𝑁))
∧ (∃𝑤 ∈
((∅ Sat ∅)‘𝑁)𝑥 = ((1st ‘𝑦)⊼𝑔(1st
‘𝑤)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑦))) ∧ 𝑢 = (1st ‘𝑦)) → ((∃𝑣 ∈ (Fmla‘𝑁)𝑥 = (𝑢⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢) ↔ (∃𝑣 ∈ (Fmla‘𝑁)𝑥 = ((1st ‘𝑦)⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st ‘𝑦)))) |
| 30 | 2 | satf0op 35382 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 ∈ ω → (𝑤 ∈ ((∅ Sat
∅)‘𝑁) ↔
∃𝑦(𝑤 = 〈𝑦, ∅〉 ∧ 〈𝑦, ∅〉 ∈ ((∅
Sat ∅)‘𝑁)))) |
| 31 | | fmlafvel 35390 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑁 ∈ ω → (𝑦 ∈ (Fmla‘𝑁) ↔ 〈𝑦, ∅〉 ∈ ((∅
Sat ∅)‘𝑁))) |
| 32 | 31 | biimprd 248 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑁 ∈ ω →
(〈𝑦, ∅〉
∈ ((∅ Sat ∅)‘𝑁) → 𝑦 ∈ (Fmla‘𝑁))) |
| 33 | 32 | adantld 490 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑁 ∈ ω → ((𝑤 = 〈𝑦, ∅〉 ∧ 〈𝑦, ∅〉 ∈ ((∅
Sat ∅)‘𝑁))
→ 𝑦 ∈
(Fmla‘𝑁))) |
| 34 | 33 | imp 406 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑁 ∈ ω ∧ (𝑤 = 〈𝑦, ∅〉 ∧ 〈𝑦, ∅〉 ∈ ((∅
Sat ∅)‘𝑁)))
→ 𝑦 ∈
(Fmla‘𝑁)) |
| 35 | | vex 3484 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ 𝑦 ∈ V |
| 36 | 35, 14 | op1std 8024 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑤 = 〈𝑦, ∅〉 → (1st
‘𝑤) = 𝑦) |
| 37 | 36 | eleq1d 2826 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑤 = 〈𝑦, ∅〉 → ((1st
‘𝑤) ∈
(Fmla‘𝑁) ↔ 𝑦 ∈ (Fmla‘𝑁))) |
| 38 | 37 | ad2antrl 728 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑁 ∈ ω ∧ (𝑤 = 〈𝑦, ∅〉 ∧ 〈𝑦, ∅〉 ∈ ((∅
Sat ∅)‘𝑁)))
→ ((1st ‘𝑤) ∈ (Fmla‘𝑁) ↔ 𝑦 ∈ (Fmla‘𝑁))) |
| 39 | 34, 38 | mpbird 257 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑁 ∈ ω ∧ (𝑤 = 〈𝑦, ∅〉 ∧ 〈𝑦, ∅〉 ∈ ((∅
Sat ∅)‘𝑁)))
→ (1st ‘𝑤) ∈ (Fmla‘𝑁)) |
| 40 | 39 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑁 ∈ ω ∧ (𝑤 = 〈𝑦, ∅〉 ∧ 〈𝑦, ∅〉 ∈ ((∅
Sat ∅)‘𝑁)))
∧ 𝑥 = (𝑧⊼𝑔(1st
‘𝑤))) →
(1st ‘𝑤)
∈ (Fmla‘𝑁)) |
| 41 | | oveq2 7439 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑣 = (1st ‘𝑤) → (𝑧⊼𝑔𝑣) = (𝑧⊼𝑔(1st
‘𝑤))) |
| 42 | 41 | eqeq2d 2748 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑣 = (1st ‘𝑤) → (𝑥 = (𝑧⊼𝑔𝑣) ↔ 𝑥 = (𝑧⊼𝑔(1st
‘𝑤)))) |
| 43 | 42 | adantl 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑁 ∈ ω ∧ (𝑤 = 〈𝑦, ∅〉 ∧ 〈𝑦, ∅〉 ∈ ((∅
Sat ∅)‘𝑁)))
∧ 𝑥 = (𝑧⊼𝑔(1st
‘𝑤))) ∧ 𝑣 = (1st ‘𝑤)) → (𝑥 = (𝑧⊼𝑔𝑣) ↔ 𝑥 = (𝑧⊼𝑔(1st
‘𝑤)))) |
| 44 | | simpr 484 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑁 ∈ ω ∧ (𝑤 = 〈𝑦, ∅〉 ∧ 〈𝑦, ∅〉 ∈ ((∅
Sat ∅)‘𝑁)))
∧ 𝑥 = (𝑧⊼𝑔(1st
‘𝑤))) → 𝑥 = (𝑧⊼𝑔(1st
‘𝑤))) |
| 45 | 40, 43, 44 | rspcedvd 3624 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑁 ∈ ω ∧ (𝑤 = 〈𝑦, ∅〉 ∧ 〈𝑦, ∅〉 ∈ ((∅
Sat ∅)‘𝑁)))
∧ 𝑥 = (𝑧⊼𝑔(1st
‘𝑤))) →
∃𝑣 ∈
(Fmla‘𝑁)𝑥 = (𝑧⊼𝑔𝑣)) |
| 46 | 45 | exp31 419 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑁 ∈ ω → ((𝑤 = 〈𝑦, ∅〉 ∧ 〈𝑦, ∅〉 ∈ ((∅
Sat ∅)‘𝑁))
→ (𝑥 = (𝑧⊼𝑔(1st
‘𝑤)) →
∃𝑣 ∈
(Fmla‘𝑁)𝑥 = (𝑧⊼𝑔𝑣)))) |
| 47 | 46 | exlimdv 1933 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 ∈ ω →
(∃𝑦(𝑤 = 〈𝑦, ∅〉 ∧ 〈𝑦, ∅〉 ∈ ((∅
Sat ∅)‘𝑁))
→ (𝑥 = (𝑧⊼𝑔(1st
‘𝑤)) →
∃𝑣 ∈
(Fmla‘𝑁)𝑥 = (𝑧⊼𝑔𝑣)))) |
| 48 | 30, 47 | sylbid 240 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈ ω → (𝑤 ∈ ((∅ Sat
∅)‘𝑁) →
(𝑥 = (𝑧⊼𝑔(1st
‘𝑤)) →
∃𝑣 ∈
(Fmla‘𝑁)𝑥 = (𝑧⊼𝑔𝑣)))) |
| 49 | 48 | rexlimdv 3153 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈ ω →
(∃𝑤 ∈ ((∅
Sat ∅)‘𝑁)𝑥 = (𝑧⊼𝑔(1st
‘𝑤)) →
∃𝑣 ∈
(Fmla‘𝑁)𝑥 = (𝑧⊼𝑔𝑣))) |
| 50 | 49 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ω ∧ (𝑦 = 〈𝑧, ∅〉 ∧ 〈𝑧, ∅〉 ∈ ((∅
Sat ∅)‘𝑁)))
→ (∃𝑤 ∈
((∅ Sat ∅)‘𝑁)𝑥 = (𝑧⊼𝑔(1st
‘𝑤)) →
∃𝑣 ∈
(Fmla‘𝑁)𝑥 = (𝑧⊼𝑔𝑣))) |
| 51 | 15 | oveq1d 7446 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 = 〈𝑧, ∅〉 → ((1st
‘𝑦)⊼𝑔(1st
‘𝑤)) = (𝑧⊼𝑔(1st
‘𝑤))) |
| 52 | 51 | eqeq2d 2748 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 = 〈𝑧, ∅〉 → (𝑥 = ((1st ‘𝑦)⊼𝑔(1st
‘𝑤)) ↔ 𝑥 = (𝑧⊼𝑔(1st
‘𝑤)))) |
| 53 | 52 | rexbidv 3179 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = 〈𝑧, ∅〉 → (∃𝑤 ∈ ((∅ Sat
∅)‘𝑁)𝑥 = ((1st ‘𝑦)⊼𝑔(1st
‘𝑤)) ↔
∃𝑤 ∈ ((∅
Sat ∅)‘𝑁)𝑥 = (𝑧⊼𝑔(1st
‘𝑤)))) |
| 54 | 15 | oveq1d 7446 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 = 〈𝑧, ∅〉 → ((1st
‘𝑦)⊼𝑔𝑣) = (𝑧⊼𝑔𝑣)) |
| 55 | 54 | eqeq2d 2748 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 = 〈𝑧, ∅〉 → (𝑥 = ((1st ‘𝑦)⊼𝑔𝑣) ↔ 𝑥 = (𝑧⊼𝑔𝑣))) |
| 56 | 55 | rexbidv 3179 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = 〈𝑧, ∅〉 → (∃𝑣 ∈ (Fmla‘𝑁)𝑥 = ((1st ‘𝑦)⊼𝑔𝑣) ↔ ∃𝑣 ∈ (Fmla‘𝑁)𝑥 = (𝑧⊼𝑔𝑣))) |
| 57 | 53, 56 | imbi12d 344 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = 〈𝑧, ∅〉 → ((∃𝑤 ∈ ((∅ Sat
∅)‘𝑁)𝑥 = ((1st ‘𝑦)⊼𝑔(1st
‘𝑤)) →
∃𝑣 ∈
(Fmla‘𝑁)𝑥 = ((1st ‘𝑦)⊼𝑔𝑣)) ↔ (∃𝑤 ∈ ((∅ Sat
∅)‘𝑁)𝑥 = (𝑧⊼𝑔(1st
‘𝑤)) →
∃𝑣 ∈
(Fmla‘𝑁)𝑥 = (𝑧⊼𝑔𝑣)))) |
| 58 | 57 | ad2antrl 728 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ω ∧ (𝑦 = 〈𝑧, ∅〉 ∧ 〈𝑧, ∅〉 ∈ ((∅
Sat ∅)‘𝑁)))
→ ((∃𝑤 ∈
((∅ Sat ∅)‘𝑁)𝑥 = ((1st ‘𝑦)⊼𝑔(1st
‘𝑤)) →
∃𝑣 ∈
(Fmla‘𝑁)𝑥 = ((1st ‘𝑦)⊼𝑔𝑣)) ↔ (∃𝑤 ∈ ((∅ Sat
∅)‘𝑁)𝑥 = (𝑧⊼𝑔(1st
‘𝑤)) →
∃𝑣 ∈
(Fmla‘𝑁)𝑥 = (𝑧⊼𝑔𝑣)))) |
| 59 | 50, 58 | mpbird 257 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ω ∧ (𝑦 = 〈𝑧, ∅〉 ∧ 〈𝑧, ∅〉 ∈ ((∅
Sat ∅)‘𝑁)))
→ (∃𝑤 ∈
((∅ Sat ∅)‘𝑁)𝑥 = ((1st ‘𝑦)⊼𝑔(1st
‘𝑤)) →
∃𝑣 ∈
(Fmla‘𝑁)𝑥 = ((1st ‘𝑦)⊼𝑔𝑣))) |
| 60 | 59 | orim1d 968 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ω ∧ (𝑦 = 〈𝑧, ∅〉 ∧ 〈𝑧, ∅〉 ∈ ((∅
Sat ∅)‘𝑁)))
→ ((∃𝑤 ∈
((∅ Sat ∅)‘𝑁)𝑥 = ((1st ‘𝑦)⊼𝑔(1st
‘𝑤)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑦)) → (∃𝑣 ∈ (Fmla‘𝑁)𝑥 = ((1st ‘𝑦)⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st ‘𝑦)))) |
| 61 | 60 | 3impia 1118 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ω ∧ (𝑦 = 〈𝑧, ∅〉 ∧ 〈𝑧, ∅〉 ∈ ((∅
Sat ∅)‘𝑁))
∧ (∃𝑤 ∈
((∅ Sat ∅)‘𝑁)𝑥 = ((1st ‘𝑦)⊼𝑔(1st
‘𝑤)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑦))) → (∃𝑣 ∈ (Fmla‘𝑁)𝑥 = ((1st ‘𝑦)⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st ‘𝑦))) |
| 62 | 19, 29, 61 | rspcedvd 3624 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ω ∧ (𝑦 = 〈𝑧, ∅〉 ∧ 〈𝑧, ∅〉 ∈ ((∅
Sat ∅)‘𝑁))
∧ (∃𝑤 ∈
((∅ Sat ∅)‘𝑁)𝑥 = ((1st ‘𝑦)⊼𝑔(1st
‘𝑤)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑦))) → ∃𝑢 ∈ (Fmla‘𝑁)(∃𝑣 ∈ (Fmla‘𝑁)𝑥 = (𝑢⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢)) |
| 63 | 62 | 3exp 1120 |
. . . . . . . . 9
⊢ (𝑁 ∈ ω → ((𝑦 = 〈𝑧, ∅〉 ∧ 〈𝑧, ∅〉 ∈ ((∅
Sat ∅)‘𝑁))
→ ((∃𝑤 ∈
((∅ Sat ∅)‘𝑁)𝑥 = ((1st ‘𝑦)⊼𝑔(1st
‘𝑤)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑦)) → ∃𝑢 ∈ (Fmla‘𝑁)(∃𝑣 ∈ (Fmla‘𝑁)𝑥 = (𝑢⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢)))) |
| 64 | 63 | exlimdv 1933 |
. . . . . . . 8
⊢ (𝑁 ∈ ω →
(∃𝑧(𝑦 = 〈𝑧, ∅〉 ∧ 〈𝑧, ∅〉 ∈ ((∅
Sat ∅)‘𝑁))
→ ((∃𝑤 ∈
((∅ Sat ∅)‘𝑁)𝑥 = ((1st ‘𝑦)⊼𝑔(1st
‘𝑤)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑦)) → ∃𝑢 ∈ (Fmla‘𝑁)(∃𝑣 ∈ (Fmla‘𝑁)𝑥 = (𝑢⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢)))) |
| 65 | 8, 64 | syl7bi 255 |
. . . . . . 7
⊢ (𝑁 ∈ ω →
(∃𝑧(𝑦 = 〈𝑧, ∅〉 ∧ 〈𝑧, ∅〉 ∈ ((∅
Sat ∅)‘𝑁))
→ ((∃𝑧 ∈
((∅ Sat ∅)‘𝑁)𝑥 = ((1st ‘𝑦)⊼𝑔(1st
‘𝑧)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑦)) → ∃𝑢 ∈ (Fmla‘𝑁)(∃𝑣 ∈ (Fmla‘𝑁)𝑥 = (𝑢⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢)))) |
| 66 | 3, 65 | sylbid 240 |
. . . . . 6
⊢ (𝑁 ∈ ω → (𝑦 ∈ ((∅ Sat
∅)‘𝑁) →
((∃𝑧 ∈ ((∅
Sat ∅)‘𝑁)𝑥 = ((1st ‘𝑦)⊼𝑔(1st
‘𝑧)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑦)) → ∃𝑢 ∈ (Fmla‘𝑁)(∃𝑣 ∈ (Fmla‘𝑁)𝑥 = (𝑢⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢)))) |
| 67 | 66 | rexlimdv 3153 |
. . . . 5
⊢ (𝑁 ∈ ω →
(∃𝑦 ∈ ((∅
Sat ∅)‘𝑁)(∃𝑧 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = ((1st ‘𝑦)⊼𝑔(1st
‘𝑧)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑦)) → ∃𝑢 ∈ (Fmla‘𝑁)(∃𝑣 ∈ (Fmla‘𝑁)𝑥 = (𝑢⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢))) |
| 68 | | fmlafvel 35390 |
. . . . . . . . 9
⊢ (𝑁 ∈ ω → (𝑢 ∈ (Fmla‘𝑁) ↔ 〈𝑢, ∅〉 ∈ ((∅
Sat ∅)‘𝑁))) |
| 69 | 68 | biimpa 476 |
. . . . . . . 8
⊢ ((𝑁 ∈ ω ∧ 𝑢 ∈ (Fmla‘𝑁)) → 〈𝑢, ∅〉 ∈ ((∅
Sat ∅)‘𝑁)) |
| 70 | 69 | adantr 480 |
. . . . . . 7
⊢ (((𝑁 ∈ ω ∧ 𝑢 ∈ (Fmla‘𝑁)) ∧ (∃𝑣 ∈ (Fmla‘𝑁)𝑥 = (𝑢⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢)) → 〈𝑢, ∅〉 ∈ ((∅ Sat
∅)‘𝑁)) |
| 71 | | vex 3484 |
. . . . . . . . . . . . 13
⊢ 𝑢 ∈ V |
| 72 | 71, 14 | op1std 8024 |
. . . . . . . . . . . 12
⊢ (𝑦 = 〈𝑢, ∅〉 → (1st
‘𝑦) = 𝑢) |
| 73 | 72 | oveq1d 7446 |
. . . . . . . . . . 11
⊢ (𝑦 = 〈𝑢, ∅〉 → ((1st
‘𝑦)⊼𝑔(1st
‘𝑧)) = (𝑢⊼𝑔(1st
‘𝑧))) |
| 74 | 73 | eqeq2d 2748 |
. . . . . . . . . 10
⊢ (𝑦 = 〈𝑢, ∅〉 → (𝑥 = ((1st ‘𝑦)⊼𝑔(1st
‘𝑧)) ↔ 𝑥 = (𝑢⊼𝑔(1st
‘𝑧)))) |
| 75 | 74 | rexbidv 3179 |
. . . . . . . . 9
⊢ (𝑦 = 〈𝑢, ∅〉 → (∃𝑧 ∈ ((∅ Sat
∅)‘𝑁)𝑥 = ((1st ‘𝑦)⊼𝑔(1st
‘𝑧)) ↔
∃𝑧 ∈ ((∅
Sat ∅)‘𝑁)𝑥 = (𝑢⊼𝑔(1st
‘𝑧)))) |
| 76 | | eqidd 2738 |
. . . . . . . . . . . 12
⊢ (𝑦 = 〈𝑢, ∅〉 → 𝑖 = 𝑖) |
| 77 | 76, 72 | goaleq12d 35356 |
. . . . . . . . . . 11
⊢ (𝑦 = 〈𝑢, ∅〉 →
∀𝑔𝑖(1st ‘𝑦) = ∀𝑔𝑖𝑢) |
| 78 | 77 | eqeq2d 2748 |
. . . . . . . . . 10
⊢ (𝑦 = 〈𝑢, ∅〉 → (𝑥 = ∀𝑔𝑖(1st ‘𝑦) ↔ 𝑥 = ∀𝑔𝑖𝑢)) |
| 79 | 78 | rexbidv 3179 |
. . . . . . . . 9
⊢ (𝑦 = 〈𝑢, ∅〉 → (∃𝑖 ∈ ω 𝑥 =
∀𝑔𝑖(1st ‘𝑦) ↔ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢)) |
| 80 | 75, 79 | orbi12d 919 |
. . . . . . . 8
⊢ (𝑦 = 〈𝑢, ∅〉 → ((∃𝑧 ∈ ((∅ Sat
∅)‘𝑁)𝑥 = ((1st ‘𝑦)⊼𝑔(1st
‘𝑧)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑦)) ↔ (∃𝑧 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = (𝑢⊼𝑔(1st
‘𝑧)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖𝑢))) |
| 81 | 80 | adantl 481 |
. . . . . . 7
⊢ ((((𝑁 ∈ ω ∧ 𝑢 ∈ (Fmla‘𝑁)) ∧ (∃𝑣 ∈ (Fmla‘𝑁)𝑥 = (𝑢⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢)) ∧ 𝑦 = 〈𝑢, ∅〉) → ((∃𝑧 ∈ ((∅ Sat
∅)‘𝑁)𝑥 = ((1st ‘𝑦)⊼𝑔(1st
‘𝑧)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑦)) ↔ (∃𝑧 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = (𝑢⊼𝑔(1st
‘𝑧)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖𝑢))) |
| 82 | | fmlafvel 35390 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈ ω → (𝑣 ∈ (Fmla‘𝑁) ↔ 〈𝑣, ∅〉 ∈ ((∅
Sat ∅)‘𝑁))) |
| 83 | 82 | biimpd 229 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈ ω → (𝑣 ∈ (Fmla‘𝑁) → 〈𝑣, ∅〉 ∈ ((∅
Sat ∅)‘𝑁))) |
| 84 | 83 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ω ∧ 𝑢 ∈ (Fmla‘𝑁)) → (𝑣 ∈ (Fmla‘𝑁) → 〈𝑣, ∅〉 ∈ ((∅ Sat
∅)‘𝑁))) |
| 85 | 84 | imp 406 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ω ∧ 𝑢 ∈ (Fmla‘𝑁)) ∧ 𝑣 ∈ (Fmla‘𝑁)) → 〈𝑣, ∅〉 ∈ ((∅ Sat
∅)‘𝑁)) |
| 86 | 85 | adantr 480 |
. . . . . . . . . . 11
⊢ ((((𝑁 ∈ ω ∧ 𝑢 ∈ (Fmla‘𝑁)) ∧ 𝑣 ∈ (Fmla‘𝑁)) ∧ 𝑥 = (𝑢⊼𝑔𝑣)) → 〈𝑣, ∅〉 ∈ ((∅ Sat
∅)‘𝑁)) |
| 87 | | vex 3484 |
. . . . . . . . . . . . . . 15
⊢ 𝑣 ∈ V |
| 88 | 87, 14 | op1std 8024 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = 〈𝑣, ∅〉 → (1st
‘𝑧) = 𝑣) |
| 89 | 88 | oveq2d 7447 |
. . . . . . . . . . . . 13
⊢ (𝑧 = 〈𝑣, ∅〉 → (𝑢⊼𝑔(1st
‘𝑧)) = (𝑢⊼𝑔𝑣)) |
| 90 | 89 | eqeq2d 2748 |
. . . . . . . . . . . 12
⊢ (𝑧 = 〈𝑣, ∅〉 → (𝑥 = (𝑢⊼𝑔(1st
‘𝑧)) ↔ 𝑥 = (𝑢⊼𝑔𝑣))) |
| 91 | 90 | adantl 481 |
. . . . . . . . . . 11
⊢
(((((𝑁 ∈
ω ∧ 𝑢 ∈
(Fmla‘𝑁)) ∧ 𝑣 ∈ (Fmla‘𝑁)) ∧ 𝑥 = (𝑢⊼𝑔𝑣)) ∧ 𝑧 = 〈𝑣, ∅〉) → (𝑥 = (𝑢⊼𝑔(1st
‘𝑧)) ↔ 𝑥 = (𝑢⊼𝑔𝑣))) |
| 92 | | simpr 484 |
. . . . . . . . . . 11
⊢ ((((𝑁 ∈ ω ∧ 𝑢 ∈ (Fmla‘𝑁)) ∧ 𝑣 ∈ (Fmla‘𝑁)) ∧ 𝑥 = (𝑢⊼𝑔𝑣)) → 𝑥 = (𝑢⊼𝑔𝑣)) |
| 93 | 86, 91, 92 | rspcedvd 3624 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ ω ∧ 𝑢 ∈ (Fmla‘𝑁)) ∧ 𝑣 ∈ (Fmla‘𝑁)) ∧ 𝑥 = (𝑢⊼𝑔𝑣)) → ∃𝑧 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = (𝑢⊼𝑔(1st
‘𝑧))) |
| 94 | 93 | rexlimdva2 3157 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ω ∧ 𝑢 ∈ (Fmla‘𝑁)) → (∃𝑣 ∈ (Fmla‘𝑁)𝑥 = (𝑢⊼𝑔𝑣) → ∃𝑧 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = (𝑢⊼𝑔(1st
‘𝑧)))) |
| 95 | 94 | orim1d 968 |
. . . . . . . 8
⊢ ((𝑁 ∈ ω ∧ 𝑢 ∈ (Fmla‘𝑁)) → ((∃𝑣 ∈ (Fmla‘𝑁)𝑥 = (𝑢⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢) → (∃𝑧 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = (𝑢⊼𝑔(1st
‘𝑧)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖𝑢))) |
| 96 | 95 | imp 406 |
. . . . . . 7
⊢ (((𝑁 ∈ ω ∧ 𝑢 ∈ (Fmla‘𝑁)) ∧ (∃𝑣 ∈ (Fmla‘𝑁)𝑥 = (𝑢⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢)) → (∃𝑧 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = (𝑢⊼𝑔(1st
‘𝑧)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖𝑢)) |
| 97 | 70, 81, 96 | rspcedvd 3624 |
. . . . . 6
⊢ (((𝑁 ∈ ω ∧ 𝑢 ∈ (Fmla‘𝑁)) ∧ (∃𝑣 ∈ (Fmla‘𝑁)𝑥 = (𝑢⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢)) → ∃𝑦 ∈ ((∅ Sat ∅)‘𝑁)(∃𝑧 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = ((1st ‘𝑦)⊼𝑔(1st
‘𝑧)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑦))) |
| 98 | 97 | rexlimdva2 3157 |
. . . . 5
⊢ (𝑁 ∈ ω →
(∃𝑢 ∈
(Fmla‘𝑁)(∃𝑣 ∈ (Fmla‘𝑁)𝑥 = (𝑢⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢) → ∃𝑦 ∈ ((∅ Sat ∅)‘𝑁)(∃𝑧 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = ((1st ‘𝑦)⊼𝑔(1st
‘𝑧)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑦)))) |
| 99 | 67, 98 | impbid 212 |
. . . 4
⊢ (𝑁 ∈ ω →
(∃𝑦 ∈ ((∅
Sat ∅)‘𝑁)(∃𝑧 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = ((1st ‘𝑦)⊼𝑔(1st
‘𝑧)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑦)) ↔ ∃𝑢 ∈ (Fmla‘𝑁)(∃𝑣 ∈ (Fmla‘𝑁)𝑥 = (𝑢⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢))) |
| 100 | 99 | abbidv 2808 |
. . 3
⊢ (𝑁 ∈ ω → {𝑥 ∣ ∃𝑦 ∈ ((∅ Sat
∅)‘𝑁)(∃𝑧 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = ((1st ‘𝑦)⊼𝑔(1st
‘𝑧)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑦))} = {𝑥 ∣ ∃𝑢 ∈ (Fmla‘𝑁)(∃𝑣 ∈ (Fmla‘𝑁)𝑥 = (𝑢⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢)}) |
| 101 | 100 | uneq2d 4168 |
. 2
⊢ (𝑁 ∈ ω →
((Fmla‘𝑁) ∪
{𝑥 ∣ ∃𝑦 ∈ ((∅ Sat
∅)‘𝑁)(∃𝑧 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = ((1st ‘𝑦)⊼𝑔(1st
‘𝑧)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑦))}) = ((Fmla‘𝑁) ∪ {𝑥 ∣ ∃𝑢 ∈ (Fmla‘𝑁)(∃𝑣 ∈ (Fmla‘𝑁)𝑥 = (𝑢⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢)})) |
| 102 | 1, 101 | eqtrd 2777 |
1
⊢ (𝑁 ∈ ω →
(Fmla‘suc 𝑁) =
((Fmla‘𝑁) ∪
{𝑥 ∣ ∃𝑢 ∈ (Fmla‘𝑁)(∃𝑣 ∈ (Fmla‘𝑁)𝑥 = (𝑢⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢)})) |