bcth3

Description: Baire's Category Theorem, version 3: The intersection of countably many dense open sets is dense. (Contributed by Mario Carneiro, 10-Jan-2014)

		Ref	Expression
	Hypothesis	bcth.2	$⊢ J = MetOpen (D)$
	Assertion	bcth3	$⊢ (D \in CMet (X) \land M : ℕ ⟶ J \land \forall k \in ℕ cls (J) (M (k)) = X) \to cls (J) (⋂ ran M) = X$

Proof

Step	Hyp	Ref	Expression
1		bcth.2	$⊢ J = MetOpen (D)$
2		cmetmet	$⊢ D \in CMet (X) \to D \in Met (X)$
3		metxmet	$⊢ D \in Met (X) \to D \in ∞Met (X)$
4	2 3	syl	$⊢ D \in CMet (X) \to D \in ∞Met (X)$
5	1	mopntop	$⊢ D \in ∞Met (X) \to J \in Top$
6	5	ad2antrr	$⊢ ((D \in ∞Met (X) \land M : ℕ ⟶ J) \land k \in ℕ) \to J \in Top$
7		ffvelrn	$⊢ (M : ℕ ⟶ J \land k \in ℕ) \to M (k) \in J$
8		elssuni	$⊢ M (k) \in J \to M (k) \subseteq ⋃ J$
9	7 8	syl	$⊢ (M : ℕ ⟶ J \land k \in ℕ) \to M (k) \subseteq ⋃ J$
10	9	adantll	$⊢ ((D \in ∞Met (X) \land M : ℕ ⟶ J) \land k \in ℕ) \to M (k) \subseteq ⋃ J$
11		eqid	$⊢ ⋃ J = ⋃ J$
12	11	clsval2	$⊢ (J \in Top \land M (k) \subseteq ⋃ J) \to cls (J) (M (k)) = ⋃ J ∖ int (J) (⋃ J ∖ M (k))$
13	6 10 12	syl2anc	$⊢ ((D \in ∞Met (X) \land M : ℕ ⟶ J) \land k \in ℕ) \to cls (J) (M (k)) = ⋃ J ∖ int (J) (⋃ J ∖ M (k))$
14	1	mopnuni	$⊢ D \in ∞Met (X) \to X = ⋃ J$
15	14	ad2antrr	$⊢ ((D \in ∞Met (X) \land M : ℕ ⟶ J) \land k \in ℕ) \to X = ⋃ J$
16	13 15	eqeq12d	$⊢ ((D \in ∞Met (X) \land M : ℕ ⟶ J) \land k \in ℕ) \to (cls (J) (M (k)) = X \leftrightarrow ⋃ J ∖ int (J) (⋃ J ∖ M (k)) = ⋃ J)$
17		difeq2	$⊢ ⋃ J ∖ int (J) (⋃ J ∖ M (k)) = ⋃ J \to ⋃ J ∖ (⋃ J ∖ int (J) (⋃ J ∖ M (k))) = ⋃ J ∖ ⋃ J$
18		difid	$⊢ ⋃ J ∖ ⋃ J = \emptyset$
19	17 18	syl6eq	$⊢ ⋃ J ∖ int (J) (⋃ J ∖ M (k)) = ⋃ J \to ⋃ J ∖ (⋃ J ∖ int (J) (⋃ J ∖ M (k))) = \emptyset$
20		difss	$⊢ ⋃ J ∖ M (k) \subseteq ⋃ J$
21	11	ntropn	$⊢ (J \in Top \land ⋃ J ∖ M (k) \subseteq ⋃ J) \to int (J) (⋃ J ∖ M (k)) \in J$
22	6 20 21	sylancl	$⊢ ((D \in ∞Met (X) \land M : ℕ ⟶ J) \land k \in ℕ) \to int (J) (⋃ J ∖ M (k)) \in J$
23		elssuni	$⊢ int (J) (⋃ J ∖ M (k)) \in J \to int (J) (⋃ J ∖ M (k)) \subseteq ⋃ J$
24	22 23	syl	$⊢ ((D \in ∞Met (X) \land M : ℕ ⟶ J) \land k \in ℕ) \to int (J) (⋃ J ∖ M (k)) \subseteq ⋃ J$
25		dfss4	$⊢ int (J) (⋃ J ∖ M (k)) \subseteq ⋃ J \leftrightarrow ⋃ J ∖ (⋃ J ∖ int (J) (⋃ J ∖ M (k))) = int (J) (⋃ J ∖ M (k))$
26	24 25	sylib	$⊢ ((D \in ∞Met (X) \land M : ℕ ⟶ J) \land k \in ℕ) \to ⋃ J ∖ (⋃ J ∖ int (J) (⋃ J ∖ M (k))) = int (J) (⋃ J ∖ M (k))$
27		id	$⊢ k \in ℕ \to k \in ℕ$
28		elfvdm	$⊢ D \in ∞Met (X) \to X \in dom ∞Met$
29		difexg	$⊢ X \in dom ∞Met \to X ∖ M (k) \in V$
30	28 29	syl	$⊢ D \in ∞Met (X) \to X ∖ M (k) \in V$
31	30	adantr	$⊢ (D \in ∞Met (X) \land M : ℕ ⟶ J) \to X ∖ M (k) \in V$
32		fveq2	$⊢ x = k \to M (x) = M (k)$
33	32	difeq2d	$⊢ x = k \to X ∖ M (x) = X ∖ M (k)$
34		eqid	$⊢ (x \in ℕ ⟼ X ∖ M (x)) = (x \in ℕ ⟼ X ∖ M (x))$
35	33 34	fvmptg	$⊢ (k \in ℕ \land X ∖ M (k) \in V) \to (x \in ℕ ⟼ X ∖ M (x)) (k) = X ∖ M (k)$
36	27 31 35	syl2anr	$⊢ ((D \in ∞Met (X) \land M : ℕ ⟶ J) \land k \in ℕ) \to (x \in ℕ ⟼ X ∖ M (x)) (k) = X ∖ M (k)$
37	15	difeq1d	$⊢ ((D \in ∞Met (X) \land M : ℕ ⟶ J) \land k \in ℕ) \to X ∖ M (k) = ⋃ J ∖ M (k)$
38	36 37	eqtrd	$⊢ ((D \in ∞Met (X) \land M : ℕ ⟶ J) \land k \in ℕ) \to (x \in ℕ ⟼ X ∖ M (x)) (k) = ⋃ J ∖ M (k)$
39	38	fveq2d	$⊢ ((D \in ∞Met (X) \land M : ℕ ⟶ J) \land k \in ℕ) \to int (J) ((x \in ℕ ⟼ X ∖ M (x)) (k)) = int (J) (⋃ J ∖ M (k))$
40	26 39	eqtr4d	$⊢ ((D \in ∞Met (X) \land M : ℕ ⟶ J) \land k \in ℕ) \to ⋃ J ∖ (⋃ J ∖ int (J) (⋃ J ∖ M (k))) = int (J) ((x \in ℕ ⟼ X ∖ M (x)) (k))$
41	40	eqeq1d	$⊢ ((D \in ∞Met (X) \land M : ℕ ⟶ J) \land k \in ℕ) \to (⋃ J ∖ (⋃ J ∖ int (J) (⋃ J ∖ M (k))) = \emptyset \leftrightarrow int (J) ((x \in ℕ ⟼ X ∖ M (x)) (k)) = \emptyset)$
42	19 41	syl5ib	$⊢ ((D \in ∞Met (X) \land M : ℕ ⟶ J) \land k \in ℕ) \to (⋃ J ∖ int (J) (⋃ J ∖ M (k)) = ⋃ J \to int (J) ((x \in ℕ ⟼ X ∖ M (x)) (k)) = \emptyset)$
43	16 42	sylbid	$⊢ ((D \in ∞Met (X) \land M : ℕ ⟶ J) \land k \in ℕ) \to (cls (J) (M (k)) = X \to int (J) ((x \in ℕ ⟼ X ∖ M (x)) (k)) = \emptyset)$
44	43	ralimdva	$⊢ (D \in ∞Met (X) \land M : ℕ ⟶ J) \to (\forall k \in ℕ cls (J) (M (k)) = X \to \forall k \in ℕ int (J) ((x \in ℕ ⟼ X ∖ M (x)) (k)) = \emptyset)$
45	4 44	sylan	$⊢ (D \in CMet (X) \land M : ℕ ⟶ J) \to (\forall k \in ℕ cls (J) (M (k)) = X \to \forall k \in ℕ int (J) ((x \in ℕ ⟼ X ∖ M (x)) (k)) = \emptyset)$
46		ffvelrn	$⊢ (M : ℕ ⟶ J \land x \in ℕ) \to M (x) \in J$
47	14	difeq1d	$⊢ D \in ∞Met (X) \to X ∖ M (x) = ⋃ J ∖ M (x)$
48	47	adantr	$⊢ (D \in ∞Met (X) \land M (x) \in J) \to X ∖ M (x) = ⋃ J ∖ M (x)$
49	11	opncld	$⊢ (J \in Top \land M (x) \in J) \to ⋃ J ∖ M (x) \in Clsd (J)$
50	5 49	sylan	$⊢ (D \in ∞Met (X) \land M (x) \in J) \to ⋃ J ∖ M (x) \in Clsd (J)$
51	48 50	eqeltrd	$⊢ (D \in ∞Met (X) \land M (x) \in J) \to X ∖ M (x) \in Clsd (J)$
52	46 51	sylan2	$⊢ (D \in ∞Met (X) \land (M : ℕ ⟶ J \land x \in ℕ)) \to X ∖ M (x) \in Clsd (J)$
53	52	anassrs	$⊢ ((D \in ∞Met (X) \land M : ℕ ⟶ J) \land x \in ℕ) \to X ∖ M (x) \in Clsd (J)$
54	53	ralrimiva	$⊢ (D \in ∞Met (X) \land M : ℕ ⟶ J) \to \forall x \in ℕ X ∖ M (x) \in Clsd (J)$
55	4 54	sylan	$⊢ (D \in CMet (X) \land M : ℕ ⟶ J) \to \forall x \in ℕ X ∖ M (x) \in Clsd (J)$
56	34	fmpt	$⊢ \forall x \in ℕ X ∖ M (x) \in Clsd (J) \leftrightarrow (x \in ℕ ⟼ X ∖ M (x)) : ℕ ⟶ Clsd (J)$
57	55 56	sylib	$⊢ (D \in CMet (X) \land M : ℕ ⟶ J) \to (x \in ℕ ⟼ X ∖ M (x)) : ℕ ⟶ Clsd (J)$
58		nne	$⊢ \neg int (J) ((x \in ℕ ⟼ X ∖ M (x)) (k)) \neq \emptyset \leftrightarrow int (J) ((x \in ℕ ⟼ X ∖ M (x)) (k)) = \emptyset$
59	58	ralbii	$⊢ \forall k \in ℕ \neg int (J) ((x \in ℕ ⟼ X ∖ M (x)) (k)) \neq \emptyset \leftrightarrow \forall k \in ℕ int (J) ((x \in ℕ ⟼ X ∖ M (x)) (k)) = \emptyset$
60		ralnex	$⊢ \forall k \in ℕ \neg int (J) ((x \in ℕ ⟼ X ∖ M (x)) (k)) \neq \emptyset \leftrightarrow \neg \exists k \in ℕ int (J) ((x \in ℕ ⟼ X ∖ M (x)) (k)) \neq \emptyset$
61	59 60	bitr3i	$⊢ \forall k \in ℕ int (J) ((x \in ℕ ⟼ X ∖ M (x)) (k)) = \emptyset \leftrightarrow \neg \exists k \in ℕ int (J) ((x \in ℕ ⟼ X ∖ M (x)) (k)) \neq \emptyset$
62	1	bcth	$⊢ (D \in CMet (X) \land (x \in ℕ ⟼ X ∖ M (x)) : ℕ ⟶ Clsd (J) \land int (J) (⋃ ran (x \in ℕ ⟼ X ∖ M (x))) \neq \emptyset) \to \exists k \in ℕ int (J) ((x \in ℕ ⟼ X ∖ M (x)) (k)) \neq \emptyset$
63	62	3expia	$⊢ (D \in CMet (X) \land (x \in ℕ ⟼ X ∖ M (x)) : ℕ ⟶ Clsd (J)) \to (int (J) (⋃ ran (x \in ℕ ⟼ X ∖ M (x))) \neq \emptyset \to \exists k \in ℕ int (J) ((x \in ℕ ⟼ X ∖ M (x)) (k)) \neq \emptyset)$
64	63	necon1bd	$⊢ (D \in CMet (X) \land (x \in ℕ ⟼ X ∖ M (x)) : ℕ ⟶ Clsd (J)) \to (\neg \exists k \in ℕ int (J) ((x \in ℕ ⟼ X ∖ M (x)) (k)) \neq \emptyset \to int (J) (⋃ ran (x \in ℕ ⟼ X ∖ M (x))) = \emptyset)$
65	61 64	syl5bi	$⊢ (D \in CMet (X) \land (x \in ℕ ⟼ X ∖ M (x)) : ℕ ⟶ Clsd (J)) \to (\forall k \in ℕ int (J) ((x \in ℕ ⟼ X ∖ M (x)) (k)) = \emptyset \to int (J) (⋃ ran (x \in ℕ ⟼ X ∖ M (x))) = \emptyset)$
66	57 65	syldan	$⊢ (D \in CMet (X) \land M : ℕ ⟶ J) \to (\forall k \in ℕ int (J) ((x \in ℕ ⟼ X ∖ M (x)) (k)) = \emptyset \to int (J) (⋃ ran (x \in ℕ ⟼ X ∖ M (x))) = \emptyset)$
67		difeq2	$⊢ int (J) (⋃ ran (x \in ℕ ⟼ X ∖ M (x))) = \emptyset \to ⋃ J ∖ int (J) (⋃ ran (x \in ℕ ⟼ X ∖ M (x))) = ⋃ J ∖ \emptyset$
68		difexg	$⊢ X \in dom ∞Met \to X ∖ M (x) \in V$
69	28 68	syl	$⊢ D \in ∞Met (X) \to X ∖ M (x) \in V$
70	69	ad2antrr	$⊢ ((D \in ∞Met (X) \land M : ℕ ⟶ J) \land x \in ℕ) \to X ∖ M (x) \in V$
71	70	ralrimiva	$⊢ (D \in ∞Met (X) \land M : ℕ ⟶ J) \to \forall x \in ℕ X ∖ M (x) \in V$
72	34	fnmpt	$⊢ \forall x \in ℕ X ∖ M (x) \in V \to (x \in ℕ ⟼ X ∖ M (x)) Fn ℕ$
73		fniunfv	$⊢ (x \in ℕ ⟼ X ∖ M (x)) Fn ℕ \to ⋃_{k \in ℕ} (x \in ℕ ⟼ X ∖ M (x)) (k) = ⋃ ran (x \in ℕ ⟼ X ∖ M (x))$
74	71 72 73	3syl	$⊢ (D \in ∞Met (X) \land M : ℕ ⟶ J) \to ⋃_{k \in ℕ} (x \in ℕ ⟼ X ∖ M (x)) (k) = ⋃ ran (x \in ℕ ⟼ X ∖ M (x))$
75	36	iuneq2dv	$⊢ (D \in ∞Met (X) \land M : ℕ ⟶ J) \to ⋃_{k \in ℕ} (x \in ℕ ⟼ X ∖ M (x)) (k) = ⋃_{k \in ℕ} (X ∖ M (k))$
76	33	cbviunv	$⊢ ⋃_{x \in ℕ} (X ∖ M (x)) = ⋃_{k \in ℕ} (X ∖ M (k))$
77	75 76	syl6eqr	$⊢ (D \in ∞Met (X) \land M : ℕ ⟶ J) \to ⋃_{k \in ℕ} (x \in ℕ ⟼ X ∖ M (x)) (k) = ⋃_{x \in ℕ} (X ∖ M (x))$
78	74 77	eqtr3d	$⊢ (D \in ∞Met (X) \land M : ℕ ⟶ J) \to ⋃ ran (x \in ℕ ⟼ X ∖ M (x)) = ⋃_{x \in ℕ} (X ∖ M (x))$
79		iundif2	$⊢ ⋃_{x \in ℕ} (X ∖ M (x)) = X ∖ ⋂_{x \in ℕ} M (x)$
80	78 79	syl6eq	$⊢ (D \in ∞Met (X) \land M : ℕ ⟶ J) \to ⋃ ran (x \in ℕ ⟼ X ∖ M (x)) = X ∖ ⋂_{x \in ℕ} M (x)$
81		ffn	$⊢ M : ℕ ⟶ J \to M Fn ℕ$
82	81	adantl	$⊢ (D \in ∞Met (X) \land M : ℕ ⟶ J) \to M Fn ℕ$
83		fniinfv	$⊢ M Fn ℕ \to ⋂_{x \in ℕ} M (x) = ⋂ ran M$
84	82 83	syl	$⊢ (D \in ∞Met (X) \land M : ℕ ⟶ J) \to ⋂_{x \in ℕ} M (x) = ⋂ ran M$
85	84	difeq2d	$⊢ (D \in ∞Met (X) \land M : ℕ ⟶ J) \to X ∖ ⋂_{x \in ℕ} M (x) = X ∖ ⋂ ran M$
86	14	adantr	$⊢ (D \in ∞Met (X) \land M : ℕ ⟶ J) \to X = ⋃ J$
87	86	difeq1d	$⊢ (D \in ∞Met (X) \land M : ℕ ⟶ J) \to X ∖ ⋂ ran M = ⋃ J ∖ ⋂ ran M$
88	80 85 87	3eqtrd	$⊢ (D \in ∞Met (X) \land M : ℕ ⟶ J) \to ⋃ ran (x \in ℕ ⟼ X ∖ M (x)) = ⋃ J ∖ ⋂ ran M$
89	88	fveq2d	$⊢ (D \in ∞Met (X) \land M : ℕ ⟶ J) \to int (J) (⋃ ran (x \in ℕ ⟼ X ∖ M (x))) = int (J) (⋃ J ∖ ⋂ ran M)$
90	89	difeq2d	$⊢ (D \in ∞Met (X) \land M : ℕ ⟶ J) \to ⋃ J ∖ int (J) (⋃ ran (x \in ℕ ⟼ X ∖ M (x))) = ⋃ J ∖ int (J) (⋃ J ∖ ⋂ ran M)$
91	5	adantr	$⊢ (D \in ∞Met (X) \land M : ℕ ⟶ J) \to J \in Top$
92		1nn	$⊢ 1 \in ℕ$
93		biidd	$⊢ k = 1 \to (((D \in ∞Met (X) \land M : ℕ ⟶ J) \to ⋂ ran M \subseteq ⋃ J) \leftrightarrow ((D \in ∞Met (X) \land M : ℕ ⟶ J) \to ⋂ ran M \subseteq ⋃ J))$
94		fnfvelrn	$⊢ (M Fn ℕ \land k \in ℕ) \to M (k) \in ran M$
95	82 94	sylan	$⊢ ((D \in ∞Met (X) \land M : ℕ ⟶ J) \land k \in ℕ) \to M (k) \in ran M$
96		intss1	$⊢ M (k) \in ran M \to ⋂ ran M \subseteq M (k)$
97	95 96	syl	$⊢ ((D \in ∞Met (X) \land M : ℕ ⟶ J) \land k \in ℕ) \to ⋂ ran M \subseteq M (k)$
98	97 10	sstrd	$⊢ ((D \in ∞Met (X) \land M : ℕ ⟶ J) \land k \in ℕ) \to ⋂ ran M \subseteq ⋃ J$
99	98	expcom	$⊢ k \in ℕ \to ((D \in ∞Met (X) \land M : ℕ ⟶ J) \to ⋂ ran M \subseteq ⋃ J)$
100	93 99	vtoclga	$⊢ 1 \in ℕ \to ((D \in ∞Met (X) \land M : ℕ ⟶ J) \to ⋂ ran M \subseteq ⋃ J)$
101	92 100	ax-mp	$⊢ (D \in ∞Met (X) \land M : ℕ ⟶ J) \to ⋂ ran M \subseteq ⋃ J$
102	11	clsval2	$⊢ (J \in Top \land ⋂ ran M \subseteq ⋃ J) \to cls (J) (⋂ ran M) = ⋃ J ∖ int (J) (⋃ J ∖ ⋂ ran M)$
103	91 101 102	syl2anc	$⊢ (D \in ∞Met (X) \land M : ℕ ⟶ J) \to cls (J) (⋂ ran M) = ⋃ J ∖ int (J) (⋃ J ∖ ⋂ ran M)$
104	90 103	eqtr4d	$⊢ (D \in ∞Met (X) \land M : ℕ ⟶ J) \to ⋃ J ∖ int (J) (⋃ ran (x \in ℕ ⟼ X ∖ M (x))) = cls (J) (⋂ ran M)$
105		dif0	$⊢ ⋃ J ∖ \emptyset = ⋃ J$
106	86 105	syl6reqr	$⊢ (D \in ∞Met (X) \land M : ℕ ⟶ J) \to ⋃ J ∖ \emptyset = X$
107	104 106	eqeq12d	$⊢ (D \in ∞Met (X) \land M : ℕ ⟶ J) \to (⋃ J ∖ int (J) (⋃ ran (x \in ℕ ⟼ X ∖ M (x))) = ⋃ J ∖ \emptyset \leftrightarrow cls (J) (⋂ ran M) = X)$
108	67 107	syl5ib	$⊢ (D \in ∞Met (X) \land M : ℕ ⟶ J) \to (int (J) (⋃ ran (x \in ℕ ⟼ X ∖ M (x))) = \emptyset \to cls (J) (⋂ ran M) = X)$
109	4 108	sylan	$⊢ (D \in CMet (X) \land M : ℕ ⟶ J) \to (int (J) (⋃ ran (x \in ℕ ⟼ X ∖ M (x))) = \emptyset \to cls (J) (⋂ ran M) = X)$
110	45 66 109	3syld	$⊢ (D \in CMet (X) \land M : ℕ ⟶ J) \to (\forall k \in ℕ cls (J) (M (k)) = X \to cls (J) (⋂ ran M) = X)$
111	110	3impia	$⊢ (D \in CMet (X) \land M : ℕ ⟶ J \land \forall k \in ℕ cls (J) (M (k)) = X) \to cls (J) (⋂ ran M) = X$

Metamath Proof Explorer

Theorem bcth3

Proof