This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem occl

Description: Closure of complement of Hilbert subset. Part of Remark 3.12 of Beran p. 107. (Contributed by NM, 8-Aug-2000) (Proof shortened by Mario Carneiro, 14-May-2014) (New usage is discouraged.)

Ref Expression
Assertion occl ( 𝐴 ⊆ ℋ → ( ⊥ ‘ 𝐴 ) ∈ Cℋ )

Proof

Step Hyp Ref Expression
1 ocsh ⊢ ( 𝐴 ⊆ ℋ → ( ⊥ ‘ 𝐴 ) ∈ Sℋ )
2 ax-hcompl ⊢ ( 𝑓 ∈ Cauchy → ∃ 𝑥 ∈ ℋ 𝑓 ⇝𝑣 𝑥 )
3 vex ⊢ 𝑓 ∈ V
4 vex ⊢ 𝑥 ∈ V
5 3 4 breldm ⊢ ( 𝑓 ⇝𝑣 𝑥 → 𝑓 ∈ dom ⇝𝑣 )
6 5 rexlimivw ⊢ ( ∃ 𝑥 ∈ ℋ 𝑓 ⇝𝑣 𝑥 → 𝑓 ∈ dom ⇝𝑣 )
7 2 6 syl ⊢ ( 𝑓 ∈ Cauchy → 𝑓 ∈ dom ⇝𝑣 )
8 7 ad2antlr ⊢ ( ( ( 𝐴 ⊆ ℋ ∧ 𝑓 ∈ Cauchy ) ∧ 𝑓 : ℕ ⟶ ( ⊥ ‘ 𝐴 ) ) → 𝑓 ∈ dom ⇝𝑣 )
9 hlimf ⊢ ⇝𝑣 : dom ⇝𝑣 ⟶ ℋ
10 9 ffvelcdmi ⊢ ( 𝑓 ∈ dom ⇝𝑣 → ( ⇝𝑣 ‘ 𝑓 ) ∈ ℋ )
11 8 10 syl ⊢ ( ( ( 𝐴 ⊆ ℋ ∧ 𝑓 ∈ Cauchy ) ∧ 𝑓 : ℕ ⟶ ( ⊥ ‘ 𝐴 ) ) → ( ⇝𝑣 ‘ 𝑓 ) ∈ ℋ )
12 simplll ⊢ ( ( ( ( 𝐴 ⊆ ℋ ∧ 𝑓 ∈ Cauchy ) ∧ 𝑓 : ℕ ⟶ ( ⊥ ‘ 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) → 𝐴 ⊆ ℋ )
13 simpllr ⊢ ( ( ( ( 𝐴 ⊆ ℋ ∧ 𝑓 ∈ Cauchy ) ∧ 𝑓 : ℕ ⟶ ( ⊥ ‘ 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) → 𝑓 ∈ Cauchy )
14 simplr ⊢ ( ( ( ( 𝐴 ⊆ ℋ ∧ 𝑓 ∈ Cauchy ) ∧ 𝑓 : ℕ ⟶ ( ⊥ ‘ 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) → 𝑓 : ℕ ⟶ ( ⊥ ‘ 𝐴 ) )
15 simpr ⊢ ( ( ( ( 𝐴 ⊆ ℋ ∧ 𝑓 ∈ Cauchy ) ∧ 𝑓 : ℕ ⟶ ( ⊥ ‘ 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ 𝐴 )
16 12 13 14 15 occllem ⊢ ( ( ( ( 𝐴 ⊆ ℋ ∧ 𝑓 ∈ Cauchy ) ∧ 𝑓 : ℕ ⟶ ( ⊥ ‘ 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) → ( ( ⇝𝑣 ‘ 𝑓 ) ·ih 𝑥 ) = 0 )
17 16 ralrimiva ⊢ ( ( ( 𝐴 ⊆ ℋ ∧ 𝑓 ∈ Cauchy ) ∧ 𝑓 : ℕ ⟶ ( ⊥ ‘ 𝐴 ) ) → ∀ 𝑥 ∈ 𝐴 ( ( ⇝𝑣 ‘ 𝑓 ) ·ih 𝑥 ) = 0 )
18 ocel ⊢ ( 𝐴 ⊆ ℋ → ( ( ⇝𝑣 ‘ 𝑓 ) ∈ ( ⊥ ‘ 𝐴 ) ↔ ( ( ⇝𝑣 ‘ 𝑓 ) ∈ ℋ ∧ ∀ 𝑥 ∈ 𝐴 ( ( ⇝𝑣 ‘ 𝑓 ) ·ih 𝑥 ) = 0 ) ) )
19 18 ad2antrr ⊢ ( ( ( 𝐴 ⊆ ℋ ∧ 𝑓 ∈ Cauchy ) ∧ 𝑓 : ℕ ⟶ ( ⊥ ‘ 𝐴 ) ) → ( ( ⇝𝑣 ‘ 𝑓 ) ∈ ( ⊥ ‘ 𝐴 ) ↔ ( ( ⇝𝑣 ‘ 𝑓 ) ∈ ℋ ∧ ∀ 𝑥 ∈ 𝐴 ( ( ⇝𝑣 ‘ 𝑓 ) ·ih 𝑥 ) = 0 ) ) )
20 11 17 19 mpbir2and ⊢ ( ( ( 𝐴 ⊆ ℋ ∧ 𝑓 ∈ Cauchy ) ∧ 𝑓 : ℕ ⟶ ( ⊥ ‘ 𝐴 ) ) → ( ⇝𝑣 ‘ 𝑓 ) ∈ ( ⊥ ‘ 𝐴 ) )
21 ffun ⊢ ( ⇝𝑣 : dom ⇝𝑣 ⟶ ℋ → Fun ⇝𝑣 )
22 funfvbrb ⊢ ( Fun ⇝𝑣 → ( 𝑓 ∈ dom ⇝𝑣 ↔ 𝑓 ⇝𝑣 ( ⇝𝑣 ‘ 𝑓 ) ) )
23 9 21 22 mp2b ⊢ ( 𝑓 ∈ dom ⇝𝑣 ↔ 𝑓 ⇝𝑣 ( ⇝𝑣 ‘ 𝑓 ) )
24 8 23 sylib ⊢ ( ( ( 𝐴 ⊆ ℋ ∧ 𝑓 ∈ Cauchy ) ∧ 𝑓 : ℕ ⟶ ( ⊥ ‘ 𝐴 ) ) → 𝑓 ⇝𝑣 ( ⇝𝑣 ‘ 𝑓 ) )
25 breq2 ⊢ ( 𝑥 = ( ⇝𝑣 ‘ 𝑓 ) → ( 𝑓 ⇝𝑣 𝑥 ↔ 𝑓 ⇝𝑣 ( ⇝𝑣 ‘ 𝑓 ) ) )
26 25 rspcev ⊢ ( ( ( ⇝𝑣 ‘ 𝑓 ) ∈ ( ⊥ ‘ 𝐴 ) ∧ 𝑓 ⇝𝑣 ( ⇝𝑣 ‘ 𝑓 ) ) → ∃ 𝑥 ∈ ( ⊥ ‘ 𝐴 ) 𝑓 ⇝𝑣 𝑥 )
27 20 24 26 syl2anc ⊢ ( ( ( 𝐴 ⊆ ℋ ∧ 𝑓 ∈ Cauchy ) ∧ 𝑓 : ℕ ⟶ ( ⊥ ‘ 𝐴 ) ) → ∃ 𝑥 ∈ ( ⊥ ‘ 𝐴 ) 𝑓 ⇝𝑣 𝑥 )
28 27 ex ⊢ ( ( 𝐴 ⊆ ℋ ∧ 𝑓 ∈ Cauchy ) → ( 𝑓 : ℕ ⟶ ( ⊥ ‘ 𝐴 ) → ∃ 𝑥 ∈ ( ⊥ ‘ 𝐴 ) 𝑓 ⇝𝑣 𝑥 ) )
29 28 ralrimiva ⊢ ( 𝐴 ⊆ ℋ → ∀ 𝑓 ∈ Cauchy ( 𝑓 : ℕ ⟶ ( ⊥ ‘ 𝐴 ) → ∃ 𝑥 ∈ ( ⊥ ‘ 𝐴 ) 𝑓 ⇝𝑣 𝑥 ) )
30 isch3 ⊢ ( ( ⊥ ‘ 𝐴 ) ∈ Cℋ ↔ ( ( ⊥ ‘ 𝐴 ) ∈ Sℋ ∧ ∀ 𝑓 ∈ Cauchy ( 𝑓 : ℕ ⟶ ( ⊥ ‘ 𝐴 ) → ∃ 𝑥 ∈ ( ⊥ ‘ 𝐴 ) 𝑓 ⇝𝑣 𝑥 ) ) )
31 1 29 30 sylanbrc ⊢ ( 𝐴 ⊆ ℋ → ( ⊥ ‘ 𝐴 ) ∈ Cℋ )