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ℋ )