elcls3

Description: Membership in a closure in terms of the members of a basis. Theorem 6.5(b) of Munkres p. 95. (Contributed by NM, 26-Feb-2007) (Revised by Mario Carneiro, 3-Sep-2015)

	Ref	Expression
Hypotheses	elcls3.1	⊢ ( 𝜑 → 𝐽 = ( topGen ‘ 𝐵 ) )
	elcls3.2	⊢ ( 𝜑 → 𝑋 = ∪ 𝐽 )
	elcls3.3	⊢ ( 𝜑 → 𝐵 ∈ TopBases )
	elcls3.4	⊢ ( 𝜑 → 𝑆 ⊆ 𝑋 )
	elcls3.5	⊢ ( 𝜑 → 𝑃 ∈ 𝑋 )
Assertion	elcls3	⊢ ( 𝜑 → ( 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ↔ ∀ 𝑥 ∈ 𝐵 ( 𝑃 ∈ 𝑥 → ( 𝑥 ∩ 𝑆 ) ≠ ∅ ) ) )

Proof

Step	Hyp	Ref	Expression
1		elcls3.1	⊢ ( 𝜑 → 𝐽 = ( topGen ‘ 𝐵 ) )
2		elcls3.2	⊢ ( 𝜑 → 𝑋 = ∪ 𝐽 )
3		elcls3.3	⊢ ( 𝜑 → 𝐵 ∈ TopBases )
4		elcls3.4	⊢ ( 𝜑 → 𝑆 ⊆ 𝑋 )
5		elcls3.5	⊢ ( 𝜑 → 𝑃 ∈ 𝑋 )
6		tgcl	⊢ ( 𝐵 ∈ TopBases → ( topGen ‘ 𝐵 ) ∈ Top )
7	3 6	syl	⊢ ( 𝜑 → ( topGen ‘ 𝐵 ) ∈ Top )
8	1 7	eqeltrd	⊢ ( 𝜑 → 𝐽 ∈ Top )
9	4 2	sseqtrd	⊢ ( 𝜑 → 𝑆 ⊆ ∪ 𝐽 )
10	5 2	eleqtrd	⊢ ( 𝜑 → 𝑃 ∈ ∪ 𝐽 )
11		eqid	⊢ ∪ 𝐽 = ∪ 𝐽
12	11	elcls	⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ ∪ 𝐽 ∧ 𝑃 ∈ ∪ 𝐽 ) → ( 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ↔ ∀ 𝑦 ∈ 𝐽 ( 𝑃 ∈ 𝑦 → ( 𝑦 ∩ 𝑆 ) ≠ ∅ ) ) )
13	8 9 10 12	syl3anc	⊢ ( 𝜑 → ( 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ↔ ∀ 𝑦 ∈ 𝐽 ( 𝑃 ∈ 𝑦 → ( 𝑦 ∩ 𝑆 ) ≠ ∅ ) ) )
14		bastg	⊢ ( 𝐵 ∈ TopBases → 𝐵 ⊆ ( topGen ‘ 𝐵 ) )
15	3 14	syl	⊢ ( 𝜑 → 𝐵 ⊆ ( topGen ‘ 𝐵 ) )
16	15 1	sseqtrrd	⊢ ( 𝜑 → 𝐵 ⊆ 𝐽 )
17	16	sseld	⊢ ( 𝜑 → ( 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐽 ) )
18	17	imim1d	⊢ ( 𝜑 → ( ( 𝑦 ∈ 𝐽 → ( 𝑃 ∈ 𝑦 → ( 𝑦 ∩ 𝑆 ) ≠ ∅ ) ) → ( 𝑦 ∈ 𝐵 → ( 𝑃 ∈ 𝑦 → ( 𝑦 ∩ 𝑆 ) ≠ ∅ ) ) ) )
19	18	ralimdv2	⊢ ( 𝜑 → ( ∀ 𝑦 ∈ 𝐽 ( 𝑃 ∈ 𝑦 → ( 𝑦 ∩ 𝑆 ) ≠ ∅ ) → ∀ 𝑦 ∈ 𝐵 ( 𝑃 ∈ 𝑦 → ( 𝑦 ∩ 𝑆 ) ≠ ∅ ) ) )
20		eleq2w	⊢ ( 𝑦 = 𝑥 → ( 𝑃 ∈ 𝑦 ↔ 𝑃 ∈ 𝑥 ) )
21		ineq1	⊢ ( 𝑦 = 𝑥 → ( 𝑦 ∩ 𝑆 ) = ( 𝑥 ∩ 𝑆 ) )
22	21	neeq1d	⊢ ( 𝑦 = 𝑥 → ( ( 𝑦 ∩ 𝑆 ) ≠ ∅ ↔ ( 𝑥 ∩ 𝑆 ) ≠ ∅ ) )
23	20 22	imbi12d	⊢ ( 𝑦 = 𝑥 → ( ( 𝑃 ∈ 𝑦 → ( 𝑦 ∩ 𝑆 ) ≠ ∅ ) ↔ ( 𝑃 ∈ 𝑥 → ( 𝑥 ∩ 𝑆 ) ≠ ∅ ) ) )
24	23	cbvralvw	⊢ ( ∀ 𝑦 ∈ 𝐵 ( 𝑃 ∈ 𝑦 → ( 𝑦 ∩ 𝑆 ) ≠ ∅ ) ↔ ∀ 𝑥 ∈ 𝐵 ( 𝑃 ∈ 𝑥 → ( 𝑥 ∩ 𝑆 ) ≠ ∅ ) )
25	19 24	imbitrdi	⊢ ( 𝜑 → ( ∀ 𝑦 ∈ 𝐽 ( 𝑃 ∈ 𝑦 → ( 𝑦 ∩ 𝑆 ) ≠ ∅ ) → ∀ 𝑥 ∈ 𝐵 ( 𝑃 ∈ 𝑥 → ( 𝑥 ∩ 𝑆 ) ≠ ∅ ) ) )
26		simprl	⊢ ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑃 ∈ 𝑥 → ( 𝑥 ∩ 𝑆 ) ≠ ∅ ) ) ∧ ( 𝑦 ∈ 𝐽 ∧ 𝑃 ∈ 𝑦 ) ) → 𝑦 ∈ 𝐽 )
27	1	ad2antrr	⊢ ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑃 ∈ 𝑥 → ( 𝑥 ∩ 𝑆 ) ≠ ∅ ) ) ∧ ( 𝑦 ∈ 𝐽 ∧ 𝑃 ∈ 𝑦 ) ) → 𝐽 = ( topGen ‘ 𝐵 ) )
28	26 27	eleqtrd	⊢ ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑃 ∈ 𝑥 → ( 𝑥 ∩ 𝑆 ) ≠ ∅ ) ) ∧ ( 𝑦 ∈ 𝐽 ∧ 𝑃 ∈ 𝑦 ) ) → 𝑦 ∈ ( topGen ‘ 𝐵 ) )
29		simprr	⊢ ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑃 ∈ 𝑥 → ( 𝑥 ∩ 𝑆 ) ≠ ∅ ) ) ∧ ( 𝑦 ∈ 𝐽 ∧ 𝑃 ∈ 𝑦 ) ) → 𝑃 ∈ 𝑦 )
30		tg2	⊢ ( ( 𝑦 ∈ ( topGen ‘ 𝐵 ) ∧ 𝑃 ∈ 𝑦 ) → ∃ 𝑧 ∈ 𝐵 ( 𝑃 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑦 ) )
31	28 29 30	syl2anc	⊢ ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑃 ∈ 𝑥 → ( 𝑥 ∩ 𝑆 ) ≠ ∅ ) ) ∧ ( 𝑦 ∈ 𝐽 ∧ 𝑃 ∈ 𝑦 ) ) → ∃ 𝑧 ∈ 𝐵 ( 𝑃 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑦 ) )
32		eleq2w	⊢ ( 𝑥 = 𝑧 → ( 𝑃 ∈ 𝑥 ↔ 𝑃 ∈ 𝑧 ) )
33		ineq1	⊢ ( 𝑥 = 𝑧 → ( 𝑥 ∩ 𝑆 ) = ( 𝑧 ∩ 𝑆 ) )
34	33	neeq1d	⊢ ( 𝑥 = 𝑧 → ( ( 𝑥 ∩ 𝑆 ) ≠ ∅ ↔ ( 𝑧 ∩ 𝑆 ) ≠ ∅ ) )
35	32 34	imbi12d	⊢ ( 𝑥 = 𝑧 → ( ( 𝑃 ∈ 𝑥 → ( 𝑥 ∩ 𝑆 ) ≠ ∅ ) ↔ ( 𝑃 ∈ 𝑧 → ( 𝑧 ∩ 𝑆 ) ≠ ∅ ) ) )
36	35	rspccva	⊢ ( ( ∀ 𝑥 ∈ 𝐵 ( 𝑃 ∈ 𝑥 → ( 𝑥 ∩ 𝑆 ) ≠ ∅ ) ∧ 𝑧 ∈ 𝐵 ) → ( 𝑃 ∈ 𝑧 → ( 𝑧 ∩ 𝑆 ) ≠ ∅ ) )
37	36	imp	⊢ ( ( ( ∀ 𝑥 ∈ 𝐵 ( 𝑃 ∈ 𝑥 → ( 𝑥 ∩ 𝑆 ) ≠ ∅ ) ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑃 ∈ 𝑧 ) → ( 𝑧 ∩ 𝑆 ) ≠ ∅ )
38		ssdisj	⊢ ( ( 𝑧 ⊆ 𝑦 ∧ ( 𝑦 ∩ 𝑆 ) = ∅ ) → ( 𝑧 ∩ 𝑆 ) = ∅ )
39	38	ex	⊢ ( 𝑧 ⊆ 𝑦 → ( ( 𝑦 ∩ 𝑆 ) = ∅ → ( 𝑧 ∩ 𝑆 ) = ∅ ) )
40	39	necon3d	⊢ ( 𝑧 ⊆ 𝑦 → ( ( 𝑧 ∩ 𝑆 ) ≠ ∅ → ( 𝑦 ∩ 𝑆 ) ≠ ∅ ) )
41	37 40	syl5com	⊢ ( ( ( ∀ 𝑥 ∈ 𝐵 ( 𝑃 ∈ 𝑥 → ( 𝑥 ∩ 𝑆 ) ≠ ∅ ) ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑃 ∈ 𝑧 ) → ( 𝑧 ⊆ 𝑦 → ( 𝑦 ∩ 𝑆 ) ≠ ∅ ) )
42	41	exp31	⊢ ( ∀ 𝑥 ∈ 𝐵 ( 𝑃 ∈ 𝑥 → ( 𝑥 ∩ 𝑆 ) ≠ ∅ ) → ( 𝑧 ∈ 𝐵 → ( 𝑃 ∈ 𝑧 → ( 𝑧 ⊆ 𝑦 → ( 𝑦 ∩ 𝑆 ) ≠ ∅ ) ) ) )
43	42	imp4a	⊢ ( ∀ 𝑥 ∈ 𝐵 ( 𝑃 ∈ 𝑥 → ( 𝑥 ∩ 𝑆 ) ≠ ∅ ) → ( 𝑧 ∈ 𝐵 → ( ( 𝑃 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑦 ) → ( 𝑦 ∩ 𝑆 ) ≠ ∅ ) ) )
44	43	rexlimdv	⊢ ( ∀ 𝑥 ∈ 𝐵 ( 𝑃 ∈ 𝑥 → ( 𝑥 ∩ 𝑆 ) ≠ ∅ ) → ( ∃ 𝑧 ∈ 𝐵 ( 𝑃 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑦 ) → ( 𝑦 ∩ 𝑆 ) ≠ ∅ ) )
45	44	ad2antlr	⊢ ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑃 ∈ 𝑥 → ( 𝑥 ∩ 𝑆 ) ≠ ∅ ) ) ∧ ( 𝑦 ∈ 𝐽 ∧ 𝑃 ∈ 𝑦 ) ) → ( ∃ 𝑧 ∈ 𝐵 ( 𝑃 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑦 ) → ( 𝑦 ∩ 𝑆 ) ≠ ∅ ) )
46	31 45	mpd	⊢ ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑃 ∈ 𝑥 → ( 𝑥 ∩ 𝑆 ) ≠ ∅ ) ) ∧ ( 𝑦 ∈ 𝐽 ∧ 𝑃 ∈ 𝑦 ) ) → ( 𝑦 ∩ 𝑆 ) ≠ ∅ )
47	46	exp43	⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝐵 ( 𝑃 ∈ 𝑥 → ( 𝑥 ∩ 𝑆 ) ≠ ∅ ) → ( 𝑦 ∈ 𝐽 → ( 𝑃 ∈ 𝑦 → ( 𝑦 ∩ 𝑆 ) ≠ ∅ ) ) ) )
48	47	ralrimdv	⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝐵 ( 𝑃 ∈ 𝑥 → ( 𝑥 ∩ 𝑆 ) ≠ ∅ ) → ∀ 𝑦 ∈ 𝐽 ( 𝑃 ∈ 𝑦 → ( 𝑦 ∩ 𝑆 ) ≠ ∅ ) ) )
49	25 48	impbid	⊢ ( 𝜑 → ( ∀ 𝑦 ∈ 𝐽 ( 𝑃 ∈ 𝑦 → ( 𝑦 ∩ 𝑆 ) ≠ ∅ ) ↔ ∀ 𝑥 ∈ 𝐵 ( 𝑃 ∈ 𝑥 → ( 𝑥 ∩ 𝑆 ) ≠ ∅ ) ) )
50	13 49	bitrd	⊢ ( 𝜑 → ( 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ↔ ∀ 𝑥 ∈ 𝐵 ( 𝑃 ∈ 𝑥 → ( 𝑥 ∩ 𝑆 ) ≠ ∅ ) ) )

Metamath Proof Explorer

Theorem elcls3

Proof