locfincmp

Description: For a compact space, the locally finite covers are precisely the finite covers. Sadly, this property does not properly characterize all compact spaces. (Contributed by Jeff Hankins, 22-Jan-2010) (Proof shortened by Mario Carneiro, 11-Sep-2015)

	Ref	Expression
Hypotheses	locfincmp.1	$⊢ X = ⋃ J$
	locfincmp.2	$⊢ Y = ⋃ C$
Assertion	locfincmp	$⊢ J \in Comp \to (C \in LocFin (J) \leftrightarrow (C \in Fin \land X = Y))$

Proof

Step	Hyp	Ref	Expression
1		locfincmp.1	$⊢ X = ⋃ J$
2		locfincmp.2	$⊢ Y = ⋃ C$
3	1	locfinnei	$⊢ (C \in LocFin (J) \land x \in X) \to \exists o \in J (x \in o \land \{s \in C \| s \cap o \neq \emptyset\} \in Fin)$
4	3	ralrimiva	$⊢ C \in LocFin (J) \to \forall x \in X \exists o \in J (x \in o \land \{s \in C \| s \cap o \neq \emptyset\} \in Fin)$
5	1	cmpcov2	$⊢ (J \in Comp \land \forall x \in X \exists o \in J (x \in o \land \{s \in C \| s \cap o \neq \emptyset\} \in Fin)) \to \exists c \in (𝒫 J \cap Fin) (X = ⋃ c \land \forall o \in c \{s \in C \| s \cap o \neq \emptyset\} \in Fin)$
6	4 5	sylan2	$⊢ (J \in Comp \land C \in LocFin (J)) \to \exists c \in (𝒫 J \cap Fin) (X = ⋃ c \land \forall o \in c \{s \in C \| s \cap o \neq \emptyset\} \in Fin)$
7		elfpw	$⊢ c \in (𝒫 J \cap Fin) \leftrightarrow (c \subseteq J \land c \in Fin)$
8		simplrr	$⊢ (((J \in Comp \land C \in LocFin (J)) \land (c \subseteq J \land c \in Fin)) \land X = ⋃ c) \to c \in Fin$
9		eldifsn	$⊢ x \in (C ∖ \{\emptyset\}) \leftrightarrow (x \in C \land x \neq \emptyset)$
10		ineq1	$⊢ s = x \to s \cap o = x \cap o$
11	10	neeq1d	$⊢ s = x \to (s \cap o \neq \emptyset \leftrightarrow x \cap o \neq \emptyset)$
12		simplrl	$⊢ (((((J \in Comp \land C \in LocFin (J)) \land (c \subseteq J \land c \in Fin)) \land X = ⋃ c) \land (x \in C \land y \in x)) \land (o \in c \land y \in o)) \to x \in C$
13		simplrr	$⊢ (((((J \in Comp \land C \in LocFin (J)) \land (c \subseteq J \land c \in Fin)) \land X = ⋃ c) \land (x \in C \land y \in x)) \land (o \in c \land y \in o)) \to y \in x$
14		simprr	$⊢ (((((J \in Comp \land C \in LocFin (J)) \land (c \subseteq J \land c \in Fin)) \land X = ⋃ c) \land (x \in C \land y \in x)) \land (o \in c \land y \in o)) \to y \in o$
15		inelcm	$⊢ (y \in x \land y \in o) \to x \cap o \neq \emptyset$
16	13 14 15	syl2anc	$⊢ (((((J \in Comp \land C \in LocFin (J)) \land (c \subseteq J \land c \in Fin)) \land X = ⋃ c) \land (x \in C \land y \in x)) \land (o \in c \land y \in o)) \to x \cap o \neq \emptyset$
17	11 12 16	elrabd	$⊢ (((((J \in Comp \land C \in LocFin (J)) \land (c \subseteq J \land c \in Fin)) \land X = ⋃ c) \land (x \in C \land y \in x)) \land (o \in c \land y \in o)) \to x \in \{s \in C \| s \cap o \neq \emptyset\}$
18		elunii	$⊢ (y \in x \land x \in C) \to y \in ⋃ C$
19	18 2	eleqtrrdi	$⊢ (y \in x \land x \in C) \to y \in Y$
20	19	ancoms	$⊢ (x \in C \land y \in x) \to y \in Y$
21	20	adantl	$⊢ ((((J \in Comp \land C \in LocFin (J)) \land (c \subseteq J \land c \in Fin)) \land X = ⋃ c) \land (x \in C \land y \in x)) \to y \in Y$
22	1 2	locfinbas	$⊢ C \in LocFin (J) \to X = Y$
23	22	adantl	$⊢ (J \in Comp \land C \in LocFin (J)) \to X = Y$
24	23	ad3antrrr	$⊢ ((((J \in Comp \land C \in LocFin (J)) \land (c \subseteq J \land c \in Fin)) \land X = ⋃ c) \land (x \in C \land y \in x)) \to X = Y$
25	21 24	eleqtrrd	$⊢ ((((J \in Comp \land C \in LocFin (J)) \land (c \subseteq J \land c \in Fin)) \land X = ⋃ c) \land (x \in C \land y \in x)) \to y \in X$
26		simplr	$⊢ ((((J \in Comp \land C \in LocFin (J)) \land (c \subseteq J \land c \in Fin)) \land X = ⋃ c) \land (x \in C \land y \in x)) \to X = ⋃ c$
27	25 26	eleqtrd	$⊢ ((((J \in Comp \land C \in LocFin (J)) \land (c \subseteq J \land c \in Fin)) \land X = ⋃ c) \land (x \in C \land y \in x)) \to y \in ⋃ c$
28		eluni2	$⊢ y \in ⋃ c \leftrightarrow \exists o \in c y \in o$
29	27 28	sylib	$⊢ ((((J \in Comp \land C \in LocFin (J)) \land (c \subseteq J \land c \in Fin)) \land X = ⋃ c) \land (x \in C \land y \in x)) \to \exists o \in c y \in o$
30	17 29	reximddv	$⊢ ((((J \in Comp \land C \in LocFin (J)) \land (c \subseteq J \land c \in Fin)) \land X = ⋃ c) \land (x \in C \land y \in x)) \to \exists o \in c x \in \{s \in C \| s \cap o \neq \emptyset\}$
31	30	expr	$⊢ ((((J \in Comp \land C \in LocFin (J)) \land (c \subseteq J \land c \in Fin)) \land X = ⋃ c) \land x \in C) \to (y \in x \to \exists o \in c x \in \{s \in C \| s \cap o \neq \emptyset\})$
32	31	exlimdv	$⊢ ((((J \in Comp \land C \in LocFin (J)) \land (c \subseteq J \land c \in Fin)) \land X = ⋃ c) \land x \in C) \to (\exists y y \in x \to \exists o \in c x \in \{s \in C \| s \cap o \neq \emptyset\})$
33		n0	$⊢ x \neq \emptyset \leftrightarrow \exists y y \in x$
34		eliun	$⊢ x \in ⋃_{o \in c} \{s \in C \| s \cap o \neq \emptyset\} \leftrightarrow \exists o \in c x \in \{s \in C \| s \cap o \neq \emptyset\}$
35	32 33 34	3imtr4g	$⊢ ((((J \in Comp \land C \in LocFin (J)) \land (c \subseteq J \land c \in Fin)) \land X = ⋃ c) \land x \in C) \to (x \neq \emptyset \to x \in ⋃_{o \in c} \{s \in C \| s \cap o \neq \emptyset\})$
36	35	expimpd	$⊢ (((J \in Comp \land C \in LocFin (J)) \land (c \subseteq J \land c \in Fin)) \land X = ⋃ c) \to ((x \in C \land x \neq \emptyset) \to x \in ⋃_{o \in c} \{s \in C \| s \cap o \neq \emptyset\})$
37	9 36	syl5bi	$⊢ (((J \in Comp \land C \in LocFin (J)) \land (c \subseteq J \land c \in Fin)) \land X = ⋃ c) \to (x \in (C ∖ \{\emptyset\}) \to x \in ⋃_{o \in c} \{s \in C \| s \cap o \neq \emptyset\})$
38	37	ssrdv	$⊢ (((J \in Comp \land C \in LocFin (J)) \land (c \subseteq J \land c \in Fin)) \land X = ⋃ c) \to C ∖ \{\emptyset\} \subseteq ⋃_{o \in c} \{s \in C \| s \cap o \neq \emptyset\}$
39		iunfi	$⊢ (c \in Fin \land \forall o \in c \{s \in C \| s \cap o \neq \emptyset\} \in Fin) \to ⋃_{o \in c} \{s \in C \| s \cap o \neq \emptyset\} \in Fin$
40	39	ex	$⊢ c \in Fin \to (\forall o \in c \{s \in C \| s \cap o \neq \emptyset\} \in Fin \to ⋃_{o \in c} \{s \in C \| s \cap o \neq \emptyset\} \in Fin)$
41		ssfi	$⊢ (⋃_{o \in c} \{s \in C \| s \cap o \neq \emptyset\} \in Fin \land C ∖ \{\emptyset\} \subseteq ⋃_{o \in c} \{s \in C \| s \cap o \neq \emptyset\}) \to C ∖ \{\emptyset\} \in Fin$
42	41	expcom	$⊢ C ∖ \{\emptyset\} \subseteq ⋃_{o \in c} \{s \in C \| s \cap o \neq \emptyset\} \to (⋃_{o \in c} \{s \in C \| s \cap o \neq \emptyset\} \in Fin \to C ∖ \{\emptyset\} \in Fin)$
43	40 42	sylan9	$⊢ (c \in Fin \land C ∖ \{\emptyset\} \subseteq ⋃_{o \in c} \{s \in C \| s \cap o \neq \emptyset\}) \to (\forall o \in c \{s \in C \| s \cap o \neq \emptyset\} \in Fin \to C ∖ \{\emptyset\} \in Fin)$
44	8 38 43	syl2anc	$⊢ (((J \in Comp \land C \in LocFin (J)) \land (c \subseteq J \land c \in Fin)) \land X = ⋃ c) \to (\forall o \in c \{s \in C \| s \cap o \neq \emptyset\} \in Fin \to C ∖ \{\emptyset\} \in Fin)$
45	44	expimpd	$⊢ ((J \in Comp \land C \in LocFin (J)) \land (c \subseteq J \land c \in Fin)) \to ((X = ⋃ c \land \forall o \in c \{s \in C \| s \cap o \neq \emptyset\} \in Fin) \to C ∖ \{\emptyset\} \in Fin)$
46	7 45	sylan2b	$⊢ ((J \in Comp \land C \in LocFin (J)) \land c \in (𝒫 J \cap Fin)) \to ((X = ⋃ c \land \forall o \in c \{s \in C \| s \cap o \neq \emptyset\} \in Fin) \to C ∖ \{\emptyset\} \in Fin)$
47	46	rexlimdva	$⊢ (J \in Comp \land C \in LocFin (J)) \to (\exists c \in (𝒫 J \cap Fin) (X = ⋃ c \land \forall o \in c \{s \in C \| s \cap o \neq \emptyset\} \in Fin) \to C ∖ \{\emptyset\} \in Fin)$
48	6 47	mpd	$⊢ (J \in Comp \land C \in LocFin (J)) \to C ∖ \{\emptyset\} \in Fin$
49		snfi	$⊢ \{\emptyset\} \in Fin$
50		unfi	$⊢ (C ∖ \{\emptyset\} \in Fin \land \{\emptyset\} \in Fin) \to (C ∖ \{\emptyset\}) \cup \{\emptyset\} \in Fin$
51	48 49 50	sylancl	$⊢ (J \in Comp \land C \in LocFin (J)) \to (C ∖ \{\emptyset\}) \cup \{\emptyset\} \in Fin$
52		ssun1	$⊢ C \subseteq C \cup \{\emptyset\}$
53		undif1	$⊢ (C ∖ \{\emptyset\}) \cup \{\emptyset\} = C \cup \{\emptyset\}$
54	52 53	sseqtrri	$⊢ C \subseteq (C ∖ \{\emptyset\}) \cup \{\emptyset\}$
55		ssfi	$⊢ ((C ∖ \{\emptyset\}) \cup \{\emptyset\} \in Fin \land C \subseteq (C ∖ \{\emptyset\}) \cup \{\emptyset\}) \to C \in Fin$
56	51 54 55	sylancl	$⊢ (J \in Comp \land C \in LocFin (J)) \to C \in Fin$
57	56 23	jca	$⊢ (J \in Comp \land C \in LocFin (J)) \to (C \in Fin \land X = Y)$
58	57	ex	$⊢ J \in Comp \to (C \in LocFin (J) \to (C \in Fin \land X = Y))$
59		cmptop	$⊢ J \in Comp \to J \in Top$
60	1 2	finlocfin	$⊢ (J \in Top \land C \in Fin \land X = Y) \to C \in LocFin (J)$
61	60	3expib	$⊢ J \in Top \to ((C \in Fin \land X = Y) \to C \in LocFin (J))$
62	59 61	syl	$⊢ J \in Comp \to ((C \in Fin \land X = Y) \to C \in LocFin (J))$
63	58 62	impbid	$⊢ J \in Comp \to (C \in LocFin (J) \leftrightarrow (C \in Fin \land X = Y))$

Metamath Proof Explorer

Theorem locfincmp

Proof