locfincf

Description: A locally finite cover in a coarser topology is locally finite in a finer topology. (Contributed by Jeff Hankins, 22-Jan-2010) (Proof shortened by Mario Carneiro, 11-Sep-2015)

		Ref	Expression
	Hypothesis	locfincf.1	$⊢ X = ⋃ J$
	Assertion	locfincf	$⊢ (K \in TopOn (X) \land J \subseteq K) \to LocFin (J) \subseteq LocFin (K)$

Proof

Step	Hyp	Ref	Expression
1		locfincf.1	$⊢ X = ⋃ J$
2		topontop	$⊢ K \in TopOn (X) \to K \in Top$
3	2	ad2antrr	$⊢ ((K \in TopOn (X) \land J \subseteq K) \land x \in LocFin (J)) \to K \in Top$
4		toponuni	$⊢ K \in TopOn (X) \to X = ⋃ K$
5	4	ad2antrr	$⊢ ((K \in TopOn (X) \land J \subseteq K) \land x \in LocFin (J)) \to X = ⋃ K$
6		eqid	$⊢ ⋃ x = ⋃ x$
7	1 6	locfinbas	$⊢ x \in LocFin (J) \to X = ⋃ x$
8	7	adantl	$⊢ ((K \in TopOn (X) \land J \subseteq K) \land x \in LocFin (J)) \to X = ⋃ x$
9	5 8	eqtr3d	$⊢ ((K \in TopOn (X) \land J \subseteq K) \land x \in LocFin (J)) \to ⋃ K = ⋃ x$
10	5	eleq2d	$⊢ ((K \in TopOn (X) \land J \subseteq K) \land x \in LocFin (J)) \to (y \in X \leftrightarrow y \in ⋃ K)$
11	1	locfinnei	$⊢ (x \in LocFin (J) \land y \in X) \to \exists n \in J (y \in n \land \{s \in x \| s \cap n \neq \emptyset\} \in Fin)$
12	11	ex	$⊢ x \in LocFin (J) \to (y \in X \to \exists n \in J (y \in n \land \{s \in x \| s \cap n \neq \emptyset\} \in Fin))$
13		ssrexv	$⊢ J \subseteq K \to (\exists n \in J (y \in n \land \{s \in x \| s \cap n \neq \emptyset\} \in Fin) \to \exists n \in K (y \in n \land \{s \in x \| s \cap n \neq \emptyset\} \in Fin))$
14	13	adantl	$⊢ (K \in TopOn (X) \land J \subseteq K) \to (\exists n \in J (y \in n \land \{s \in x \| s \cap n \neq \emptyset\} \in Fin) \to \exists n \in K (y \in n \land \{s \in x \| s \cap n \neq \emptyset\} \in Fin))$
15	12 14	sylan9r	$⊢ ((K \in TopOn (X) \land J \subseteq K) \land x \in LocFin (J)) \to (y \in X \to \exists n \in K (y \in n \land \{s \in x \| s \cap n \neq \emptyset\} \in Fin))$
16	10 15	sylbird	$⊢ ((K \in TopOn (X) \land J \subseteq K) \land x \in LocFin (J)) \to (y \in ⋃ K \to \exists n \in K (y \in n \land \{s \in x \| s \cap n \neq \emptyset\} \in Fin))$
17	16	ralrimiv	$⊢ ((K \in TopOn (X) \land J \subseteq K) \land x \in LocFin (J)) \to \forall y \in ⋃ K \exists n \in K (y \in n \land \{s \in x \| s \cap n \neq \emptyset\} \in Fin)$
18		eqid	$⊢ ⋃ K = ⋃ K$
19	18 6	islocfin	$⊢ x \in LocFin (K) \leftrightarrow (K \in Top \land ⋃ K = ⋃ x \land \forall y \in ⋃ K \exists n \in K (y \in n \land \{s \in x \| s \cap n \neq \emptyset\} \in Fin))$
20	3 9 17 19	syl3anbrc	$⊢ ((K \in TopOn (X) \land J \subseteq K) \land x \in LocFin (J)) \to x \in LocFin (K)$
21	20	ex	$⊢ (K \in TopOn (X) \land J \subseteq K) \to (x \in LocFin (J) \to x \in LocFin (K))$
22	21	ssrdv	$⊢ (K \in TopOn (X) \land J \subseteq K) \to LocFin (J) \subseteq LocFin (K)$

Metamath Proof Explorer

Theorem locfincf

Proof