Proof of Theorem kmlem15
Step | Hyp | Ref
| Expression |
1 | | kmlem14.3 |
. . . 4
⊢ (𝜒 ↔ ∀𝑧 ∈ 𝑥 ∃!𝑣 𝑣 ∈ (𝑧 ∩ 𝑦)) |
2 | | nfv 1917 |
. . . . . . 7
⊢
Ⅎ𝑢 𝑣 ∈ (𝑧 ∩ 𝑦) |
3 | 2 | eu1 2612 |
. . . . . 6
⊢
(∃!𝑣 𝑣 ∈ (𝑧 ∩ 𝑦) ↔ ∃𝑣(𝑣 ∈ (𝑧 ∩ 𝑦) ∧ ∀𝑢([𝑢 / 𝑣]𝑣 ∈ (𝑧 ∩ 𝑦) → 𝑣 = 𝑢))) |
4 | | elin 3903 |
. . . . . . . . 9
⊢ (𝑣 ∈ (𝑧 ∩ 𝑦) ↔ (𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦)) |
5 | | clelsb1 2866 |
. . . . . . . . . . . 12
⊢ ([𝑢 / 𝑣]𝑣 ∈ (𝑧 ∩ 𝑦) ↔ 𝑢 ∈ (𝑧 ∩ 𝑦)) |
6 | | elin 3903 |
. . . . . . . . . . . 12
⊢ (𝑢 ∈ (𝑧 ∩ 𝑦) ↔ (𝑢 ∈ 𝑧 ∧ 𝑢 ∈ 𝑦)) |
7 | 5, 6 | bitri 274 |
. . . . . . . . . . 11
⊢ ([𝑢 / 𝑣]𝑣 ∈ (𝑧 ∩ 𝑦) ↔ (𝑢 ∈ 𝑧 ∧ 𝑢 ∈ 𝑦)) |
8 | | equcom 2021 |
. . . . . . . . . . 11
⊢ (𝑣 = 𝑢 ↔ 𝑢 = 𝑣) |
9 | 7, 8 | imbi12i 351 |
. . . . . . . . . 10
⊢ (([𝑢 / 𝑣]𝑣 ∈ (𝑧 ∩ 𝑦) → 𝑣 = 𝑢) ↔ ((𝑢 ∈ 𝑧 ∧ 𝑢 ∈ 𝑦) → 𝑢 = 𝑣)) |
10 | 9 | albii 1822 |
. . . . . . . . 9
⊢
(∀𝑢([𝑢 / 𝑣]𝑣 ∈ (𝑧 ∩ 𝑦) → 𝑣 = 𝑢) ↔ ∀𝑢((𝑢 ∈ 𝑧 ∧ 𝑢 ∈ 𝑦) → 𝑢 = 𝑣)) |
11 | 4, 10 | anbi12i 627 |
. . . . . . . 8
⊢ ((𝑣 ∈ (𝑧 ∩ 𝑦) ∧ ∀𝑢([𝑢 / 𝑣]𝑣 ∈ (𝑧 ∩ 𝑦) → 𝑣 = 𝑢)) ↔ ((𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦) ∧ ∀𝑢((𝑢 ∈ 𝑧 ∧ 𝑢 ∈ 𝑦) → 𝑢 = 𝑣))) |
12 | | 19.28v 1994 |
. . . . . . . 8
⊢
(∀𝑢((𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦) ∧ ((𝑢 ∈ 𝑧 ∧ 𝑢 ∈ 𝑦) → 𝑢 = 𝑣)) ↔ ((𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦) ∧ ∀𝑢((𝑢 ∈ 𝑧 ∧ 𝑢 ∈ 𝑦) → 𝑢 = 𝑣))) |
13 | 11, 12 | bitr4i 277 |
. . . . . . 7
⊢ ((𝑣 ∈ (𝑧 ∩ 𝑦) ∧ ∀𝑢([𝑢 / 𝑣]𝑣 ∈ (𝑧 ∩ 𝑦) → 𝑣 = 𝑢)) ↔ ∀𝑢((𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦) ∧ ((𝑢 ∈ 𝑧 ∧ 𝑢 ∈ 𝑦) → 𝑢 = 𝑣))) |
14 | 13 | exbii 1850 |
. . . . . 6
⊢
(∃𝑣(𝑣 ∈ (𝑧 ∩ 𝑦) ∧ ∀𝑢([𝑢 / 𝑣]𝑣 ∈ (𝑧 ∩ 𝑦) → 𝑣 = 𝑢)) ↔ ∃𝑣∀𝑢((𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦) ∧ ((𝑢 ∈ 𝑧 ∧ 𝑢 ∈ 𝑦) → 𝑢 = 𝑣))) |
15 | 3, 14 | bitri 274 |
. . . . 5
⊢
(∃!𝑣 𝑣 ∈ (𝑧 ∩ 𝑦) ↔ ∃𝑣∀𝑢((𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦) ∧ ((𝑢 ∈ 𝑧 ∧ 𝑢 ∈ 𝑦) → 𝑢 = 𝑣))) |
16 | 15 | ralbii 3092 |
. . . 4
⊢
(∀𝑧 ∈
𝑥 ∃!𝑣 𝑣 ∈ (𝑧 ∩ 𝑦) ↔ ∀𝑧 ∈ 𝑥 ∃𝑣∀𝑢((𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦) ∧ ((𝑢 ∈ 𝑧 ∧ 𝑢 ∈ 𝑦) → 𝑢 = 𝑣))) |
17 | | df-ral 3069 |
. . . . 5
⊢
(∀𝑧 ∈
𝑥 ∃𝑣∀𝑢((𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦) ∧ ((𝑢 ∈ 𝑧 ∧ 𝑢 ∈ 𝑦) → 𝑢 = 𝑣)) ↔ ∀𝑧(𝑧 ∈ 𝑥 → ∃𝑣∀𝑢((𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦) ∧ ((𝑢 ∈ 𝑧 ∧ 𝑢 ∈ 𝑦) → 𝑢 = 𝑣)))) |
18 | | kmlem14.2 |
. . . . . . . . . 10
⊢ (𝜓 ↔ (𝑧 ∈ 𝑥 → ((𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦) ∧ ((𝑢 ∈ 𝑧 ∧ 𝑢 ∈ 𝑦) → 𝑢 = 𝑣)))) |
19 | 18 | albii 1822 |
. . . . . . . . 9
⊢
(∀𝑢𝜓 ↔ ∀𝑢(𝑧 ∈ 𝑥 → ((𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦) ∧ ((𝑢 ∈ 𝑧 ∧ 𝑢 ∈ 𝑦) → 𝑢 = 𝑣)))) |
20 | | 19.21v 1942 |
. . . . . . . . 9
⊢
(∀𝑢(𝑧 ∈ 𝑥 → ((𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦) ∧ ((𝑢 ∈ 𝑧 ∧ 𝑢 ∈ 𝑦) → 𝑢 = 𝑣))) ↔ (𝑧 ∈ 𝑥 → ∀𝑢((𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦) ∧ ((𝑢 ∈ 𝑧 ∧ 𝑢 ∈ 𝑦) → 𝑢 = 𝑣)))) |
21 | 19, 20 | bitri 274 |
. . . . . . . 8
⊢
(∀𝑢𝜓 ↔ (𝑧 ∈ 𝑥 → ∀𝑢((𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦) ∧ ((𝑢 ∈ 𝑧 ∧ 𝑢 ∈ 𝑦) → 𝑢 = 𝑣)))) |
22 | 21 | exbii 1850 |
. . . . . . 7
⊢
(∃𝑣∀𝑢𝜓 ↔ ∃𝑣(𝑧 ∈ 𝑥 → ∀𝑢((𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦) ∧ ((𝑢 ∈ 𝑧 ∧ 𝑢 ∈ 𝑦) → 𝑢 = 𝑣)))) |
23 | | 19.37v 1995 |
. . . . . . 7
⊢
(∃𝑣(𝑧 ∈ 𝑥 → ∀𝑢((𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦) ∧ ((𝑢 ∈ 𝑧 ∧ 𝑢 ∈ 𝑦) → 𝑢 = 𝑣))) ↔ (𝑧 ∈ 𝑥 → ∃𝑣∀𝑢((𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦) ∧ ((𝑢 ∈ 𝑧 ∧ 𝑢 ∈ 𝑦) → 𝑢 = 𝑣)))) |
24 | 22, 23 | bitri 274 |
. . . . . 6
⊢
(∃𝑣∀𝑢𝜓 ↔ (𝑧 ∈ 𝑥 → ∃𝑣∀𝑢((𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦) ∧ ((𝑢 ∈ 𝑧 ∧ 𝑢 ∈ 𝑦) → 𝑢 = 𝑣)))) |
25 | 24 | albii 1822 |
. . . . 5
⊢
(∀𝑧∃𝑣∀𝑢𝜓 ↔ ∀𝑧(𝑧 ∈ 𝑥 → ∃𝑣∀𝑢((𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦) ∧ ((𝑢 ∈ 𝑧 ∧ 𝑢 ∈ 𝑦) → 𝑢 = 𝑣)))) |
26 | 17, 25 | bitr4i 277 |
. . . 4
⊢
(∀𝑧 ∈
𝑥 ∃𝑣∀𝑢((𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦) ∧ ((𝑢 ∈ 𝑧 ∧ 𝑢 ∈ 𝑦) → 𝑢 = 𝑣)) ↔ ∀𝑧∃𝑣∀𝑢𝜓) |
27 | 1, 16, 26 | 3bitri 297 |
. . 3
⊢ (𝜒 ↔ ∀𝑧∃𝑣∀𝑢𝜓) |
28 | 27 | anbi2i 623 |
. 2
⊢ ((¬
𝑦 ∈ 𝑥 ∧ 𝜒) ↔ (¬ 𝑦 ∈ 𝑥 ∧ ∀𝑧∃𝑣∀𝑢𝜓)) |
29 | | 19.28v 1994 |
. 2
⊢
(∀𝑧(¬
𝑦 ∈ 𝑥 ∧ ∃𝑣∀𝑢𝜓) ↔ (¬ 𝑦 ∈ 𝑥 ∧ ∀𝑧∃𝑣∀𝑢𝜓)) |
30 | | 19.28v 1994 |
. . . . 5
⊢
(∀𝑢(¬
𝑦 ∈ 𝑥 ∧ 𝜓) ↔ (¬ 𝑦 ∈ 𝑥 ∧ ∀𝑢𝜓)) |
31 | 30 | exbii 1850 |
. . . 4
⊢
(∃𝑣∀𝑢(¬ 𝑦 ∈ 𝑥 ∧ 𝜓) ↔ ∃𝑣(¬ 𝑦 ∈ 𝑥 ∧ ∀𝑢𝜓)) |
32 | | 19.42v 1957 |
. . . 4
⊢
(∃𝑣(¬
𝑦 ∈ 𝑥 ∧ ∀𝑢𝜓) ↔ (¬ 𝑦 ∈ 𝑥 ∧ ∃𝑣∀𝑢𝜓)) |
33 | 31, 32 | bitr2i 275 |
. . 3
⊢ ((¬
𝑦 ∈ 𝑥 ∧ ∃𝑣∀𝑢𝜓) ↔ ∃𝑣∀𝑢(¬ 𝑦 ∈ 𝑥 ∧ 𝜓)) |
34 | 33 | albii 1822 |
. 2
⊢
(∀𝑧(¬
𝑦 ∈ 𝑥 ∧ ∃𝑣∀𝑢𝜓) ↔ ∀𝑧∃𝑣∀𝑢(¬ 𝑦 ∈ 𝑥 ∧ 𝜓)) |
35 | 28, 29, 34 | 3bitr2i 299 |
1
⊢ ((¬
𝑦 ∈ 𝑥 ∧ 𝜒) ↔ ∀𝑧∃𝑣∀𝑢(¬ 𝑦 ∈ 𝑥 ∧ 𝜓)) |