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	$⊢ A \subseteq ℋ \to ⊥ (A) \in C_{ℋ}$

Proof

Step	Hyp	Ref	Expression
1		ocsh	$⊢ A \subseteq ℋ \to ⊥ (A) \in S_{ℋ}$
2		ax-hcompl	$⊢ f \in Cauchy \to \exists x \in ℋ f \underset{v}{⇝} x$
3		vex	$⊢ f \in V$
4		vex	$⊢ x \in V$
5	3 4	breldm	$⊢ f \underset{v}{⇝} x \to f \in dom \underset{v}{⇝}$
6	5	rexlimivw	$⊢ \exists x \in ℋ f \underset{v}{⇝} x \to f \in dom \underset{v}{⇝}$
7	2 6	syl	$⊢ f \in Cauchy \to f \in dom \underset{v}{⇝}$
8	7	ad2antlr	$⊢ ((A \subseteq ℋ \land f \in Cauchy) \land f : ℕ ⟶ ⊥ (A)) \to f \in dom \underset{v}{⇝}$
9		hlimf	$⊢ \underset{v}{⇝} : dom \underset{v}{⇝} ⟶ ℋ$
10	9	ffvelcdmi	$⊢ f \in dom \underset{v}{⇝} \to \underset{v}{⇝} (f) \in ℋ$
11	8 10	syl	$⊢ ((A \subseteq ℋ \land f \in Cauchy) \land f : ℕ ⟶ ⊥ (A)) \to \underset{v}{⇝} (f) \in ℋ$
12		simplll	$⊢ (((A \subseteq ℋ \land f \in Cauchy) \land f : ℕ ⟶ ⊥ (A)) \land x \in A) \to A \subseteq ℋ$
13		simpllr	$⊢ (((A \subseteq ℋ \land f \in Cauchy) \land f : ℕ ⟶ ⊥ (A)) \land x \in A) \to f \in Cauchy$
14		simplr	$⊢ (((A \subseteq ℋ \land f \in Cauchy) \land f : ℕ ⟶ ⊥ (A)) \land x \in A) \to f : ℕ ⟶ ⊥ (A)$
15		simpr	$⊢ (((A \subseteq ℋ \land f \in Cauchy) \land f : ℕ ⟶ ⊥ (A)) \land x \in A) \to x \in A$
16	12 13 14 15	occllem	$⊢ (((A \subseteq ℋ \land f \in Cauchy) \land f : ℕ ⟶ ⊥ (A)) \land x \in A) \to \underset{v}{⇝} (f) \cdot_{ih} x = 0$
17	16	ralrimiva	$⊢ ((A \subseteq ℋ \land f \in Cauchy) \land f : ℕ ⟶ ⊥ (A)) \to \forall x \in A \underset{v}{⇝} (f) \cdot_{ih} x = 0$
18		ocel	$⊢ A \subseteq ℋ \to (\underset{v}{⇝} (f) \in ⊥ (A) \leftrightarrow (\underset{v}{⇝} (f) \in ℋ \land \forall x \in A \underset{v}{⇝} (f) \cdot_{ih} x = 0))$
19	18	ad2antrr	$⊢ ((A \subseteq ℋ \land f \in Cauchy) \land f : ℕ ⟶ ⊥ (A)) \to (\underset{v}{⇝} (f) \in ⊥ (A) \leftrightarrow (\underset{v}{⇝} (f) \in ℋ \land \forall x \in A \underset{v}{⇝} (f) \cdot_{ih} x = 0))$
20	11 17 19	mpbir2and	$⊢ ((A \subseteq ℋ \land f \in Cauchy) \land f : ℕ ⟶ ⊥ (A)) \to \underset{v}{⇝} (f) \in ⊥ (A)$
21		ffun	$⊢ \underset{v}{⇝} : dom \underset{v}{⇝} ⟶ ℋ \to Fun \underset{v}{⇝}$
22		funfvbrb	$⊢ Fun \underset{v}{⇝} \to (f \in dom \underset{v}{⇝} \leftrightarrow f \underset{v}{⇝} \underset{v}{⇝} (f))$
23	9 21 22	mp2b	$⊢ f \in dom \underset{v}{⇝} \leftrightarrow f \underset{v}{⇝} \underset{v}{⇝} (f)$
24	8 23	sylib	$⊢ ((A \subseteq ℋ \land f \in Cauchy) \land f : ℕ ⟶ ⊥ (A)) \to f \underset{v}{⇝} \underset{v}{⇝} (f)$
25		breq2	$⊢ x = \underset{v}{⇝} (f) \to (f \underset{v}{⇝} x \leftrightarrow f \underset{v}{⇝} \underset{v}{⇝} (f))$
26	25	rspcev	$⊢ (\underset{v}{⇝} (f) \in ⊥ (A) \land f \underset{v}{⇝} \underset{v}{⇝} (f)) \to \exists x \in ⊥ (A) f \underset{v}{⇝} x$
27	20 24 26	syl2anc	$⊢ ((A \subseteq ℋ \land f \in Cauchy) \land f : ℕ ⟶ ⊥ (A)) \to \exists x \in ⊥ (A) f \underset{v}{⇝} x$
28	27	ex	$⊢ (A \subseteq ℋ \land f \in Cauchy) \to (f : ℕ ⟶ ⊥ (A) \to \exists x \in ⊥ (A) f \underset{v}{⇝} x)$
29	28	ralrimiva	$⊢ A \subseteq ℋ \to \forall f \in Cauchy (f : ℕ ⟶ ⊥ (A) \to \exists x \in ⊥ (A) f \underset{v}{⇝} x)$
30		isch3	$⊢ ⊥ (A) \in C_{ℋ} \leftrightarrow (⊥ (A) \in S_{ℋ} \land \forall f \in Cauchy (f : ℕ ⟶ ⊥ (A) \to \exists x \in ⊥ (A) f \underset{v}{⇝} x))$
31	1 29 30	sylanbrc	$⊢ A \subseteq ℋ \to ⊥ (A) \in C_{ℋ}$

Metamath Proof Explorer

Theorem occl

Proof