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 22913

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 4871	. . . . . . . 8 ⊢ (𝑢 ⊆ (topGen‘𝐵) → ∪ 𝑢 ⊆ ∪ (topGen‘𝐵))
2	1	adantl 481	. . . . . . 7 ⊢ ((𝐵 ∈ TopBases ∧ 𝑢 ⊆ (topGen‘𝐵)) → ∪ 𝑢 ⊆ ∪ (topGen‘𝐵))
3		unitg 22911	. . . . . . . 8 ⊢ (𝐵 ∈ TopBases → ∪ (topGen‘𝐵) = ∪ 𝐵)
4	3	adantr 480	. . . . . . 7 ⊢ ((𝐵 ∈ TopBases ∧ 𝑢 ⊆ (topGen‘𝐵)) → ∪ (topGen‘𝐵) = ∪ 𝐵)
5	2, 4	sseqtrd 3970	. . . . . 6 ⊢ ((𝐵 ∈ TopBases ∧ 𝑢 ⊆ (topGen‘𝐵)) → ∪ 𝑢 ⊆ ∪ 𝐵)
6		eluni2 4867	. . . . . . . 8 ⊢ (𝑥 ∈ ∪ 𝑢 ↔ ∃𝑡 ∈ 𝑢 𝑥 ∈ 𝑡)
7		ssel2 3928	. . . . . . . . . . . 12 ⊢ ((𝑢 ⊆ (topGen‘𝐵) ∧ 𝑡 ∈ 𝑢) → 𝑡 ∈ (topGen‘𝐵))
8		eltg2b 22903	. . . . . . . . . . . . . . 15 ⊢ (𝐵 ∈ TopBases → (𝑡 ∈ (topGen‘𝐵) ↔ ∀𝑥 ∈ 𝑡 ∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑡)))
9		rsp 3224	. . . . . . . . . . . . . . 15 ⊢ (∀𝑥 ∈ 𝑡 ∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑡) → (𝑥 ∈ 𝑡 → ∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑡)))
10	8, 9	biimtrdi 253	. . . . . . . . . . . . . 14 ⊢ (𝐵 ∈ TopBases → (𝑡 ∈ (topGen‘𝐵) → (𝑥 ∈ 𝑡 → ∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑡))))
11	10	imp31 417	. . . . . . . . . . . . 13 ⊢ (((𝐵 ∈ TopBases ∧ 𝑡 ∈ (topGen‘𝐵)) ∧ 𝑥 ∈ 𝑡) → ∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑡))
12	11	an32s 652	. . . . . . . . . . . 12 ⊢ (((𝐵 ∈ TopBases ∧ 𝑥 ∈ 𝑡) ∧ 𝑡 ∈ (topGen‘𝐵)) → ∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑡))
13	7, 12	sylan2 593	. . . . . . . . . . 11 ⊢ (((𝐵 ∈ TopBases ∧ 𝑥 ∈ 𝑡) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑡 ∈ 𝑢)) → ∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑡))
14	13	an42s 661	. . . . . . . . . 10 ⊢ (((𝐵 ∈ TopBases ∧ 𝑢 ⊆ (topGen‘𝐵)) ∧ (𝑡 ∈ 𝑢 ∧ 𝑥 ∈ 𝑡)) → ∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑡))
15		elssuni 4894	. . . . . . . . . . . . . 14 ⊢ (𝑡 ∈ 𝑢 → 𝑡 ⊆ ∪ 𝑢)
16		sstr2 3940	. . . . . . . . . . . . . 14 ⊢ (𝑦 ⊆ 𝑡 → (𝑡 ⊆ ∪ 𝑢 → 𝑦 ⊆ ∪ 𝑢))
17	15, 16	syl5com 31	. . . . . . . . . . . . 13 ⊢ (𝑡 ∈ 𝑢 → (𝑦 ⊆ 𝑡 → 𝑦 ⊆ ∪ 𝑢))
18	17	anim2d 612	. . . . . . . . . . . 12 ⊢ (𝑡 ∈ 𝑢 → ((𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑡) → (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ ∪ 𝑢)))
19	18	reximdv 3151	. . . . . . . . . . 11 ⊢ (𝑡 ∈ 𝑢 → (∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑡) → ∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ ∪ 𝑢)))
20	19	ad2antrl 728	. . . . . . . . . 10 ⊢ (((𝐵 ∈ TopBases ∧ 𝑢 ⊆ (topGen‘𝐵)) ∧ (𝑡 ∈ 𝑢 ∧ 𝑥 ∈ 𝑡)) → (∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑡) → ∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ ∪ 𝑢)))
21	14, 20	mpd 15	. . . . . . . . 9 ⊢ (((𝐵 ∈ TopBases ∧ 𝑢 ⊆ (topGen‘𝐵)) ∧ (𝑡 ∈ 𝑢 ∧ 𝑥 ∈ 𝑡)) → ∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ ∪ 𝑢))
22	21	rexlimdvaa 3138	. . . . . . . 8 ⊢ ((𝐵 ∈ TopBases ∧ 𝑢 ⊆ (topGen‘𝐵)) → (∃𝑡 ∈ 𝑢 𝑥 ∈ 𝑡 → ∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ ∪ 𝑢)))
23	6, 22	biimtrid 242	. . . . . . 7 ⊢ ((𝐵 ∈ TopBases ∧ 𝑢 ⊆ (topGen‘𝐵)) → (𝑥 ∈ ∪ 𝑢 → ∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ ∪ 𝑢)))
24	23	ralrimiv 3127	. . . . . 6 ⊢ ((𝐵 ∈ TopBases ∧ 𝑢 ⊆ (topGen‘𝐵)) → ∀𝑥 ∈ ∪ 𝑢∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ ∪ 𝑢))
25	5, 24	jca 511	. . . . 5 ⊢ ((𝐵 ∈ TopBases ∧ 𝑢 ⊆ (topGen‘𝐵)) → (∪ 𝑢 ⊆ ∪ 𝐵 ∧ ∀𝑥 ∈ ∪ 𝑢∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ ∪ 𝑢)))
26	25	ex 412	. . . 4 ⊢ (𝐵 ∈ TopBases → (𝑢 ⊆ (topGen‘𝐵) → (∪ 𝑢 ⊆ ∪ 𝐵 ∧ ∀𝑥 ∈ ∪ 𝑢∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ ∪ 𝑢))))
27		eltg2 22902	. . . 4 ⊢ (𝐵 ∈ TopBases → (∪ 𝑢 ∈ (topGen‘𝐵) ↔ (∪ 𝑢 ⊆ ∪ 𝐵 ∧ ∀𝑥 ∈ ∪ 𝑢∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ ∪ 𝑢))))
28	26, 27	sylibrd 259	. . 3 ⊢ (𝐵 ∈ TopBases → (𝑢 ⊆ (topGen‘𝐵) → ∪ 𝑢 ∈ (topGen‘𝐵)))
29	28	alrimiv 1928	. 2 ⊢ (𝐵 ∈ TopBases → ∀𝑢(𝑢 ⊆ (topGen‘𝐵) → ∪ 𝑢 ∈ (topGen‘𝐵)))
30		inss1 4189	. . . . . . . 8 ⊢ (𝑢 ∩ 𝑣) ⊆ 𝑢
31		tg1 22908	. . . . . . . 8 ⊢ (𝑢 ∈ (topGen‘𝐵) → 𝑢 ⊆ ∪ 𝐵)
32	30, 31	sstrid 3945	. . . . . . 7 ⊢ (𝑢 ∈ (topGen‘𝐵) → (𝑢 ∩ 𝑣) ⊆ ∪ 𝐵)
33	32	ad2antrl 728	. . . . . 6 ⊢ ((𝐵 ∈ TopBases ∧ (𝑢 ∈ (topGen‘𝐵) ∧ 𝑣 ∈ (topGen‘𝐵))) → (𝑢 ∩ 𝑣) ⊆ ∪ 𝐵)
34		eltg2 22902	. . . . . . . . . . . . 13 ⊢ (𝐵 ∈ TopBases → (𝑢 ∈ (topGen‘𝐵) ↔ (𝑢 ⊆ ∪ 𝐵 ∧ ∀𝑥 ∈ 𝑢 ∃𝑧 ∈ 𝐵 (𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑢))))
35	34	simplbda 499	. . . . . . . . . . . 12 ⊢ ((𝐵 ∈ TopBases ∧ 𝑢 ∈ (topGen‘𝐵)) → ∀𝑥 ∈ 𝑢 ∃𝑧 ∈ 𝐵 (𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑢))
36		rsp 3224	. . . . . . . . . . . 12 ⊢ (∀𝑥 ∈ 𝑢 ∃𝑧 ∈ 𝐵 (𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑢) → (𝑥 ∈ 𝑢 → ∃𝑧 ∈ 𝐵 (𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑢)))
37	35, 36	syl 17	. . . . . . . . . . 11 ⊢ ((𝐵 ∈ TopBases ∧ 𝑢 ∈ (topGen‘𝐵)) → (𝑥 ∈ 𝑢 → ∃𝑧 ∈ 𝐵 (𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑢)))
38		eltg2 22902	. . . . . . . . . . . . 13 ⊢ (𝐵 ∈ TopBases → (𝑣 ∈ (topGen‘𝐵) ↔ (𝑣 ⊆ ∪ 𝐵 ∧ ∀𝑥 ∈ 𝑣 ∃𝑤 ∈ 𝐵 (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑣))))
39	38	simplbda 499	. . . . . . . . . . . 12 ⊢ ((𝐵 ∈ TopBases ∧ 𝑣 ∈ (topGen‘𝐵)) → ∀𝑥 ∈ 𝑣 ∃𝑤 ∈ 𝐵 (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑣))
40		rsp 3224	. . . . . . . . . . . 12 ⊢ (∀𝑥 ∈ 𝑣 ∃𝑤 ∈ 𝐵 (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑣) → (𝑥 ∈ 𝑣 → ∃𝑤 ∈ 𝐵 (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑣)))
41	39, 40	syl 17	. . . . . . . . . . 11 ⊢ ((𝐵 ∈ TopBases ∧ 𝑣 ∈ (topGen‘𝐵)) → (𝑥 ∈ 𝑣 → ∃𝑤 ∈ 𝐵 (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑣)))
42	37, 41	im2anan9 620	. . . . . . . . . 10 ⊢ (((𝐵 ∈ TopBases ∧ 𝑢 ∈ (topGen‘𝐵)) ∧ (𝐵 ∈ TopBases ∧ 𝑣 ∈ (topGen‘𝐵))) → ((𝑥 ∈ 𝑢 ∧ 𝑥 ∈ 𝑣) → (∃𝑧 ∈ 𝐵 (𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑢) ∧ ∃𝑤 ∈ 𝐵 (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑣))))
43		elin 3917	. . . . . . . . . 10 ⊢ (𝑥 ∈ (𝑢 ∩ 𝑣) ↔ (𝑥 ∈ 𝑢 ∧ 𝑥 ∈ 𝑣))
44		reeanv 3208	. . . . . . . . . 10 ⊢ (∃𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐵 ((𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑢) ∧ (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑣)) ↔ (∃𝑧 ∈ 𝐵 (𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑢) ∧ ∃𝑤 ∈ 𝐵 (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑣)))
45	42, 43, 44	3imtr4g 296	. . . . . . . . 9 ⊢ (((𝐵 ∈ TopBases ∧ 𝑢 ∈ (topGen‘𝐵)) ∧ (𝐵 ∈ TopBases ∧ 𝑣 ∈ (topGen‘𝐵))) → (𝑥 ∈ (𝑢 ∩ 𝑣) → ∃𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐵 ((𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑢) ∧ (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑣))))
46	45	anandis 678	. . . . . . . 8 ⊢ ((𝐵 ∈ TopBases ∧ (𝑢 ∈ (topGen‘𝐵) ∧ 𝑣 ∈ (topGen‘𝐵))) → (𝑥 ∈ (𝑢 ∩ 𝑣) → ∃𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐵 ((𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑢) ∧ (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑣))))
47		elin 3917	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ (𝑧 ∩ 𝑤) ↔ (𝑥 ∈ 𝑧 ∧ 𝑥 ∈ 𝑤))
48	47	biimpri 228	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ 𝑧 ∧ 𝑥 ∈ 𝑤) → 𝑥 ∈ (𝑧 ∩ 𝑤))
49		ss2in 4197	. . . . . . . . . . . . . . . 16 ⊢ ((𝑧 ⊆ 𝑢 ∧ 𝑤 ⊆ 𝑣) → (𝑧 ∩ 𝑤) ⊆ (𝑢 ∩ 𝑣))
50	48, 49	anim12i 613	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ 𝑧 ∧ 𝑥 ∈ 𝑤) ∧ (𝑧 ⊆ 𝑢 ∧ 𝑤 ⊆ 𝑣)) → (𝑥 ∈ (𝑧 ∩ 𝑤) ∧ (𝑧 ∩ 𝑤) ⊆ (𝑢 ∩ 𝑣)))
51	50	an4s 660	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑢) ∧ (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑣)) → (𝑥 ∈ (𝑧 ∩ 𝑤) ∧ (𝑧 ∩ 𝑤) ⊆ (𝑢 ∩ 𝑣)))
52		basis2 22895	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐵 ∈ TopBases ∧ 𝑧 ∈ 𝐵) ∧ (𝑤 ∈ 𝐵 ∧ 𝑥 ∈ (𝑧 ∩ 𝑤))) → ∃𝑡 ∈ 𝐵 (𝑥 ∈ 𝑡 ∧ 𝑡 ⊆ (𝑧 ∩ 𝑤)))
53	52	adantllr 719	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐵 ∈ TopBases ∧ 𝑥 ∈ (𝑢 ∩ 𝑣)) ∧ 𝑧 ∈ 𝐵) ∧ (𝑤 ∈ 𝐵 ∧ 𝑥 ∈ (𝑧 ∩ 𝑤))) → ∃𝑡 ∈ 𝐵 (𝑥 ∈ 𝑡 ∧ 𝑡 ⊆ (𝑧 ∩ 𝑤)))
54	53	adantrrr 725	. . . . . . . . . . . . . . 15 ⊢ ((((𝐵 ∈ TopBases ∧ 𝑥 ∈ (𝑢 ∩ 𝑣)) ∧ 𝑧 ∈ 𝐵) ∧ (𝑤 ∈ 𝐵 ∧ (𝑥 ∈ (𝑧 ∩ 𝑤) ∧ (𝑧 ∩ 𝑤) ⊆ (𝑢 ∩ 𝑣)))) → ∃𝑡 ∈ 𝐵 (𝑥 ∈ 𝑡 ∧ 𝑡 ⊆ (𝑧 ∩ 𝑤)))
55		sstr2 3940	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑡 ⊆ (𝑧 ∩ 𝑤) → ((𝑧 ∩ 𝑤) ⊆ (𝑢 ∩ 𝑣) → 𝑡 ⊆ (𝑢 ∩ 𝑣)))
56	55	com12 32	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑧 ∩ 𝑤) ⊆ (𝑢 ∩ 𝑣) → (𝑡 ⊆ (𝑧 ∩ 𝑤) → 𝑡 ⊆ (𝑢 ∩ 𝑣)))
57	56	anim2d 612	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑧 ∩ 𝑤) ⊆ (𝑢 ∩ 𝑣) → ((𝑥 ∈ 𝑡 ∧ 𝑡 ⊆ (𝑧 ∩ 𝑤)) → (𝑥 ∈ 𝑡 ∧ 𝑡 ⊆ (𝑢 ∩ 𝑣))))
58	57	reximdv 3151	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑧 ∩ 𝑤) ⊆ (𝑢 ∩ 𝑣) → (∃𝑡 ∈ 𝐵 (𝑥 ∈ 𝑡 ∧ 𝑡 ⊆ (𝑧 ∩ 𝑤)) → ∃𝑡 ∈ 𝐵 (𝑥 ∈ 𝑡 ∧ 𝑡 ⊆ (𝑢 ∩ 𝑣))))
59	58	adantl 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ (𝑧 ∩ 𝑤) ∧ (𝑧 ∩ 𝑤) ⊆ (𝑢 ∩ 𝑣)) → (∃𝑡 ∈ 𝐵 (𝑥 ∈ 𝑡 ∧ 𝑡 ⊆ (𝑧 ∩ 𝑤)) → ∃𝑡 ∈ 𝐵 (𝑥 ∈ 𝑡 ∧ 𝑡 ⊆ (𝑢 ∩ 𝑣))))
60	59	ad2antll 729	. . . . . . . . . . . . . . 15 ⊢ ((((𝐵 ∈ TopBases ∧ 𝑥 ∈ (𝑢 ∩ 𝑣)) ∧ 𝑧 ∈ 𝐵) ∧ (𝑤 ∈ 𝐵 ∧ (𝑥 ∈ (𝑧 ∩ 𝑤) ∧ (𝑧 ∩ 𝑤) ⊆ (𝑢 ∩ 𝑣)))) → (∃𝑡 ∈ 𝐵 (𝑥 ∈ 𝑡 ∧ 𝑡 ⊆ (𝑧 ∩ 𝑤)) → ∃𝑡 ∈ 𝐵 (𝑥 ∈ 𝑡 ∧ 𝑡 ⊆ (𝑢 ∩ 𝑣))))
61	54, 60	mpd 15	. . . . . . . . . . . . . 14 ⊢ ((((𝐵 ∈ TopBases ∧ 𝑥 ∈ (𝑢 ∩ 𝑣)) ∧ 𝑧 ∈ 𝐵) ∧ (𝑤 ∈ 𝐵 ∧ (𝑥 ∈ (𝑧 ∩ 𝑤) ∧ (𝑧 ∩ 𝑤) ⊆ (𝑢 ∩ 𝑣)))) → ∃𝑡 ∈ 𝐵 (𝑥 ∈ 𝑡 ∧ 𝑡 ⊆ (𝑢 ∩ 𝑣)))
62	51, 61	sylanr2 683	. . . . . . . . . . . . 13 ⊢ ((((𝐵 ∈ TopBases ∧ 𝑥 ∈ (𝑢 ∩ 𝑣)) ∧ 𝑧 ∈ 𝐵) ∧ (𝑤 ∈ 𝐵 ∧ ((𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑢) ∧ (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑣)))) → ∃𝑡 ∈ 𝐵 (𝑥 ∈ 𝑡 ∧ 𝑡 ⊆ (𝑢 ∩ 𝑣)))
63	62	rexlimdvaa 3138	. . . . . . . . . . . 12 ⊢ (((𝐵 ∈ TopBases ∧ 𝑥 ∈ (𝑢 ∩ 𝑣)) ∧ 𝑧 ∈ 𝐵) → (∃𝑤 ∈ 𝐵 ((𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑢) ∧ (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑣)) → ∃𝑡 ∈ 𝐵 (𝑥 ∈ 𝑡 ∧ 𝑡 ⊆ (𝑢 ∩ 𝑣))))
64	63	rexlimdva 3137	. . . . . . . . . . 11 ⊢ ((𝐵 ∈ TopBases ∧ 𝑥 ∈ (𝑢 ∩ 𝑣)) → (∃𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐵 ((𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑢) ∧ (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑣)) → ∃𝑡 ∈ 𝐵 (𝑥 ∈ 𝑡 ∧ 𝑡 ⊆ (𝑢 ∩ 𝑣))))
65	64	ex 412	. . . . . . . . . 10 ⊢ (𝐵 ∈ TopBases → (𝑥 ∈ (𝑢 ∩ 𝑣) → (∃𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐵 ((𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑢) ∧ (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑣)) → ∃𝑡 ∈ 𝐵 (𝑥 ∈ 𝑡 ∧ 𝑡 ⊆ (𝑢 ∩ 𝑣)))))
66	65	a2d 29	. . . . . . . . 9 ⊢ (𝐵 ∈ TopBases → ((𝑥 ∈ (𝑢 ∩ 𝑣) → ∃𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐵 ((𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑢) ∧ (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑣))) → (𝑥 ∈ (𝑢 ∩ 𝑣) → ∃𝑡 ∈ 𝐵 (𝑥 ∈ 𝑡 ∧ 𝑡 ⊆ (𝑢 ∩ 𝑣)))))
67	66	imp 406	. . . . . . . 8 ⊢ ((𝐵 ∈ TopBases ∧ (𝑥 ∈ (𝑢 ∩ 𝑣) → ∃𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐵 ((𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑢) ∧ (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑣)))) → (𝑥 ∈ (𝑢 ∩ 𝑣) → ∃𝑡 ∈ 𝐵 (𝑥 ∈ 𝑡 ∧ 𝑡 ⊆ (𝑢 ∩ 𝑣))))
68	46, 67	syldan 591	. . . . . . 7 ⊢ ((𝐵 ∈ TopBases ∧ (𝑢 ∈ (topGen‘𝐵) ∧ 𝑣 ∈ (topGen‘𝐵))) → (𝑥 ∈ (𝑢 ∩ 𝑣) → ∃𝑡 ∈ 𝐵 (𝑥 ∈ 𝑡 ∧ 𝑡 ⊆ (𝑢 ∩ 𝑣))))
69	68	ralrimiv 3127	. . . . . 6 ⊢ ((𝐵 ∈ TopBases ∧ (𝑢 ∈ (topGen‘𝐵) ∧ 𝑣 ∈ (topGen‘𝐵))) → ∀𝑥 ∈ (𝑢 ∩ 𝑣)∃𝑡 ∈ 𝐵 (𝑥 ∈ 𝑡 ∧ 𝑡 ⊆ (𝑢 ∩ 𝑣)))
70	33, 69	jca 511	. . . . 5 ⊢ ((𝐵 ∈ TopBases ∧ (𝑢 ∈ (topGen‘𝐵) ∧ 𝑣 ∈ (topGen‘𝐵))) → ((𝑢 ∩ 𝑣) ⊆ ∪ 𝐵 ∧ ∀𝑥 ∈ (𝑢 ∩ 𝑣)∃𝑡 ∈ 𝐵 (𝑥 ∈ 𝑡 ∧ 𝑡 ⊆ (𝑢 ∩ 𝑣))))
71	70	ex 412	. . . 4 ⊢ (𝐵 ∈ TopBases → ((𝑢 ∈ (topGen‘𝐵) ∧ 𝑣 ∈ (topGen‘𝐵)) → ((𝑢 ∩ 𝑣) ⊆ ∪ 𝐵 ∧ ∀𝑥 ∈ (𝑢 ∩ 𝑣)∃𝑡 ∈ 𝐵 (𝑥 ∈ 𝑡 ∧ 𝑡 ⊆ (𝑢 ∩ 𝑣)))))
72		eltg2 22902	. . . 4 ⊢ (𝐵 ∈ TopBases → ((𝑢 ∩ 𝑣) ∈ (topGen‘𝐵) ↔ ((𝑢 ∩ 𝑣) ⊆ ∪ 𝐵 ∧ ∀𝑥 ∈ (𝑢 ∩ 𝑣)∃𝑡 ∈ 𝐵 (𝑥 ∈ 𝑡 ∧ 𝑡 ⊆ (𝑢 ∩ 𝑣)))))
73	71, 72	sylibrd 259	. . 3 ⊢ (𝐵 ∈ TopBases → ((𝑢 ∈ (topGen‘𝐵) ∧ 𝑣 ∈ (topGen‘𝐵)) → (𝑢 ∩ 𝑣) ∈ (topGen‘𝐵)))
74	73	ralrimivv 3177	. 2 ⊢ (𝐵 ∈ TopBases → ∀𝑢 ∈ (topGen‘𝐵)∀𝑣 ∈ (topGen‘𝐵)(𝑢 ∩ 𝑣) ∈ (topGen‘𝐵))
75		fvex 6847	. . 3 ⊢ (topGen‘𝐵) ∈ V
76		istopg 22839	. . 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 206 ∧ wa 395 ∀wal 1539 = wceq 1541 ∈ wcel 2113 ∀wral 3051 ∃wrex 3060 Vcvv 3440 ∩ cin 3900 ⊆ wss 3901 ∪ cuni 4863 ‘cfv 6492 topGenctg 17357 Topctop 22837 TopBasesctb 22889

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2115 ax-9 2123 ax-10 2146 ax-11 2162 ax-12 2184 ax-ext 2708 ax-sep 5241 ax-nul 5251 ax-pow 5310 ax-pr 5377 ax-un 7680

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2539 df-eu 2569 df-clab 2715 df-cleq 2728 df-clel 2811 df-nfc 2885 df-ne 2933 df-ral 3052 df-rex 3061 df-rab 3400 df-v 3442 df-dif 3904 df-un 3906 df-in 3908 df-ss 3918 df-nul 4286 df-if 4480 df-pw 4556 df-sn 4581 df-pr 4583 df-op 4587 df-uni 4864 df-br 5099 df-opab 5161 df-mpt 5180 df-id 5519 df-xp 5630 df-rel 5631 df-cnv 5632 df-co 5633 df-dm 5634 df-iota 6448 df-fun 6494 df-fv 6500 df-topgen 17363 df-top 22838 df-bases 22890

This theorem is referenced by: tgclb 22914 tgtopon 22915 bastop 22925 elcls3 23027 resttop 23104 leordtval2 23156 tgcmp 23345 2ndctop 23391 2ndcsb 23393 2ndcsep 23403 txtop 23513 pttop 23526 xkotop 23532 alexsubALT 23995 retop 24705 onsuctop 36627 kelac2lem 43306

W3C validator