tgcl - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > tgcl		Structured version Visualization version GIF version

Theorem tgcl 23195

Description: Show that a basis generates a topology. Remark in [Munkres] p. 79. (Contributed by NM, 17-Jul-2006.)

**Assertion**
Ref	Expression
tgcl	⊢ (𝐵 ∈ TopBases → (topGen‘𝐵) ∈ Top)

Proof of Theorem tgcl Dummy variables 𝑥 𝑦 𝑧 𝑢 𝑡 𝑣 𝑤 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		uniss 4875	. . . . . . . 8 ⊢ (𝑢 ⊆ (topGen‘𝐵) → ∪ 𝑢 ⊆ ∪ (topGen‘𝐵))
2	1	adantl 487	. . . . . . 7 ⊢ ((𝐵 ∈ TopBases ∧ 𝑢 ⊆ (topGen‘𝐵)) → ∪ 𝑢 ⊆ ∪ (topGen‘𝐵))
3		unitg 23193	. . . . . . . 8 ⊢ (𝐵 ∈ TopBases → ∪ (topGen‘𝐵) = ∪ 𝐵)
4	3	adantr 486	. . . . . . 7 ⊢ ((𝐵 ∈ TopBases ∧ 𝑢 ⊆ (topGen‘𝐵)) → ∪ (topGen‘𝐵) = ∪ 𝐵)
5	2, 4	sseqtrd 3967	. . . . . 6 ⊢ ((𝐵 ∈ TopBases ∧ 𝑢 ⊆ (topGen‘𝐵)) → ∪ 𝑢 ⊆ ∪ 𝐵)
6		eluni2 4871	. . . . . . . 8 ⊢ (𝑥 ∈ ∪ 𝑢 ↔ ∃𝑡 ∈ 𝑢 𝑥 ∈ 𝑡)
7		ssel2 3926	. . . . . . . . . . . 12 ⊢ ((𝑢 ⊆ (topGen‘𝐵) ∧ 𝑡 ∈ 𝑢) → 𝑡 ∈ (topGen‘𝐵))
8		eltg2b 23185	. . . . . . . . . . . . . . 15 ⊢ (𝐵 ∈ TopBases → (𝑡 ∈ (topGen‘𝐵) ↔ ∀𝑥 ∈ 𝑡 ∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑡)))
9		rsp 3250	. . . . . . . . . . . . . . 15 ⊢ (∀𝑥 ∈ 𝑡 ∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑡) → (𝑥 ∈ 𝑡 → ∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑡)))
10	8, 9	biimtrdi 256	. . . . . . . . . . . . . 14 ⊢ (𝐵 ∈ TopBases → (𝑡 ∈ (topGen‘𝐵) → (𝑥 ∈ 𝑡 → ∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑡))))
11	10	imp31 423	. . . . . . . . . . . . 13 ⊢ (((𝐵 ∈ TopBases ∧ 𝑡 ∈ (topGen‘𝐵)) ∧ 𝑥 ∈ 𝑡) → ∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑡))
12	11	an32s 665	. . . . . . . . . . . 12 ⊢ (((𝐵 ∈ TopBases ∧ 𝑥 ∈ 𝑡) ∧ 𝑡 ∈ (topGen‘𝐵)) → ∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑡))
13	7, 12	sylan2 605	. . . . . . . . . . 11 ⊢ (((𝐵 ∈ TopBases ∧ 𝑥 ∈ 𝑡) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑡 ∈ 𝑢)) → ∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑡))
14	13	an42s 674	. . . . . . . . . 10 ⊢ (((𝐵 ∈ TopBases ∧ 𝑢 ⊆ (topGen‘𝐵)) ∧ (𝑡 ∈ 𝑢 ∧ 𝑥 ∈ 𝑡)) → ∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑡))
15		elssuni 4899	. . . . . . . . . . . . . 14 ⊢ (𝑡 ∈ 𝑢 → 𝑡 ⊆ ∪ 𝑢)
16		sstr2 3938	. . . . . . . . . . . . . 14 ⊢ (𝑦 ⊆ 𝑡 → (𝑡 ⊆ ∪ 𝑢 → 𝑦 ⊆ ∪ 𝑢))
17	15, 16	syl5com 32	. . . . . . . . . . . . 13 ⊢ (𝑡 ∈ 𝑢 → (𝑦 ⊆ 𝑡 → 𝑦 ⊆ ∪ 𝑢))
18	17	anim2d 624	. . . . . . . . . . . 12 ⊢ (𝑡 ∈ 𝑢 → ((𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑡) → (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ ∪ 𝑢)))
19	18	reximdv 3177	. . . . . . . . . . 11 ⊢ (𝑡 ∈ 𝑢 → (∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑡) → ∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ ∪ 𝑢)))
20	19	ad2antrl 741	. . . . . . . . . 10 ⊢ (((𝐵 ∈ TopBases ∧ 𝑢 ⊆ (topGen‘𝐵)) ∧ (𝑡 ∈ 𝑢 ∧ 𝑥 ∈ 𝑡)) → (∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑡) → ∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ ∪ 𝑢)))
21	14, 20	mpd 16	. . . . . . . . 9 ⊢ (((𝐵 ∈ TopBases ∧ 𝑢 ⊆ (topGen‘𝐵)) ∧ (𝑡 ∈ 𝑢 ∧ 𝑥 ∈ 𝑡)) → ∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ ∪ 𝑢))
22	21	rexlimdvaa 3164	. . . . . . . 8 ⊢ ((𝐵 ∈ TopBases ∧ 𝑢 ⊆ (topGen‘𝐵)) → (∃𝑡 ∈ 𝑢 𝑥 ∈ 𝑡 → ∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ ∪ 𝑢)))
23	6, 22	biimtrid 245	. . . . . . 7 ⊢ ((𝐵 ∈ TopBases ∧ 𝑢 ⊆ (topGen‘𝐵)) → (𝑥 ∈ ∪ 𝑢 → ∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ ∪ 𝑢)))
24	23	ralrimiv 3153	. . . . . 6 ⊢ ((𝐵 ∈ TopBases ∧ 𝑢 ⊆ (topGen‘𝐵)) → ∀𝑥 ∈ ∪ 𝑢∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ ∪ 𝑢))
25	5, 24	jca 521	. . . . 5 ⊢ ((𝐵 ∈ TopBases ∧ 𝑢 ⊆ (topGen‘𝐵)) → (∪ 𝑢 ⊆ ∪ 𝐵 ∧ ∀𝑥 ∈ ∪ 𝑢∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ ∪ 𝑢)))
26	25	ex 418	. . . 4 ⊢ (𝐵 ∈ TopBases → (𝑢 ⊆ (topGen‘𝐵) → (∪ 𝑢 ⊆ ∪ 𝐵 ∧ ∀𝑥 ∈ ∪ 𝑢∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ ∪ 𝑢))))
27		eltg2 23184	. . . 4 ⊢ (𝐵 ∈ TopBases → (∪ 𝑢 ∈ (topGen‘𝐵) ↔ (∪ 𝑢 ⊆ ∪ 𝐵 ∧ ∀𝑥 ∈ ∪ 𝑢∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ ∪ 𝑢))))
28	26, 27	sylibrd 262	. . 3 ⊢ (𝐵 ∈ TopBases → (𝑢 ⊆ (topGen‘𝐵) → ∪ 𝑢 ∈ (topGen‘𝐵)))
29	28	alrimiv 1960	. 2 ⊢ (𝐵 ∈ TopBases → ∀𝑢(𝑢 ⊆ (topGen‘𝐵) → ∪ 𝑢 ∈ (topGen‘𝐵)))
30		inss1 4182	. . . . . . . 8 ⊢ (𝑢 ∩ 𝑣) ⊆ 𝑢
31		tg1 23190	. . . . . . . 8 ⊢ (𝑢 ∈ (topGen‘𝐵) → 𝑢 ⊆ ∪ 𝐵)
32	30, 31	sstrid 3942	. . . . . . 7 ⊢ (𝑢 ∈ (topGen‘𝐵) → (𝑢 ∩ 𝑣) ⊆ ∪ 𝐵)
33	32	ad2antrl 741	. . . . . 6 ⊢ ((𝐵 ∈ TopBases ∧ (𝑢 ∈ (topGen‘𝐵) ∧ 𝑣 ∈ (topGen‘𝐵))) → (𝑢 ∩ 𝑣) ⊆ ∪ 𝐵)
34		eltg2 23184	. . . . . . . . . . . . 13 ⊢ (𝐵 ∈ TopBases → (𝑢 ∈ (topGen‘𝐵) ↔ (𝑢 ⊆ ∪ 𝐵 ∧ ∀𝑥 ∈ 𝑢 ∃𝑧 ∈ 𝐵 (𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑢))))
35	34	simplbda 505	. . . . . . . . . . . 12 ⊢ ((𝐵 ∈ TopBases ∧ 𝑢 ∈ (topGen‘𝐵)) → ∀𝑥 ∈ 𝑢 ∃𝑧 ∈ 𝐵 (𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑢))
36		rsp 3250	. . . . . . . . . . . 12 ⊢ (∀𝑥 ∈ 𝑢 ∃𝑧 ∈ 𝐵 (𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑢) → (𝑥 ∈ 𝑢 → ∃𝑧 ∈ 𝐵 (𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑢)))
37	35, 36	syl 18	. . . . . . . . . . 11 ⊢ ((𝐵 ∈ TopBases ∧ 𝑢 ∈ (topGen‘𝐵)) → (𝑥 ∈ 𝑢 → ∃𝑧 ∈ 𝐵 (𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑢)))
38		eltg2 23184	. . . . . . . . . . . . 13 ⊢ (𝐵 ∈ TopBases → (𝑣 ∈ (topGen‘𝐵) ↔ (𝑣 ⊆ ∪ 𝐵 ∧ ∀𝑥 ∈ 𝑣 ∃𝑤 ∈ 𝐵 (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑣))))
39	38	simplbda 505	. . . . . . . . . . . 12 ⊢ ((𝐵 ∈ TopBases ∧ 𝑣 ∈ (topGen‘𝐵)) → ∀𝑥 ∈ 𝑣 ∃𝑤 ∈ 𝐵 (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑣))
40		rsp 3250	. . . . . . . . . . . 12 ⊢ (∀𝑥 ∈ 𝑣 ∃𝑤 ∈ 𝐵 (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑣) → (𝑥 ∈ 𝑣 → ∃𝑤 ∈ 𝐵 (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑣)))
41	39, 40	syl 18	. . . . . . . . . . 11 ⊢ ((𝐵 ∈ TopBases ∧ 𝑣 ∈ (topGen‘𝐵)) → (𝑥 ∈ 𝑣 → ∃𝑤 ∈ 𝐵 (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑣)))
42	37, 41	im2anan9 632	. . . . . . . . . 10 ⊢ (((𝐵 ∈ TopBases ∧ 𝑢 ∈ (topGen‘𝐵)) ∧ (𝐵 ∈ TopBases ∧ 𝑣 ∈ (topGen‘𝐵))) → ((𝑥 ∈ 𝑢 ∧ 𝑥 ∈ 𝑣) → (∃𝑧 ∈ 𝐵 (𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑢) ∧ ∃𝑤 ∈ 𝐵 (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑣))))
43		elin 3915	. . . . . . . . . 10 ⊢ (𝑥 ∈ (𝑢 ∩ 𝑣) ↔ (𝑥 ∈ 𝑢 ∧ 𝑥 ∈ 𝑣))
44		reeanv 3234	. . . . . . . . . 10 ⊢ (∃𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐵 ((𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑢) ∧ (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑣)) ↔ (∃𝑧 ∈ 𝐵 (𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑢) ∧ ∃𝑤 ∈ 𝐵 (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑣)))
45	42, 43, 44	3imtr4g 299	. . . . . . . . 9 ⊢ (((𝐵 ∈ TopBases ∧ 𝑢 ∈ (topGen‘𝐵)) ∧ (𝐵 ∈ TopBases ∧ 𝑣 ∈ (topGen‘𝐵))) → (𝑥 ∈ (𝑢 ∩ 𝑣) → ∃𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐵 ((𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑢) ∧ (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑣))))
46	45	anandis 691	. . . . . . . 8 ⊢ ((𝐵 ∈ TopBases ∧ (𝑢 ∈ (topGen‘𝐵) ∧ 𝑣 ∈ (topGen‘𝐵))) → (𝑥 ∈ (𝑢 ∩ 𝑣) → ∃𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐵 ((𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑢) ∧ (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑣))))
47		elin 3915	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ (𝑧 ∩ 𝑤) ↔ (𝑥 ∈ 𝑧 ∧ 𝑥 ∈ 𝑤))
48	47	biimpri 231	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ 𝑧 ∧ 𝑥 ∈ 𝑤) → 𝑥 ∈ (𝑧 ∩ 𝑤))
49		ss2in 4190	. . . . . . . . . . . . . . . 16 ⊢ ((𝑧 ⊆ 𝑢 ∧ 𝑤 ⊆ 𝑣) → (𝑧 ∩ 𝑤) ⊆ (𝑢 ∩ 𝑣))
50	48, 49	anim12i 625	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ 𝑧 ∧ 𝑥 ∈ 𝑤) ∧ (𝑧 ⊆ 𝑢 ∧ 𝑤 ⊆ 𝑣)) → (𝑥 ∈ (𝑧 ∩ 𝑤) ∧ (𝑧 ∩ 𝑤) ⊆ (𝑢 ∩ 𝑣)))
51	50	an4s 673	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑢) ∧ (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑣)) → (𝑥 ∈ (𝑧 ∩ 𝑤) ∧ (𝑧 ∩ 𝑤) ⊆ (𝑢 ∩ 𝑣)))
52		basis2 23177	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐵 ∈ TopBases ∧ 𝑧 ∈ 𝐵) ∧ (𝑤 ∈ 𝐵 ∧ 𝑥 ∈ (𝑧 ∩ 𝑤))) → ∃𝑡 ∈ 𝐵 (𝑥 ∈ 𝑡 ∧ 𝑡 ⊆ (𝑧 ∩ 𝑤)))
53	52	adantllr 732	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐵 ∈ TopBases ∧ 𝑥 ∈ (𝑢 ∩ 𝑣)) ∧ 𝑧 ∈ 𝐵) ∧ (𝑤 ∈ 𝐵 ∧ 𝑥 ∈ (𝑧 ∩ 𝑤))) → ∃𝑡 ∈ 𝐵 (𝑥 ∈ 𝑡 ∧ 𝑡 ⊆ (𝑧 ∩ 𝑤)))
54	53	adantrrr 738	. . . . . . . . . . . . . . 15 ⊢ ((((𝐵 ∈ TopBases ∧ 𝑥 ∈ (𝑢 ∩ 𝑣)) ∧ 𝑧 ∈ 𝐵) ∧ (𝑤 ∈ 𝐵 ∧ (𝑥 ∈ (𝑧 ∩ 𝑤) ∧ (𝑧 ∩ 𝑤) ⊆ (𝑢 ∩ 𝑣)))) → ∃𝑡 ∈ 𝐵 (𝑥 ∈ 𝑡 ∧ 𝑡 ⊆ (𝑧 ∩ 𝑤)))
55		sstr2 3938	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑡 ⊆ (𝑧 ∩ 𝑤) → ((𝑧 ∩ 𝑤) ⊆ (𝑢 ∩ 𝑣) → 𝑡 ⊆ (𝑢 ∩ 𝑣)))
56	55	com12 33	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑧 ∩ 𝑤) ⊆ (𝑢 ∩ 𝑣) → (𝑡 ⊆ (𝑧 ∩ 𝑤) → 𝑡 ⊆ (𝑢 ∩ 𝑣)))
57	56	anim2d 624	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑧 ∩ 𝑤) ⊆ (𝑢 ∩ 𝑣) → ((𝑥 ∈ 𝑡 ∧ 𝑡 ⊆ (𝑧 ∩ 𝑤)) → (𝑥 ∈ 𝑡 ∧ 𝑡 ⊆ (𝑢 ∩ 𝑣))))
58	57	reximdv 3177	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑧 ∩ 𝑤) ⊆ (𝑢 ∩ 𝑣) → (∃𝑡 ∈ 𝐵 (𝑥 ∈ 𝑡 ∧ 𝑡 ⊆ (𝑧 ∩ 𝑤)) → ∃𝑡 ∈ 𝐵 (𝑥 ∈ 𝑡 ∧ 𝑡 ⊆ (𝑢 ∩ 𝑣))))
59	58	adantl 487	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ (𝑧 ∩ 𝑤) ∧ (𝑧 ∩ 𝑤) ⊆ (𝑢 ∩ 𝑣)) → (∃𝑡 ∈ 𝐵 (𝑥 ∈ 𝑡 ∧ 𝑡 ⊆ (𝑧 ∩ 𝑤)) → ∃𝑡 ∈ 𝐵 (𝑥 ∈ 𝑡 ∧ 𝑡 ⊆ (𝑢 ∩ 𝑣))))
60	59	ad2antll 742	. . . . . . . . . . . . . . 15 ⊢ ((((𝐵 ∈ TopBases ∧ 𝑥 ∈ (𝑢 ∩ 𝑣)) ∧ 𝑧 ∈ 𝐵) ∧ (𝑤 ∈ 𝐵 ∧ (𝑥 ∈ (𝑧 ∩ 𝑤) ∧ (𝑧 ∩ 𝑤) ⊆ (𝑢 ∩ 𝑣)))) → (∃𝑡 ∈ 𝐵 (𝑥 ∈ 𝑡 ∧ 𝑡 ⊆ (𝑧 ∩ 𝑤)) → ∃𝑡 ∈ 𝐵 (𝑥 ∈ 𝑡 ∧ 𝑡 ⊆ (𝑢 ∩ 𝑣))))
61	54, 60	mpd 16	. . . . . . . . . . . . . 14 ⊢ ((((𝐵 ∈ TopBases ∧ 𝑥 ∈ (𝑢 ∩ 𝑣)) ∧ 𝑧 ∈ 𝐵) ∧ (𝑤 ∈ 𝐵 ∧ (𝑥 ∈ (𝑧 ∩ 𝑤) ∧ (𝑧 ∩ 𝑤) ⊆ (𝑢 ∩ 𝑣)))) → ∃𝑡 ∈ 𝐵 (𝑥 ∈ 𝑡 ∧ 𝑡 ⊆ (𝑢 ∩ 𝑣)))
62	51, 61	sylanr2 696	. . . . . . . . . . . . 13 ⊢ ((((𝐵 ∈ TopBases ∧ 𝑥 ∈ (𝑢 ∩ 𝑣)) ∧ 𝑧 ∈ 𝐵) ∧ (𝑤 ∈ 𝐵 ∧ ((𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑢) ∧ (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑣)))) → ∃𝑡 ∈ 𝐵 (𝑥 ∈ 𝑡 ∧ 𝑡 ⊆ (𝑢 ∩ 𝑣)))
63	62	rexlimdvaa 3164	. . . . . . . . . . . 12 ⊢ (((𝐵 ∈ TopBases ∧ 𝑥 ∈ (𝑢 ∩ 𝑣)) ∧ 𝑧 ∈ 𝐵) → (∃𝑤 ∈ 𝐵 ((𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑢) ∧ (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑣)) → ∃𝑡 ∈ 𝐵 (𝑥 ∈ 𝑡 ∧ 𝑡 ⊆ (𝑢 ∩ 𝑣))))
64	63	rexlimdva 3163	. . . . . . . . . . 11 ⊢ ((𝐵 ∈ TopBases ∧ 𝑥 ∈ (𝑢 ∩ 𝑣)) → (∃𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐵 ((𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑢) ∧ (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑣)) → ∃𝑡 ∈ 𝐵 (𝑥 ∈ 𝑡 ∧ 𝑡 ⊆ (𝑢 ∩ 𝑣))))
65	64	ex 418	. . . . . . . . . 10 ⊢ (𝐵 ∈ TopBases → (𝑥 ∈ (𝑢 ∩ 𝑣) → (∃𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐵 ((𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑢) ∧ (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑣)) → ∃𝑡 ∈ 𝐵 (𝑥 ∈ 𝑡 ∧ 𝑡 ⊆ (𝑢 ∩ 𝑣)))))
66	65	a2d 30	. . . . . . . . 9 ⊢ (𝐵 ∈ TopBases → ((𝑥 ∈ (𝑢 ∩ 𝑣) → ∃𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐵 ((𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑢) ∧ (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑣))) → (𝑥 ∈ (𝑢 ∩ 𝑣) → ∃𝑡 ∈ 𝐵 (𝑥 ∈ 𝑡 ∧ 𝑡 ⊆ (𝑢 ∩ 𝑣)))))
67	66	imp 412	. . . . . . . 8 ⊢ ((𝐵 ∈ TopBases ∧ (𝑥 ∈ (𝑢 ∩ 𝑣) → ∃𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐵 ((𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑢) ∧ (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑣)))) → (𝑥 ∈ (𝑢 ∩ 𝑣) → ∃𝑡 ∈ 𝐵 (𝑥 ∈ 𝑡 ∧ 𝑡 ⊆ (𝑢 ∩ 𝑣))))
68	46, 67	syldan 603	. . . . . . 7 ⊢ ((𝐵 ∈ TopBases ∧ (𝑢 ∈ (topGen‘𝐵) ∧ 𝑣 ∈ (topGen‘𝐵))) → (𝑥 ∈ (𝑢 ∩ 𝑣) → ∃𝑡 ∈ 𝐵 (𝑥 ∈ 𝑡 ∧ 𝑡 ⊆ (𝑢 ∩ 𝑣))))
69	68	ralrimiv 3153	. . . . . 6 ⊢ ((𝐵 ∈ TopBases ∧ (𝑢 ∈ (topGen‘𝐵) ∧ 𝑣 ∈ (topGen‘𝐵))) → ∀𝑥 ∈ (𝑢 ∩ 𝑣)∃𝑡 ∈ 𝐵 (𝑥 ∈ 𝑡 ∧ 𝑡 ⊆ (𝑢 ∩ 𝑣)))
70	33, 69	jca 521	. . . . 5 ⊢ ((𝐵 ∈ TopBases ∧ (𝑢 ∈ (topGen‘𝐵) ∧ 𝑣 ∈ (topGen‘𝐵))) → ((𝑢 ∩ 𝑣) ⊆ ∪ 𝐵 ∧ ∀𝑥 ∈ (𝑢 ∩ 𝑣)∃𝑡 ∈ 𝐵 (𝑥 ∈ 𝑡 ∧ 𝑡 ⊆ (𝑢 ∩ 𝑣))))
71	70	ex 418	. . . 4 ⊢ (𝐵 ∈ TopBases → ((𝑢 ∈ (topGen‘𝐵) ∧ 𝑣 ∈ (topGen‘𝐵)) → ((𝑢 ∩ 𝑣) ⊆ ∪ 𝐵 ∧ ∀𝑥 ∈ (𝑢 ∩ 𝑣)∃𝑡 ∈ 𝐵 (𝑥 ∈ 𝑡 ∧ 𝑡 ⊆ (𝑢 ∩ 𝑣)))))
72		eltg2 23184	. . . 4 ⊢ (𝐵 ∈ TopBases → ((𝑢 ∩ 𝑣) ∈ (topGen‘𝐵) ↔ ((𝑢 ∩ 𝑣) ⊆ ∪ 𝐵 ∧ ∀𝑥 ∈ (𝑢 ∩ 𝑣)∃𝑡 ∈ 𝐵 (𝑥 ∈ 𝑡 ∧ 𝑡 ⊆ (𝑢 ∩ 𝑣)))))
73	71, 72	sylibrd 262	. . 3 ⊢ (𝐵 ∈ TopBases → ((𝑢 ∈ (topGen‘𝐵) ∧ 𝑣 ∈ (topGen‘𝐵)) → (𝑢 ∩ 𝑣) ∈ (topGen‘𝐵)))
74	73	ralrimivv 3203	. 2 ⊢ (𝐵 ∈ TopBases → ∀𝑢 ∈ (topGen‘𝐵)∀𝑣 ∈ (topGen‘𝐵)(𝑢 ∩ 𝑣) ∈ (topGen‘𝐵))
75		fvex 6892	. . 3 ⊢ (topGen‘𝐵) ∈ V
76		istopg 23121	. . 3 ⊢ ((topGen‘𝐵) ∈ V → ((topGen‘𝐵) ∈ Top ↔ (∀𝑢(𝑢 ⊆ (topGen‘𝐵) → ∪ 𝑢 ∈ (topGen‘𝐵)) ∧ ∀𝑢 ∈ (topGen‘𝐵)∀𝑣 ∈ (topGen‘𝐵)(𝑢 ∩ 𝑣) ∈ (topGen‘𝐵))))
77	75, 76	ax-mp 5	. 2 ⊢ ((topGen‘𝐵) ∈ Top ↔ (∀𝑢(𝑢 ⊆ (topGen‘𝐵) → ∪ 𝑢 ∈ (topGen‘𝐵)) ∧ ∀𝑢 ∈ (topGen‘𝐵)∀𝑣 ∈ (topGen‘𝐵)(𝑢 ∩ 𝑣) ∈ (topGen‘𝐵)))
78	29, 74, 77	sylanbrc 595	1 ⊢ (𝐵 ∈ TopBases → (topGen‘𝐵) ∈ Top)

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 ∀wal 1568 = wceq 1570 ∈ wcel 2145 ∀wral 3076 ∃wrex 3086 Vcvv 3450 ∩ cin 3898 ⊆ wss 3899 ∪ cuni 4867 ‘cfv 6533 topGenctg 17523 Topctop 23119 TopBasesctb 23171

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2213 ax-ext 2732 ax-sep 5251 ax-nul 5263 ax-pow 5330 ax-pr 5398 ax-un 7737

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-ral 3077 df-rex 3087 df-rab 3413 df-v 3452 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-nul 4280 df-if 4483 df-pw 4559 df-sn 4585 df-pr 4587 df-op 4591 df-uni 4868 df-br 5104 df-opab 5168 df-mpt 5187 df-id 5550 df-xp 5661 df-rel 5662 df-cnv 5663 df-co 5664 df-dm 5665 df-iota 6489 df-fun 6535 df-fv 6541 df-topgen 17529 df-top 23120 df-bases 23172

This theorem is used by: tgclb 23196 tgtopon 23197 bastop 23207 elcls3 23309 resttop 23386 leordtval2 23438 tgcmp 23627 2ndctop 23673 2ndcsb 23675 2ndcsep 23686 txtop 23796 pttop 23809 xkotop 23815 alexsubALT 24278 retop 24988 onsuctop 37053 kelac2lem 43906

W3C validator