Proof of Theorem vtocl3
Step | Hyp | Ref
| Expression |
1 | | vtocl3.1 |
. . . . . . 7
⊢ 𝐴 ∈ V |
2 | 1 | isseti 2732 |
. . . . . 6
⊢
∃𝑥 𝑥 = 𝐴 |
3 | | vtocl3.2 |
. . . . . . 7
⊢ 𝐵 ∈ V |
4 | 3 | isseti 2732 |
. . . . . 6
⊢
∃𝑦 𝑦 = 𝐵 |
5 | | vtocl3.3 |
. . . . . . 7
⊢ 𝐶 ∈ V |
6 | 5 | isseti 2732 |
. . . . . 6
⊢
∃𝑧 𝑧 = 𝐶 |
7 | | eeeanv 1920 |
. . . . . . 7
⊢
(∃𝑥∃𝑦∃𝑧(𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶) ↔ (∃𝑥 𝑥 = 𝐴 ∧ ∃𝑦 𝑦 = 𝐵 ∧ ∃𝑧 𝑧 = 𝐶)) |
8 | | vtocl3.4 |
. . . . . . . . . 10
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶) → (𝜑 ↔ 𝜓)) |
9 | 8 | biimpd 143 |
. . . . . . . . 9
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶) → (𝜑 → 𝜓)) |
10 | 9 | eximi 1587 |
. . . . . . . 8
⊢
(∃𝑧(𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶) → ∃𝑧(𝜑 → 𝜓)) |
11 | 10 | 2eximi 1588 |
. . . . . . 7
⊢
(∃𝑥∃𝑦∃𝑧(𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶) → ∃𝑥∃𝑦∃𝑧(𝜑 → 𝜓)) |
12 | 7, 11 | sylbir 134 |
. . . . . 6
⊢
((∃𝑥 𝑥 = 𝐴 ∧ ∃𝑦 𝑦 = 𝐵 ∧ ∃𝑧 𝑧 = 𝐶) → ∃𝑥∃𝑦∃𝑧(𝜑 → 𝜓)) |
13 | 2, 4, 6, 12 | mp3an 1326 |
. . . . 5
⊢
∃𝑥∃𝑦∃𝑧(𝜑 → 𝜓) |
14 | | nfv 1515 |
. . . . . . 7
⊢
Ⅎ𝑧𝜓 |
15 | 14 | 19.36-1 1660 |
. . . . . 6
⊢
(∃𝑧(𝜑 → 𝜓) → (∀𝑧𝜑 → 𝜓)) |
16 | 15 | 2eximi 1588 |
. . . . 5
⊢
(∃𝑥∃𝑦∃𝑧(𝜑 → 𝜓) → ∃𝑥∃𝑦(∀𝑧𝜑 → 𝜓)) |
17 | 13, 16 | ax-mp 5 |
. . . 4
⊢
∃𝑥∃𝑦(∀𝑧𝜑 → 𝜓) |
18 | | nfv 1515 |
. . . . 5
⊢
Ⅎ𝑦𝜓 |
19 | 18 | 19.36-1 1660 |
. . . 4
⊢
(∃𝑦(∀𝑧𝜑 → 𝜓) → (∀𝑦∀𝑧𝜑 → 𝜓)) |
20 | 17, 19 | eximii 1589 |
. . 3
⊢
∃𝑥(∀𝑦∀𝑧𝜑 → 𝜓) |
21 | 20 | 19.36aiv 1888 |
. 2
⊢
(∀𝑥∀𝑦∀𝑧𝜑 → 𝜓) |
22 | | vtocl3.5 |
. . 3
⊢ 𝜑 |
23 | 22 | gen2 1437 |
. 2
⊢
∀𝑦∀𝑧𝜑 |
24 | 21, 23 | mpg 1438 |
1
⊢ 𝜓 |