cvmcov2

Description: The covering map property can be restricted to an open subset. (Contributed by Mario Carneiro, 7-Jul-2015)

		Ref	Expression
	Hypothesis	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))))\})$
	Assertion	cvmcov2	$⊢ (F \in (C CovMap J) \land U \in J \land P \in U) \to \exists x \in 𝒫 U (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		simp1	$⊢ (F \in (C CovMap J) \land U \in J \land P \in U) \to F \in (C CovMap J)$
3		simp3	$⊢ (F \in (C CovMap J) \land U \in J \land P \in U) \to P \in U$
4		simp2	$⊢ (F \in (C CovMap J) \land U \in J \land P \in U) \to U \in J$
5		elunii	$⊢ (P \in U \land U \in J) \to P \in ⋃ J$
6	3 4 5	syl2anc	$⊢ (F \in (C CovMap J) \land U \in J \land P \in U) \to P \in ⋃ J$
7		eqid	$⊢ ⋃ J = ⋃ J$
8	1 7	cvmcov	$⊢ (F \in (C CovMap J) \land P \in ⋃ J) \to \exists y \in J (P \in y \land S (y) \neq \emptyset)$
9	2 6 8	syl2anc	$⊢ (F \in (C CovMap J) \land U \in J \land P \in U) \to \exists y \in J (P \in y \land S (y) \neq \emptyset)$
10		inss2	$⊢ y \cap U \subseteq U$
11		vex	$⊢ y \in V$
12	11	inex1	$⊢ y \cap U \in V$
13	12	elpw	$⊢ y \cap U \in 𝒫 U \leftrightarrow y \cap U \subseteq U$
14	10 13	mpbir	$⊢ y \cap U \in 𝒫 U$
15	14	a1i	$⊢ ((F \in (C CovMap J) \land U \in J \land P \in U) \land (y \in J \land (P \in y \land S (y) \neq \emptyset))) \to y \cap U \in 𝒫 U$
16		simprrl	$⊢ ((F \in (C CovMap J) \land U \in J \land P \in U) \land (y \in J \land (P \in y \land S (y) \neq \emptyset))) \to P \in y$
17	3	adantr	$⊢ ((F \in (C CovMap J) \land U \in J \land P \in U) \land (y \in J \land (P \in y \land S (y) \neq \emptyset))) \to P \in U$
18	16 17	elind	$⊢ ((F \in (C CovMap J) \land U \in J \land P \in U) \land (y \in J \land (P \in y \land S (y) \neq \emptyset))) \to P \in (y \cap U)$
19		simprrr	$⊢ ((F \in (C CovMap J) \land U \in J \land P \in U) \land (y \in J \land (P \in y \land S (y) \neq \emptyset))) \to S (y) \neq \emptyset$
20	2	adantr	$⊢ ((F \in (C CovMap J) \land U \in J \land P \in U) \land (y \in J \land (P \in y \land S (y) \neq \emptyset))) \to F \in (C CovMap J)$
21		cvmtop2	$⊢ F \in (C CovMap J) \to J \in Top$
22	20 21	syl	$⊢ ((F \in (C CovMap J) \land U \in J \land P \in U) \land (y \in J \land (P \in y \land S (y) \neq \emptyset))) \to J \in Top$
23		simprl	$⊢ ((F \in (C CovMap J) \land U \in J \land P \in U) \land (y \in J \land (P \in y \land S (y) \neq \emptyset))) \to y \in J$
24	4	adantr	$⊢ ((F \in (C CovMap J) \land U \in J \land P \in U) \land (y \in J \land (P \in y \land S (y) \neq \emptyset))) \to U \in J$
25		inopn	$⊢ (J \in Top \land y \in J \land U \in J) \to y \cap U \in J$
26	22 23 24 25	syl3anc	$⊢ ((F \in (C CovMap J) \land U \in J \land P \in U) \land (y \in J \land (P \in y \land S (y) \neq \emptyset))) \to y \cap U \in J$
27		inss1	$⊢ y \cap U \subseteq y$
28	27	a1i	$⊢ ((F \in (C CovMap J) \land U \in J \land P \in U) \land (y \in J \land (P \in y \land S (y) \neq \emptyset))) \to y \cap U \subseteq y$
29	1	cvmsss2	$⊢ (F \in (C CovMap J) \land y \cap U \in J \land y \cap U \subseteq y) \to (S (y) \neq \emptyset \to S (y \cap U) \neq \emptyset)$
30	20 26 28 29	syl3anc	$⊢ ((F \in (C CovMap J) \land U \in J \land P \in U) \land (y \in J \land (P \in y \land S (y) \neq \emptyset))) \to (S (y) \neq \emptyset \to S (y \cap U) \neq \emptyset)$
31	19 30	mpd	$⊢ ((F \in (C CovMap J) \land U \in J \land P \in U) \land (y \in J \land (P \in y \land S (y) \neq \emptyset))) \to S (y \cap U) \neq \emptyset$
32		eleq2	$⊢ x = y \cap U \to (P \in x \leftrightarrow P \in (y \cap U))$
33		fveq2	$⊢ x = y \cap U \to S (x) = S (y \cap U)$
34	33	neeq1d	$⊢ x = y \cap U \to (S (x) \neq \emptyset \leftrightarrow S (y \cap U) \neq \emptyset)$
35	32 34	anbi12d	$⊢ x = y \cap U \to ((P \in x \land S (x) \neq \emptyset) \leftrightarrow (P \in (y \cap U) \land S (y \cap U) \neq \emptyset))$
36	35	rspcev	$⊢ (y \cap U \in 𝒫 U \land (P \in (y \cap U) \land S (y \cap U) \neq \emptyset)) \to \exists x \in 𝒫 U (P \in x \land S (x) \neq \emptyset)$
37	15 18 31 36	syl12anc	$⊢ ((F \in (C CovMap J) \land U \in J \land P \in U) \land (y \in J \land (P \in y \land S (y) \neq \emptyset))) \to \exists x \in 𝒫 U (P \in x \land S (x) \neq \emptyset)$
38	9 37	rexlimddv	$⊢ (F \in (C CovMap J) \land U \in J \land P \in U) \to \exists x \in 𝒫 U (P \in x \land S (x) \neq \emptyset)$

Metamath Proof Explorer

Theorem cvmcov2

Proof