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	eqtrdi	$⊢ ⋃ 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	28	difexd	$⊢ D \in ∞Met (X) \to X ∖ M (k) \in V$
30	29	adantr	$⊢ (D \in ∞Met (X) \land M : ℕ ⟶ J) \to X ∖ M (k) \in V$
31		fveq2	$⊢ x = k \to M (x) = M (k)$
32	31	difeq2d	$⊢ x = k \to X ∖ M (x) = X ∖ M (k)$
33		eqid	$⊢ (x \in ℕ ⟼ X ∖ M (x)) = (x \in ℕ ⟼ X ∖ M (x))$
34	32 33	fvmptg	$⊢ (k \in ℕ \land X ∖ M (k) \in V) \to (x \in ℕ ⟼ X ∖ M (x)) (k) = X ∖ M (k)$
35	27 30 34	syl2anr	$⊢ ((D \in ∞Met (X) \land M : ℕ ⟶ J) \land k \in ℕ) \to (x \in ℕ ⟼ X ∖ M (x)) (k) = X ∖ M (k)$
36	15	difeq1d	$⊢ ((D \in ∞Met (X) \land M : ℕ ⟶ J) \land k \in ℕ) \to X ∖ M (k) = ⋃ J ∖ M (k)$
37	35 36	eqtrd	$⊢ ((D \in ∞Met (X) \land M : ℕ ⟶ J) \land k \in ℕ) \to (x \in ℕ ⟼ X ∖ M (x)) (k) = ⋃ J ∖ M (k)$
38	37	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))$
39	26 38	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))$
40	39	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)$
41	19 40	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)$
42	16 41	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)$
43	42	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)$
44	4 43	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)$
45		ffvelrn	$⊢ (M : ℕ ⟶ J \land x \in ℕ) \to M (x) \in J$
46	14	difeq1d	$⊢ D \in ∞Met (X) \to X ∖ M (x) = ⋃ J ∖ M (x)$
47	46	adantr	$⊢ (D \in ∞Met (X) \land M (x) \in J) \to X ∖ M (x) = ⋃ J ∖ M (x)$
48	11	opncld	$⊢ (J \in Top \land M (x) \in J) \to ⋃ J ∖ M (x) \in Clsd (J)$
49	5 48	sylan	$⊢ (D \in ∞Met (X) \land M (x) \in J) \to ⋃ J ∖ M (x) \in Clsd (J)$
50	47 49	eqeltrd	$⊢ (D \in ∞Met (X) \land M (x) \in J) \to X ∖ M (x) \in Clsd (J)$
51	45 50	sylan2	$⊢ (D \in ∞Met (X) \land (M : ℕ ⟶ J \land x \in ℕ)) \to X ∖ M (x) \in Clsd (J)$
52	51	anassrs	$⊢ ((D \in ∞Met (X) \land M : ℕ ⟶ J) \land x \in ℕ) \to X ∖ M (x) \in Clsd (J)$
53	52	ralrimiva	$⊢ (D \in ∞Met (X) \land M : ℕ ⟶ J) \to \forall x \in ℕ X ∖ M (x) \in Clsd (J)$
54	4 53	sylan	$⊢ (D \in CMet (X) \land M : ℕ ⟶ J) \to \forall x \in ℕ X ∖ M (x) \in Clsd (J)$
55	33	fmpt	$⊢ \forall x \in ℕ X ∖ M (x) \in Clsd (J) \leftrightarrow (x \in ℕ ⟼ X ∖ M (x)) : ℕ ⟶ Clsd (J)$
56	54 55	sylib	$⊢ (D \in CMet (X) \land M : ℕ ⟶ J) \to (x \in ℕ ⟼ X ∖ M (x)) : ℕ ⟶ Clsd (J)$
57		nne	$⊢ \neg int (J) ((x \in ℕ ⟼ X ∖ M (x)) (k)) \neq \emptyset \leftrightarrow int (J) ((x \in ℕ ⟼ X ∖ M (x)) (k)) = \emptyset$
58	57	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$
59		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$
60	58 59	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$
61	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$
62	61	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)$
63	62	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)$
64	60 63	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)$
65	56 64	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)$
66		difeq2	$⊢ int (J) (⋃ ran (x \in ℕ ⟼ X ∖ M (x))) = \emptyset \to ⋃ J ∖ int (J) (⋃ ran (x \in ℕ ⟼ X ∖ M (x))) = ⋃ J ∖ \emptyset$
67	28	difexd	$⊢ D \in ∞Met (X) \to X ∖ M (x) \in V$
68	67	ad2antrr	$⊢ ((D \in ∞Met (X) \land M : ℕ ⟶ J) \land x \in ℕ) \to X ∖ M (x) \in V$
69	68	ralrimiva	$⊢ (D \in ∞Met (X) \land M : ℕ ⟶ J) \to \forall x \in ℕ X ∖ M (x) \in V$
70	33	fnmpt	$⊢ \forall x \in ℕ X ∖ M (x) \in V \to (x \in ℕ ⟼ X ∖ M (x)) Fn ℕ$
71		fniunfv	$⊢ (x \in ℕ ⟼ X ∖ M (x)) Fn ℕ \to ⋃_{k \in ℕ} (x \in ℕ ⟼ X ∖ M (x)) (k) = ⋃ ran (x \in ℕ ⟼ X ∖ M (x))$
72	69 70 71	3syl	$⊢ (D \in ∞Met (X) \land M : ℕ ⟶ J) \to ⋃_{k \in ℕ} (x \in ℕ ⟼ X ∖ M (x)) (k) = ⋃ ran (x \in ℕ ⟼ X ∖ M (x))$
73	35	iuneq2dv	$⊢ (D \in ∞Met (X) \land M : ℕ ⟶ J) \to ⋃_{k \in ℕ} (x \in ℕ ⟼ X ∖ M (x)) (k) = ⋃_{k \in ℕ} (X ∖ M (k))$
74	32	cbviunv	$⊢ ⋃_{x \in ℕ} (X ∖ M (x)) = ⋃_{k \in ℕ} (X ∖ M (k))$
75	73 74	eqtr4di	$⊢ (D \in ∞Met (X) \land M : ℕ ⟶ J) \to ⋃_{k \in ℕ} (x \in ℕ ⟼ X ∖ M (x)) (k) = ⋃_{x \in ℕ} (X ∖ M (x))$
76	72 75	eqtr3d	$⊢ (D \in ∞Met (X) \land M : ℕ ⟶ J) \to ⋃ ran (x \in ℕ ⟼ X ∖ M (x)) = ⋃_{x \in ℕ} (X ∖ M (x))$
77		iundif2	$⊢ ⋃_{x \in ℕ} (X ∖ M (x)) = X ∖ ⋂_{x \in ℕ} M (x)$
78	76 77	eqtrdi	$⊢ (D \in ∞Met (X) \land M : ℕ ⟶ J) \to ⋃ ran (x \in ℕ ⟼ X ∖ M (x)) = X ∖ ⋂_{x \in ℕ} M (x)$
79		ffn	$⊢ M : ℕ ⟶ J \to M Fn ℕ$
80	79	adantl	$⊢ (D \in ∞Met (X) \land M : ℕ ⟶ J) \to M Fn ℕ$
81		fniinfv	$⊢ M Fn ℕ \to ⋂_{x \in ℕ} M (x) = ⋂ ran M$
82	80 81	syl	$⊢ (D \in ∞Met (X) \land M : ℕ ⟶ J) \to ⋂_{x \in ℕ} M (x) = ⋂ ran M$
83	82	difeq2d	$⊢ (D \in ∞Met (X) \land M : ℕ ⟶ J) \to X ∖ ⋂_{x \in ℕ} M (x) = X ∖ ⋂ ran M$
84	14	adantr	$⊢ (D \in ∞Met (X) \land M : ℕ ⟶ J) \to X = ⋃ J$
85	84	difeq1d	$⊢ (D \in ∞Met (X) \land M : ℕ ⟶ J) \to X ∖ ⋂ ran M = ⋃ J ∖ ⋂ ran M$
86	78 83 85	3eqtrd	$⊢ (D \in ∞Met (X) \land M : ℕ ⟶ J) \to ⋃ ran (x \in ℕ ⟼ X ∖ M (x)) = ⋃ J ∖ ⋂ ran M$
87	86	fveq2d	$⊢ (D \in ∞Met (X) \land M : ℕ ⟶ J) \to int (J) (⋃ ran (x \in ℕ ⟼ X ∖ M (x))) = int (J) (⋃ J ∖ ⋂ ran M)$
88	87	difeq2d	$⊢ (D \in ∞Met (X) \land M : ℕ ⟶ J) \to ⋃ J ∖ int (J) (⋃ ran (x \in ℕ ⟼ X ∖ M (x))) = ⋃ J ∖ int (J) (⋃ J ∖ ⋂ ran M)$
89	5	adantr	$⊢ (D \in ∞Met (X) \land M : ℕ ⟶ J) \to J \in Top$
90		1nn	$⊢ 1 \in ℕ$
91		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))$
92		fnfvelrn	$⊢ (M Fn ℕ \land k \in ℕ) \to M (k) \in ran M$
93	80 92	sylan	$⊢ ((D \in ∞Met (X) \land M : ℕ ⟶ J) \land k \in ℕ) \to M (k) \in ran M$
94		intss1	$⊢ M (k) \in ran M \to ⋂ ran M \subseteq M (k)$
95	93 94	syl	$⊢ ((D \in ∞Met (X) \land M : ℕ ⟶ J) \land k \in ℕ) \to ⋂ ran M \subseteq M (k)$
96	95 10	sstrd	$⊢ ((D \in ∞Met (X) \land M : ℕ ⟶ J) \land k \in ℕ) \to ⋂ ran M \subseteq ⋃ J$
97	96	expcom	$⊢ k \in ℕ \to ((D \in ∞Met (X) \land M : ℕ ⟶ J) \to ⋂ ran M \subseteq ⋃ J)$
98	91 97	vtoclga	$⊢ 1 \in ℕ \to ((D \in ∞Met (X) \land M : ℕ ⟶ J) \to ⋂ ran M \subseteq ⋃ J)$
99	90 98	ax-mp	$⊢ (D \in ∞Met (X) \land M : ℕ ⟶ J) \to ⋂ ran M \subseteq ⋃ J$
100	11	clsval2	$⊢ (J \in Top \land ⋂ ran M \subseteq ⋃ J) \to cls (J) (⋂ ran M) = ⋃ J ∖ int (J) (⋃ J ∖ ⋂ ran M)$
101	89 99 100	syl2anc	$⊢ (D \in ∞Met (X) \land M : ℕ ⟶ J) \to cls (J) (⋂ ran M) = ⋃ J ∖ int (J) (⋃ J ∖ ⋂ ran M)$
102	88 101	eqtr4d	$⊢ (D \in ∞Met (X) \land M : ℕ ⟶ J) \to ⋃ J ∖ int (J) (⋃ ran (x \in ℕ ⟼ X ∖ M (x))) = cls (J) (⋂ ran M)$
103		dif0	$⊢ ⋃ J ∖ \emptyset = ⋃ J$
104	103 84	eqtr4id	$⊢ (D \in ∞Met (X) \land M : ℕ ⟶ J) \to ⋃ J ∖ \emptyset = X$
105	102 104	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)$
106	66 105	syl5ib	$⊢ (D \in ∞Met (X) \land M : ℕ ⟶ J) \to (int (J) (⋃ ran (x \in ℕ ⟼ X ∖ M (x))) = \emptyset \to cls (J) (⋂ ran M) = X)$
107	4 106	sylan	$⊢ (D \in CMet (X) \land M : ℕ ⟶ J) \to (int (J) (⋃ ran (x \in ℕ ⟼ X ∖ M (x))) = \emptyset \to cls (J) (⋂ ran M) = X)$
108	44 65 107	3syld	$⊢ (D \in CMet (X) \land M : ℕ ⟶ J) \to (\forall k \in ℕ cls (J) (M (k)) = X \to cls (J) (⋂ ran M) = X)$
109	108	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