Proof of Theorem vtocl3
Step | Hyp | Ref
| Expression |
1 | | vtocl3.1 |
. . . . . . 7
⊢ 𝐴 ∈ V |
2 | 1 | isseti 3426 |
. . . . . 6
⊢
∃𝑥 𝑥 = 𝐴 |
3 | | vtocl3.2 |
. . . . . . 7
⊢ 𝐵 ∈ V |
4 | 3 | isseti 3426 |
. . . . . 6
⊢
∃𝑦 𝑦 = 𝐵 |
5 | | vtocl3.3 |
. . . . . . 7
⊢ 𝐶 ∈ V |
6 | 5 | isseti 3426 |
. . . . . 6
⊢
∃𝑧 𝑧 = 𝐶 |
7 | | eeeanv 2374 |
. . . . . . 7
⊢
(∃𝑥∃𝑦∃𝑧(𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶) ↔ (∃𝑥 𝑥 = 𝐴 ∧ ∃𝑦 𝑦 = 𝐵 ∧ ∃𝑧 𝑧 = 𝐶)) |
8 | | vtocl3.4 |
. . . . . . . . . 10
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶) → (𝜑 ↔ 𝜓)) |
9 | 8 | biimpd 221 |
. . . . . . . . 9
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶) → (𝜑 → 𝜓)) |
10 | 9 | eximi 1933 |
. . . . . . . 8
⊢
(∃𝑧(𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶) → ∃𝑧(𝜑 → 𝜓)) |
11 | 10 | 2eximi 1934 |
. . . . . . 7
⊢
(∃𝑥∃𝑦∃𝑧(𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶) → ∃𝑥∃𝑦∃𝑧(𝜑 → 𝜓)) |
12 | 7, 11 | sylbir 227 |
. . . . . 6
⊢
((∃𝑥 𝑥 = 𝐴 ∧ ∃𝑦 𝑦 = 𝐵 ∧ ∃𝑧 𝑧 = 𝐶) → ∃𝑥∃𝑦∃𝑧(𝜑 → 𝜓)) |
13 | 2, 4, 6, 12 | mp3an 1589 |
. . . . 5
⊢
∃𝑥∃𝑦∃𝑧(𝜑 → 𝜓) |
14 | | 19.36v 2091 |
. . . . . 6
⊢
(∃𝑧(𝜑 → 𝜓) ↔ (∀𝑧𝜑 → 𝜓)) |
15 | 14 | 2exbii 1948 |
. . . . 5
⊢
(∃𝑥∃𝑦∃𝑧(𝜑 → 𝜓) ↔ ∃𝑥∃𝑦(∀𝑧𝜑 → 𝜓)) |
16 | 13, 15 | mpbi 222 |
. . . 4
⊢
∃𝑥∃𝑦(∀𝑧𝜑 → 𝜓) |
17 | | 19.36v 2091 |
. . . . 5
⊢
(∃𝑦(∀𝑧𝜑 → 𝜓) ↔ (∀𝑦∀𝑧𝜑 → 𝜓)) |
18 | 17 | exbii 1947 |
. . . 4
⊢
(∃𝑥∃𝑦(∀𝑧𝜑 → 𝜓) ↔ ∃𝑥(∀𝑦∀𝑧𝜑 → 𝜓)) |
19 | 16, 18 | mpbi 222 |
. . 3
⊢
∃𝑥(∀𝑦∀𝑧𝜑 → 𝜓) |
20 | 19 | 19.36iv 2045 |
. 2
⊢
(∀𝑥∀𝑦∀𝑧𝜑 → 𝜓) |
21 | | vtocl3.5 |
. . 3
⊢ 𝜑 |
22 | 21 | gen2 1895 |
. 2
⊢
∀𝑦∀𝑧𝜑 |
23 | 20, 22 | mpg 1896 |
1
⊢ 𝜓 |