Step |
Hyp |
Ref |
Expression |
1 |
|
isch2 |
⊢ ( 𝐻 ∈ Cℋ ↔ ( 𝐻 ∈ Sℋ ∧ ∀ 𝑓 ∀ 𝑥 ( ( 𝑓 : ℕ ⟶ 𝐻 ∧ 𝑓 ⇝𝑣 𝑥 ) → 𝑥 ∈ 𝐻 ) ) ) |
2 |
|
ax-hcompl |
⊢ ( 𝑓 ∈ Cauchy → ∃ 𝑥 ∈ ℋ 𝑓 ⇝𝑣 𝑥 ) |
3 |
|
rexex |
⊢ ( ∃ 𝑥 ∈ ℋ 𝑓 ⇝𝑣 𝑥 → ∃ 𝑥 𝑓 ⇝𝑣 𝑥 ) |
4 |
2 3
|
syl |
⊢ ( 𝑓 ∈ Cauchy → ∃ 𝑥 𝑓 ⇝𝑣 𝑥 ) |
5 |
|
19.29 |
⊢ ( ( ∀ 𝑥 ( ( 𝑓 : ℕ ⟶ 𝐻 ∧ 𝑓 ⇝𝑣 𝑥 ) → 𝑥 ∈ 𝐻 ) ∧ ∃ 𝑥 𝑓 ⇝𝑣 𝑥 ) → ∃ 𝑥 ( ( ( 𝑓 : ℕ ⟶ 𝐻 ∧ 𝑓 ⇝𝑣 𝑥 ) → 𝑥 ∈ 𝐻 ) ∧ 𝑓 ⇝𝑣 𝑥 ) ) |
6 |
4 5
|
sylan2 |
⊢ ( ( ∀ 𝑥 ( ( 𝑓 : ℕ ⟶ 𝐻 ∧ 𝑓 ⇝𝑣 𝑥 ) → 𝑥 ∈ 𝐻 ) ∧ 𝑓 ∈ Cauchy ) → ∃ 𝑥 ( ( ( 𝑓 : ℕ ⟶ 𝐻 ∧ 𝑓 ⇝𝑣 𝑥 ) → 𝑥 ∈ 𝐻 ) ∧ 𝑓 ⇝𝑣 𝑥 ) ) |
7 |
|
id |
⊢ ( ( ( 𝑓 : ℕ ⟶ 𝐻 ∧ 𝑓 ⇝𝑣 𝑥 ) → 𝑥 ∈ 𝐻 ) → ( ( 𝑓 : ℕ ⟶ 𝐻 ∧ 𝑓 ⇝𝑣 𝑥 ) → 𝑥 ∈ 𝐻 ) ) |
8 |
7
|
imp |
⊢ ( ( ( ( 𝑓 : ℕ ⟶ 𝐻 ∧ 𝑓 ⇝𝑣 𝑥 ) → 𝑥 ∈ 𝐻 ) ∧ ( 𝑓 : ℕ ⟶ 𝐻 ∧ 𝑓 ⇝𝑣 𝑥 ) ) → 𝑥 ∈ 𝐻 ) |
9 |
8
|
an12s |
⊢ ( ( 𝑓 : ℕ ⟶ 𝐻 ∧ ( ( ( 𝑓 : ℕ ⟶ 𝐻 ∧ 𝑓 ⇝𝑣 𝑥 ) → 𝑥 ∈ 𝐻 ) ∧ 𝑓 ⇝𝑣 𝑥 ) ) → 𝑥 ∈ 𝐻 ) |
10 |
|
simprr |
⊢ ( ( 𝑓 : ℕ ⟶ 𝐻 ∧ ( ( ( 𝑓 : ℕ ⟶ 𝐻 ∧ 𝑓 ⇝𝑣 𝑥 ) → 𝑥 ∈ 𝐻 ) ∧ 𝑓 ⇝𝑣 𝑥 ) ) → 𝑓 ⇝𝑣 𝑥 ) |
11 |
9 10
|
jca |
⊢ ( ( 𝑓 : ℕ ⟶ 𝐻 ∧ ( ( ( 𝑓 : ℕ ⟶ 𝐻 ∧ 𝑓 ⇝𝑣 𝑥 ) → 𝑥 ∈ 𝐻 ) ∧ 𝑓 ⇝𝑣 𝑥 ) ) → ( 𝑥 ∈ 𝐻 ∧ 𝑓 ⇝𝑣 𝑥 ) ) |
12 |
11
|
ex |
⊢ ( 𝑓 : ℕ ⟶ 𝐻 → ( ( ( ( 𝑓 : ℕ ⟶ 𝐻 ∧ 𝑓 ⇝𝑣 𝑥 ) → 𝑥 ∈ 𝐻 ) ∧ 𝑓 ⇝𝑣 𝑥 ) → ( 𝑥 ∈ 𝐻 ∧ 𝑓 ⇝𝑣 𝑥 ) ) ) |
13 |
12
|
eximdv |
⊢ ( 𝑓 : ℕ ⟶ 𝐻 → ( ∃ 𝑥 ( ( ( 𝑓 : ℕ ⟶ 𝐻 ∧ 𝑓 ⇝𝑣 𝑥 ) → 𝑥 ∈ 𝐻 ) ∧ 𝑓 ⇝𝑣 𝑥 ) → ∃ 𝑥 ( 𝑥 ∈ 𝐻 ∧ 𝑓 ⇝𝑣 𝑥 ) ) ) |
14 |
13
|
com12 |
⊢ ( ∃ 𝑥 ( ( ( 𝑓 : ℕ ⟶ 𝐻 ∧ 𝑓 ⇝𝑣 𝑥 ) → 𝑥 ∈ 𝐻 ) ∧ 𝑓 ⇝𝑣 𝑥 ) → ( 𝑓 : ℕ ⟶ 𝐻 → ∃ 𝑥 ( 𝑥 ∈ 𝐻 ∧ 𝑓 ⇝𝑣 𝑥 ) ) ) |
15 |
|
df-rex |
⊢ ( ∃ 𝑥 ∈ 𝐻 𝑓 ⇝𝑣 𝑥 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐻 ∧ 𝑓 ⇝𝑣 𝑥 ) ) |
16 |
14 15
|
syl6ibr |
⊢ ( ∃ 𝑥 ( ( ( 𝑓 : ℕ ⟶ 𝐻 ∧ 𝑓 ⇝𝑣 𝑥 ) → 𝑥 ∈ 𝐻 ) ∧ 𝑓 ⇝𝑣 𝑥 ) → ( 𝑓 : ℕ ⟶ 𝐻 → ∃ 𝑥 ∈ 𝐻 𝑓 ⇝𝑣 𝑥 ) ) |
17 |
6 16
|
syl |
⊢ ( ( ∀ 𝑥 ( ( 𝑓 : ℕ ⟶ 𝐻 ∧ 𝑓 ⇝𝑣 𝑥 ) → 𝑥 ∈ 𝐻 ) ∧ 𝑓 ∈ Cauchy ) → ( 𝑓 : ℕ ⟶ 𝐻 → ∃ 𝑥 ∈ 𝐻 𝑓 ⇝𝑣 𝑥 ) ) |
18 |
17
|
ex |
⊢ ( ∀ 𝑥 ( ( 𝑓 : ℕ ⟶ 𝐻 ∧ 𝑓 ⇝𝑣 𝑥 ) → 𝑥 ∈ 𝐻 ) → ( 𝑓 ∈ Cauchy → ( 𝑓 : ℕ ⟶ 𝐻 → ∃ 𝑥 ∈ 𝐻 𝑓 ⇝𝑣 𝑥 ) ) ) |
19 |
|
nfv |
⊢ Ⅎ 𝑥 𝑓 ∈ Cauchy |
20 |
|
nfv |
⊢ Ⅎ 𝑥 𝑓 : ℕ ⟶ 𝐻 |
21 |
|
nfre1 |
⊢ Ⅎ 𝑥 ∃ 𝑥 ∈ 𝐻 𝑓 ⇝𝑣 𝑥 |
22 |
20 21
|
nfim |
⊢ Ⅎ 𝑥 ( 𝑓 : ℕ ⟶ 𝐻 → ∃ 𝑥 ∈ 𝐻 𝑓 ⇝𝑣 𝑥 ) |
23 |
19 22
|
nfim |
⊢ Ⅎ 𝑥 ( 𝑓 ∈ Cauchy → ( 𝑓 : ℕ ⟶ 𝐻 → ∃ 𝑥 ∈ 𝐻 𝑓 ⇝𝑣 𝑥 ) ) |
24 |
|
bi2.04 |
⊢ ( ( 𝑓 ∈ Cauchy → ( 𝑓 : ℕ ⟶ 𝐻 → ∃ 𝑥 ∈ 𝐻 𝑓 ⇝𝑣 𝑥 ) ) ↔ ( 𝑓 : ℕ ⟶ 𝐻 → ( 𝑓 ∈ Cauchy → ∃ 𝑥 ∈ 𝐻 𝑓 ⇝𝑣 𝑥 ) ) ) |
25 |
|
hlimcaui |
⊢ ( 𝑓 ⇝𝑣 𝑥 → 𝑓 ∈ Cauchy ) |
26 |
25
|
imim1i |
⊢ ( ( 𝑓 ∈ Cauchy → ∃ 𝑥 ∈ 𝐻 𝑓 ⇝𝑣 𝑥 ) → ( 𝑓 ⇝𝑣 𝑥 → ∃ 𝑥 ∈ 𝐻 𝑓 ⇝𝑣 𝑥 ) ) |
27 |
|
rexex |
⊢ ( ∃ 𝑥 ∈ 𝐻 𝑓 ⇝𝑣 𝑥 → ∃ 𝑥 𝑓 ⇝𝑣 𝑥 ) |
28 |
|
hlimeui |
⊢ ( ∃ 𝑥 𝑓 ⇝𝑣 𝑥 ↔ ∃! 𝑥 𝑓 ⇝𝑣 𝑥 ) |
29 |
27 28
|
sylib |
⊢ ( ∃ 𝑥 ∈ 𝐻 𝑓 ⇝𝑣 𝑥 → ∃! 𝑥 𝑓 ⇝𝑣 𝑥 ) |
30 |
|
exancom |
⊢ ( ∃ 𝑥 ( 𝑥 ∈ 𝐻 ∧ 𝑓 ⇝𝑣 𝑥 ) ↔ ∃ 𝑥 ( 𝑓 ⇝𝑣 𝑥 ∧ 𝑥 ∈ 𝐻 ) ) |
31 |
15 30
|
sylbb |
⊢ ( ∃ 𝑥 ∈ 𝐻 𝑓 ⇝𝑣 𝑥 → ∃ 𝑥 ( 𝑓 ⇝𝑣 𝑥 ∧ 𝑥 ∈ 𝐻 ) ) |
32 |
|
eupick |
⊢ ( ( ∃! 𝑥 𝑓 ⇝𝑣 𝑥 ∧ ∃ 𝑥 ( 𝑓 ⇝𝑣 𝑥 ∧ 𝑥 ∈ 𝐻 ) ) → ( 𝑓 ⇝𝑣 𝑥 → 𝑥 ∈ 𝐻 ) ) |
33 |
29 31 32
|
syl2anc |
⊢ ( ∃ 𝑥 ∈ 𝐻 𝑓 ⇝𝑣 𝑥 → ( 𝑓 ⇝𝑣 𝑥 → 𝑥 ∈ 𝐻 ) ) |
34 |
26 33
|
syli |
⊢ ( ( 𝑓 ∈ Cauchy → ∃ 𝑥 ∈ 𝐻 𝑓 ⇝𝑣 𝑥 ) → ( 𝑓 ⇝𝑣 𝑥 → 𝑥 ∈ 𝐻 ) ) |
35 |
34
|
imim2i |
⊢ ( ( 𝑓 : ℕ ⟶ 𝐻 → ( 𝑓 ∈ Cauchy → ∃ 𝑥 ∈ 𝐻 𝑓 ⇝𝑣 𝑥 ) ) → ( 𝑓 : ℕ ⟶ 𝐻 → ( 𝑓 ⇝𝑣 𝑥 → 𝑥 ∈ 𝐻 ) ) ) |
36 |
24 35
|
sylbi |
⊢ ( ( 𝑓 ∈ Cauchy → ( 𝑓 : ℕ ⟶ 𝐻 → ∃ 𝑥 ∈ 𝐻 𝑓 ⇝𝑣 𝑥 ) ) → ( 𝑓 : ℕ ⟶ 𝐻 → ( 𝑓 ⇝𝑣 𝑥 → 𝑥 ∈ 𝐻 ) ) ) |
37 |
36
|
impd |
⊢ ( ( 𝑓 ∈ Cauchy → ( 𝑓 : ℕ ⟶ 𝐻 → ∃ 𝑥 ∈ 𝐻 𝑓 ⇝𝑣 𝑥 ) ) → ( ( 𝑓 : ℕ ⟶ 𝐻 ∧ 𝑓 ⇝𝑣 𝑥 ) → 𝑥 ∈ 𝐻 ) ) |
38 |
23 37
|
alrimi |
⊢ ( ( 𝑓 ∈ Cauchy → ( 𝑓 : ℕ ⟶ 𝐻 → ∃ 𝑥 ∈ 𝐻 𝑓 ⇝𝑣 𝑥 ) ) → ∀ 𝑥 ( ( 𝑓 : ℕ ⟶ 𝐻 ∧ 𝑓 ⇝𝑣 𝑥 ) → 𝑥 ∈ 𝐻 ) ) |
39 |
18 38
|
impbii |
⊢ ( ∀ 𝑥 ( ( 𝑓 : ℕ ⟶ 𝐻 ∧ 𝑓 ⇝𝑣 𝑥 ) → 𝑥 ∈ 𝐻 ) ↔ ( 𝑓 ∈ Cauchy → ( 𝑓 : ℕ ⟶ 𝐻 → ∃ 𝑥 ∈ 𝐻 𝑓 ⇝𝑣 𝑥 ) ) ) |
40 |
39
|
albii |
⊢ ( ∀ 𝑓 ∀ 𝑥 ( ( 𝑓 : ℕ ⟶ 𝐻 ∧ 𝑓 ⇝𝑣 𝑥 ) → 𝑥 ∈ 𝐻 ) ↔ ∀ 𝑓 ( 𝑓 ∈ Cauchy → ( 𝑓 : ℕ ⟶ 𝐻 → ∃ 𝑥 ∈ 𝐻 𝑓 ⇝𝑣 𝑥 ) ) ) |
41 |
|
df-ral |
⊢ ( ∀ 𝑓 ∈ Cauchy ( 𝑓 : ℕ ⟶ 𝐻 → ∃ 𝑥 ∈ 𝐻 𝑓 ⇝𝑣 𝑥 ) ↔ ∀ 𝑓 ( 𝑓 ∈ Cauchy → ( 𝑓 : ℕ ⟶ 𝐻 → ∃ 𝑥 ∈ 𝐻 𝑓 ⇝𝑣 𝑥 ) ) ) |
42 |
40 41
|
bitr4i |
⊢ ( ∀ 𝑓 ∀ 𝑥 ( ( 𝑓 : ℕ ⟶ 𝐻 ∧ 𝑓 ⇝𝑣 𝑥 ) → 𝑥 ∈ 𝐻 ) ↔ ∀ 𝑓 ∈ Cauchy ( 𝑓 : ℕ ⟶ 𝐻 → ∃ 𝑥 ∈ 𝐻 𝑓 ⇝𝑣 𝑥 ) ) |
43 |
42
|
anbi2i |
⊢ ( ( 𝐻 ∈ Sℋ ∧ ∀ 𝑓 ∀ 𝑥 ( ( 𝑓 : ℕ ⟶ 𝐻 ∧ 𝑓 ⇝𝑣 𝑥 ) → 𝑥 ∈ 𝐻 ) ) ↔ ( 𝐻 ∈ Sℋ ∧ ∀ 𝑓 ∈ Cauchy ( 𝑓 : ℕ ⟶ 𝐻 → ∃ 𝑥 ∈ 𝐻 𝑓 ⇝𝑣 𝑥 ) ) ) |
44 |
1 43
|
bitri |
⊢ ( 𝐻 ∈ Cℋ ↔ ( 𝐻 ∈ Sℋ ∧ ∀ 𝑓 ∈ Cauchy ( 𝑓 : ℕ ⟶ 𝐻 → ∃ 𝑥 ∈ 𝐻 𝑓 ⇝𝑣 𝑥 ) ) ) |