cvmscld

Description: The sets of an even covering are clopen in the subspace topology on T . (Contributed by Mario Carneiro, 14-Feb-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	cvmscld	$⊢ (F \in (C CovMap J) \land T \in S (U) \land A \in T) \to A \in Clsd (C ↾_{𝑡} F^{-1} [U])$

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		cvmtop1	$⊢ F \in (C CovMap J) \to C \in Top$
3	2	3ad2ant1	$⊢ (F \in (C CovMap J) \land T \in S (U) \land A \in T) \to C \in Top$
4	1	cvmsuni	$⊢ T \in S (U) \to ⋃ T = F^{-1} [U]$
5	4	3ad2ant2	$⊢ (F \in (C CovMap J) \land T \in S (U) \land A \in T) \to ⋃ T = F^{-1} [U]$
6	1	cvmsss	$⊢ T \in S (U) \to T \subseteq C$
7	6	3ad2ant2	$⊢ (F \in (C CovMap J) \land T \in S (U) \land A \in T) \to T \subseteq C$
8	7	unissd	$⊢ (F \in (C CovMap J) \land T \in S (U) \land A \in T) \to ⋃ T \subseteq ⋃ C$
9	5 8	eqsstrrd	$⊢ (F \in (C CovMap J) \land T \in S (U) \land A \in T) \to F^{-1} [U] \subseteq ⋃ C$
10		eqid	$⊢ ⋃ C = ⋃ C$
11	10	restuni	$⊢ (C \in Top \land F^{-1} [U] \subseteq ⋃ C) \to F^{-1} [U] = ⋃ (C ↾_{𝑡} F^{-1} [U])$
12	3 9 11	syl2anc	$⊢ (F \in (C CovMap J) \land T \in S (U) \land A \in T) \to F^{-1} [U] = ⋃ (C ↾_{𝑡} F^{-1} [U])$
13	12	difeq1d	$⊢ (F \in (C CovMap J) \land T \in S (U) \land A \in T) \to F^{-1} [U] ∖ ⋃ (T ∖ \{A\}) = ⋃ (C ↾_{𝑡} F^{-1} [U]) ∖ ⋃ (T ∖ \{A\})$
14		unisng	$⊢ A \in T \to ⋃ \{A\} = A$
15	14	3ad2ant3	$⊢ (F \in (C CovMap J) \land T \in S (U) \land A \in T) \to ⋃ \{A\} = A$
16	15	uneq2d	$⊢ (F \in (C CovMap J) \land T \in S (U) \land A \in T) \to ⋃ (T ∖ \{A\}) \cup ⋃ \{A\} = ⋃ (T ∖ \{A\}) \cup A$
17		uniun	$⊢ ⋃ ((T ∖ \{A\}) \cup \{A\}) = ⋃ (T ∖ \{A\}) \cup ⋃ \{A\}$
18		undif1	$⊢ (T ∖ \{A\}) \cup \{A\} = T \cup \{A\}$
19		simp3	$⊢ (F \in (C CovMap J) \land T \in S (U) \land A \in T) \to A \in T$
20	19	snssd	$⊢ (F \in (C CovMap J) \land T \in S (U) \land A \in T) \to \{A\} \subseteq T$
21		ssequn2	$⊢ \{A\} \subseteq T \leftrightarrow T \cup \{A\} = T$
22	20 21	sylib	$⊢ (F \in (C CovMap J) \land T \in S (U) \land A \in T) \to T \cup \{A\} = T$
23	18 22	syl5eq	$⊢ (F \in (C CovMap J) \land T \in S (U) \land A \in T) \to (T ∖ \{A\}) \cup \{A\} = T$
24	23	unieqd	$⊢ (F \in (C CovMap J) \land T \in S (U) \land A \in T) \to ⋃ ((T ∖ \{A\}) \cup \{A\}) = ⋃ T$
25	24 5	eqtrd	$⊢ (F \in (C CovMap J) \land T \in S (U) \land A \in T) \to ⋃ ((T ∖ \{A\}) \cup \{A\}) = F^{-1} [U]$
26	17 25	eqtr3id	$⊢ (F \in (C CovMap J) \land T \in S (U) \land A \in T) \to ⋃ (T ∖ \{A\}) \cup ⋃ \{A\} = F^{-1} [U]$
27	16 26	eqtr3d	$⊢ (F \in (C CovMap J) \land T \in S (U) \land A \in T) \to ⋃ (T ∖ \{A\}) \cup A = F^{-1} [U]$
28		difss	$⊢ T ∖ \{A\} \subseteq T$
29	28	unissi	$⊢ ⋃ (T ∖ \{A\}) \subseteq ⋃ T$
30	29 5	sseqtrid	$⊢ (F \in (C CovMap J) \land T \in S (U) \land A \in T) \to ⋃ (T ∖ \{A\}) \subseteq F^{-1} [U]$
31		uniiun	$⊢ ⋃ (T ∖ \{A\}) = ⋃_{x \in T ∖ \{A\}} x$
32	31	ineq2i	$⊢ A \cap ⋃ (T ∖ \{A\}) = A \cap ⋃_{x \in T ∖ \{A\}} x$
33		incom	$⊢ ⋃ (T ∖ \{A\}) \cap A = A \cap ⋃ (T ∖ \{A\})$
34		iunin2	$⊢ ⋃_{x \in T ∖ \{A\}} (A \cap x) = A \cap ⋃_{x \in T ∖ \{A\}} x$
35	32 33 34	3eqtr4i	$⊢ ⋃ (T ∖ \{A\}) \cap A = ⋃_{x \in T ∖ \{A\}} (A \cap x)$
36		eldifsn	$⊢ x \in (T ∖ \{A\}) \leftrightarrow (x \in T \land x \neq A)$
37		nesym	$⊢ x \neq A \leftrightarrow \neg A = x$
38	1	cvmsdisj	$⊢ (T \in S (U) \land A \in T \land x \in T) \to (A = x \lor A \cap x = \emptyset)$
39	38	3expa	$⊢ ((T \in S (U) \land A \in T) \land x \in T) \to (A = x \lor A \cap x = \emptyset)$
40	39	ord	$⊢ ((T \in S (U) \land A \in T) \land x \in T) \to (\neg A = x \to A \cap x = \emptyset)$
41	37 40	syl5bi	$⊢ ((T \in S (U) \land A \in T) \land x \in T) \to (x \neq A \to A \cap x = \emptyset)$
42	41	impr	$⊢ ((T \in S (U) \land A \in T) \land (x \in T \land x \neq A)) \to A \cap x = \emptyset$
43	36 42	sylan2b	$⊢ ((T \in S (U) \land A \in T) \land x \in (T ∖ \{A\})) \to A \cap x = \emptyset$
44	43	iuneq2dv	$⊢ (T \in S (U) \land A \in T) \to ⋃_{x \in T ∖ \{A\}} (A \cap x) = ⋃_{x \in T ∖ \{A\}} \emptyset$
45	44	3adant1	$⊢ (F \in (C CovMap J) \land T \in S (U) \land A \in T) \to ⋃_{x \in T ∖ \{A\}} (A \cap x) = ⋃_{x \in T ∖ \{A\}} \emptyset$
46		iun0	$⊢ ⋃_{x \in T ∖ \{A\}} \emptyset = \emptyset$
47	45 46	eqtrdi	$⊢ (F \in (C CovMap J) \land T \in S (U) \land A \in T) \to ⋃_{x \in T ∖ \{A\}} (A \cap x) = \emptyset$
48	35 47	syl5eq	$⊢ (F \in (C CovMap J) \land T \in S (U) \land A \in T) \to ⋃ (T ∖ \{A\}) \cap A = \emptyset$
49		uneqdifeq	$⊢ (⋃ (T ∖ \{A\}) \subseteq F^{-1} [U] \land ⋃ (T ∖ \{A\}) \cap A = \emptyset) \to (⋃ (T ∖ \{A\}) \cup A = F^{-1} [U] \leftrightarrow F^{-1} [U] ∖ ⋃ (T ∖ \{A\}) = A)$
50	30 48 49	syl2anc	$⊢ (F \in (C CovMap J) \land T \in S (U) \land A \in T) \to (⋃ (T ∖ \{A\}) \cup A = F^{-1} [U] \leftrightarrow F^{-1} [U] ∖ ⋃ (T ∖ \{A\}) = A)$
51	27 50	mpbid	$⊢ (F \in (C CovMap J) \land T \in S (U) \land A \in T) \to F^{-1} [U] ∖ ⋃ (T ∖ \{A\}) = A$
52	13 51	eqtr3d	$⊢ (F \in (C CovMap J) \land T \in S (U) \land A \in T) \to ⋃ (C ↾_{𝑡} F^{-1} [U]) ∖ ⋃ (T ∖ \{A\}) = A$
53		uniexg	$⊢ T \in S (U) \to ⋃ T \in V$
54	53	3ad2ant2	$⊢ (F \in (C CovMap J) \land T \in S (U) \land A \in T) \to ⋃ T \in V$
55	5 54	eqeltrrd	$⊢ (F \in (C CovMap J) \land T \in S (U) \land A \in T) \to F^{-1} [U] \in V$
56		resttop	$⊢ (C \in Top \land F^{-1} [U] \in V) \to C ↾_{𝑡} F^{-1} [U] \in Top$
57	3 55 56	syl2anc	$⊢ (F \in (C CovMap J) \land T \in S (U) \land A \in T) \to C ↾_{𝑡} F^{-1} [U] \in Top$
58		elssuni	$⊢ x \in T \to x \subseteq ⋃ T$
59	58	adantl	$⊢ ((F \in (C CovMap J) \land T \in S (U) \land A \in T) \land x \in T) \to x \subseteq ⋃ T$
60	5	adantr	$⊢ ((F \in (C CovMap J) \land T \in S (U) \land A \in T) \land x \in T) \to ⋃ T = F^{-1} [U]$
61	59 60	sseqtrd	$⊢ ((F \in (C CovMap J) \land T \in S (U) \land A \in T) \land x \in T) \to x \subseteq F^{-1} [U]$
62		df-ss	$⊢ x \subseteq F^{-1} [U] \leftrightarrow x \cap F^{-1} [U] = x$
63	61 62	sylib	$⊢ ((F \in (C CovMap J) \land T \in S (U) \land A \in T) \land x \in T) \to x \cap F^{-1} [U] = x$
64	3	adantr	$⊢ ((F \in (C CovMap J) \land T \in S (U) \land A \in T) \land x \in T) \to C \in Top$
65	55	adantr	$⊢ ((F \in (C CovMap J) \land T \in S (U) \land A \in T) \land x \in T) \to F^{-1} [U] \in V$
66	7	sselda	$⊢ ((F \in (C CovMap J) \land T \in S (U) \land A \in T) \land x \in T) \to x \in C$
67		elrestr	$⊢ (C \in Top \land F^{-1} [U] \in V \land x \in C) \to x \cap F^{-1} [U] \in (C ↾_{𝑡} F^{-1} [U])$
68	64 65 66 67	syl3anc	$⊢ ((F \in (C CovMap J) \land T \in S (U) \land A \in T) \land x \in T) \to x \cap F^{-1} [U] \in (C ↾_{𝑡} F^{-1} [U])$
69	63 68	eqeltrrd	$⊢ ((F \in (C CovMap J) \land T \in S (U) \land A \in T) \land x \in T) \to x \in (C ↾_{𝑡} F^{-1} [U])$
70	69	ex	$⊢ (F \in (C CovMap J) \land T \in S (U) \land A \in T) \to (x \in T \to x \in (C ↾_{𝑡} F^{-1} [U]))$
71	70	ssrdv	$⊢ (F \in (C CovMap J) \land T \in S (U) \land A \in T) \to T \subseteq C ↾_{𝑡} F^{-1} [U]$
72	71	ssdifssd	$⊢ (F \in (C CovMap J) \land T \in S (U) \land A \in T) \to T ∖ \{A\} \subseteq C ↾_{𝑡} F^{-1} [U]$
73		uniopn	$⊢ (C ↾_{𝑡} F^{-1} [U] \in Top \land T ∖ \{A\} \subseteq C ↾_{𝑡} F^{-1} [U]) \to ⋃ (T ∖ \{A\}) \in (C ↾_{𝑡} F^{-1} [U])$
74	57 72 73	syl2anc	$⊢ (F \in (C CovMap J) \land T \in S (U) \land A \in T) \to ⋃ (T ∖ \{A\}) \in (C ↾_{𝑡} F^{-1} [U])$
75		eqid	$⊢ ⋃ (C ↾_{𝑡} F^{-1} [U]) = ⋃ (C ↾_{𝑡} F^{-1} [U])$
76	75	opncld	$⊢ (C ↾_{𝑡} F^{-1} [U] \in Top \land ⋃ (T ∖ \{A\}) \in (C ↾_{𝑡} F^{-1} [U])) \to ⋃ (C ↾_{𝑡} F^{-1} [U]) ∖ ⋃ (T ∖ \{A\}) \in Clsd (C ↾_{𝑡} F^{-1} [U])$
77	57 74 76	syl2anc	$⊢ (F \in (C CovMap J) \land T \in S (U) \land A \in T) \to ⋃ (C ↾_{𝑡} F^{-1} [U]) ∖ ⋃ (T ∖ \{A\}) \in Clsd (C ↾_{𝑡} F^{-1} [U])$
78	52 77	eqeltrrd	$⊢ (F \in (C CovMap J) \land T \in S (U) \land A \in T) \to A \in Clsd (C ↾_{𝑡} F^{-1} [U])$

Metamath Proof Explorer

Theorem cvmscld

Proof