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 22119

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 4847	. . . . . . . 8 ⊢ (𝑢 ⊆ (topGen‘𝐵) → ∪ 𝑢 ⊆ ∪ (topGen‘𝐵))
2	1	adantl 482	. . . . . . 7 ⊢ ((𝐵 ∈ TopBases ∧ 𝑢 ⊆ (topGen‘𝐵)) → ∪ 𝑢 ⊆ ∪ (topGen‘𝐵))
3		unitg 22117	. . . . . . . 8 ⊢ (𝐵 ∈ TopBases → ∪ (topGen‘𝐵) = ∪ 𝐵)
4	3	adantr 481	. . . . . . 7 ⊢ ((𝐵 ∈ TopBases ∧ 𝑢 ⊆ (topGen‘𝐵)) → ∪ (topGen‘𝐵) = ∪ 𝐵)
5	2, 4	sseqtrd 3961	. . . . . 6 ⊢ ((𝐵 ∈ TopBases ∧ 𝑢 ⊆ (topGen‘𝐵)) → ∪ 𝑢 ⊆ ∪ 𝐵)
6		eluni2 4843	. . . . . . . 8 ⊢ (𝑥 ∈ ∪ 𝑢 ↔ ∃𝑡 ∈ 𝑢 𝑥 ∈ 𝑡)
7		ssel2 3916	. . . . . . . . . . . 12 ⊢ ((𝑢 ⊆ (topGen‘𝐵) ∧ 𝑡 ∈ 𝑢) → 𝑡 ∈ (topGen‘𝐵))
8		eltg2b 22109	. . . . . . . . . . . . . . 15 ⊢ (𝐵 ∈ TopBases → (𝑡 ∈ (topGen‘𝐵) ↔ ∀𝑥 ∈ 𝑡 ∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑡)))
9		rsp 3131	. . . . . . . . . . . . . . 15 ⊢ (∀𝑥 ∈ 𝑡 ∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑡) → (𝑥 ∈ 𝑡 → ∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑡)))
10	8, 9	syl6bi 252	. . . . . . . . . . . . . 14 ⊢ (𝐵 ∈ TopBases → (𝑡 ∈ (topGen‘𝐵) → (𝑥 ∈ 𝑡 → ∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑡))))
11	10	imp31 418	. . . . . . . . . . . . 13 ⊢ (((𝐵 ∈ TopBases ∧ 𝑡 ∈ (topGen‘𝐵)) ∧ 𝑥 ∈ 𝑡) → ∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑡))
12	11	an32s 649	. . . . . . . . . . . 12 ⊢ (((𝐵 ∈ TopBases ∧ 𝑥 ∈ 𝑡) ∧ 𝑡 ∈ (topGen‘𝐵)) → ∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑡))
13	7, 12	sylan2 593	. . . . . . . . . . 11 ⊢ (((𝐵 ∈ TopBases ∧ 𝑥 ∈ 𝑡) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑡 ∈ 𝑢)) → ∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑡))
14	13	an42s 658	. . . . . . . . . 10 ⊢ (((𝐵 ∈ TopBases ∧ 𝑢 ⊆ (topGen‘𝐵)) ∧ (𝑡 ∈ 𝑢 ∧ 𝑥 ∈ 𝑡)) → ∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑡))
15		elssuni 4871	. . . . . . . . . . . . . 14 ⊢ (𝑡 ∈ 𝑢 → 𝑡 ⊆ ∪ 𝑢)
16		sstr2 3928	. . . . . . . . . . . . . 14 ⊢ (𝑦 ⊆ 𝑡 → (𝑡 ⊆ ∪ 𝑢 → 𝑦 ⊆ ∪ 𝑢))
17	15, 16	syl5com 31	. . . . . . . . . . . . 13 ⊢ (𝑡 ∈ 𝑢 → (𝑦 ⊆ 𝑡 → 𝑦 ⊆ ∪ 𝑢))
18	17	anim2d 612	. . . . . . . . . . . 12 ⊢ (𝑡 ∈ 𝑢 → ((𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑡) → (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ ∪ 𝑢)))
19	18	reximdv 3202	. . . . . . . . . . 11 ⊢ (𝑡 ∈ 𝑢 → (∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑡) → ∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ ∪ 𝑢)))
20	19	ad2antrl 725	. . . . . . . . . 10 ⊢ (((𝐵 ∈ TopBases ∧ 𝑢 ⊆ (topGen‘𝐵)) ∧ (𝑡 ∈ 𝑢 ∧ 𝑥 ∈ 𝑡)) → (∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑡) → ∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ ∪ 𝑢)))
21	14, 20	mpd 15	. . . . . . . . 9 ⊢ (((𝐵 ∈ TopBases ∧ 𝑢 ⊆ (topGen‘𝐵)) ∧ (𝑡 ∈ 𝑢 ∧ 𝑥 ∈ 𝑡)) → ∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ ∪ 𝑢))
22	21	rexlimdvaa 3214	. . . . . . . 8 ⊢ ((𝐵 ∈ TopBases ∧ 𝑢 ⊆ (topGen‘𝐵)) → (∃𝑡 ∈ 𝑢 𝑥 ∈ 𝑡 → ∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ ∪ 𝑢)))
23	6, 22	syl5bi 241	. . . . . . 7 ⊢ ((𝐵 ∈ TopBases ∧ 𝑢 ⊆ (topGen‘𝐵)) → (𝑥 ∈ ∪ 𝑢 → ∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ ∪ 𝑢)))
24	23	ralrimiv 3102	. . . . . 6 ⊢ ((𝐵 ∈ TopBases ∧ 𝑢 ⊆ (topGen‘𝐵)) → ∀𝑥 ∈ ∪ 𝑢∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ ∪ 𝑢))
25	5, 24	jca 512	. . . . 5 ⊢ ((𝐵 ∈ TopBases ∧ 𝑢 ⊆ (topGen‘𝐵)) → (∪ 𝑢 ⊆ ∪ 𝐵 ∧ ∀𝑥 ∈ ∪ 𝑢∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ ∪ 𝑢)))
26	25	ex 413	. . . 4 ⊢ (𝐵 ∈ TopBases → (𝑢 ⊆ (topGen‘𝐵) → (∪ 𝑢 ⊆ ∪ 𝐵 ∧ ∀𝑥 ∈ ∪ 𝑢∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ ∪ 𝑢))))
27		eltg2 22108	. . . 4 ⊢ (𝐵 ∈ TopBases → (∪ 𝑢 ∈ (topGen‘𝐵) ↔ (∪ 𝑢 ⊆ ∪ 𝐵 ∧ ∀𝑥 ∈ ∪ 𝑢∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ ∪ 𝑢))))
28	26, 27	sylibrd 258	. . 3 ⊢ (𝐵 ∈ TopBases → (𝑢 ⊆ (topGen‘𝐵) → ∪ 𝑢 ∈ (topGen‘𝐵)))
29	28	alrimiv 1930	. 2 ⊢ (𝐵 ∈ TopBases → ∀𝑢(𝑢 ⊆ (topGen‘𝐵) → ∪ 𝑢 ∈ (topGen‘𝐵)))
30		inss1 4162	. . . . . . . 8 ⊢ (𝑢 ∩ 𝑣) ⊆ 𝑢
31		tg1 22114	. . . . . . . 8 ⊢ (𝑢 ∈ (topGen‘𝐵) → 𝑢 ⊆ ∪ 𝐵)
32	30, 31	sstrid 3932	. . . . . . 7 ⊢ (𝑢 ∈ (topGen‘𝐵) → (𝑢 ∩ 𝑣) ⊆ ∪ 𝐵)
33	32	ad2antrl 725	. . . . . 6 ⊢ ((𝐵 ∈ TopBases ∧ (𝑢 ∈ (topGen‘𝐵) ∧ 𝑣 ∈ (topGen‘𝐵))) → (𝑢 ∩ 𝑣) ⊆ ∪ 𝐵)
34		eltg2 22108	. . . . . . . . . . . . 13 ⊢ (𝐵 ∈ TopBases → (𝑢 ∈ (topGen‘𝐵) ↔ (𝑢 ⊆ ∪ 𝐵 ∧ ∀𝑥 ∈ 𝑢 ∃𝑧 ∈ 𝐵 (𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑢))))
35	34	simplbda 500	. . . . . . . . . . . 12 ⊢ ((𝐵 ∈ TopBases ∧ 𝑢 ∈ (topGen‘𝐵)) → ∀𝑥 ∈ 𝑢 ∃𝑧 ∈ 𝐵 (𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑢))
36		rsp 3131	. . . . . . . . . . . 12 ⊢ (∀𝑥 ∈ 𝑢 ∃𝑧 ∈ 𝐵 (𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑢) → (𝑥 ∈ 𝑢 → ∃𝑧 ∈ 𝐵 (𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑢)))
37	35, 36	syl 17	. . . . . . . . . . 11 ⊢ ((𝐵 ∈ TopBases ∧ 𝑢 ∈ (topGen‘𝐵)) → (𝑥 ∈ 𝑢 → ∃𝑧 ∈ 𝐵 (𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑢)))
38		eltg2 22108	. . . . . . . . . . . . 13 ⊢ (𝐵 ∈ TopBases → (𝑣 ∈ (topGen‘𝐵) ↔ (𝑣 ⊆ ∪ 𝐵 ∧ ∀𝑥 ∈ 𝑣 ∃𝑤 ∈ 𝐵 (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑣))))
39	38	simplbda 500	. . . . . . . . . . . 12 ⊢ ((𝐵 ∈ TopBases ∧ 𝑣 ∈ (topGen‘𝐵)) → ∀𝑥 ∈ 𝑣 ∃𝑤 ∈ 𝐵 (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑣))
40		rsp 3131	. . . . . . . . . . . 12 ⊢ (∀𝑥 ∈ 𝑣 ∃𝑤 ∈ 𝐵 (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑣) → (𝑥 ∈ 𝑣 → ∃𝑤 ∈ 𝐵 (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑣)))
41	39, 40	syl 17	. . . . . . . . . . 11 ⊢ ((𝐵 ∈ TopBases ∧ 𝑣 ∈ (topGen‘𝐵)) → (𝑥 ∈ 𝑣 → ∃𝑤 ∈ 𝐵 (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑣)))
42	37, 41	im2anan9 620	. . . . . . . . . 10 ⊢ (((𝐵 ∈ TopBases ∧ 𝑢 ∈ (topGen‘𝐵)) ∧ (𝐵 ∈ TopBases ∧ 𝑣 ∈ (topGen‘𝐵))) → ((𝑥 ∈ 𝑢 ∧ 𝑥 ∈ 𝑣) → (∃𝑧 ∈ 𝐵 (𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑢) ∧ ∃𝑤 ∈ 𝐵 (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑣))))
43		elin 3903	. . . . . . . . . 10 ⊢ (𝑥 ∈ (𝑢 ∩ 𝑣) ↔ (𝑥 ∈ 𝑢 ∧ 𝑥 ∈ 𝑣))
44		reeanv 3294	. . . . . . . . . 10 ⊢ (∃𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐵 ((𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑢) ∧ (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑣)) ↔ (∃𝑧 ∈ 𝐵 (𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑢) ∧ ∃𝑤 ∈ 𝐵 (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑣)))
45	42, 43, 44	3imtr4g 296	. . . . . . . . 9 ⊢ (((𝐵 ∈ TopBases ∧ 𝑢 ∈ (topGen‘𝐵)) ∧ (𝐵 ∈ TopBases ∧ 𝑣 ∈ (topGen‘𝐵))) → (𝑥 ∈ (𝑢 ∩ 𝑣) → ∃𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐵 ((𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑢) ∧ (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑣))))
46	45	anandis 675	. . . . . . . 8 ⊢ ((𝐵 ∈ TopBases ∧ (𝑢 ∈ (topGen‘𝐵) ∧ 𝑣 ∈ (topGen‘𝐵))) → (𝑥 ∈ (𝑢 ∩ 𝑣) → ∃𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐵 ((𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑢) ∧ (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑣))))
47		elin 3903	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ (𝑧 ∩ 𝑤) ↔ (𝑥 ∈ 𝑧 ∧ 𝑥 ∈ 𝑤))
48	47	biimpri 227	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ 𝑧 ∧ 𝑥 ∈ 𝑤) → 𝑥 ∈ (𝑧 ∩ 𝑤))
49		ss2in 4170	. . . . . . . . . . . . . . . 16 ⊢ ((𝑧 ⊆ 𝑢 ∧ 𝑤 ⊆ 𝑣) → (𝑧 ∩ 𝑤) ⊆ (𝑢 ∩ 𝑣))
50	48, 49	anim12i 613	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ 𝑧 ∧ 𝑥 ∈ 𝑤) ∧ (𝑧 ⊆ 𝑢 ∧ 𝑤 ⊆ 𝑣)) → (𝑥 ∈ (𝑧 ∩ 𝑤) ∧ (𝑧 ∩ 𝑤) ⊆ (𝑢 ∩ 𝑣)))
51	50	an4s 657	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑢) ∧ (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑣)) → (𝑥 ∈ (𝑧 ∩ 𝑤) ∧ (𝑧 ∩ 𝑤) ⊆ (𝑢 ∩ 𝑣)))
52		basis2 22101	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐵 ∈ TopBases ∧ 𝑧 ∈ 𝐵) ∧ (𝑤 ∈ 𝐵 ∧ 𝑥 ∈ (𝑧 ∩ 𝑤))) → ∃𝑡 ∈ 𝐵 (𝑥 ∈ 𝑡 ∧ 𝑡 ⊆ (𝑧 ∩ 𝑤)))
53	52	adantllr 716	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐵 ∈ TopBases ∧ 𝑥 ∈ (𝑢 ∩ 𝑣)) ∧ 𝑧 ∈ 𝐵) ∧ (𝑤 ∈ 𝐵 ∧ 𝑥 ∈ (𝑧 ∩ 𝑤))) → ∃𝑡 ∈ 𝐵 (𝑥 ∈ 𝑡 ∧ 𝑡 ⊆ (𝑧 ∩ 𝑤)))
54	53	adantrrr 722	. . . . . . . . . . . . . . 15 ⊢ ((((𝐵 ∈ TopBases ∧ 𝑥 ∈ (𝑢 ∩ 𝑣)) ∧ 𝑧 ∈ 𝐵) ∧ (𝑤 ∈ 𝐵 ∧ (𝑥 ∈ (𝑧 ∩ 𝑤) ∧ (𝑧 ∩ 𝑤) ⊆ (𝑢 ∩ 𝑣)))) → ∃𝑡 ∈ 𝐵 (𝑥 ∈ 𝑡 ∧ 𝑡 ⊆ (𝑧 ∩ 𝑤)))
55		sstr2 3928	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑡 ⊆ (𝑧 ∩ 𝑤) → ((𝑧 ∩ 𝑤) ⊆ (𝑢 ∩ 𝑣) → 𝑡 ⊆ (𝑢 ∩ 𝑣)))
56	55	com12 32	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑧 ∩ 𝑤) ⊆ (𝑢 ∩ 𝑣) → (𝑡 ⊆ (𝑧 ∩ 𝑤) → 𝑡 ⊆ (𝑢 ∩ 𝑣)))
57	56	anim2d 612	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑧 ∩ 𝑤) ⊆ (𝑢 ∩ 𝑣) → ((𝑥 ∈ 𝑡 ∧ 𝑡 ⊆ (𝑧 ∩ 𝑤)) → (𝑥 ∈ 𝑡 ∧ 𝑡 ⊆ (𝑢 ∩ 𝑣))))
58	57	reximdv 3202	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑧 ∩ 𝑤) ⊆ (𝑢 ∩ 𝑣) → (∃𝑡 ∈ 𝐵 (𝑥 ∈ 𝑡 ∧ 𝑡 ⊆ (𝑧 ∩ 𝑤)) → ∃𝑡 ∈ 𝐵 (𝑥 ∈ 𝑡 ∧ 𝑡 ⊆ (𝑢 ∩ 𝑣))))
59	58	adantl 482	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ (𝑧 ∩ 𝑤) ∧ (𝑧 ∩ 𝑤) ⊆ (𝑢 ∩ 𝑣)) → (∃𝑡 ∈ 𝐵 (𝑥 ∈ 𝑡 ∧ 𝑡 ⊆ (𝑧 ∩ 𝑤)) → ∃𝑡 ∈ 𝐵 (𝑥 ∈ 𝑡 ∧ 𝑡 ⊆ (𝑢 ∩ 𝑣))))
60	59	ad2antll 726	. . . . . . . . . . . . . . 15 ⊢ ((((𝐵 ∈ TopBases ∧ 𝑥 ∈ (𝑢 ∩ 𝑣)) ∧ 𝑧 ∈ 𝐵) ∧ (𝑤 ∈ 𝐵 ∧ (𝑥 ∈ (𝑧 ∩ 𝑤) ∧ (𝑧 ∩ 𝑤) ⊆ (𝑢 ∩ 𝑣)))) → (∃𝑡 ∈ 𝐵 (𝑥 ∈ 𝑡 ∧ 𝑡 ⊆ (𝑧 ∩ 𝑤)) → ∃𝑡 ∈ 𝐵 (𝑥 ∈ 𝑡 ∧ 𝑡 ⊆ (𝑢 ∩ 𝑣))))
61	54, 60	mpd 15	. . . . . . . . . . . . . 14 ⊢ ((((𝐵 ∈ TopBases ∧ 𝑥 ∈ (𝑢 ∩ 𝑣)) ∧ 𝑧 ∈ 𝐵) ∧ (𝑤 ∈ 𝐵 ∧ (𝑥 ∈ (𝑧 ∩ 𝑤) ∧ (𝑧 ∩ 𝑤) ⊆ (𝑢 ∩ 𝑣)))) → ∃𝑡 ∈ 𝐵 (𝑥 ∈ 𝑡 ∧ 𝑡 ⊆ (𝑢 ∩ 𝑣)))
62	51, 61	sylanr2 680	. . . . . . . . . . . . 13 ⊢ ((((𝐵 ∈ TopBases ∧ 𝑥 ∈ (𝑢 ∩ 𝑣)) ∧ 𝑧 ∈ 𝐵) ∧ (𝑤 ∈ 𝐵 ∧ ((𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑢) ∧ (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑣)))) → ∃𝑡 ∈ 𝐵 (𝑥 ∈ 𝑡 ∧ 𝑡 ⊆ (𝑢 ∩ 𝑣)))
63	62	rexlimdvaa 3214	. . . . . . . . . . . 12 ⊢ (((𝐵 ∈ TopBases ∧ 𝑥 ∈ (𝑢 ∩ 𝑣)) ∧ 𝑧 ∈ 𝐵) → (∃𝑤 ∈ 𝐵 ((𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑢) ∧ (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑣)) → ∃𝑡 ∈ 𝐵 (𝑥 ∈ 𝑡 ∧ 𝑡 ⊆ (𝑢 ∩ 𝑣))))
64	63	rexlimdva 3213	. . . . . . . . . . 11 ⊢ ((𝐵 ∈ TopBases ∧ 𝑥 ∈ (𝑢 ∩ 𝑣)) → (∃𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐵 ((𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑢) ∧ (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑣)) → ∃𝑡 ∈ 𝐵 (𝑥 ∈ 𝑡 ∧ 𝑡 ⊆ (𝑢 ∩ 𝑣))))
65	64	ex 413	. . . . . . . . . 10 ⊢ (𝐵 ∈ TopBases → (𝑥 ∈ (𝑢 ∩ 𝑣) → (∃𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐵 ((𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑢) ∧ (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑣)) → ∃𝑡 ∈ 𝐵 (𝑥 ∈ 𝑡 ∧ 𝑡 ⊆ (𝑢 ∩ 𝑣)))))
66	65	a2d 29	. . . . . . . . 9 ⊢ (𝐵 ∈ TopBases → ((𝑥 ∈ (𝑢 ∩ 𝑣) → ∃𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐵 ((𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑢) ∧ (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑣))) → (𝑥 ∈ (𝑢 ∩ 𝑣) → ∃𝑡 ∈ 𝐵 (𝑥 ∈ 𝑡 ∧ 𝑡 ⊆ (𝑢 ∩ 𝑣)))))
67	66	imp 407	. . . . . . . 8 ⊢ ((𝐵 ∈ TopBases ∧ (𝑥 ∈ (𝑢 ∩ 𝑣) → ∃𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐵 ((𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑢) ∧ (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑣)))) → (𝑥 ∈ (𝑢 ∩ 𝑣) → ∃𝑡 ∈ 𝐵 (𝑥 ∈ 𝑡 ∧ 𝑡 ⊆ (𝑢 ∩ 𝑣))))
68	46, 67	syldan 591	. . . . . . 7 ⊢ ((𝐵 ∈ TopBases ∧ (𝑢 ∈ (topGen‘𝐵) ∧ 𝑣 ∈ (topGen‘𝐵))) → (𝑥 ∈ (𝑢 ∩ 𝑣) → ∃𝑡 ∈ 𝐵 (𝑥 ∈ 𝑡 ∧ 𝑡 ⊆ (𝑢 ∩ 𝑣))))
69	68	ralrimiv 3102	. . . . . 6 ⊢ ((𝐵 ∈ TopBases ∧ (𝑢 ∈ (topGen‘𝐵) ∧ 𝑣 ∈ (topGen‘𝐵))) → ∀𝑥 ∈ (𝑢 ∩ 𝑣)∃𝑡 ∈ 𝐵 (𝑥 ∈ 𝑡 ∧ 𝑡 ⊆ (𝑢 ∩ 𝑣)))
70	33, 69	jca 512	. . . . 5 ⊢ ((𝐵 ∈ TopBases ∧ (𝑢 ∈ (topGen‘𝐵) ∧ 𝑣 ∈ (topGen‘𝐵))) → ((𝑢 ∩ 𝑣) ⊆ ∪ 𝐵 ∧ ∀𝑥 ∈ (𝑢 ∩ 𝑣)∃𝑡 ∈ 𝐵 (𝑥 ∈ 𝑡 ∧ 𝑡 ⊆ (𝑢 ∩ 𝑣))))
71	70	ex 413	. . . 4 ⊢ (𝐵 ∈ TopBases → ((𝑢 ∈ (topGen‘𝐵) ∧ 𝑣 ∈ (topGen‘𝐵)) → ((𝑢 ∩ 𝑣) ⊆ ∪ 𝐵 ∧ ∀𝑥 ∈ (𝑢 ∩ 𝑣)∃𝑡 ∈ 𝐵 (𝑥 ∈ 𝑡 ∧ 𝑡 ⊆ (𝑢 ∩ 𝑣)))))
72		eltg2 22108	. . . 4 ⊢ (𝐵 ∈ TopBases → ((𝑢 ∩ 𝑣) ∈ (topGen‘𝐵) ↔ ((𝑢 ∩ 𝑣) ⊆ ∪ 𝐵 ∧ ∀𝑥 ∈ (𝑢 ∩ 𝑣)∃𝑡 ∈ 𝐵 (𝑥 ∈ 𝑡 ∧ 𝑡 ⊆ (𝑢 ∩ 𝑣)))))
73	71, 72	sylibrd 258	. . 3 ⊢ (𝐵 ∈ TopBases → ((𝑢 ∈ (topGen‘𝐵) ∧ 𝑣 ∈ (topGen‘𝐵)) → (𝑢 ∩ 𝑣) ∈ (topGen‘𝐵)))
74	73	ralrimivv 3122	. 2 ⊢ (𝐵 ∈ TopBases → ∀𝑢 ∈ (topGen‘𝐵)∀𝑣 ∈ (topGen‘𝐵)(𝑢 ∩ 𝑣) ∈ (topGen‘𝐵))
75		fvex 6787	. . 3 ⊢ (topGen‘𝐵) ∈ V
76		istopg 22044	. . 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 583	1 ⊢ (𝐵 ∈ TopBases → (topGen‘𝐵) ∈ Top)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 396 ∀wal 1537 = wceq 1539 ∈ wcel 2106 ∀wral 3064 ∃wrex 3065 Vcvv 3432 ∩ cin 3886 ⊆ wss 3887 ∪ cuni 4839 ‘cfv 6433 topGenctg 17148 Topctop 22042 TopBasesctb 22095

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2709 ax-sep 5223 ax-nul 5230 ax-pow 5288 ax-pr 5352 ax-un 7588

This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1783 df-nf 1787 df-sb 2068 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2816 df-nfc 2889 df-ral 3069 df-rex 3070 df-rab 3073 df-v 3434 df-dif 3890 df-un 3892 df-in 3894 df-ss 3904 df-nul 4257 df-if 4460 df-pw 4535 df-sn 4562 df-pr 4564 df-op 4568 df-uni 4840 df-br 5075 df-opab 5137 df-mpt 5158 df-id 5489 df-xp 5595 df-rel 5596 df-cnv 5597 df-co 5598 df-dm 5599 df-iota 6391 df-fun 6435 df-fv 6441 df-topgen 17154 df-top 22043 df-bases 22096

This theorem is referenced by: tgclb 22120 tgtopon 22121 bastop 22131 elcls3 22234 resttop 22311 leordtval2 22363 tgcmp 22552 2ndctop 22598 2ndcsb 22600 2ndcsep 22610 txtop 22720 pttop 22733 xkotop 22739 alexsubALT 23202 retop 23925 onsuctop 34622 kelac2lem 40889

W3C validator