Step | Hyp | Ref
| Expression |
1 | | fmlasuc0 32920 |
. 2
⊢ (𝑁 ∈ ω →
(Fmla‘suc 𝑁) =
((Fmla‘𝑁) ∪
{𝑥 ∣ ∃𝑦 ∈ ((∅ Sat
∅)‘𝑁)(∃𝑧 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = ((1st ‘𝑦)⊼𝑔(1st
‘𝑧)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑦))})) |
2 | | eqid 2739 |
. . . . . . . 8
⊢ (∅
Sat ∅) = (∅ Sat ∅) |
3 | 2 | satf0op 32913 |
. . . . . . 7
⊢ (𝑁 ∈ ω → (𝑦 ∈ ((∅ Sat
∅)‘𝑁) ↔
∃𝑧(𝑦 = 〈𝑧, ∅〉 ∧ 〈𝑧, ∅〉 ∈ ((∅
Sat ∅)‘𝑁)))) |
4 | | fveq2 6677 |
. . . . . . . . . . . 12
⊢ (𝑧 = 𝑤 → (1st ‘𝑧) = (1st ‘𝑤)) |
5 | 4 | oveq2d 7189 |
. . . . . . . . . . 11
⊢ (𝑧 = 𝑤 → ((1st ‘𝑦)⊼𝑔(1st
‘𝑧)) =
((1st ‘𝑦)⊼𝑔(1st
‘𝑤))) |
6 | 5 | eqeq2d 2750 |
. . . . . . . . . 10
⊢ (𝑧 = 𝑤 → (𝑥 = ((1st ‘𝑦)⊼𝑔(1st
‘𝑧)) ↔ 𝑥 = ((1st ‘𝑦)⊼𝑔(1st
‘𝑤)))) |
7 | 6 | cbvrexvw 3351 |
. . . . . . . . 9
⊢
(∃𝑧 ∈
((∅ Sat ∅)‘𝑁)𝑥 = ((1st ‘𝑦)⊼𝑔(1st
‘𝑧)) ↔
∃𝑤 ∈ ((∅
Sat ∅)‘𝑁)𝑥 = ((1st ‘𝑦)⊼𝑔(1st
‘𝑤))) |
8 | 7 | orbi1i 913 |
. . . . . . . 8
⊢
((∃𝑧 ∈
((∅ Sat ∅)‘𝑁)𝑥 = ((1st ‘𝑦)⊼𝑔(1st
‘𝑧)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑦)) ↔ (∃𝑤 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = ((1st ‘𝑦)⊼𝑔(1st
‘𝑤)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑦))) |
9 | | fmlafvel 32921 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈ ω → (𝑧 ∈ (Fmla‘𝑁) ↔ 〈𝑧, ∅〉 ∈ ((∅
Sat ∅)‘𝑁))) |
10 | 9 | biimprd 251 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈ ω →
(〈𝑧, ∅〉
∈ ((∅ Sat ∅)‘𝑁) → 𝑧 ∈ (Fmla‘𝑁))) |
11 | 10 | adantld 494 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈ ω → ((𝑦 = 〈𝑧, ∅〉 ∧ 〈𝑧, ∅〉 ∈ ((∅
Sat ∅)‘𝑁))
→ 𝑧 ∈
(Fmla‘𝑁))) |
12 | 11 | imp 410 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ω ∧ (𝑦 = 〈𝑧, ∅〉 ∧ 〈𝑧, ∅〉 ∈ ((∅
Sat ∅)‘𝑁)))
→ 𝑧 ∈
(Fmla‘𝑁)) |
13 | | vex 3403 |
. . . . . . . . . . . . . . . 16
⊢ 𝑧 ∈ V |
14 | | 0ex 5176 |
. . . . . . . . . . . . . . . 16
⊢ ∅
∈ V |
15 | 13, 14 | op1std 7727 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = 〈𝑧, ∅〉 → (1st
‘𝑦) = 𝑧) |
16 | 15 | eleq1d 2818 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = 〈𝑧, ∅〉 → ((1st
‘𝑦) ∈
(Fmla‘𝑁) ↔ 𝑧 ∈ (Fmla‘𝑁))) |
17 | 16 | ad2antrl 728 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ω ∧ (𝑦 = 〈𝑧, ∅〉 ∧ 〈𝑧, ∅〉 ∈ ((∅
Sat ∅)‘𝑁)))
→ ((1st ‘𝑦) ∈ (Fmla‘𝑁) ↔ 𝑧 ∈ (Fmla‘𝑁))) |
18 | 12, 17 | mpbird 260 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ω ∧ (𝑦 = 〈𝑧, ∅〉 ∧ 〈𝑧, ∅〉 ∈ ((∅
Sat ∅)‘𝑁)))
→ (1st ‘𝑦) ∈ (Fmla‘𝑁)) |
19 | 18 | 3adant3 1133 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ω ∧ (𝑦 = 〈𝑧, ∅〉 ∧ 〈𝑧, ∅〉 ∈ ((∅
Sat ∅)‘𝑁))
∧ (∃𝑤 ∈
((∅ Sat ∅)‘𝑁)𝑥 = ((1st ‘𝑦)⊼𝑔(1st
‘𝑤)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑦))) → (1st ‘𝑦) ∈ (Fmla‘𝑁)) |
20 | | oveq1 7180 |
. . . . . . . . . . . . . . 15
⊢ (𝑢 = (1st ‘𝑦) → (𝑢⊼𝑔𝑣) = ((1st ‘𝑦)⊼𝑔𝑣)) |
21 | 20 | eqeq2d 2750 |
. . . . . . . . . . . . . 14
⊢ (𝑢 = (1st ‘𝑦) → (𝑥 = (𝑢⊼𝑔𝑣) ↔ 𝑥 = ((1st ‘𝑦)⊼𝑔𝑣))) |
22 | 21 | rexbidv 3208 |
. . . . . . . . . . . . 13
⊢ (𝑢 = (1st ‘𝑦) → (∃𝑣 ∈ (Fmla‘𝑁)𝑥 = (𝑢⊼𝑔𝑣) ↔ ∃𝑣 ∈ (Fmla‘𝑁)𝑥 = ((1st ‘𝑦)⊼𝑔𝑣))) |
23 | | eqidd 2740 |
. . . . . . . . . . . . . . . 16
⊢ (𝑢 = (1st ‘𝑦) → 𝑖 = 𝑖) |
24 | | id 22 |
. . . . . . . . . . . . . . . 16
⊢ (𝑢 = (1st ‘𝑦) → 𝑢 = (1st ‘𝑦)) |
25 | 23, 24 | goaleq12d 32887 |
. . . . . . . . . . . . . . 15
⊢ (𝑢 = (1st ‘𝑦) →
∀𝑔𝑖𝑢 = ∀𝑔𝑖(1st ‘𝑦)) |
26 | 25 | eqeq2d 2750 |
. . . . . . . . . . . . . 14
⊢ (𝑢 = (1st ‘𝑦) → (𝑥 = ∀𝑔𝑖𝑢 ↔ 𝑥 = ∀𝑔𝑖(1st ‘𝑦))) |
27 | 26 | rexbidv 3208 |
. . . . . . . . . . . . 13
⊢ (𝑢 = (1st ‘𝑦) → (∃𝑖 ∈ ω 𝑥 =
∀𝑔𝑖𝑢 ↔ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st ‘𝑦))) |
28 | 22, 27 | orbi12d 918 |
. . . . . . . . . . . 12
⊢ (𝑢 = (1st ‘𝑦) → ((∃𝑣 ∈ (Fmla‘𝑁)𝑥 = (𝑢⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢) ↔ (∃𝑣 ∈ (Fmla‘𝑁)𝑥 = ((1st ‘𝑦)⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st ‘𝑦)))) |
29 | 28 | adantl 485 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ω ∧ (𝑦 = 〈𝑧, ∅〉 ∧ 〈𝑧, ∅〉 ∈ ((∅
Sat ∅)‘𝑁))
∧ (∃𝑤 ∈
((∅ Sat ∅)‘𝑁)𝑥 = ((1st ‘𝑦)⊼𝑔(1st
‘𝑤)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑦))) ∧ 𝑢 = (1st ‘𝑦)) → ((∃𝑣 ∈ (Fmla‘𝑁)𝑥 = (𝑢⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢) ↔ (∃𝑣 ∈ (Fmla‘𝑁)𝑥 = ((1st ‘𝑦)⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st ‘𝑦)))) |
30 | 2 | satf0op 32913 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 ∈ ω → (𝑤 ∈ ((∅ Sat
∅)‘𝑁) ↔
∃𝑦(𝑤 = 〈𝑦, ∅〉 ∧ 〈𝑦, ∅〉 ∈ ((∅
Sat ∅)‘𝑁)))) |
31 | | fmlafvel 32921 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑁 ∈ ω → (𝑦 ∈ (Fmla‘𝑁) ↔ 〈𝑦, ∅〉 ∈ ((∅
Sat ∅)‘𝑁))) |
32 | 31 | biimprd 251 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑁 ∈ ω →
(〈𝑦, ∅〉
∈ ((∅ Sat ∅)‘𝑁) → 𝑦 ∈ (Fmla‘𝑁))) |
33 | 32 | adantld 494 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑁 ∈ ω → ((𝑤 = 〈𝑦, ∅〉 ∧ 〈𝑦, ∅〉 ∈ ((∅
Sat ∅)‘𝑁))
→ 𝑦 ∈
(Fmla‘𝑁))) |
34 | 33 | imp 410 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑁 ∈ ω ∧ (𝑤 = 〈𝑦, ∅〉 ∧ 〈𝑦, ∅〉 ∈ ((∅
Sat ∅)‘𝑁)))
→ 𝑦 ∈
(Fmla‘𝑁)) |
35 | | vex 3403 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ 𝑦 ∈ V |
36 | 35, 14 | op1std 7727 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑤 = 〈𝑦, ∅〉 → (1st
‘𝑤) = 𝑦) |
37 | 36 | eleq1d 2818 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑤 = 〈𝑦, ∅〉 → ((1st
‘𝑤) ∈
(Fmla‘𝑁) ↔ 𝑦 ∈ (Fmla‘𝑁))) |
38 | 37 | ad2antrl 728 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑁 ∈ ω ∧ (𝑤 = 〈𝑦, ∅〉 ∧ 〈𝑦, ∅〉 ∈ ((∅
Sat ∅)‘𝑁)))
→ ((1st ‘𝑤) ∈ (Fmla‘𝑁) ↔ 𝑦 ∈ (Fmla‘𝑁))) |
39 | 34, 38 | mpbird 260 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑁 ∈ ω ∧ (𝑤 = 〈𝑦, ∅〉 ∧ 〈𝑦, ∅〉 ∈ ((∅
Sat ∅)‘𝑁)))
→ (1st ‘𝑤) ∈ (Fmla‘𝑁)) |
40 | 39 | adantr 484 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑁 ∈ ω ∧ (𝑤 = 〈𝑦, ∅〉 ∧ 〈𝑦, ∅〉 ∈ ((∅
Sat ∅)‘𝑁)))
∧ 𝑥 = (𝑧⊼𝑔(1st
‘𝑤))) →
(1st ‘𝑤)
∈ (Fmla‘𝑁)) |
41 | | oveq2 7181 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑣 = (1st ‘𝑤) → (𝑧⊼𝑔𝑣) = (𝑧⊼𝑔(1st
‘𝑤))) |
42 | 41 | eqeq2d 2750 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑣 = (1st ‘𝑤) → (𝑥 = (𝑧⊼𝑔𝑣) ↔ 𝑥 = (𝑧⊼𝑔(1st
‘𝑤)))) |
43 | 42 | adantl 485 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑁 ∈ ω ∧ (𝑤 = 〈𝑦, ∅〉 ∧ 〈𝑦, ∅〉 ∈ ((∅
Sat ∅)‘𝑁)))
∧ 𝑥 = (𝑧⊼𝑔(1st
‘𝑤))) ∧ 𝑣 = (1st ‘𝑤)) → (𝑥 = (𝑧⊼𝑔𝑣) ↔ 𝑥 = (𝑧⊼𝑔(1st
‘𝑤)))) |
44 | | simpr 488 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑁 ∈ ω ∧ (𝑤 = 〈𝑦, ∅〉 ∧ 〈𝑦, ∅〉 ∈ ((∅
Sat ∅)‘𝑁)))
∧ 𝑥 = (𝑧⊼𝑔(1st
‘𝑤))) → 𝑥 = (𝑧⊼𝑔(1st
‘𝑤))) |
45 | 40, 43, 44 | rspcedvd 3530 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑁 ∈ ω ∧ (𝑤 = 〈𝑦, ∅〉 ∧ 〈𝑦, ∅〉 ∈ ((∅
Sat ∅)‘𝑁)))
∧ 𝑥 = (𝑧⊼𝑔(1st
‘𝑤))) →
∃𝑣 ∈
(Fmla‘𝑁)𝑥 = (𝑧⊼𝑔𝑣)) |
46 | 45 | exp31 423 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑁 ∈ ω → ((𝑤 = 〈𝑦, ∅〉 ∧ 〈𝑦, ∅〉 ∈ ((∅
Sat ∅)‘𝑁))
→ (𝑥 = (𝑧⊼𝑔(1st
‘𝑤)) →
∃𝑣 ∈
(Fmla‘𝑁)𝑥 = (𝑧⊼𝑔𝑣)))) |
47 | 46 | exlimdv 1940 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 ∈ ω →
(∃𝑦(𝑤 = 〈𝑦, ∅〉 ∧ 〈𝑦, ∅〉 ∈ ((∅
Sat ∅)‘𝑁))
→ (𝑥 = (𝑧⊼𝑔(1st
‘𝑤)) →
∃𝑣 ∈
(Fmla‘𝑁)𝑥 = (𝑧⊼𝑔𝑣)))) |
48 | 30, 47 | sylbid 243 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈ ω → (𝑤 ∈ ((∅ Sat
∅)‘𝑁) →
(𝑥 = (𝑧⊼𝑔(1st
‘𝑤)) →
∃𝑣 ∈
(Fmla‘𝑁)𝑥 = (𝑧⊼𝑔𝑣)))) |
49 | 48 | rexlimdv 3194 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈ ω →
(∃𝑤 ∈ ((∅
Sat ∅)‘𝑁)𝑥 = (𝑧⊼𝑔(1st
‘𝑤)) →
∃𝑣 ∈
(Fmla‘𝑁)𝑥 = (𝑧⊼𝑔𝑣))) |
50 | 49 | adantr 484 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ω ∧ (𝑦 = 〈𝑧, ∅〉 ∧ 〈𝑧, ∅〉 ∈ ((∅
Sat ∅)‘𝑁)))
→ (∃𝑤 ∈
((∅ Sat ∅)‘𝑁)𝑥 = (𝑧⊼𝑔(1st
‘𝑤)) →
∃𝑣 ∈
(Fmla‘𝑁)𝑥 = (𝑧⊼𝑔𝑣))) |
51 | 15 | oveq1d 7188 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 = 〈𝑧, ∅〉 → ((1st
‘𝑦)⊼𝑔(1st
‘𝑤)) = (𝑧⊼𝑔(1st
‘𝑤))) |
52 | 51 | eqeq2d 2750 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 = 〈𝑧, ∅〉 → (𝑥 = ((1st ‘𝑦)⊼𝑔(1st
‘𝑤)) ↔ 𝑥 = (𝑧⊼𝑔(1st
‘𝑤)))) |
53 | 52 | rexbidv 3208 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = 〈𝑧, ∅〉 → (∃𝑤 ∈ ((∅ Sat
∅)‘𝑁)𝑥 = ((1st ‘𝑦)⊼𝑔(1st
‘𝑤)) ↔
∃𝑤 ∈ ((∅
Sat ∅)‘𝑁)𝑥 = (𝑧⊼𝑔(1st
‘𝑤)))) |
54 | 15 | oveq1d 7188 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 = 〈𝑧, ∅〉 → ((1st
‘𝑦)⊼𝑔𝑣) = (𝑧⊼𝑔𝑣)) |
55 | 54 | eqeq2d 2750 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 = 〈𝑧, ∅〉 → (𝑥 = ((1st ‘𝑦)⊼𝑔𝑣) ↔ 𝑥 = (𝑧⊼𝑔𝑣))) |
56 | 55 | rexbidv 3208 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = 〈𝑧, ∅〉 → (∃𝑣 ∈ (Fmla‘𝑁)𝑥 = ((1st ‘𝑦)⊼𝑔𝑣) ↔ ∃𝑣 ∈ (Fmla‘𝑁)𝑥 = (𝑧⊼𝑔𝑣))) |
57 | 53, 56 | imbi12d 348 |
. . . . . . . . . . . . . . 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 260 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ω ∧ (𝑦 = 〈𝑧, ∅〉 ∧ 〈𝑧, ∅〉 ∈ ((∅
Sat ∅)‘𝑁)))
→ (∃𝑤 ∈
((∅ Sat ∅)‘𝑁)𝑥 = ((1st ‘𝑦)⊼𝑔(1st
‘𝑤)) →
∃𝑣 ∈
(Fmla‘𝑁)𝑥 = ((1st ‘𝑦)⊼𝑔𝑣))) |
60 | 59 | orim1d 965 |
. . . . . . . . . . . 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 3530 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ω ∧ (𝑦 = 〈𝑧, ∅〉 ∧ 〈𝑧, ∅〉 ∈ ((∅
Sat ∅)‘𝑁))
∧ (∃𝑤 ∈
((∅ Sat ∅)‘𝑁)𝑥 = ((1st ‘𝑦)⊼𝑔(1st
‘𝑤)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑦))) → ∃𝑢 ∈ (Fmla‘𝑁)(∃𝑣 ∈ (Fmla‘𝑁)𝑥 = (𝑢⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢)) |
63 | 62 | 3exp 1120 |
. . . . . . . . 9
⊢ (𝑁 ∈ ω → ((𝑦 = 〈𝑧, ∅〉 ∧ 〈𝑧, ∅〉 ∈ ((∅
Sat ∅)‘𝑁))
→ ((∃𝑤 ∈
((∅ Sat ∅)‘𝑁)𝑥 = ((1st ‘𝑦)⊼𝑔(1st
‘𝑤)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑦)) → ∃𝑢 ∈ (Fmla‘𝑁)(∃𝑣 ∈ (Fmla‘𝑁)𝑥 = (𝑢⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢)))) |
64 | 63 | exlimdv 1940 |
. . . . . . . 8
⊢ (𝑁 ∈ ω →
(∃𝑧(𝑦 = 〈𝑧, ∅〉 ∧ 〈𝑧, ∅〉 ∈ ((∅
Sat ∅)‘𝑁))
→ ((∃𝑤 ∈
((∅ Sat ∅)‘𝑁)𝑥 = ((1st ‘𝑦)⊼𝑔(1st
‘𝑤)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑦)) → ∃𝑢 ∈ (Fmla‘𝑁)(∃𝑣 ∈ (Fmla‘𝑁)𝑥 = (𝑢⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢)))) |
65 | 8, 64 | syl7bi 258 |
. . . . . . 7
⊢ (𝑁 ∈ ω →
(∃𝑧(𝑦 = 〈𝑧, ∅〉 ∧ 〈𝑧, ∅〉 ∈ ((∅
Sat ∅)‘𝑁))
→ ((∃𝑧 ∈
((∅ Sat ∅)‘𝑁)𝑥 = ((1st ‘𝑦)⊼𝑔(1st
‘𝑧)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑦)) → ∃𝑢 ∈ (Fmla‘𝑁)(∃𝑣 ∈ (Fmla‘𝑁)𝑥 = (𝑢⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢)))) |
66 | 3, 65 | sylbid 243 |
. . . . . 6
⊢ (𝑁 ∈ ω → (𝑦 ∈ ((∅ Sat
∅)‘𝑁) →
((∃𝑧 ∈ ((∅
Sat ∅)‘𝑁)𝑥 = ((1st ‘𝑦)⊼𝑔(1st
‘𝑧)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑦)) → ∃𝑢 ∈ (Fmla‘𝑁)(∃𝑣 ∈ (Fmla‘𝑁)𝑥 = (𝑢⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢)))) |
67 | 66 | rexlimdv 3194 |
. . . . 5
⊢ (𝑁 ∈ ω →
(∃𝑦 ∈ ((∅
Sat ∅)‘𝑁)(∃𝑧 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = ((1st ‘𝑦)⊼𝑔(1st
‘𝑧)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑦)) → ∃𝑢 ∈ (Fmla‘𝑁)(∃𝑣 ∈ (Fmla‘𝑁)𝑥 = (𝑢⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢))) |
68 | | fmlafvel 32921 |
. . . . . . . . 9
⊢ (𝑁 ∈ ω → (𝑢 ∈ (Fmla‘𝑁) ↔ 〈𝑢, ∅〉 ∈ ((∅
Sat ∅)‘𝑁))) |
69 | 68 | biimpa 480 |
. . . . . . . 8
⊢ ((𝑁 ∈ ω ∧ 𝑢 ∈ (Fmla‘𝑁)) → 〈𝑢, ∅〉 ∈ ((∅
Sat ∅)‘𝑁)) |
70 | 69 | adantr 484 |
. . . . . . 7
⊢ (((𝑁 ∈ ω ∧ 𝑢 ∈ (Fmla‘𝑁)) ∧ (∃𝑣 ∈ (Fmla‘𝑁)𝑥 = (𝑢⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢)) → 〈𝑢, ∅〉 ∈ ((∅ Sat
∅)‘𝑁)) |
71 | | vex 3403 |
. . . . . . . . . . . . 13
⊢ 𝑢 ∈ V |
72 | 71, 14 | op1std 7727 |
. . . . . . . . . . . 12
⊢ (𝑦 = 〈𝑢, ∅〉 → (1st
‘𝑦) = 𝑢) |
73 | 72 | oveq1d 7188 |
. . . . . . . . . . 11
⊢ (𝑦 = 〈𝑢, ∅〉 → ((1st
‘𝑦)⊼𝑔(1st
‘𝑧)) = (𝑢⊼𝑔(1st
‘𝑧))) |
74 | 73 | eqeq2d 2750 |
. . . . . . . . . 10
⊢ (𝑦 = 〈𝑢, ∅〉 → (𝑥 = ((1st ‘𝑦)⊼𝑔(1st
‘𝑧)) ↔ 𝑥 = (𝑢⊼𝑔(1st
‘𝑧)))) |
75 | 74 | rexbidv 3208 |
. . . . . . . . 9
⊢ (𝑦 = 〈𝑢, ∅〉 → (∃𝑧 ∈ ((∅ Sat
∅)‘𝑁)𝑥 = ((1st ‘𝑦)⊼𝑔(1st
‘𝑧)) ↔
∃𝑧 ∈ ((∅
Sat ∅)‘𝑁)𝑥 = (𝑢⊼𝑔(1st
‘𝑧)))) |
76 | | eqidd 2740 |
. . . . . . . . . . . 12
⊢ (𝑦 = 〈𝑢, ∅〉 → 𝑖 = 𝑖) |
77 | 76, 72 | goaleq12d 32887 |
. . . . . . . . . . 11
⊢ (𝑦 = 〈𝑢, ∅〉 →
∀𝑔𝑖(1st ‘𝑦) = ∀𝑔𝑖𝑢) |
78 | 77 | eqeq2d 2750 |
. . . . . . . . . 10
⊢ (𝑦 = 〈𝑢, ∅〉 → (𝑥 = ∀𝑔𝑖(1st ‘𝑦) ↔ 𝑥 = ∀𝑔𝑖𝑢)) |
79 | 78 | rexbidv 3208 |
. . . . . . . . 9
⊢ (𝑦 = 〈𝑢, ∅〉 → (∃𝑖 ∈ ω 𝑥 =
∀𝑔𝑖(1st ‘𝑦) ↔ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢)) |
80 | 75, 79 | orbi12d 918 |
. . . . . . . 8
⊢ (𝑦 = 〈𝑢, ∅〉 → ((∃𝑧 ∈ ((∅ Sat
∅)‘𝑁)𝑥 = ((1st ‘𝑦)⊼𝑔(1st
‘𝑧)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑦)) ↔ (∃𝑧 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = (𝑢⊼𝑔(1st
‘𝑧)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖𝑢))) |
81 | 80 | adantl 485 |
. . . . . . 7
⊢ ((((𝑁 ∈ ω ∧ 𝑢 ∈ (Fmla‘𝑁)) ∧ (∃𝑣 ∈ (Fmla‘𝑁)𝑥 = (𝑢⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢)) ∧ 𝑦 = 〈𝑢, ∅〉) → ((∃𝑧 ∈ ((∅ Sat
∅)‘𝑁)𝑥 = ((1st ‘𝑦)⊼𝑔(1st
‘𝑧)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑦)) ↔ (∃𝑧 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = (𝑢⊼𝑔(1st
‘𝑧)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖𝑢))) |
82 | | fmlafvel 32921 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈ ω → (𝑣 ∈ (Fmla‘𝑁) ↔ 〈𝑣, ∅〉 ∈ ((∅
Sat ∅)‘𝑁))) |
83 | 82 | biimpd 232 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈ ω → (𝑣 ∈ (Fmla‘𝑁) → 〈𝑣, ∅〉 ∈ ((∅
Sat ∅)‘𝑁))) |
84 | 83 | adantr 484 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ω ∧ 𝑢 ∈ (Fmla‘𝑁)) → (𝑣 ∈ (Fmla‘𝑁) → 〈𝑣, ∅〉 ∈ ((∅ Sat
∅)‘𝑁))) |
85 | 84 | imp 410 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ω ∧ 𝑢 ∈ (Fmla‘𝑁)) ∧ 𝑣 ∈ (Fmla‘𝑁)) → 〈𝑣, ∅〉 ∈ ((∅ Sat
∅)‘𝑁)) |
86 | 85 | adantr 484 |
. . . . . . . . . . 11
⊢ ((((𝑁 ∈ ω ∧ 𝑢 ∈ (Fmla‘𝑁)) ∧ 𝑣 ∈ (Fmla‘𝑁)) ∧ 𝑥 = (𝑢⊼𝑔𝑣)) → 〈𝑣, ∅〉 ∈ ((∅ Sat
∅)‘𝑁)) |
87 | | vex 3403 |
. . . . . . . . . . . . . . 15
⊢ 𝑣 ∈ V |
88 | 87, 14 | op1std 7727 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = 〈𝑣, ∅〉 → (1st
‘𝑧) = 𝑣) |
89 | 88 | oveq2d 7189 |
. . . . . . . . . . . . 13
⊢ (𝑧 = 〈𝑣, ∅〉 → (𝑢⊼𝑔(1st
‘𝑧)) = (𝑢⊼𝑔𝑣)) |
90 | 89 | eqeq2d 2750 |
. . . . . . . . . . . 12
⊢ (𝑧 = 〈𝑣, ∅〉 → (𝑥 = (𝑢⊼𝑔(1st
‘𝑧)) ↔ 𝑥 = (𝑢⊼𝑔𝑣))) |
91 | 90 | adantl 485 |
. . . . . . . . . . 11
⊢
(((((𝑁 ∈
ω ∧ 𝑢 ∈
(Fmla‘𝑁)) ∧ 𝑣 ∈ (Fmla‘𝑁)) ∧ 𝑥 = (𝑢⊼𝑔𝑣)) ∧ 𝑧 = 〈𝑣, ∅〉) → (𝑥 = (𝑢⊼𝑔(1st
‘𝑧)) ↔ 𝑥 = (𝑢⊼𝑔𝑣))) |
92 | | simpr 488 |
. . . . . . . . . . 11
⊢ ((((𝑁 ∈ ω ∧ 𝑢 ∈ (Fmla‘𝑁)) ∧ 𝑣 ∈ (Fmla‘𝑁)) ∧ 𝑥 = (𝑢⊼𝑔𝑣)) → 𝑥 = (𝑢⊼𝑔𝑣)) |
93 | 86, 91, 92 | rspcedvd 3530 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ ω ∧ 𝑢 ∈ (Fmla‘𝑁)) ∧ 𝑣 ∈ (Fmla‘𝑁)) ∧ 𝑥 = (𝑢⊼𝑔𝑣)) → ∃𝑧 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = (𝑢⊼𝑔(1st
‘𝑧))) |
94 | 93 | rexlimdva2 3198 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ω ∧ 𝑢 ∈ (Fmla‘𝑁)) → (∃𝑣 ∈ (Fmla‘𝑁)𝑥 = (𝑢⊼𝑔𝑣) → ∃𝑧 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = (𝑢⊼𝑔(1st
‘𝑧)))) |
95 | 94 | orim1d 965 |
. . . . . . . 8
⊢ ((𝑁 ∈ ω ∧ 𝑢 ∈ (Fmla‘𝑁)) → ((∃𝑣 ∈ (Fmla‘𝑁)𝑥 = (𝑢⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢) → (∃𝑧 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = (𝑢⊼𝑔(1st
‘𝑧)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖𝑢))) |
96 | 95 | imp 410 |
. . . . . . 7
⊢ (((𝑁 ∈ ω ∧ 𝑢 ∈ (Fmla‘𝑁)) ∧ (∃𝑣 ∈ (Fmla‘𝑁)𝑥 = (𝑢⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢)) → (∃𝑧 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = (𝑢⊼𝑔(1st
‘𝑧)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖𝑢)) |
97 | 70, 81, 96 | rspcedvd 3530 |
. . . . . 6
⊢ (((𝑁 ∈ ω ∧ 𝑢 ∈ (Fmla‘𝑁)) ∧ (∃𝑣 ∈ (Fmla‘𝑁)𝑥 = (𝑢⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢)) → ∃𝑦 ∈ ((∅ Sat ∅)‘𝑁)(∃𝑧 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = ((1st ‘𝑦)⊼𝑔(1st
‘𝑧)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑦))) |
98 | 97 | rexlimdva2 3198 |
. . . . 5
⊢ (𝑁 ∈ ω →
(∃𝑢 ∈
(Fmla‘𝑁)(∃𝑣 ∈ (Fmla‘𝑁)𝑥 = (𝑢⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢) → ∃𝑦 ∈ ((∅ Sat ∅)‘𝑁)(∃𝑧 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = ((1st ‘𝑦)⊼𝑔(1st
‘𝑧)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑦)))) |
99 | 67, 98 | impbid 215 |
. . . 4
⊢ (𝑁 ∈ ω →
(∃𝑦 ∈ ((∅
Sat ∅)‘𝑁)(∃𝑧 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = ((1st ‘𝑦)⊼𝑔(1st
‘𝑧)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑦)) ↔ ∃𝑢 ∈ (Fmla‘𝑁)(∃𝑣 ∈ (Fmla‘𝑁)𝑥 = (𝑢⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢))) |
100 | 99 | abbidv 2803 |
. . 3
⊢ (𝑁 ∈ ω → {𝑥 ∣ ∃𝑦 ∈ ((∅ Sat
∅)‘𝑁)(∃𝑧 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = ((1st ‘𝑦)⊼𝑔(1st
‘𝑧)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑦))} = {𝑥 ∣ ∃𝑢 ∈ (Fmla‘𝑁)(∃𝑣 ∈ (Fmla‘𝑁)𝑥 = (𝑢⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢)}) |
101 | 100 | uneq2d 4054 |
. 2
⊢ (𝑁 ∈ ω →
((Fmla‘𝑁) ∪
{𝑥 ∣ ∃𝑦 ∈ ((∅ Sat
∅)‘𝑁)(∃𝑧 ∈ ((∅ Sat ∅)‘𝑁)𝑥 = ((1st ‘𝑦)⊼𝑔(1st
‘𝑧)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑦))}) = ((Fmla‘𝑁) ∪ {𝑥 ∣ ∃𝑢 ∈ (Fmla‘𝑁)(∃𝑣 ∈ (Fmla‘𝑁)𝑥 = (𝑢⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢)})) |
102 | 1, 101 | eqtrd 2774 |
1
⊢ (𝑁 ∈ ω →
(Fmla‘suc 𝑁) =
((Fmla‘𝑁) ∪
{𝑥 ∣ ∃𝑢 ∈ (Fmla‘𝑁)(∃𝑣 ∈ (Fmla‘𝑁)𝑥 = (𝑢⊼𝑔𝑣) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑢)})) |