cvmcov

Description: Property of a covering map. In order to make the covering property more manageable, we define here the set S ( k ) of all even coverings of an open set k in the range. Then the covering property states that every point has a neighborhood which has an even covering. (Contributed by Mario Carneiro, 13-Feb-2015)

	Ref	Expression
Hypotheses	cvmcov.1	$⊢ S = (k \in J ⟼ \{s \in (𝒫 C ∖ \{\emptyset\}) \| (⋃ s = F^{-1} [k] \land \forall u \in s (\forall v \in (s ∖ \{u\}) u \cap v = \emptyset \land {F ↾}_{u} \in ((C ↾_{𝑡} u) Homeo (J ↾_{𝑡} k))))\})$
	cvmcov.2	$⊢ X = ⋃ J$
Assertion	cvmcov	$⊢ (F \in (C CovMap J) \land P \in X) \to \exists x \in J (P \in x \land S (x) \neq \emptyset)$

Proof

Step	Hyp	Ref	Expression
1		cvmcov.1	$⊢ S = (k \in J ⟼ \{s \in (𝒫 C ∖ \{\emptyset\}) \| (⋃ s = F^{-1} [k] \land \forall u \in s (\forall v \in (s ∖ \{u\}) u \cap v = \emptyset \land {F ↾}_{u} \in ((C ↾_{𝑡} u) Homeo (J ↾_{𝑡} k))))\})$
2		cvmcov.2	$⊢ X = ⋃ J$
3	1 2	iscvm	$⊢ F \in (C CovMap J) \leftrightarrow ((C \in Top \land J \in Top \land F \in (C Cn J)) \land \forall x \in X \exists k \in J (x \in k \land S (k) \neq \emptyset))$
4	3	simprbi	$⊢ F \in (C CovMap J) \to \forall x \in X \exists k \in J (x \in k \land S (k) \neq \emptyset)$
5		eleq1	$⊢ x = P \to (x \in k \leftrightarrow P \in k)$
6	5	anbi1d	$⊢ x = P \to ((x \in k \land S (k) \neq \emptyset) \leftrightarrow (P \in k \land S (k) \neq \emptyset))$
7	6	rexbidv	$⊢ x = P \to (\exists k \in J (x \in k \land S (k) \neq \emptyset) \leftrightarrow \exists k \in J (P \in k \land S (k) \neq \emptyset))$
8	7	rspcv	$⊢ P \in X \to (\forall x \in X \exists k \in J (x \in k \land S (k) \neq \emptyset) \to \exists k \in J (P \in k \land S (k) \neq \emptyset))$
9	4 8	mpan9	$⊢ (F \in (C CovMap J) \land P \in X) \to \exists k \in J (P \in k \land S (k) \neq \emptyset)$
10		nfv	$⊢ Ⅎ k P \in x$
11		nfmpt1	$⊢ \underline{Ⅎ} k (k \in J ⟼ \{s \in (𝒫 C ∖ \{\emptyset\}) \| (⋃ s = F^{-1} [k] \land \forall u \in s (\forall v \in (s ∖ \{u\}) u \cap v = \emptyset \land {F ↾}_{u} \in ((C ↾_{𝑡} u) Homeo (J ↾_{𝑡} k))))\})$
12	1 11	nfcxfr	$⊢ \underline{Ⅎ} k S$
13		nfcv	$⊢ \underline{Ⅎ} k x$
14	12 13	nffv	$⊢ \underline{Ⅎ} k S (x)$
15		nfcv	$⊢ \underline{Ⅎ} k \emptyset$
16	14 15	nfne	$⊢ Ⅎ k S (x) \neq \emptyset$
17	10 16	nfan	$⊢ Ⅎ k (P \in x \land S (x) \neq \emptyset)$
18		nfv	$⊢ Ⅎ x (P \in k \land S (k) \neq \emptyset)$
19		eleq2w	$⊢ x = k \to (P \in x \leftrightarrow P \in k)$
20		fveq2	$⊢ x = k \to S (x) = S (k)$
21	20	neeq1d	$⊢ x = k \to (S (x) \neq \emptyset \leftrightarrow S (k) \neq \emptyset)$
22	19 21	anbi12d	$⊢ x = k \to ((P \in x \land S (x) \neq \emptyset) \leftrightarrow (P \in k \land S (k) \neq \emptyset))$
23	17 18 22	cbvrexw	$⊢ \exists x \in J (P \in x \land S (x) \neq \emptyset) \leftrightarrow \exists k \in J (P \in k \land S (k) \neq \emptyset)$
24	9 23	sylibr	$⊢ (F \in (C CovMap J) \land P \in X) \to \exists x \in J (P \in x \land S (x) \neq \emptyset)$

Metamath Proof Explorer

Theorem cvmcov

Proof