Proof of Theorem isch3
| Step | Hyp | Ref
| Expression |
| 1 | | isch2 31242 |
. 2
⊢ (𝐻 ∈
Cℋ ↔ (𝐻 ∈ Sℋ
∧ ∀𝑓∀𝑥((𝑓:ℕ⟶𝐻 ∧ 𝑓 ⇝𝑣 𝑥) → 𝑥 ∈ 𝐻))) |
| 2 | | ax-hcompl 31221 |
. . . . . . . . . 10
⊢ (𝑓 ∈ Cauchy →
∃𝑥 ∈ ℋ
𝑓
⇝𝑣 𝑥) |
| 3 | | rexex 3076 |
. . . . . . . . . 10
⊢
(∃𝑥 ∈
ℋ 𝑓
⇝𝑣 𝑥 → ∃𝑥 𝑓 ⇝𝑣 𝑥) |
| 4 | 2, 3 | syl 17 |
. . . . . . . . 9
⊢ (𝑓 ∈ Cauchy →
∃𝑥 𝑓 ⇝𝑣 𝑥) |
| 5 | | 19.29 1873 |
. . . . . . . . 9
⊢
((∀𝑥((𝑓:ℕ⟶𝐻 ∧ 𝑓 ⇝𝑣 𝑥) → 𝑥 ∈ 𝐻) ∧ ∃𝑥 𝑓 ⇝𝑣 𝑥) → ∃𝑥(((𝑓:ℕ⟶𝐻 ∧ 𝑓 ⇝𝑣 𝑥) → 𝑥 ∈ 𝐻) ∧ 𝑓 ⇝𝑣 𝑥)) |
| 6 | 4, 5 | sylan2 593 |
. . . . . . . 8
⊢
((∀𝑥((𝑓:ℕ⟶𝐻 ∧ 𝑓 ⇝𝑣 𝑥) → 𝑥 ∈ 𝐻) ∧ 𝑓 ∈ Cauchy) → ∃𝑥(((𝑓:ℕ⟶𝐻 ∧ 𝑓 ⇝𝑣 𝑥) → 𝑥 ∈ 𝐻) ∧ 𝑓 ⇝𝑣 𝑥)) |
| 7 | | id 22 |
. . . . . . . . . . . . . . 15
⊢ (((𝑓:ℕ⟶𝐻 ∧ 𝑓 ⇝𝑣 𝑥) → 𝑥 ∈ 𝐻) → ((𝑓:ℕ⟶𝐻 ∧ 𝑓 ⇝𝑣 𝑥) → 𝑥 ∈ 𝐻)) |
| 8 | 7 | imp 406 |
. . . . . . . . . . . . . 14
⊢ ((((𝑓:ℕ⟶𝐻 ∧ 𝑓 ⇝𝑣 𝑥) → 𝑥 ∈ 𝐻) ∧ (𝑓:ℕ⟶𝐻 ∧ 𝑓 ⇝𝑣 𝑥)) → 𝑥 ∈ 𝐻) |
| 9 | 8 | an12s 649 |
. . . . . . . . . . . . 13
⊢ ((𝑓:ℕ⟶𝐻 ∧ (((𝑓:ℕ⟶𝐻 ∧ 𝑓 ⇝𝑣 𝑥) → 𝑥 ∈ 𝐻) ∧ 𝑓 ⇝𝑣 𝑥)) → 𝑥 ∈ 𝐻) |
| 10 | | simprr 773 |
. . . . . . . . . . . . 13
⊢ ((𝑓:ℕ⟶𝐻 ∧ (((𝑓:ℕ⟶𝐻 ∧ 𝑓 ⇝𝑣 𝑥) → 𝑥 ∈ 𝐻) ∧ 𝑓 ⇝𝑣 𝑥)) → 𝑓 ⇝𝑣 𝑥) |
| 11 | 9, 10 | jca 511 |
. . . . . . . . . . . 12
⊢ ((𝑓:ℕ⟶𝐻 ∧ (((𝑓:ℕ⟶𝐻 ∧ 𝑓 ⇝𝑣 𝑥) → 𝑥 ∈ 𝐻) ∧ 𝑓 ⇝𝑣 𝑥)) → (𝑥 ∈ 𝐻 ∧ 𝑓 ⇝𝑣 𝑥)) |
| 12 | 11 | ex 412 |
. . . . . . . . . . 11
⊢ (𝑓:ℕ⟶𝐻 → ((((𝑓:ℕ⟶𝐻 ∧ 𝑓 ⇝𝑣 𝑥) → 𝑥 ∈ 𝐻) ∧ 𝑓 ⇝𝑣 𝑥) → (𝑥 ∈ 𝐻 ∧ 𝑓 ⇝𝑣 𝑥))) |
| 13 | 12 | eximdv 1917 |
. . . . . . . . . 10
⊢ (𝑓:ℕ⟶𝐻 → (∃𝑥(((𝑓:ℕ⟶𝐻 ∧ 𝑓 ⇝𝑣 𝑥) → 𝑥 ∈ 𝐻) ∧ 𝑓 ⇝𝑣 𝑥) → ∃𝑥(𝑥 ∈ 𝐻 ∧ 𝑓 ⇝𝑣 𝑥))) |
| 14 | 13 | com12 32 |
. . . . . . . . 9
⊢
(∃𝑥(((𝑓:ℕ⟶𝐻 ∧ 𝑓 ⇝𝑣 𝑥) → 𝑥 ∈ 𝐻) ∧ 𝑓 ⇝𝑣 𝑥) → (𝑓:ℕ⟶𝐻 → ∃𝑥(𝑥 ∈ 𝐻 ∧ 𝑓 ⇝𝑣 𝑥))) |
| 15 | | df-rex 3071 |
. . . . . . . . 9
⊢
(∃𝑥 ∈
𝐻 𝑓 ⇝𝑣 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝐻 ∧ 𝑓 ⇝𝑣 𝑥)) |
| 16 | 14, 15 | imbitrrdi 252 |
. . . . . . . 8
⊢
(∃𝑥(((𝑓:ℕ⟶𝐻 ∧ 𝑓 ⇝𝑣 𝑥) → 𝑥 ∈ 𝐻) ∧ 𝑓 ⇝𝑣 𝑥) → (𝑓:ℕ⟶𝐻 → ∃𝑥 ∈ 𝐻 𝑓 ⇝𝑣 𝑥)) |
| 17 | 6, 16 | syl 17 |
. . . . . . 7
⊢
((∀𝑥((𝑓:ℕ⟶𝐻 ∧ 𝑓 ⇝𝑣 𝑥) → 𝑥 ∈ 𝐻) ∧ 𝑓 ∈ Cauchy) → (𝑓:ℕ⟶𝐻 → ∃𝑥 ∈ 𝐻 𝑓 ⇝𝑣 𝑥)) |
| 18 | 17 | ex 412 |
. . . . . 6
⊢
(∀𝑥((𝑓:ℕ⟶𝐻 ∧ 𝑓 ⇝𝑣 𝑥) → 𝑥 ∈ 𝐻) → (𝑓 ∈ Cauchy → (𝑓:ℕ⟶𝐻 → ∃𝑥 ∈ 𝐻 𝑓 ⇝𝑣 𝑥))) |
| 19 | | nfv 1914 |
. . . . . . . 8
⊢
Ⅎ𝑥 𝑓 ∈ Cauchy |
| 20 | | nfv 1914 |
. . . . . . . . 9
⊢
Ⅎ𝑥 𝑓:ℕ⟶𝐻 |
| 21 | | nfre1 3285 |
. . . . . . . . 9
⊢
Ⅎ𝑥∃𝑥 ∈ 𝐻 𝑓 ⇝𝑣 𝑥 |
| 22 | 20, 21 | nfim 1896 |
. . . . . . . 8
⊢
Ⅎ𝑥(𝑓:ℕ⟶𝐻 → ∃𝑥 ∈ 𝐻 𝑓 ⇝𝑣 𝑥) |
| 23 | 19, 22 | nfim 1896 |
. . . . . . 7
⊢
Ⅎ𝑥(𝑓 ∈ Cauchy → (𝑓:ℕ⟶𝐻 → ∃𝑥 ∈ 𝐻 𝑓 ⇝𝑣 𝑥)) |
| 24 | | bi2.04 387 |
. . . . . . . . 9
⊢ ((𝑓 ∈ Cauchy → (𝑓:ℕ⟶𝐻 → ∃𝑥 ∈ 𝐻 𝑓 ⇝𝑣 𝑥)) ↔ (𝑓:ℕ⟶𝐻 → (𝑓 ∈ Cauchy → ∃𝑥 ∈ 𝐻 𝑓 ⇝𝑣 𝑥))) |
| 25 | | hlimcaui 31255 |
. . . . . . . . . . . 12
⊢ (𝑓 ⇝𝑣
𝑥 → 𝑓 ∈ Cauchy) |
| 26 | 25 | imim1i 63 |
. . . . . . . . . . 11
⊢ ((𝑓 ∈ Cauchy →
∃𝑥 ∈ 𝐻 𝑓 ⇝𝑣 𝑥) → (𝑓 ⇝𝑣 𝑥 → ∃𝑥 ∈ 𝐻 𝑓 ⇝𝑣 𝑥)) |
| 27 | | rexex 3076 |
. . . . . . . . . . . . 13
⊢
(∃𝑥 ∈
𝐻 𝑓 ⇝𝑣 𝑥 → ∃𝑥 𝑓 ⇝𝑣 𝑥) |
| 28 | | hlimeui 31259 |
. . . . . . . . . . . . 13
⊢
(∃𝑥 𝑓 ⇝𝑣
𝑥 ↔ ∃!𝑥 𝑓 ⇝𝑣 𝑥) |
| 29 | 27, 28 | sylib 218 |
. . . . . . . . . . . 12
⊢
(∃𝑥 ∈
𝐻 𝑓 ⇝𝑣 𝑥 → ∃!𝑥 𝑓 ⇝𝑣 𝑥) |
| 30 | | exancom 1861 |
. . . . . . . . . . . . 13
⊢
(∃𝑥(𝑥 ∈ 𝐻 ∧ 𝑓 ⇝𝑣 𝑥) ↔ ∃𝑥(𝑓 ⇝𝑣 𝑥 ∧ 𝑥 ∈ 𝐻)) |
| 31 | 15, 30 | sylbb 219 |
. . . . . . . . . . . 12
⊢
(∃𝑥 ∈
𝐻 𝑓 ⇝𝑣 𝑥 → ∃𝑥(𝑓 ⇝𝑣 𝑥 ∧ 𝑥 ∈ 𝐻)) |
| 32 | | eupick 2633 |
. . . . . . . . . . . 12
⊢
((∃!𝑥 𝑓 ⇝𝑣
𝑥 ∧ ∃𝑥(𝑓 ⇝𝑣 𝑥 ∧ 𝑥 ∈ 𝐻)) → (𝑓 ⇝𝑣 𝑥 → 𝑥 ∈ 𝐻)) |
| 33 | 29, 31, 32 | syl2anc 584 |
. . . . . . . . . . 11
⊢
(∃𝑥 ∈
𝐻 𝑓 ⇝𝑣 𝑥 → (𝑓 ⇝𝑣 𝑥 → 𝑥 ∈ 𝐻)) |
| 34 | 26, 33 | syli 39 |
. . . . . . . . . 10
⊢ ((𝑓 ∈ Cauchy →
∃𝑥 ∈ 𝐻 𝑓 ⇝𝑣 𝑥) → (𝑓 ⇝𝑣 𝑥 → 𝑥 ∈ 𝐻)) |
| 35 | 34 | imim2i 16 |
. . . . . . . . 9
⊢ ((𝑓:ℕ⟶𝐻 → (𝑓 ∈ Cauchy → ∃𝑥 ∈ 𝐻 𝑓 ⇝𝑣 𝑥)) → (𝑓:ℕ⟶𝐻 → (𝑓 ⇝𝑣 𝑥 → 𝑥 ∈ 𝐻))) |
| 36 | 24, 35 | sylbi 217 |
. . . . . . . 8
⊢ ((𝑓 ∈ Cauchy → (𝑓:ℕ⟶𝐻 → ∃𝑥 ∈ 𝐻 𝑓 ⇝𝑣 𝑥)) → (𝑓:ℕ⟶𝐻 → (𝑓 ⇝𝑣 𝑥 → 𝑥 ∈ 𝐻))) |
| 37 | 36 | impd 410 |
. . . . . . 7
⊢ ((𝑓 ∈ Cauchy → (𝑓:ℕ⟶𝐻 → ∃𝑥 ∈ 𝐻 𝑓 ⇝𝑣 𝑥)) → ((𝑓:ℕ⟶𝐻 ∧ 𝑓 ⇝𝑣 𝑥) → 𝑥 ∈ 𝐻)) |
| 38 | 23, 37 | alrimi 2213 |
. . . . . 6
⊢ ((𝑓 ∈ Cauchy → (𝑓:ℕ⟶𝐻 → ∃𝑥 ∈ 𝐻 𝑓 ⇝𝑣 𝑥)) → ∀𝑥((𝑓:ℕ⟶𝐻 ∧ 𝑓 ⇝𝑣 𝑥) → 𝑥 ∈ 𝐻)) |
| 39 | 18, 38 | impbii 209 |
. . . . 5
⊢
(∀𝑥((𝑓:ℕ⟶𝐻 ∧ 𝑓 ⇝𝑣 𝑥) → 𝑥 ∈ 𝐻) ↔ (𝑓 ∈ Cauchy → (𝑓:ℕ⟶𝐻 → ∃𝑥 ∈ 𝐻 𝑓 ⇝𝑣 𝑥))) |
| 40 | 39 | albii 1819 |
. . . 4
⊢
(∀𝑓∀𝑥((𝑓:ℕ⟶𝐻 ∧ 𝑓 ⇝𝑣 𝑥) → 𝑥 ∈ 𝐻) ↔ ∀𝑓(𝑓 ∈ Cauchy → (𝑓:ℕ⟶𝐻 → ∃𝑥 ∈ 𝐻 𝑓 ⇝𝑣 𝑥))) |
| 41 | | df-ral 3062 |
. . . 4
⊢
(∀𝑓 ∈
Cauchy (𝑓:ℕ⟶𝐻 → ∃𝑥 ∈ 𝐻 𝑓 ⇝𝑣 𝑥) ↔ ∀𝑓(𝑓 ∈ Cauchy → (𝑓:ℕ⟶𝐻 → ∃𝑥 ∈ 𝐻 𝑓 ⇝𝑣 𝑥))) |
| 42 | 40, 41 | bitr4i 278 |
. . 3
⊢
(∀𝑓∀𝑥((𝑓:ℕ⟶𝐻 ∧ 𝑓 ⇝𝑣 𝑥) → 𝑥 ∈ 𝐻) ↔ ∀𝑓 ∈ Cauchy (𝑓:ℕ⟶𝐻 → ∃𝑥 ∈ 𝐻 𝑓 ⇝𝑣 𝑥)) |
| 43 | 42 | anbi2i 623 |
. 2
⊢ ((𝐻 ∈
Sℋ ∧ ∀𝑓∀𝑥((𝑓:ℕ⟶𝐻 ∧ 𝑓 ⇝𝑣 𝑥) → 𝑥 ∈ 𝐻)) ↔ (𝐻 ∈ Sℋ
∧ ∀𝑓 ∈
Cauchy (𝑓:ℕ⟶𝐻 → ∃𝑥 ∈ 𝐻 𝑓 ⇝𝑣 𝑥))) |
| 44 | 1, 43 | bitri 275 |
1
⊢ (𝐻 ∈
Cℋ ↔ (𝐻 ∈ Sℋ
∧ ∀𝑓 ∈
Cauchy (𝑓:ℕ⟶𝐻 → ∃𝑥 ∈ 𝐻 𝑓 ⇝𝑣 𝑥))) |