Proof of Theorem mosubopt
Step | Hyp | Ref
| Expression |
1 | | nfa1 1417 |
. . 3
⊢
Ⅎy∀y∀z∃*xφ |
2 | | nfe1 1367 |
. . . 4
⊢
Ⅎy∃y∃z(A = 〈y,
z〉 ∧
φ) |
3 | 2 | nfmo 1903 |
. . 3
⊢
Ⅎy∃*x∃y∃z(A = 〈y,
z〉 ∧
φ) |
4 | | nfa1 1417 |
. . . . 5
⊢
Ⅎz∀z∃*xφ |
5 | | nfe1 1367 |
. . . . . . 7
⊢
Ⅎz∃z(A = 〈y,
z〉 ∧
φ) |
6 | 5 | nfex 1512 |
. . . . . 6
⊢
Ⅎz∃y∃z(A = 〈y,
z〉 ∧
φ) |
7 | 6 | nfmo 1903 |
. . . . 5
⊢
Ⅎz∃*x∃y∃z(A = 〈y,
z〉 ∧
φ) |
8 | | copsexg 3954 |
. . . . . . . 8
⊢ (A = 〈y,
z〉 → (φ ↔ ∃y∃z(A = 〈y,
z〉 ∧
φ))) |
9 | 8 | mobidv 1919 |
. . . . . . 7
⊢ (A = 〈y,
z〉 → (∃*xφ ↔ ∃*x∃y∃z(A = 〈y,
z〉 ∧
φ))) |
10 | 9 | biimpcd 148 |
. . . . . 6
⊢ (∃*xφ → (A = 〈y,
z〉 → ∃*x∃y∃z(A = 〈y,
z〉 ∧
φ))) |
11 | 10 | sps 1413 |
. . . . 5
⊢ (∀z∃*xφ → (A = 〈y,
z〉 → ∃*x∃y∃z(A = 〈y,
z〉 ∧
φ))) |
12 | 4, 7, 11 | exlimd 1472 |
. . . 4
⊢ (∀z∃*xφ → (∃z A = 〈y,
z〉 → ∃*x∃y∃z(A = 〈y,
z〉 ∧
φ))) |
13 | 12 | sps 1413 |
. . 3
⊢ (∀y∀z∃*xφ → (∃z A = 〈y,
z〉 → ∃*x∃y∃z(A = 〈y,
z〉 ∧
φ))) |
14 | 1, 3, 13 | exlimd 1472 |
. 2
⊢ (∀y∀z∃*xφ → (∃y∃z A = 〈y,
z〉 → ∃*x∃y∃z(A = 〈y,
z〉 ∧
φ))) |
15 | | moanimv 1958 |
. . 3
⊢ (∃*x(∃y∃z A = 〈y,
z〉 ∧
∃y∃z(A = 〈y,
z〉 ∧
φ)) ↔ (∃y∃z A = 〈y,
z〉 → ∃*x∃y∃z(A = 〈y,
z〉 ∧
φ))) |
16 | | ax-ia1 99 |
. . . . . 6
⊢
((A = 〈y, z〉 ∧ φ) →
A = 〈y, z〉) |
17 | 16 | 2eximi 1476 |
. . . . 5
⊢ (∃y∃z(A = 〈y,
z〉 ∧
φ) → ∃y∃z A = 〈y,
z〉) |
18 | 17 | ancri 307 |
. . . 4
⊢ (∃y∃z(A = 〈y,
z〉 ∧
φ) → (∃y∃z A = 〈y,
z〉 ∧
∃y∃z(A = 〈y,
z〉 ∧
φ))) |
19 | 18 | moimi 1948 |
. . 3
⊢ (∃*x(∃y∃z A = 〈y,
z〉 ∧
∃y∃z(A = 〈y,
z〉 ∧
φ)) → ∃*x∃y∃z(A = 〈y,
z〉 ∧
φ)) |
20 | 15, 19 | sylbir 125 |
. 2
⊢ ((∃y∃z A = 〈y,
z〉 → ∃*x∃y∃z(A = 〈y,
z〉 ∧
φ)) → ∃*x∃y∃z(A = 〈y,
z〉 ∧
φ)) |
21 | 14, 20 | syl 14 |
1
⊢ (∀y∀z∃*xφ → ∃*x∃y∃z(A = 〈y,
z〉 ∧
φ)) |