islocfin

Description: The statement "is a locally finite cover." (Contributed by Jeff Hankins, 21-Jan-2010)

	Ref	Expression
Hypotheses	islocfin.1	$⊢ X = ⋃ J$
	islocfin.2	$⊢ Y = ⋃ A$
Assertion	islocfin	$⊢ A \in LocFin (J) \leftrightarrow (J \in Top \land X = Y \land \forall x \in X \exists n \in J (x \in n \land \{s \in A \| s \cap n \neq \emptyset\} \in Fin))$

Proof

Step	Hyp	Ref	Expression
1		islocfin.1	$⊢ X = ⋃ J$
2		islocfin.2	$⊢ Y = ⋃ A$
3		df-locfin	$⊢ LocFin = (j \in Top ⟼ \{y \| (⋃ j = ⋃ y \land \forall x \in ⋃ j \exists n \in j (x \in n \land \{s \in y \| s \cap n \neq \emptyset\} \in Fin))\})$
4	3	mptrcl	$⊢ A \in LocFin (J) \to J \in Top$
5		eqimss2	$⊢ X = ⋃ y \to ⋃ y \subseteq X$
6		sspwuni	$⊢ y \subseteq 𝒫 X \leftrightarrow ⋃ y \subseteq X$
7	5 6	sylibr	$⊢ X = ⋃ y \to y \subseteq 𝒫 X$
8		velpw	$⊢ y \in 𝒫 𝒫 X \leftrightarrow y \subseteq 𝒫 X$
9	7 8	sylibr	$⊢ X = ⋃ y \to y \in 𝒫 𝒫 X$
10	9	adantr	$⊢ (X = ⋃ y \land \forall x \in X \exists n \in J (x \in n \land \{s \in y \| s \cap n \neq \emptyset\} \in Fin)) \to y \in 𝒫 𝒫 X$
11	10	abssi	$⊢ \{y \| (X = ⋃ y \land \forall x \in X \exists n \in J (x \in n \land \{s \in y \| s \cap n \neq \emptyset\} \in Fin))\} \subseteq 𝒫 𝒫 X$
12	1	topopn	$⊢ J \in Top \to X \in J$
13		pwexg	$⊢ X \in J \to 𝒫 X \in V$
14		pwexg	$⊢ 𝒫 X \in V \to 𝒫 𝒫 X \in V$
15	12 13 14	3syl	$⊢ J \in Top \to 𝒫 𝒫 X \in V$
16		ssexg	$⊢ (\{y \| (X = ⋃ y \land \forall x \in X \exists n \in J (x \in n \land \{s \in y \| s \cap n \neq \emptyset\} \in Fin))\} \subseteq 𝒫 𝒫 X \land 𝒫 𝒫 X \in V) \to \{y \| (X = ⋃ y \land \forall x \in X \exists n \in J (x \in n \land \{s \in y \| s \cap n \neq \emptyset\} \in Fin))\} \in V$
17	11 15 16	sylancr	$⊢ J \in Top \to \{y \| (X = ⋃ y \land \forall x \in X \exists n \in J (x \in n \land \{s \in y \| s \cap n \neq \emptyset\} \in Fin))\} \in V$
18		unieq	$⊢ j = J \to ⋃ j = ⋃ J$
19	18 1	syl6eqr	$⊢ j = J \to ⋃ j = X$
20	19	eqeq1d	$⊢ j = J \to (⋃ j = ⋃ y \leftrightarrow X = ⋃ y)$
21		rexeq	$⊢ j = J \to (\exists n \in j (x \in n \land \{s \in y \| s \cap n \neq \emptyset\} \in Fin) \leftrightarrow \exists n \in J (x \in n \land \{s \in y \| s \cap n \neq \emptyset\} \in Fin))$
22	19 21	raleqbidv	$⊢ j = J \to (\forall x \in ⋃ j \exists n \in j (x \in n \land \{s \in y \| s \cap n \neq \emptyset\} \in Fin) \leftrightarrow \forall x \in X \exists n \in J (x \in n \land \{s \in y \| s \cap n \neq \emptyset\} \in Fin))$
23	20 22	anbi12d	$⊢ j = J \to ((⋃ j = ⋃ y \land \forall x \in ⋃ j \exists n \in j (x \in n \land \{s \in y \| s \cap n \neq \emptyset\} \in Fin)) \leftrightarrow (X = ⋃ y \land \forall x \in X \exists n \in J (x \in n \land \{s \in y \| s \cap n \neq \emptyset\} \in Fin)))$
24	23	abbidv	$⊢ j = J \to \{y \| (⋃ j = ⋃ y \land \forall x \in ⋃ j \exists n \in j (x \in n \land \{s \in y \| s \cap n \neq \emptyset\} \in Fin))\} = \{y \| (X = ⋃ y \land \forall x \in X \exists n \in J (x \in n \land \{s \in y \| s \cap n \neq \emptyset\} \in Fin))\}$
25	24 3	fvmptg	$⊢ (J \in Top \land \{y \| (X = ⋃ y \land \forall x \in X \exists n \in J (x \in n \land \{s \in y \| s \cap n \neq \emptyset\} \in Fin))\} \in V) \to LocFin (J) = \{y \| (X = ⋃ y \land \forall x \in X \exists n \in J (x \in n \land \{s \in y \| s \cap n \neq \emptyset\} \in Fin))\}$
26	17 25	mpdan	$⊢ J \in Top \to LocFin (J) = \{y \| (X = ⋃ y \land \forall x \in X \exists n \in J (x \in n \land \{s \in y \| s \cap n \neq \emptyset\} \in Fin))\}$
27	26	eleq2d	$⊢ J \in Top \to (A \in LocFin (J) \leftrightarrow A \in \{y \| (X = ⋃ y \land \forall x \in X \exists n \in J (x \in n \land \{s \in y \| s \cap n \neq \emptyset\} \in Fin))\})$
28		elex	$⊢ A \in \{y \| (X = ⋃ y \land \forall x \in X \exists n \in J (x \in n \land \{s \in y \| s \cap n \neq \emptyset\} \in Fin))\} \to A \in V$
29	28	adantl	$⊢ (J \in Top \land A \in \{y \| (X = ⋃ y \land \forall x \in X \exists n \in J (x \in n \land \{s \in y \| s \cap n \neq \emptyset\} \in Fin))\}) \to A \in V$
30		simpr	$⊢ (J \in Top \land X = Y) \to X = Y$
31	30 2	syl6eq	$⊢ (J \in Top \land X = Y) \to X = ⋃ A$
32	12	adantr	$⊢ (J \in Top \land X = Y) \to X \in J$
33	31 32	eqeltrrd	$⊢ (J \in Top \land X = Y) \to ⋃ A \in J$
34	33	elexd	$⊢ (J \in Top \land X = Y) \to ⋃ A \in V$
35		uniexb	$⊢ A \in V \leftrightarrow ⋃ A \in V$
36	34 35	sylibr	$⊢ (J \in Top \land X = Y) \to A \in V$
37	36	adantrr	$⊢ (J \in Top \land (X = Y \land \forall x \in X \exists n \in J (x \in n \land \{s \in A \| s \cap n \neq \emptyset\} \in Fin))) \to A \in V$
38		unieq	$⊢ y = A \to ⋃ y = ⋃ A$
39	38 2	syl6eqr	$⊢ y = A \to ⋃ y = Y$
40	39	eqeq2d	$⊢ y = A \to (X = ⋃ y \leftrightarrow X = Y)$
41		rabeq	$⊢ y = A \to \{s \in y \| s \cap n \neq \emptyset\} = \{s \in A \| s \cap n \neq \emptyset\}$
42	41	eleq1d	$⊢ y = A \to (\{s \in y \| s \cap n \neq \emptyset\} \in Fin \leftrightarrow \{s \in A \| s \cap n \neq \emptyset\} \in Fin)$
43	42	anbi2d	$⊢ y = A \to ((x \in n \land \{s \in y \| s \cap n \neq \emptyset\} \in Fin) \leftrightarrow (x \in n \land \{s \in A \| s \cap n \neq \emptyset\} \in Fin))$
44	43	rexbidv	$⊢ y = A \to (\exists n \in J (x \in n \land \{s \in y \| s \cap n \neq \emptyset\} \in Fin) \leftrightarrow \exists n \in J (x \in n \land \{s \in A \| s \cap n \neq \emptyset\} \in Fin))$
45	44	ralbidv	$⊢ y = A \to (\forall x \in X \exists n \in J (x \in n \land \{s \in y \| s \cap n \neq \emptyset\} \in Fin) \leftrightarrow \forall x \in X \exists n \in J (x \in n \land \{s \in A \| s \cap n \neq \emptyset\} \in Fin))$
46	40 45	anbi12d	$⊢ y = A \to ((X = ⋃ y \land \forall x \in X \exists n \in J (x \in n \land \{s \in y \| s \cap n \neq \emptyset\} \in Fin)) \leftrightarrow (X = Y \land \forall x \in X \exists n \in J (x \in n \land \{s \in A \| s \cap n \neq \emptyset\} \in Fin)))$
47	46	elabg	$⊢ A \in V \to (A \in \{y \| (X = ⋃ y \land \forall x \in X \exists n \in J (x \in n \land \{s \in y \| s \cap n \neq \emptyset\} \in Fin))\} \leftrightarrow (X = Y \land \forall x \in X \exists n \in J (x \in n \land \{s \in A \| s \cap n \neq \emptyset\} \in Fin)))$
48	29 37 47	pm5.21nd	$⊢ J \in Top \to (A \in \{y \| (X = ⋃ y \land \forall x \in X \exists n \in J (x \in n \land \{s \in y \| s \cap n \neq \emptyset\} \in Fin))\} \leftrightarrow (X = Y \land \forall x \in X \exists n \in J (x \in n \land \{s \in A \| s \cap n \neq \emptyset\} \in Fin)))$
49	27 48	bitrd	$⊢ J \in Top \to (A \in LocFin (J) \leftrightarrow (X = Y \land \forall x \in X \exists n \in J (x \in n \land \{s \in A \| s \cap n \neq \emptyset\} \in Fin)))$
50	4 49	biadanii	$⊢ A \in LocFin (J) \leftrightarrow (J \in Top \land (X = Y \land \forall x \in X \exists n \in J (x \in n \land \{s \in A \| s \cap n \neq \emptyset\} \in Fin)))$
51		3anass	$⊢ (J \in Top \land X = Y \land \forall x \in X \exists n \in J (x \in n \land \{s \in A \| s \cap n \neq \emptyset\} \in Fin)) \leftrightarrow (J \in Top \land (X = Y \land \forall x \in X \exists n \in J (x \in n \land \{s \in A \| s \cap n \neq \emptyset\} \in Fin)))$
52	50 51	bitr4i	$⊢ A \in LocFin (J) \leftrightarrow (J \in Top \land X = Y \land \forall x \in X \exists n \in J (x \in n \land \{s \in A \| s \cap n \neq \emptyset\} \in Fin))$

Metamath Proof Explorer

Theorem islocfin

Proof