tgcl - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > tgcl		GIF version

Theorem tgcl 14507

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 3870	. . . . . . . 8 ⊢ (𝑢 ⊆ (topGen‘𝐵) → ∪ 𝑢 ⊆ ∪ (topGen‘𝐵))
2	1	adantl 277	. . . . . . 7 ⊢ ((𝐵 ∈ TopBases ∧ 𝑢 ⊆ (topGen‘𝐵)) → ∪ 𝑢 ⊆ ∪ (topGen‘𝐵))
3		unitg 14505	. . . . . . . 8 ⊢ (𝐵 ∈ TopBases → ∪ (topGen‘𝐵) = ∪ 𝐵)
4	3	adantr 276	. . . . . . 7 ⊢ ((𝐵 ∈ TopBases ∧ 𝑢 ⊆ (topGen‘𝐵)) → ∪ (topGen‘𝐵) = ∪ 𝐵)
5	2, 4	sseqtrd 3230	. . . . . 6 ⊢ ((𝐵 ∈ TopBases ∧ 𝑢 ⊆ (topGen‘𝐵)) → ∪ 𝑢 ⊆ ∪ 𝐵)
6		eluni2 3853	. . . . . . . 8 ⊢ (𝑥 ∈ ∪ 𝑢 ↔ ∃𝑡 ∈ 𝑢 𝑥 ∈ 𝑡)
7		ssel2 3187	. . . . . . . . . . . 12 ⊢ ((𝑢 ⊆ (topGen‘𝐵) ∧ 𝑡 ∈ 𝑢) → 𝑡 ∈ (topGen‘𝐵))
8		eltg2b 14497	. . . . . . . . . . . . . . 15 ⊢ (𝐵 ∈ TopBases → (𝑡 ∈ (topGen‘𝐵) ↔ ∀𝑥 ∈ 𝑡 ∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑡)))
9		rsp 2552	. . . . . . . . . . . . . . 15 ⊢ (∀𝑥 ∈ 𝑡 ∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑡) → (𝑥 ∈ 𝑡 → ∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑡)))
10	8, 9	biimtrdi 163	. . . . . . . . . . . . . 14 ⊢ (𝐵 ∈ TopBases → (𝑡 ∈ (topGen‘𝐵) → (𝑥 ∈ 𝑡 → ∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑡))))
11	10	imp31 256	. . . . . . . . . . . . 13 ⊢ (((𝐵 ∈ TopBases ∧ 𝑡 ∈ (topGen‘𝐵)) ∧ 𝑥 ∈ 𝑡) → ∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑡))
12	11	an32s 568	. . . . . . . . . . . 12 ⊢ (((𝐵 ∈ TopBases ∧ 𝑥 ∈ 𝑡) ∧ 𝑡 ∈ (topGen‘𝐵)) → ∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑡))
13	7, 12	sylan2 286	. . . . . . . . . . 11 ⊢ (((𝐵 ∈ TopBases ∧ 𝑥 ∈ 𝑡) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑡 ∈ 𝑢)) → ∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑡))
14	13	an42s 589	. . . . . . . . . 10 ⊢ (((𝐵 ∈ TopBases ∧ 𝑢 ⊆ (topGen‘𝐵)) ∧ (𝑡 ∈ 𝑢 ∧ 𝑥 ∈ 𝑡)) → ∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑡))
15		elssuni 3877	. . . . . . . . . . . . . 14 ⊢ (𝑡 ∈ 𝑢 → 𝑡 ⊆ ∪ 𝑢)
16		sstr2 3199	. . . . . . . . . . . . . 14 ⊢ (𝑦 ⊆ 𝑡 → (𝑡 ⊆ ∪ 𝑢 → 𝑦 ⊆ ∪ 𝑢))
17	15, 16	syl5com 29	. . . . . . . . . . . . 13 ⊢ (𝑡 ∈ 𝑢 → (𝑦 ⊆ 𝑡 → 𝑦 ⊆ ∪ 𝑢))
18	17	anim2d 337	. . . . . . . . . . . 12 ⊢ (𝑡 ∈ 𝑢 → ((𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑡) → (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ ∪ 𝑢)))
19	18	reximdv 2606	. . . . . . . . . . 11 ⊢ (𝑡 ∈ 𝑢 → (∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑡) → ∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ ∪ 𝑢)))
20	19	ad2antrl 490	. . . . . . . . . 10 ⊢ (((𝐵 ∈ TopBases ∧ 𝑢 ⊆ (topGen‘𝐵)) ∧ (𝑡 ∈ 𝑢 ∧ 𝑥 ∈ 𝑡)) → (∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑡) → ∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ ∪ 𝑢)))
21	14, 20	mpd 13	. . . . . . . . 9 ⊢ (((𝐵 ∈ TopBases ∧ 𝑢 ⊆ (topGen‘𝐵)) ∧ (𝑡 ∈ 𝑢 ∧ 𝑥 ∈ 𝑡)) → ∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ ∪ 𝑢))
22	21	rexlimdvaa 2623	. . . . . . . 8 ⊢ ((𝐵 ∈ TopBases ∧ 𝑢 ⊆ (topGen‘𝐵)) → (∃𝑡 ∈ 𝑢 𝑥 ∈ 𝑡 → ∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ ∪ 𝑢)))
23	6, 22	biimtrid 152	. . . . . . 7 ⊢ ((𝐵 ∈ TopBases ∧ 𝑢 ⊆ (topGen‘𝐵)) → (𝑥 ∈ ∪ 𝑢 → ∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ ∪ 𝑢)))
24	23	ralrimiv 2577	. . . . . 6 ⊢ ((𝐵 ∈ TopBases ∧ 𝑢 ⊆ (topGen‘𝐵)) → ∀𝑥 ∈ ∪ 𝑢∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ ∪ 𝑢))
25	5, 24	jca 306	. . . . 5 ⊢ ((𝐵 ∈ TopBases ∧ 𝑢 ⊆ (topGen‘𝐵)) → (∪ 𝑢 ⊆ ∪ 𝐵 ∧ ∀𝑥 ∈ ∪ 𝑢∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ ∪ 𝑢)))
26	25	ex 115	. . . 4 ⊢ (𝐵 ∈ TopBases → (𝑢 ⊆ (topGen‘𝐵) → (∪ 𝑢 ⊆ ∪ 𝐵 ∧ ∀𝑥 ∈ ∪ 𝑢∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ ∪ 𝑢))))
27		eltg2 14496	. . . 4 ⊢ (𝐵 ∈ TopBases → (∪ 𝑢 ∈ (topGen‘𝐵) ↔ (∪ 𝑢 ⊆ ∪ 𝐵 ∧ ∀𝑥 ∈ ∪ 𝑢∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ ∪ 𝑢))))
28	26, 27	sylibrd 169	. . 3 ⊢ (𝐵 ∈ TopBases → (𝑢 ⊆ (topGen‘𝐵) → ∪ 𝑢 ∈ (topGen‘𝐵)))
29	28	alrimiv 1896	. 2 ⊢ (𝐵 ∈ TopBases → ∀𝑢(𝑢 ⊆ (topGen‘𝐵) → ∪ 𝑢 ∈ (topGen‘𝐵)))
30		inss1 3392	. . . . . . . 8 ⊢ (𝑢 ∩ 𝑣) ⊆ 𝑢
31		tg1 14502	. . . . . . . 8 ⊢ (𝑢 ∈ (topGen‘𝐵) → 𝑢 ⊆ ∪ 𝐵)
32	30, 31	sstrid 3203	. . . . . . 7 ⊢ (𝑢 ∈ (topGen‘𝐵) → (𝑢 ∩ 𝑣) ⊆ ∪ 𝐵)
33	32	ad2antrl 490	. . . . . 6 ⊢ ((𝐵 ∈ TopBases ∧ (𝑢 ∈ (topGen‘𝐵) ∧ 𝑣 ∈ (topGen‘𝐵))) → (𝑢 ∩ 𝑣) ⊆ ∪ 𝐵)
34		eltg2 14496	. . . . . . . . . . . . 13 ⊢ (𝐵 ∈ TopBases → (𝑢 ∈ (topGen‘𝐵) ↔ (𝑢 ⊆ ∪ 𝐵 ∧ ∀𝑥 ∈ 𝑢 ∃𝑧 ∈ 𝐵 (𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑢))))
35	34	simplbda 384	. . . . . . . . . . . 12 ⊢ ((𝐵 ∈ TopBases ∧ 𝑢 ∈ (topGen‘𝐵)) → ∀𝑥 ∈ 𝑢 ∃𝑧 ∈ 𝐵 (𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑢))
36		rsp 2552	. . . . . . . . . . . 12 ⊢ (∀𝑥 ∈ 𝑢 ∃𝑧 ∈ 𝐵 (𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑢) → (𝑥 ∈ 𝑢 → ∃𝑧 ∈ 𝐵 (𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑢)))
37	35, 36	syl 14	. . . . . . . . . . 11 ⊢ ((𝐵 ∈ TopBases ∧ 𝑢 ∈ (topGen‘𝐵)) → (𝑥 ∈ 𝑢 → ∃𝑧 ∈ 𝐵 (𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑢)))
38		eltg2 14496	. . . . . . . . . . . . 13 ⊢ (𝐵 ∈ TopBases → (𝑣 ∈ (topGen‘𝐵) ↔ (𝑣 ⊆ ∪ 𝐵 ∧ ∀𝑥 ∈ 𝑣 ∃𝑤 ∈ 𝐵 (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑣))))
39	38	simplbda 384	. . . . . . . . . . . 12 ⊢ ((𝐵 ∈ TopBases ∧ 𝑣 ∈ (topGen‘𝐵)) → ∀𝑥 ∈ 𝑣 ∃𝑤 ∈ 𝐵 (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑣))
40		rsp 2552	. . . . . . . . . . . 12 ⊢ (∀𝑥 ∈ 𝑣 ∃𝑤 ∈ 𝐵 (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑣) → (𝑥 ∈ 𝑣 → ∃𝑤 ∈ 𝐵 (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑣)))
41	39, 40	syl 14	. . . . . . . . . . 11 ⊢ ((𝐵 ∈ TopBases ∧ 𝑣 ∈ (topGen‘𝐵)) → (𝑥 ∈ 𝑣 → ∃𝑤 ∈ 𝐵 (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑣)))
42	37, 41	im2anan9 598	. . . . . . . . . 10 ⊢ (((𝐵 ∈ TopBases ∧ 𝑢 ∈ (topGen‘𝐵)) ∧ (𝐵 ∈ TopBases ∧ 𝑣 ∈ (topGen‘𝐵))) → ((𝑥 ∈ 𝑢 ∧ 𝑥 ∈ 𝑣) → (∃𝑧 ∈ 𝐵 (𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑢) ∧ ∃𝑤 ∈ 𝐵 (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑣))))
43		elin 3355	. . . . . . . . . 10 ⊢ (𝑥 ∈ (𝑢 ∩ 𝑣) ↔ (𝑥 ∈ 𝑢 ∧ 𝑥 ∈ 𝑣))
44		reeanv 2675	. . . . . . . . . 10 ⊢ (∃𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐵 ((𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑢) ∧ (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑣)) ↔ (∃𝑧 ∈ 𝐵 (𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑢) ∧ ∃𝑤 ∈ 𝐵 (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑣)))
45	42, 43, 44	3imtr4g 205	. . . . . . . . 9 ⊢ (((𝐵 ∈ TopBases ∧ 𝑢 ∈ (topGen‘𝐵)) ∧ (𝐵 ∈ TopBases ∧ 𝑣 ∈ (topGen‘𝐵))) → (𝑥 ∈ (𝑢 ∩ 𝑣) → ∃𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐵 ((𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑢) ∧ (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑣))))
46	45	anandis 592	. . . . . . . 8 ⊢ ((𝐵 ∈ TopBases ∧ (𝑢 ∈ (topGen‘𝐵) ∧ 𝑣 ∈ (topGen‘𝐵))) → (𝑥 ∈ (𝑢 ∩ 𝑣) → ∃𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐵 ((𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑢) ∧ (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑣))))
47		elin 3355	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ (𝑧 ∩ 𝑤) ↔ (𝑥 ∈ 𝑧 ∧ 𝑥 ∈ 𝑤))
48	47	biimpri 133	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ 𝑧 ∧ 𝑥 ∈ 𝑤) → 𝑥 ∈ (𝑧 ∩ 𝑤))
49		ss2in 3400	. . . . . . . . . . . . . . . 16 ⊢ ((𝑧 ⊆ 𝑢 ∧ 𝑤 ⊆ 𝑣) → (𝑧 ∩ 𝑤) ⊆ (𝑢 ∩ 𝑣))
50	48, 49	anim12i 338	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ 𝑧 ∧ 𝑥 ∈ 𝑤) ∧ (𝑧 ⊆ 𝑢 ∧ 𝑤 ⊆ 𝑣)) → (𝑥 ∈ (𝑧 ∩ 𝑤) ∧ (𝑧 ∩ 𝑤) ⊆ (𝑢 ∩ 𝑣)))
51	50	an4s 588	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑢) ∧ (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑣)) → (𝑥 ∈ (𝑧 ∩ 𝑤) ∧ (𝑧 ∩ 𝑤) ⊆ (𝑢 ∩ 𝑣)))
52		basis2 14491	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐵 ∈ TopBases ∧ 𝑧 ∈ 𝐵) ∧ (𝑤 ∈ 𝐵 ∧ 𝑥 ∈ (𝑧 ∩ 𝑤))) → ∃𝑡 ∈ 𝐵 (𝑥 ∈ 𝑡 ∧ 𝑡 ⊆ (𝑧 ∩ 𝑤)))
53	52	adantllr 481	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐵 ∈ TopBases ∧ 𝑥 ∈ (𝑢 ∩ 𝑣)) ∧ 𝑧 ∈ 𝐵) ∧ (𝑤 ∈ 𝐵 ∧ 𝑥 ∈ (𝑧 ∩ 𝑤))) → ∃𝑡 ∈ 𝐵 (𝑥 ∈ 𝑡 ∧ 𝑡 ⊆ (𝑧 ∩ 𝑤)))
54	53	adantrrr 487	. . . . . . . . . . . . . . 15 ⊢ ((((𝐵 ∈ TopBases ∧ 𝑥 ∈ (𝑢 ∩ 𝑣)) ∧ 𝑧 ∈ 𝐵) ∧ (𝑤 ∈ 𝐵 ∧ (𝑥 ∈ (𝑧 ∩ 𝑤) ∧ (𝑧 ∩ 𝑤) ⊆ (𝑢 ∩ 𝑣)))) → ∃𝑡 ∈ 𝐵 (𝑥 ∈ 𝑡 ∧ 𝑡 ⊆ (𝑧 ∩ 𝑤)))
55		sstr2 3199	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑡 ⊆ (𝑧 ∩ 𝑤) → ((𝑧 ∩ 𝑤) ⊆ (𝑢 ∩ 𝑣) → 𝑡 ⊆ (𝑢 ∩ 𝑣)))
56	55	com12 30	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑧 ∩ 𝑤) ⊆ (𝑢 ∩ 𝑣) → (𝑡 ⊆ (𝑧 ∩ 𝑤) → 𝑡 ⊆ (𝑢 ∩ 𝑣)))
57	56	anim2d 337	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑧 ∩ 𝑤) ⊆ (𝑢 ∩ 𝑣) → ((𝑥 ∈ 𝑡 ∧ 𝑡 ⊆ (𝑧 ∩ 𝑤)) → (𝑥 ∈ 𝑡 ∧ 𝑡 ⊆ (𝑢 ∩ 𝑣))))
58	57	reximdv 2606	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑧 ∩ 𝑤) ⊆ (𝑢 ∩ 𝑣) → (∃𝑡 ∈ 𝐵 (𝑥 ∈ 𝑡 ∧ 𝑡 ⊆ (𝑧 ∩ 𝑤)) → ∃𝑡 ∈ 𝐵 (𝑥 ∈ 𝑡 ∧ 𝑡 ⊆ (𝑢 ∩ 𝑣))))
59	58	adantl 277	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ (𝑧 ∩ 𝑤) ∧ (𝑧 ∩ 𝑤) ⊆ (𝑢 ∩ 𝑣)) → (∃𝑡 ∈ 𝐵 (𝑥 ∈ 𝑡 ∧ 𝑡 ⊆ (𝑧 ∩ 𝑤)) → ∃𝑡 ∈ 𝐵 (𝑥 ∈ 𝑡 ∧ 𝑡 ⊆ (𝑢 ∩ 𝑣))))
60	59	ad2antll 491	. . . . . . . . . . . . . . 15 ⊢ ((((𝐵 ∈ TopBases ∧ 𝑥 ∈ (𝑢 ∩ 𝑣)) ∧ 𝑧 ∈ 𝐵) ∧ (𝑤 ∈ 𝐵 ∧ (𝑥 ∈ (𝑧 ∩ 𝑤) ∧ (𝑧 ∩ 𝑤) ⊆ (𝑢 ∩ 𝑣)))) → (∃𝑡 ∈ 𝐵 (𝑥 ∈ 𝑡 ∧ 𝑡 ⊆ (𝑧 ∩ 𝑤)) → ∃𝑡 ∈ 𝐵 (𝑥 ∈ 𝑡 ∧ 𝑡 ⊆ (𝑢 ∩ 𝑣))))
61	54, 60	mpd 13	. . . . . . . . . . . . . 14 ⊢ ((((𝐵 ∈ TopBases ∧ 𝑥 ∈ (𝑢 ∩ 𝑣)) ∧ 𝑧 ∈ 𝐵) ∧ (𝑤 ∈ 𝐵 ∧ (𝑥 ∈ (𝑧 ∩ 𝑤) ∧ (𝑧 ∩ 𝑤) ⊆ (𝑢 ∩ 𝑣)))) → ∃𝑡 ∈ 𝐵 (𝑥 ∈ 𝑡 ∧ 𝑡 ⊆ (𝑢 ∩ 𝑣)))
62	51, 61	sylanr2 405	. . . . . . . . . . . . 13 ⊢ ((((𝐵 ∈ TopBases ∧ 𝑥 ∈ (𝑢 ∩ 𝑣)) ∧ 𝑧 ∈ 𝐵) ∧ (𝑤 ∈ 𝐵 ∧ ((𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑢) ∧ (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑣)))) → ∃𝑡 ∈ 𝐵 (𝑥 ∈ 𝑡 ∧ 𝑡 ⊆ (𝑢 ∩ 𝑣)))
63	62	rexlimdvaa 2623	. . . . . . . . . . . 12 ⊢ (((𝐵 ∈ TopBases ∧ 𝑥 ∈ (𝑢 ∩ 𝑣)) ∧ 𝑧 ∈ 𝐵) → (∃𝑤 ∈ 𝐵 ((𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑢) ∧ (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑣)) → ∃𝑡 ∈ 𝐵 (𝑥 ∈ 𝑡 ∧ 𝑡 ⊆ (𝑢 ∩ 𝑣))))
64	63	rexlimdva 2622	. . . . . . . . . . 11 ⊢ ((𝐵 ∈ TopBases ∧ 𝑥 ∈ (𝑢 ∩ 𝑣)) → (∃𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐵 ((𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑢) ∧ (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑣)) → ∃𝑡 ∈ 𝐵 (𝑥 ∈ 𝑡 ∧ 𝑡 ⊆ (𝑢 ∩ 𝑣))))
65	64	ex 115	. . . . . . . . . 10 ⊢ (𝐵 ∈ TopBases → (𝑥 ∈ (𝑢 ∩ 𝑣) → (∃𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐵 ((𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑢) ∧ (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑣)) → ∃𝑡 ∈ 𝐵 (𝑥 ∈ 𝑡 ∧ 𝑡 ⊆ (𝑢 ∩ 𝑣)))))
66	65	a2d 26	. . . . . . . . 9 ⊢ (𝐵 ∈ TopBases → ((𝑥 ∈ (𝑢 ∩ 𝑣) → ∃𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐵 ((𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑢) ∧ (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑣))) → (𝑥 ∈ (𝑢 ∩ 𝑣) → ∃𝑡 ∈ 𝐵 (𝑥 ∈ 𝑡 ∧ 𝑡 ⊆ (𝑢 ∩ 𝑣)))))
67	66	imp 124	. . . . . . . 8 ⊢ ((𝐵 ∈ TopBases ∧ (𝑥 ∈ (𝑢 ∩ 𝑣) → ∃𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐵 ((𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑢) ∧ (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑣)))) → (𝑥 ∈ (𝑢 ∩ 𝑣) → ∃𝑡 ∈ 𝐵 (𝑥 ∈ 𝑡 ∧ 𝑡 ⊆ (𝑢 ∩ 𝑣))))
68	46, 67	syldan 282	. . . . . . 7 ⊢ ((𝐵 ∈ TopBases ∧ (𝑢 ∈ (topGen‘𝐵) ∧ 𝑣 ∈ (topGen‘𝐵))) → (𝑥 ∈ (𝑢 ∩ 𝑣) → ∃𝑡 ∈ 𝐵 (𝑥 ∈ 𝑡 ∧ 𝑡 ⊆ (𝑢 ∩ 𝑣))))
69	68	ralrimiv 2577	. . . . . 6 ⊢ ((𝐵 ∈ TopBases ∧ (𝑢 ∈ (topGen‘𝐵) ∧ 𝑣 ∈ (topGen‘𝐵))) → ∀𝑥 ∈ (𝑢 ∩ 𝑣)∃𝑡 ∈ 𝐵 (𝑥 ∈ 𝑡 ∧ 𝑡 ⊆ (𝑢 ∩ 𝑣)))
70	33, 69	jca 306	. . . . 5 ⊢ ((𝐵 ∈ TopBases ∧ (𝑢 ∈ (topGen‘𝐵) ∧ 𝑣 ∈ (topGen‘𝐵))) → ((𝑢 ∩ 𝑣) ⊆ ∪ 𝐵 ∧ ∀𝑥 ∈ (𝑢 ∩ 𝑣)∃𝑡 ∈ 𝐵 (𝑥 ∈ 𝑡 ∧ 𝑡 ⊆ (𝑢 ∩ 𝑣))))
71	70	ex 115	. . . 4 ⊢ (𝐵 ∈ TopBases → ((𝑢 ∈ (topGen‘𝐵) ∧ 𝑣 ∈ (topGen‘𝐵)) → ((𝑢 ∩ 𝑣) ⊆ ∪ 𝐵 ∧ ∀𝑥 ∈ (𝑢 ∩ 𝑣)∃𝑡 ∈ 𝐵 (𝑥 ∈ 𝑡 ∧ 𝑡 ⊆ (𝑢 ∩ 𝑣)))))
72		eltg2 14496	. . . 4 ⊢ (𝐵 ∈ TopBases → ((𝑢 ∩ 𝑣) ∈ (topGen‘𝐵) ↔ ((𝑢 ∩ 𝑣) ⊆ ∪ 𝐵 ∧ ∀𝑥 ∈ (𝑢 ∩ 𝑣)∃𝑡 ∈ 𝐵 (𝑥 ∈ 𝑡 ∧ 𝑡 ⊆ (𝑢 ∩ 𝑣)))))
73	71, 72	sylibrd 169	. . 3 ⊢ (𝐵 ∈ TopBases → ((𝑢 ∈ (topGen‘𝐵) ∧ 𝑣 ∈ (topGen‘𝐵)) → (𝑢 ∩ 𝑣) ∈ (topGen‘𝐵)))
74	73	ralrimivv 2586	. 2 ⊢ (𝐵 ∈ TopBases → ∀𝑢 ∈ (topGen‘𝐵)∀𝑣 ∈ (topGen‘𝐵)(𝑢 ∩ 𝑣) ∈ (topGen‘𝐵))
75		tgvalex 13066	. . 3 ⊢ (𝐵 ∈ TopBases → (topGen‘𝐵) ∈ V)
76		istopg 14442	. . 3 ⊢ ((topGen‘𝐵) ∈ V → ((topGen‘𝐵) ∈ Top ↔ (∀𝑢(𝑢 ⊆ (topGen‘𝐵) → ∪ 𝑢 ∈ (topGen‘𝐵)) ∧ ∀𝑢 ∈ (topGen‘𝐵)∀𝑣 ∈ (topGen‘𝐵)(𝑢 ∩ 𝑣) ∈ (topGen‘𝐵))))
77	75, 76	syl 14	. 2 ⊢ (𝐵 ∈ TopBases → ((topGen‘𝐵) ∈ Top ↔ (∀𝑢(𝑢 ⊆ (topGen‘𝐵) → ∪ 𝑢 ∈ (topGen‘𝐵)) ∧ ∀𝑢 ∈ (topGen‘𝐵)∀𝑣 ∈ (topGen‘𝐵)(𝑢 ∩ 𝑣) ∈ (topGen‘𝐵))))
78	29, 74, 77	mpbir2and 946	1 ⊢ (𝐵 ∈ TopBases → (topGen‘𝐵) ∈ Top)

Colors of variables: wff set class

Syntax hints: → wi 4 ∧ wa 104 ↔ wb 105 ∀wal 1370 = wceq 1372 ∈ wcel 2175 ∀wral 2483 ∃wrex 2484 Vcvv 2771 ∩ cin 3164 ⊆ wss 3165 ∪ cuni 3849 ‘cfv 5270 topGenctg 13057 Topctop 14440 TopBasesctb 14485

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-io 710 ax-5 1469 ax-7 1470 ax-gen 1471 ax-ie1 1515 ax-ie2 1516 ax-8 1526 ax-10 1527 ax-11 1528 ax-i12 1529 ax-bndl 1531 ax-4 1532 ax-17 1548 ax-i9 1552 ax-ial 1556 ax-i5r 1557 ax-13 2177 ax-14 2178 ax-ext 2186 ax-sep 4161 ax-pow 4217 ax-pr 4252 ax-un 4479

This theorem depends on definitions: df-bi 117 df-3an 982 df-tru 1375 df-nf 1483 df-sb 1785 df-eu 2056 df-mo 2057 df-clab 2191 df-cleq 2197 df-clel 2200 df-nfc 2336 df-ral 2488 df-rex 2489 df-v 2773 df-sbc 2998 df-un 3169 df-in 3171 df-ss 3178 df-pw 3617 df-sn 3638 df-pr 3639 df-op 3641 df-uni 3850 df-br 4044 df-opab 4105 df-mpt 4106 df-id 4339 df-xp 4680 df-rel 4681 df-cnv 4682 df-co 4683 df-dm 4684 df-iota 5231 df-fun 5272 df-fv 5278 df-topgen 13063 df-top 14441 df-bases 14486

This theorem is referenced by: tgclb 14508 tgtopon 14509 bastop 14518 resttop 14613 txtop 14703 mopnval 14885 retop 14967

W3C validator