Step | Hyp | Ref
| Expression |
1 | | fveq2 6674 |
. . . . . . 7
⊢ (𝑥 = ∅ →
(Fmla‘𝑥) =
(Fmla‘∅)) |
2 | 1 | eleq2d 2818 |
. . . . . 6
⊢ (𝑥 = ∅ → (𝐹 ∈ (Fmla‘𝑥) ↔ 𝐹 ∈
(Fmla‘∅))) |
3 | | fveq2 6674 |
. . . . . . 7
⊢ (𝑥 = ∅ → ((∅ Sat
∅)‘𝑥) =
((∅ Sat ∅)‘∅)) |
4 | 3 | eleq2d 2818 |
. . . . . 6
⊢ (𝑥 = ∅ → (〈𝐹, ∅〉 ∈ ((∅
Sat ∅)‘𝑥)
↔ 〈𝐹,
∅〉 ∈ ((∅ Sat ∅)‘∅))) |
5 | 2, 4 | bibi12d 349 |
. . . . 5
⊢ (𝑥 = ∅ → ((𝐹 ∈ (Fmla‘𝑥) ↔ 〈𝐹, ∅〉 ∈ ((∅ Sat
∅)‘𝑥)) ↔
(𝐹 ∈
(Fmla‘∅) ↔ 〈𝐹, ∅〉 ∈ ((∅ Sat
∅)‘∅)))) |
6 | 5 | imbi2d 344 |
. . . 4
⊢ (𝑥 = ∅ → ((𝐹 ∈ V → (𝐹 ∈ (Fmla‘𝑥) ↔ 〈𝐹, ∅〉 ∈ ((∅ Sat
∅)‘𝑥))) ↔
(𝐹 ∈ V → (𝐹 ∈ (Fmla‘∅)
↔ 〈𝐹,
∅〉 ∈ ((∅ Sat ∅)‘∅))))) |
7 | | fveq2 6674 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → (Fmla‘𝑥) = (Fmla‘𝑦)) |
8 | 7 | eleq2d 2818 |
. . . . . 6
⊢ (𝑥 = 𝑦 → (𝐹 ∈ (Fmla‘𝑥) ↔ 𝐹 ∈ (Fmla‘𝑦))) |
9 | | fveq2 6674 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → ((∅ Sat ∅)‘𝑥) = ((∅ Sat
∅)‘𝑦)) |
10 | 9 | eleq2d 2818 |
. . . . . 6
⊢ (𝑥 = 𝑦 → (〈𝐹, ∅〉 ∈ ((∅ Sat
∅)‘𝑥) ↔
〈𝐹, ∅〉
∈ ((∅ Sat ∅)‘𝑦))) |
11 | 8, 10 | bibi12d 349 |
. . . . 5
⊢ (𝑥 = 𝑦 → ((𝐹 ∈ (Fmla‘𝑥) ↔ 〈𝐹, ∅〉 ∈ ((∅ Sat
∅)‘𝑥)) ↔
(𝐹 ∈ (Fmla‘𝑦) ↔ 〈𝐹, ∅〉 ∈ ((∅ Sat
∅)‘𝑦)))) |
12 | 11 | imbi2d 344 |
. . . 4
⊢ (𝑥 = 𝑦 → ((𝐹 ∈ V → (𝐹 ∈ (Fmla‘𝑥) ↔ 〈𝐹, ∅〉 ∈ ((∅ Sat
∅)‘𝑥))) ↔
(𝐹 ∈ V → (𝐹 ∈ (Fmla‘𝑦) ↔ 〈𝐹, ∅〉 ∈ ((∅ Sat
∅)‘𝑦))))) |
13 | | fveq2 6674 |
. . . . . . 7
⊢ (𝑥 = suc 𝑦 → (Fmla‘𝑥) = (Fmla‘suc 𝑦)) |
14 | 13 | eleq2d 2818 |
. . . . . 6
⊢ (𝑥 = suc 𝑦 → (𝐹 ∈ (Fmla‘𝑥) ↔ 𝐹 ∈ (Fmla‘suc 𝑦))) |
15 | | fveq2 6674 |
. . . . . . 7
⊢ (𝑥 = suc 𝑦 → ((∅ Sat ∅)‘𝑥) = ((∅ Sat
∅)‘suc 𝑦)) |
16 | 15 | eleq2d 2818 |
. . . . . 6
⊢ (𝑥 = suc 𝑦 → (〈𝐹, ∅〉 ∈ ((∅ Sat
∅)‘𝑥) ↔
〈𝐹, ∅〉
∈ ((∅ Sat ∅)‘suc 𝑦))) |
17 | 14, 16 | bibi12d 349 |
. . . . 5
⊢ (𝑥 = suc 𝑦 → ((𝐹 ∈ (Fmla‘𝑥) ↔ 〈𝐹, ∅〉 ∈ ((∅ Sat
∅)‘𝑥)) ↔
(𝐹 ∈ (Fmla‘suc
𝑦) ↔ 〈𝐹, ∅〉 ∈ ((∅
Sat ∅)‘suc 𝑦)))) |
18 | 17 | imbi2d 344 |
. . . 4
⊢ (𝑥 = suc 𝑦 → ((𝐹 ∈ V → (𝐹 ∈ (Fmla‘𝑥) ↔ 〈𝐹, ∅〉 ∈ ((∅ Sat
∅)‘𝑥))) ↔
(𝐹 ∈ V → (𝐹 ∈ (Fmla‘suc 𝑦) ↔ 〈𝐹, ∅〉 ∈ ((∅ Sat
∅)‘suc 𝑦))))) |
19 | | fveq2 6674 |
. . . . . . 7
⊢ (𝑥 = 𝑁 → (Fmla‘𝑥) = (Fmla‘𝑁)) |
20 | 19 | eleq2d 2818 |
. . . . . 6
⊢ (𝑥 = 𝑁 → (𝐹 ∈ (Fmla‘𝑥) ↔ 𝐹 ∈ (Fmla‘𝑁))) |
21 | | fveq2 6674 |
. . . . . . 7
⊢ (𝑥 = 𝑁 → ((∅ Sat ∅)‘𝑥) = ((∅ Sat
∅)‘𝑁)) |
22 | 21 | eleq2d 2818 |
. . . . . 6
⊢ (𝑥 = 𝑁 → (〈𝐹, ∅〉 ∈ ((∅ Sat
∅)‘𝑥) ↔
〈𝐹, ∅〉
∈ ((∅ Sat ∅)‘𝑁))) |
23 | 20, 22 | bibi12d 349 |
. . . . 5
⊢ (𝑥 = 𝑁 → ((𝐹 ∈ (Fmla‘𝑥) ↔ 〈𝐹, ∅〉 ∈ ((∅ Sat
∅)‘𝑥)) ↔
(𝐹 ∈ (Fmla‘𝑁) ↔ 〈𝐹, ∅〉 ∈ ((∅ Sat
∅)‘𝑁)))) |
24 | 23 | imbi2d 344 |
. . . 4
⊢ (𝑥 = 𝑁 → ((𝐹 ∈ V → (𝐹 ∈ (Fmla‘𝑥) ↔ 〈𝐹, ∅〉 ∈ ((∅ Sat
∅)‘𝑥))) ↔
(𝐹 ∈ V → (𝐹 ∈ (Fmla‘𝑁) ↔ 〈𝐹, ∅〉 ∈ ((∅ Sat
∅)‘𝑁))))) |
25 | | eqeq1 2742 |
. . . . . . . 8
⊢ (𝑥 = 𝐹 → (𝑥 = (𝑖∈𝑔𝑗) ↔ 𝐹 = (𝑖∈𝑔𝑗))) |
26 | 25 | 2rexbidv 3210 |
. . . . . . 7
⊢ (𝑥 = 𝐹 → (∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗) ↔ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝐹 = (𝑖∈𝑔𝑗))) |
27 | 26 | elrab 3588 |
. . . . . 6
⊢ (𝐹 ∈ {𝑥 ∈ V ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗)} ↔ (𝐹 ∈ V ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝐹 = (𝑖∈𝑔𝑗))) |
28 | | eqidd 2739 |
. . . . . . . 8
⊢ ((𝐹 ∈ V ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝐹 = (𝑖∈𝑔𝑗)) → ∅ = ∅) |
29 | | simpr 488 |
. . . . . . . 8
⊢ ((𝐹 ∈ V ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝐹 = (𝑖∈𝑔𝑗)) → ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝐹 = (𝑖∈𝑔𝑗)) |
30 | 28, 29 | jca 515 |
. . . . . . 7
⊢ ((𝐹 ∈ V ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝐹 = (𝑖∈𝑔𝑗)) → (∅ = ∅ ∧
∃𝑖 ∈ ω
∃𝑗 ∈ ω
𝐹 = (𝑖∈𝑔𝑗))) |
31 | | simpr 488 |
. . . . . . . . 9
⊢ ((∅
= ∅ ∧ ∃𝑖
∈ ω ∃𝑗
∈ ω 𝐹 = (𝑖∈𝑔𝑗)) → ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝐹 = (𝑖∈𝑔𝑗)) |
32 | 31 | anim2i 620 |
. . . . . . . 8
⊢ ((𝐹 ∈ V ∧ (∅ =
∅ ∧ ∃𝑖
∈ ω ∃𝑗
∈ ω 𝐹 = (𝑖∈𝑔𝑗))) → (𝐹 ∈ V ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝐹 = (𝑖∈𝑔𝑗))) |
33 | 32 | ex 416 |
. . . . . . 7
⊢ (𝐹 ∈ V → ((∅ =
∅ ∧ ∃𝑖
∈ ω ∃𝑗
∈ ω 𝐹 = (𝑖∈𝑔𝑗)) → (𝐹 ∈ V ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝐹 = (𝑖∈𝑔𝑗)))) |
34 | 30, 33 | impbid2 229 |
. . . . . 6
⊢ (𝐹 ∈ V → ((𝐹 ∈ V ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝐹 = (𝑖∈𝑔𝑗)) ↔ (∅ = ∅ ∧
∃𝑖 ∈ ω
∃𝑗 ∈ ω
𝐹 = (𝑖∈𝑔𝑗)))) |
35 | 27, 34 | syl5bb 286 |
. . . . 5
⊢ (𝐹 ∈ V → (𝐹 ∈ {𝑥 ∈ V ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗)} ↔ (∅ = ∅ ∧
∃𝑖 ∈ ω
∃𝑗 ∈ ω
𝐹 = (𝑖∈𝑔𝑗)))) |
36 | | fmla0 32915 |
. . . . . . 7
⊢
(Fmla‘∅) = {𝑥 ∈ V ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗)} |
37 | 36 | eleq2i 2824 |
. . . . . 6
⊢ (𝐹 ∈ (Fmla‘∅)
↔ 𝐹 ∈ {𝑥 ∈ V ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗)}) |
38 | 37 | a1i 11 |
. . . . 5
⊢ (𝐹 ∈ V → (𝐹 ∈ (Fmla‘∅)
↔ 𝐹 ∈ {𝑥 ∈ V ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗)})) |
39 | | satf00 32907 |
. . . . . . . 8
⊢ ((∅
Sat ∅)‘∅) = {〈𝑥, 𝑦〉 ∣ (𝑦 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗))} |
40 | 39 | a1i 11 |
. . . . . . 7
⊢ (𝐹 ∈ V → ((∅ Sat
∅)‘∅) = {〈𝑥, 𝑦〉 ∣ (𝑦 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗))}) |
41 | 40 | eleq2d 2818 |
. . . . . 6
⊢ (𝐹 ∈ V → (〈𝐹, ∅〉 ∈ ((∅
Sat ∅)‘∅) ↔ 〈𝐹, ∅〉 ∈ {〈𝑥, 𝑦〉 ∣ (𝑦 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗))})) |
42 | | 0ex 5175 |
. . . . . . 7
⊢ ∅
∈ V |
43 | | eqeq1 2742 |
. . . . . . . . 9
⊢ (𝑦 = ∅ → (𝑦 = ∅ ↔ ∅ =
∅)) |
44 | 43, 26 | bi2anan9r 640 |
. . . . . . . 8
⊢ ((𝑥 = 𝐹 ∧ 𝑦 = ∅) → ((𝑦 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗)) ↔ (∅ = ∅ ∧
∃𝑖 ∈ ω
∃𝑗 ∈ ω
𝐹 = (𝑖∈𝑔𝑗)))) |
45 | 44 | opelopabga 5388 |
. . . . . . 7
⊢ ((𝐹 ∈ V ∧ ∅ ∈
V) → (〈𝐹,
∅〉 ∈ {〈𝑥, 𝑦〉 ∣ (𝑦 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗))} ↔ (∅ = ∅ ∧
∃𝑖 ∈ ω
∃𝑗 ∈ ω
𝐹 = (𝑖∈𝑔𝑗)))) |
46 | 42, 45 | mpan2 691 |
. . . . . 6
⊢ (𝐹 ∈ V → (〈𝐹, ∅〉 ∈
{〈𝑥, 𝑦〉 ∣ (𝑦 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗))} ↔ (∅ = ∅ ∧
∃𝑖 ∈ ω
∃𝑗 ∈ ω
𝐹 = (𝑖∈𝑔𝑗)))) |
47 | 41, 46 | bitrd 282 |
. . . . 5
⊢ (𝐹 ∈ V → (〈𝐹, ∅〉 ∈ ((∅
Sat ∅)‘∅) ↔ (∅ = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝐹 = (𝑖∈𝑔𝑗)))) |
48 | 35, 38, 47 | 3bitr4d 314 |
. . . 4
⊢ (𝐹 ∈ V → (𝐹 ∈ (Fmla‘∅)
↔ 〈𝐹,
∅〉 ∈ ((∅ Sat ∅)‘∅))) |
49 | | eqid 2738 |
. . . . . . . . . . . 12
⊢ ∅ =
∅ |
50 | 49 | biantrur 534 |
. . . . . . . . . . 11
⊢
(∃𝑢 ∈
((∅ Sat ∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝐹 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝐹 =
∀𝑔𝑖(1st ‘𝑢)) ↔ (∅ = ∅ ∧
∃𝑢 ∈ ((∅
Sat ∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝐹 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝐹 =
∀𝑔𝑖(1st ‘𝑢)))) |
51 | 50 | bicomi 227 |
. . . . . . . . . 10
⊢ ((∅
= ∅ ∧ ∃𝑢
∈ ((∅ Sat ∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝐹 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝐹 =
∀𝑔𝑖(1st ‘𝑢))) ↔ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝐹 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝐹 =
∀𝑔𝑖(1st ‘𝑢))) |
52 | 51 | a1i 11 |
. . . . . . . . 9
⊢ (𝐹 ∈ V → ((∅ =
∅ ∧ ∃𝑢
∈ ((∅ Sat ∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝐹 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝐹 =
∀𝑔𝑖(1st ‘𝑢))) ↔ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝐹 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝐹 =
∀𝑔𝑖(1st ‘𝑢)))) |
53 | | eqeq1 2742 |
. . . . . . . . . . . 12
⊢ (𝑧 = ∅ → (𝑧 = ∅ ↔ ∅ =
∅)) |
54 | | eqeq1 2742 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝐹 → (𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ↔ 𝐹 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)))) |
55 | 54 | rexbidv 3207 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝐹 → (∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ↔
∃𝑣 ∈ ((∅
Sat ∅)‘𝑦)𝐹 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)))) |
56 | | eqeq1 2742 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝐹 → (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ↔ 𝐹 = ∀𝑔𝑖(1st ‘𝑢))) |
57 | 56 | rexbidv 3207 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝐹 → (∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st ‘𝑢) ↔ ∃𝑖 ∈ ω 𝐹 =
∀𝑔𝑖(1st ‘𝑢))) |
58 | 55, 57 | orbi12d 918 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝐹 → ((∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)) ↔ (∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝐹 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝐹 =
∀𝑔𝑖(1st ‘𝑢)))) |
59 | 58 | rexbidv 3207 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝐹 → (∃𝑢 ∈ ((∅ Sat ∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)) ↔ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝐹 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝐹 =
∀𝑔𝑖(1st ‘𝑢)))) |
60 | 53, 59 | bi2anan9r 640 |
. . . . . . . . . . 11
⊢ ((𝑥 = 𝐹 ∧ 𝑧 = ∅) → ((𝑧 = ∅ ∧ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢))) ↔ (∅ = ∅ ∧
∃𝑢 ∈ ((∅
Sat ∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝐹 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝐹 =
∀𝑔𝑖(1st ‘𝑢))))) |
61 | 60 | opelopabga 5388 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ V ∧ ∅ ∈
V) → (〈𝐹,
∅〉 ∈ {〈𝑥, 𝑧〉 ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))} ↔ (∅ = ∅ ∧
∃𝑢 ∈ ((∅
Sat ∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝐹 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝐹 =
∀𝑔𝑖(1st ‘𝑢))))) |
62 | 42, 61 | mpan2 691 |
. . . . . . . . 9
⊢ (𝐹 ∈ V → (〈𝐹, ∅〉 ∈
{〈𝑥, 𝑧〉 ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ ((∅ Sat
∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))} ↔ (∅ = ∅ ∧
∃𝑢 ∈ ((∅
Sat ∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝐹 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝐹 =
∀𝑔𝑖(1st ‘𝑢))))) |
63 | 59 | elabg 3571 |
. . . . . . . . 9
⊢ (𝐹 ∈ V → (𝐹 ∈ {𝑥 ∣ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢))} ↔ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝐹 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝐹 =
∀𝑔𝑖(1st ‘𝑢)))) |
64 | 52, 62, 63 | 3bitr4d 314 |
. . . . . . . 8
⊢ (𝐹 ∈ V → (〈𝐹, ∅〉 ∈
{〈𝑥, 𝑧〉 ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ ((∅ Sat
∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))} ↔ 𝐹 ∈ {𝑥 ∣ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢))})) |
65 | 64 | adantl 485 |
. . . . . . 7
⊢ (((𝑦 ∈ ω ∧ (𝐹 ∈ V → (𝐹 ∈ (Fmla‘𝑦) ↔ 〈𝐹, ∅〉 ∈ ((∅ Sat
∅)‘𝑦)))) ∧
𝐹 ∈ V) →
(〈𝐹, ∅〉
∈ {〈𝑥, 𝑧〉 ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ ((∅ Sat
∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))} ↔ 𝐹 ∈ {𝑥 ∣ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢))})) |
66 | 65 | orbi2d 915 |
. . . . . 6
⊢ (((𝑦 ∈ ω ∧ (𝐹 ∈ V → (𝐹 ∈ (Fmla‘𝑦) ↔ 〈𝐹, ∅〉 ∈ ((∅ Sat
∅)‘𝑦)))) ∧
𝐹 ∈ V) →
((〈𝐹, ∅〉
∈ ((∅ Sat ∅)‘𝑦) ∨ 〈𝐹, ∅〉 ∈ {〈𝑥, 𝑧〉 ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))}) ↔ (〈𝐹, ∅〉 ∈ ((∅ Sat
∅)‘𝑦) ∨
𝐹 ∈ {𝑥 ∣ ∃𝑢 ∈ ((∅ Sat
∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢))}))) |
67 | | eqid 2738 |
. . . . . . . . . 10
⊢ (∅
Sat ∅) = (∅ Sat ∅) |
68 | 67 | satf0suc 32909 |
. . . . . . . . 9
⊢ (𝑦 ∈ ω → ((∅
Sat ∅)‘suc 𝑦) =
(((∅ Sat ∅)‘𝑦) ∪ {〈𝑥, 𝑧〉 ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))})) |
69 | 68 | eleq2d 2818 |
. . . . . . . 8
⊢ (𝑦 ∈ ω →
(〈𝐹, ∅〉
∈ ((∅ Sat ∅)‘suc 𝑦) ↔ 〈𝐹, ∅〉 ∈ (((∅ Sat
∅)‘𝑦) ∪
{〈𝑥, 𝑧〉 ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ ((∅ Sat
∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))}))) |
70 | | elun 4039 |
. . . . . . . 8
⊢
(〈𝐹,
∅〉 ∈ (((∅ Sat ∅)‘𝑦) ∪ {〈𝑥, 𝑧〉 ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))}) ↔ (〈𝐹, ∅〉 ∈ ((∅ Sat
∅)‘𝑦) ∨
〈𝐹, ∅〉
∈ {〈𝑥, 𝑧〉 ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ ((∅ Sat
∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))})) |
71 | 69, 70 | bitrdi 290 |
. . . . . . 7
⊢ (𝑦 ∈ ω →
(〈𝐹, ∅〉
∈ ((∅ Sat ∅)‘suc 𝑦) ↔ (〈𝐹, ∅〉 ∈ ((∅ Sat
∅)‘𝑦) ∨
〈𝐹, ∅〉
∈ {〈𝑥, 𝑧〉 ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ ((∅ Sat
∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))}))) |
72 | 71 | ad2antrr 726 |
. . . . . 6
⊢ (((𝑦 ∈ ω ∧ (𝐹 ∈ V → (𝐹 ∈ (Fmla‘𝑦) ↔ 〈𝐹, ∅〉 ∈ ((∅ Sat
∅)‘𝑦)))) ∧
𝐹 ∈ V) →
(〈𝐹, ∅〉
∈ ((∅ Sat ∅)‘suc 𝑦) ↔ (〈𝐹, ∅〉 ∈ ((∅ Sat
∅)‘𝑦) ∨
〈𝐹, ∅〉
∈ {〈𝑥, 𝑧〉 ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ ((∅ Sat
∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))}))) |
73 | | fmlasuc0 32917 |
. . . . . . . . 9
⊢ (𝑦 ∈ ω →
(Fmla‘suc 𝑦) =
((Fmla‘𝑦) ∪
{𝑥 ∣ ∃𝑢 ∈ ((∅ Sat
∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢))})) |
74 | 73 | eleq2d 2818 |
. . . . . . . 8
⊢ (𝑦 ∈ ω → (𝐹 ∈ (Fmla‘suc 𝑦) ↔ 𝐹 ∈ ((Fmla‘𝑦) ∪ {𝑥 ∣ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢))}))) |
75 | 74 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝑦 ∈ ω ∧ (𝐹 ∈ V → (𝐹 ∈ (Fmla‘𝑦) ↔ 〈𝐹, ∅〉 ∈ ((∅ Sat
∅)‘𝑦)))) ∧
𝐹 ∈ V) → (𝐹 ∈ (Fmla‘suc 𝑦) ↔ 𝐹 ∈ ((Fmla‘𝑦) ∪ {𝑥 ∣ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢))}))) |
76 | | elun 4039 |
. . . . . . . 8
⊢ (𝐹 ∈ ((Fmla‘𝑦) ∪ {𝑥 ∣ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢))}) ↔ (𝐹 ∈ (Fmla‘𝑦) ∨ 𝐹 ∈ {𝑥 ∣ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢))})) |
77 | 76 | a1i 11 |
. . . . . . 7
⊢ (((𝑦 ∈ ω ∧ (𝐹 ∈ V → (𝐹 ∈ (Fmla‘𝑦) ↔ 〈𝐹, ∅〉 ∈ ((∅ Sat
∅)‘𝑦)))) ∧
𝐹 ∈ V) → (𝐹 ∈ ((Fmla‘𝑦) ∪ {𝑥 ∣ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢))}) ↔ (𝐹 ∈ (Fmla‘𝑦) ∨ 𝐹 ∈ {𝑥 ∣ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢))}))) |
78 | | simpr 488 |
. . . . . . . . 9
⊢ ((𝑦 ∈ ω ∧ (𝐹 ∈ V → (𝐹 ∈ (Fmla‘𝑦) ↔ 〈𝐹, ∅〉 ∈ ((∅ Sat
∅)‘𝑦)))) →
(𝐹 ∈ V → (𝐹 ∈ (Fmla‘𝑦) ↔ 〈𝐹, ∅〉 ∈ ((∅ Sat
∅)‘𝑦)))) |
79 | 78 | imp 410 |
. . . . . . . 8
⊢ (((𝑦 ∈ ω ∧ (𝐹 ∈ V → (𝐹 ∈ (Fmla‘𝑦) ↔ 〈𝐹, ∅〉 ∈ ((∅ Sat
∅)‘𝑦)))) ∧
𝐹 ∈ V) → (𝐹 ∈ (Fmla‘𝑦) ↔ 〈𝐹, ∅〉 ∈ ((∅ Sat
∅)‘𝑦))) |
80 | 79 | orbi1d 916 |
. . . . . . 7
⊢ (((𝑦 ∈ ω ∧ (𝐹 ∈ V → (𝐹 ∈ (Fmla‘𝑦) ↔ 〈𝐹, ∅〉 ∈ ((∅ Sat
∅)‘𝑦)))) ∧
𝐹 ∈ V) → ((𝐹 ∈ (Fmla‘𝑦) ∨ 𝐹 ∈ {𝑥 ∣ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢))}) ↔ (〈𝐹, ∅〉 ∈ ((∅ Sat
∅)‘𝑦) ∨
𝐹 ∈ {𝑥 ∣ ∃𝑢 ∈ ((∅ Sat
∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢))}))) |
81 | 75, 77, 80 | 3bitrd 308 |
. . . . . 6
⊢ (((𝑦 ∈ ω ∧ (𝐹 ∈ V → (𝐹 ∈ (Fmla‘𝑦) ↔ 〈𝐹, ∅〉 ∈ ((∅ Sat
∅)‘𝑦)))) ∧
𝐹 ∈ V) → (𝐹 ∈ (Fmla‘suc 𝑦) ↔ (〈𝐹, ∅〉 ∈ ((∅
Sat ∅)‘𝑦) ∨
𝐹 ∈ {𝑥 ∣ ∃𝑢 ∈ ((∅ Sat
∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢))}))) |
82 | 66, 72, 81 | 3bitr4rd 315 |
. . . . 5
⊢ (((𝑦 ∈ ω ∧ (𝐹 ∈ V → (𝐹 ∈ (Fmla‘𝑦) ↔ 〈𝐹, ∅〉 ∈ ((∅ Sat
∅)‘𝑦)))) ∧
𝐹 ∈ V) → (𝐹 ∈ (Fmla‘suc 𝑦) ↔ 〈𝐹, ∅〉 ∈ ((∅ Sat
∅)‘suc 𝑦))) |
83 | 82 | exp31 423 |
. . . 4
⊢ (𝑦 ∈ ω → ((𝐹 ∈ V → (𝐹 ∈ (Fmla‘𝑦) ↔ 〈𝐹, ∅〉 ∈ ((∅ Sat
∅)‘𝑦))) →
(𝐹 ∈ V → (𝐹 ∈ (Fmla‘suc 𝑦) ↔ 〈𝐹, ∅〉 ∈ ((∅ Sat
∅)‘suc 𝑦))))) |
84 | 6, 12, 18, 24, 48, 83 | finds 7629 |
. . 3
⊢ (𝑁 ∈ ω → (𝐹 ∈ V → (𝐹 ∈ (Fmla‘𝑁) ↔ 〈𝐹, ∅〉 ∈ ((∅ Sat
∅)‘𝑁)))) |
85 | 84 | com12 32 |
. 2
⊢ (𝐹 ∈ V → (𝑁 ∈ ω → (𝐹 ∈ (Fmla‘𝑁) ↔ 〈𝐹, ∅〉 ∈ ((∅ Sat
∅)‘𝑁)))) |
86 | | prcnel 3421 |
. . . . 5
⊢ (¬
𝐹 ∈ V → ¬
𝐹 ∈ (Fmla‘𝑁)) |
87 | 86 | adantr 484 |
. . . 4
⊢ ((¬
𝐹 ∈ V ∧ 𝑁 ∈ ω) → ¬
𝐹 ∈ (Fmla‘𝑁)) |
88 | | opprc1 4785 |
. . . . . 6
⊢ (¬
𝐹 ∈ V →
〈𝐹, ∅〉 =
∅) |
89 | 88 | adantr 484 |
. . . . 5
⊢ ((¬
𝐹 ∈ V ∧ 𝑁 ∈ ω) →
〈𝐹, ∅〉 =
∅) |
90 | | satf0n0 32911 |
. . . . . . 7
⊢ (𝑁 ∈ ω → ∅
∉ ((∅ Sat ∅)‘𝑁)) |
91 | | df-nel 3039 |
. . . . . . 7
⊢ (∅
∉ ((∅ Sat ∅)‘𝑁) ↔ ¬ ∅ ∈ ((∅ Sat
∅)‘𝑁)) |
92 | 90, 91 | sylib 221 |
. . . . . 6
⊢ (𝑁 ∈ ω → ¬
∅ ∈ ((∅ Sat ∅)‘𝑁)) |
93 | 92 | adantl 485 |
. . . . 5
⊢ ((¬
𝐹 ∈ V ∧ 𝑁 ∈ ω) → ¬
∅ ∈ ((∅ Sat ∅)‘𝑁)) |
94 | 89, 93 | eqneltrd 2852 |
. . . 4
⊢ ((¬
𝐹 ∈ V ∧ 𝑁 ∈ ω) → ¬
〈𝐹, ∅〉
∈ ((∅ Sat ∅)‘𝑁)) |
95 | 87, 94 | 2falsed 380 |
. . 3
⊢ ((¬
𝐹 ∈ V ∧ 𝑁 ∈ ω) → (𝐹 ∈ (Fmla‘𝑁) ↔ 〈𝐹, ∅〉 ∈ ((∅ Sat
∅)‘𝑁))) |
96 | 95 | ex 416 |
. 2
⊢ (¬
𝐹 ∈ V → (𝑁 ∈ ω → (𝐹 ∈ (Fmla‘𝑁) ↔ 〈𝐹, ∅〉 ∈ ((∅ Sat
∅)‘𝑁)))) |
97 | 85, 96 | pm2.61i 185 |
1
⊢ (𝑁 ∈ ω → (𝐹 ∈ (Fmla‘𝑁) ↔ 〈𝐹, ∅〉 ∈ ((∅ Sat
∅)‘𝑁))) |