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

Theorem tgcl 21552
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.
StepHypRef Expression
1 uniss 4819 . . . . . . . 8 (𝑢 ⊆ (topGen‘𝐵) → 𝑢 (topGen‘𝐵))
21adantl 485 . . . . . . 7 ((𝐵 ∈ TopBases ∧ 𝑢 ⊆ (topGen‘𝐵)) → 𝑢 (topGen‘𝐵))
3 unitg 21550 . . . . . . . 8 (𝐵 ∈ TopBases → (topGen‘𝐵) = 𝐵)
43adantr 484 . . . . . . 7 ((𝐵 ∈ TopBases ∧ 𝑢 ⊆ (topGen‘𝐵)) → (topGen‘𝐵) = 𝐵)
52, 4sseqtrd 3983 . . . . . 6 ((𝐵 ∈ TopBases ∧ 𝑢 ⊆ (topGen‘𝐵)) → 𝑢 𝐵)
6 eluni2 4815 . . . . . . . 8 (𝑥 𝑢 ↔ ∃𝑡𝑢 𝑥𝑡)
7 ssel2 3938 . . . . . . . . . . . 12 ((𝑢 ⊆ (topGen‘𝐵) ∧ 𝑡𝑢) → 𝑡 ∈ (topGen‘𝐵))
8 eltg2b 21542 . . . . . . . . . . . . . . 15 (𝐵 ∈ TopBases → (𝑡 ∈ (topGen‘𝐵) ↔ ∀𝑥𝑡𝑦𝐵 (𝑥𝑦𝑦𝑡)))
9 rsp 3193 . . . . . . . . . . . . . . 15 (∀𝑥𝑡𝑦𝐵 (𝑥𝑦𝑦𝑡) → (𝑥𝑡 → ∃𝑦𝐵 (𝑥𝑦𝑦𝑡)))
108, 9syl6bi 256 . . . . . . . . . . . . . 14 (𝐵 ∈ TopBases → (𝑡 ∈ (topGen‘𝐵) → (𝑥𝑡 → ∃𝑦𝐵 (𝑥𝑦𝑦𝑡))))
1110imp31 421 . . . . . . . . . . . . 13 (((𝐵 ∈ TopBases ∧ 𝑡 ∈ (topGen‘𝐵)) ∧ 𝑥𝑡) → ∃𝑦𝐵 (𝑥𝑦𝑦𝑡))
1211an32s 651 . . . . . . . . . . . 12 (((𝐵 ∈ TopBases ∧ 𝑥𝑡) ∧ 𝑡 ∈ (topGen‘𝐵)) → ∃𝑦𝐵 (𝑥𝑦𝑦𝑡))
137, 12sylan2 595 . . . . . . . . . . 11 (((𝐵 ∈ TopBases ∧ 𝑥𝑡) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑡𝑢)) → ∃𝑦𝐵 (𝑥𝑦𝑦𝑡))
1413an42s 660 . . . . . . . . . 10 (((𝐵 ∈ TopBases ∧ 𝑢 ⊆ (topGen‘𝐵)) ∧ (𝑡𝑢𝑥𝑡)) → ∃𝑦𝐵 (𝑥𝑦𝑦𝑡))
15 elssuni 4841 . . . . . . . . . . . . . 14 (𝑡𝑢𝑡 𝑢)
16 sstr2 3950 . . . . . . . . . . . . . 14 (𝑦𝑡 → (𝑡 𝑢𝑦 𝑢))
1715, 16syl5com 31 . . . . . . . . . . . . 13 (𝑡𝑢 → (𝑦𝑡𝑦 𝑢))
1817anim2d 614 . . . . . . . . . . . 12 (𝑡𝑢 → ((𝑥𝑦𝑦𝑡) → (𝑥𝑦𝑦 𝑢)))
1918reximdv 3259 . . . . . . . . . . 11 (𝑡𝑢 → (∃𝑦𝐵 (𝑥𝑦𝑦𝑡) → ∃𝑦𝐵 (𝑥𝑦𝑦 𝑢)))
2019ad2antrl 727 . . . . . . . . . 10 (((𝐵 ∈ TopBases ∧ 𝑢 ⊆ (topGen‘𝐵)) ∧ (𝑡𝑢𝑥𝑡)) → (∃𝑦𝐵 (𝑥𝑦𝑦𝑡) → ∃𝑦𝐵 (𝑥𝑦𝑦 𝑢)))
2114, 20mpd 15 . . . . . . . . 9 (((𝐵 ∈ TopBases ∧ 𝑢 ⊆ (topGen‘𝐵)) ∧ (𝑡𝑢𝑥𝑡)) → ∃𝑦𝐵 (𝑥𝑦𝑦 𝑢))
2221rexlimdvaa 3271 . . . . . . . 8 ((𝐵 ∈ TopBases ∧ 𝑢 ⊆ (topGen‘𝐵)) → (∃𝑡𝑢 𝑥𝑡 → ∃𝑦𝐵 (𝑥𝑦𝑦 𝑢)))
236, 22syl5bi 245 . . . . . . 7 ((𝐵 ∈ TopBases ∧ 𝑢 ⊆ (topGen‘𝐵)) → (𝑥 𝑢 → ∃𝑦𝐵 (𝑥𝑦𝑦 𝑢)))
2423ralrimiv 3169 . . . . . 6 ((𝐵 ∈ TopBases ∧ 𝑢 ⊆ (topGen‘𝐵)) → ∀𝑥 𝑢𝑦𝐵 (𝑥𝑦𝑦 𝑢))
255, 24jca 515 . . . . 5 ((𝐵 ∈ TopBases ∧ 𝑢 ⊆ (topGen‘𝐵)) → ( 𝑢 𝐵 ∧ ∀𝑥 𝑢𝑦𝐵 (𝑥𝑦𝑦 𝑢)))
2625ex 416 . . . 4 (𝐵 ∈ TopBases → (𝑢 ⊆ (topGen‘𝐵) → ( 𝑢 𝐵 ∧ ∀𝑥 𝑢𝑦𝐵 (𝑥𝑦𝑦 𝑢))))
27 eltg2 21541 . . . 4 (𝐵 ∈ TopBases → ( 𝑢 ∈ (topGen‘𝐵) ↔ ( 𝑢 𝐵 ∧ ∀𝑥 𝑢𝑦𝐵 (𝑥𝑦𝑦 𝑢))))
2826, 27sylibrd 262 . . 3 (𝐵 ∈ TopBases → (𝑢 ⊆ (topGen‘𝐵) → 𝑢 ∈ (topGen‘𝐵)))
2928alrimiv 1929 . 2 (𝐵 ∈ TopBases → ∀𝑢(𝑢 ⊆ (topGen‘𝐵) → 𝑢 ∈ (topGen‘𝐵)))
30 inss1 4180 . . . . . . . 8 (𝑢𝑣) ⊆ 𝑢
31 tg1 21547 . . . . . . . 8 (𝑢 ∈ (topGen‘𝐵) → 𝑢 𝐵)
3230, 31sstrid 3954 . . . . . . 7 (𝑢 ∈ (topGen‘𝐵) → (𝑢𝑣) ⊆ 𝐵)
3332ad2antrl 727 . . . . . 6 ((𝐵 ∈ TopBases ∧ (𝑢 ∈ (topGen‘𝐵) ∧ 𝑣 ∈ (topGen‘𝐵))) → (𝑢𝑣) ⊆ 𝐵)
34 eltg2 21541 . . . . . . . . . . . . 13 (𝐵 ∈ TopBases → (𝑢 ∈ (topGen‘𝐵) ↔ (𝑢 𝐵 ∧ ∀𝑥𝑢𝑧𝐵 (𝑥𝑧𝑧𝑢))))
3534simplbda 503 . . . . . . . . . . . 12 ((𝐵 ∈ TopBases ∧ 𝑢 ∈ (topGen‘𝐵)) → ∀𝑥𝑢𝑧𝐵 (𝑥𝑧𝑧𝑢))
36 rsp 3193 . . . . . . . . . . . 12 (∀𝑥𝑢𝑧𝐵 (𝑥𝑧𝑧𝑢) → (𝑥𝑢 → ∃𝑧𝐵 (𝑥𝑧𝑧𝑢)))
3735, 36syl 17 . . . . . . . . . . 11 ((𝐵 ∈ TopBases ∧ 𝑢 ∈ (topGen‘𝐵)) → (𝑥𝑢 → ∃𝑧𝐵 (𝑥𝑧𝑧𝑢)))
38 eltg2 21541 . . . . . . . . . . . . 13 (𝐵 ∈ TopBases → (𝑣 ∈ (topGen‘𝐵) ↔ (𝑣 𝐵 ∧ ∀𝑥𝑣𝑤𝐵 (𝑥𝑤𝑤𝑣))))
3938simplbda 503 . . . . . . . . . . . 12 ((𝐵 ∈ TopBases ∧ 𝑣 ∈ (topGen‘𝐵)) → ∀𝑥𝑣𝑤𝐵 (𝑥𝑤𝑤𝑣))
40 rsp 3193 . . . . . . . . . . . 12 (∀𝑥𝑣𝑤𝐵 (𝑥𝑤𝑤𝑣) → (𝑥𝑣 → ∃𝑤𝐵 (𝑥𝑤𝑤𝑣)))
4139, 40syl 17 . . . . . . . . . . 11 ((𝐵 ∈ TopBases ∧ 𝑣 ∈ (topGen‘𝐵)) → (𝑥𝑣 → ∃𝑤𝐵 (𝑥𝑤𝑤𝑣)))
4237, 41im2anan9 622 . . . . . . . . . 10 (((𝐵 ∈ TopBases ∧ 𝑢 ∈ (topGen‘𝐵)) ∧ (𝐵 ∈ TopBases ∧ 𝑣 ∈ (topGen‘𝐵))) → ((𝑥𝑢𝑥𝑣) → (∃𝑧𝐵 (𝑥𝑧𝑧𝑢) ∧ ∃𝑤𝐵 (𝑥𝑤𝑤𝑣))))
43 elin 3926 . . . . . . . . . 10 (𝑥 ∈ (𝑢𝑣) ↔ (𝑥𝑢𝑥𝑣))
44 reeanv 3352 . . . . . . . . . 10 (∃𝑧𝐵𝑤𝐵 ((𝑥𝑧𝑧𝑢) ∧ (𝑥𝑤𝑤𝑣)) ↔ (∃𝑧𝐵 (𝑥𝑧𝑧𝑢) ∧ ∃𝑤𝐵 (𝑥𝑤𝑤𝑣)))
4542, 43, 443imtr4g 299 . . . . . . . . 9 (((𝐵 ∈ TopBases ∧ 𝑢 ∈ (topGen‘𝐵)) ∧ (𝐵 ∈ TopBases ∧ 𝑣 ∈ (topGen‘𝐵))) → (𝑥 ∈ (𝑢𝑣) → ∃𝑧𝐵𝑤𝐵 ((𝑥𝑧𝑧𝑢) ∧ (𝑥𝑤𝑤𝑣))))
4645anandis 677 . . . . . . . 8 ((𝐵 ∈ TopBases ∧ (𝑢 ∈ (topGen‘𝐵) ∧ 𝑣 ∈ (topGen‘𝐵))) → (𝑥 ∈ (𝑢𝑣) → ∃𝑧𝐵𝑤𝐵 ((𝑥𝑧𝑧𝑢) ∧ (𝑥𝑤𝑤𝑣))))
47 elin 3926 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ (𝑧𝑤) ↔ (𝑥𝑧𝑥𝑤))
4847biimpri 231 . . . . . . . . . . . . . . . 16 ((𝑥𝑧𝑥𝑤) → 𝑥 ∈ (𝑧𝑤))
49 ss2in 4188 . . . . . . . . . . . . . . . 16 ((𝑧𝑢𝑤𝑣) → (𝑧𝑤) ⊆ (𝑢𝑣))
5048, 49anim12i 615 . . . . . . . . . . . . . . 15 (((𝑥𝑧𝑥𝑤) ∧ (𝑧𝑢𝑤𝑣)) → (𝑥 ∈ (𝑧𝑤) ∧ (𝑧𝑤) ⊆ (𝑢𝑣)))
5150an4s 659 . . . . . . . . . . . . . 14 (((𝑥𝑧𝑧𝑢) ∧ (𝑥𝑤𝑤𝑣)) → (𝑥 ∈ (𝑧𝑤) ∧ (𝑧𝑤) ⊆ (𝑢𝑣)))
52 basis2 21534 . . . . . . . . . . . . . . . . 17 (((𝐵 ∈ TopBases ∧ 𝑧𝐵) ∧ (𝑤𝐵𝑥 ∈ (𝑧𝑤))) → ∃𝑡𝐵 (𝑥𝑡𝑡 ⊆ (𝑧𝑤)))
5352adantllr 718 . . . . . . . . . . . . . . . 16 ((((𝐵 ∈ TopBases ∧ 𝑥 ∈ (𝑢𝑣)) ∧ 𝑧𝐵) ∧ (𝑤𝐵𝑥 ∈ (𝑧𝑤))) → ∃𝑡𝐵 (𝑥𝑡𝑡 ⊆ (𝑧𝑤)))
5453adantrrr 724 . . . . . . . . . . . . . . 15 ((((𝐵 ∈ TopBases ∧ 𝑥 ∈ (𝑢𝑣)) ∧ 𝑧𝐵) ∧ (𝑤𝐵 ∧ (𝑥 ∈ (𝑧𝑤) ∧ (𝑧𝑤) ⊆ (𝑢𝑣)))) → ∃𝑡𝐵 (𝑥𝑡𝑡 ⊆ (𝑧𝑤)))
55 sstr2 3950 . . . . . . . . . . . . . . . . . . . 20 (𝑡 ⊆ (𝑧𝑤) → ((𝑧𝑤) ⊆ (𝑢𝑣) → 𝑡 ⊆ (𝑢𝑣)))
5655com12 32 . . . . . . . . . . . . . . . . . . 19 ((𝑧𝑤) ⊆ (𝑢𝑣) → (𝑡 ⊆ (𝑧𝑤) → 𝑡 ⊆ (𝑢𝑣)))
5756anim2d 614 . . . . . . . . . . . . . . . . . 18 ((𝑧𝑤) ⊆ (𝑢𝑣) → ((𝑥𝑡𝑡 ⊆ (𝑧𝑤)) → (𝑥𝑡𝑡 ⊆ (𝑢𝑣))))
5857reximdv 3259 . . . . . . . . . . . . . . . . 17 ((𝑧𝑤) ⊆ (𝑢𝑣) → (∃𝑡𝐵 (𝑥𝑡𝑡 ⊆ (𝑧𝑤)) → ∃𝑡𝐵 (𝑥𝑡𝑡 ⊆ (𝑢𝑣))))
5958adantl 485 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ (𝑧𝑤) ∧ (𝑧𝑤) ⊆ (𝑢𝑣)) → (∃𝑡𝐵 (𝑥𝑡𝑡 ⊆ (𝑧𝑤)) → ∃𝑡𝐵 (𝑥𝑡𝑡 ⊆ (𝑢𝑣))))
6059ad2antll 728 . . . . . . . . . . . . . . 15 ((((𝐵 ∈ TopBases ∧ 𝑥 ∈ (𝑢𝑣)) ∧ 𝑧𝐵) ∧ (𝑤𝐵 ∧ (𝑥 ∈ (𝑧𝑤) ∧ (𝑧𝑤) ⊆ (𝑢𝑣)))) → (∃𝑡𝐵 (𝑥𝑡𝑡 ⊆ (𝑧𝑤)) → ∃𝑡𝐵 (𝑥𝑡𝑡 ⊆ (𝑢𝑣))))
6154, 60mpd 15 . . . . . . . . . . . . . 14 ((((𝐵 ∈ TopBases ∧ 𝑥 ∈ (𝑢𝑣)) ∧ 𝑧𝐵) ∧ (𝑤𝐵 ∧ (𝑥 ∈ (𝑧𝑤) ∧ (𝑧𝑤) ⊆ (𝑢𝑣)))) → ∃𝑡𝐵 (𝑥𝑡𝑡 ⊆ (𝑢𝑣)))
6251, 61sylanr2 682 . . . . . . . . . . . . 13 ((((𝐵 ∈ TopBases ∧ 𝑥 ∈ (𝑢𝑣)) ∧ 𝑧𝐵) ∧ (𝑤𝐵 ∧ ((𝑥𝑧𝑧𝑢) ∧ (𝑥𝑤𝑤𝑣)))) → ∃𝑡𝐵 (𝑥𝑡𝑡 ⊆ (𝑢𝑣)))
6362rexlimdvaa 3271 . . . . . . . . . . . 12 (((𝐵 ∈ TopBases ∧ 𝑥 ∈ (𝑢𝑣)) ∧ 𝑧𝐵) → (∃𝑤𝐵 ((𝑥𝑧𝑧𝑢) ∧ (𝑥𝑤𝑤𝑣)) → ∃𝑡𝐵 (𝑥𝑡𝑡 ⊆ (𝑢𝑣))))
6463rexlimdva 3270 . . . . . . . . . . 11 ((𝐵 ∈ TopBases ∧ 𝑥 ∈ (𝑢𝑣)) → (∃𝑧𝐵𝑤𝐵 ((𝑥𝑧𝑧𝑢) ∧ (𝑥𝑤𝑤𝑣)) → ∃𝑡𝐵 (𝑥𝑡𝑡 ⊆ (𝑢𝑣))))
6564ex 416 . . . . . . . . . 10 (𝐵 ∈ TopBases → (𝑥 ∈ (𝑢𝑣) → (∃𝑧𝐵𝑤𝐵 ((𝑥𝑧𝑧𝑢) ∧ (𝑥𝑤𝑤𝑣)) → ∃𝑡𝐵 (𝑥𝑡𝑡 ⊆ (𝑢𝑣)))))
6665a2d 29 . . . . . . . . 9 (𝐵 ∈ TopBases → ((𝑥 ∈ (𝑢𝑣) → ∃𝑧𝐵𝑤𝐵 ((𝑥𝑧𝑧𝑢) ∧ (𝑥𝑤𝑤𝑣))) → (𝑥 ∈ (𝑢𝑣) → ∃𝑡𝐵 (𝑥𝑡𝑡 ⊆ (𝑢𝑣)))))
6766imp 410 . . . . . . . 8 ((𝐵 ∈ TopBases ∧ (𝑥 ∈ (𝑢𝑣) → ∃𝑧𝐵𝑤𝐵 ((𝑥𝑧𝑧𝑢) ∧ (𝑥𝑤𝑤𝑣)))) → (𝑥 ∈ (𝑢𝑣) → ∃𝑡𝐵 (𝑥𝑡𝑡 ⊆ (𝑢𝑣))))
6846, 67syldan 594 . . . . . . 7 ((𝐵 ∈ TopBases ∧ (𝑢 ∈ (topGen‘𝐵) ∧ 𝑣 ∈ (topGen‘𝐵))) → (𝑥 ∈ (𝑢𝑣) → ∃𝑡𝐵 (𝑥𝑡𝑡 ⊆ (𝑢𝑣))))
6968ralrimiv 3169 . . . . . 6 ((𝐵 ∈ TopBases ∧ (𝑢 ∈ (topGen‘𝐵) ∧ 𝑣 ∈ (topGen‘𝐵))) → ∀𝑥 ∈ (𝑢𝑣)∃𝑡𝐵 (𝑥𝑡𝑡 ⊆ (𝑢𝑣)))
7033, 69jca 515 . . . . 5 ((𝐵 ∈ TopBases ∧ (𝑢 ∈ (topGen‘𝐵) ∧ 𝑣 ∈ (topGen‘𝐵))) → ((𝑢𝑣) ⊆ 𝐵 ∧ ∀𝑥 ∈ (𝑢𝑣)∃𝑡𝐵 (𝑥𝑡𝑡 ⊆ (𝑢𝑣))))
7170ex 416 . . . 4 (𝐵 ∈ TopBases → ((𝑢 ∈ (topGen‘𝐵) ∧ 𝑣 ∈ (topGen‘𝐵)) → ((𝑢𝑣) ⊆ 𝐵 ∧ ∀𝑥 ∈ (𝑢𝑣)∃𝑡𝐵 (𝑥𝑡𝑡 ⊆ (𝑢𝑣)))))
72 eltg2 21541 . . . 4 (𝐵 ∈ TopBases → ((𝑢𝑣) ∈ (topGen‘𝐵) ↔ ((𝑢𝑣) ⊆ 𝐵 ∧ ∀𝑥 ∈ (𝑢𝑣)∃𝑡𝐵 (𝑥𝑡𝑡 ⊆ (𝑢𝑣)))))
7371, 72sylibrd 262 . . 3 (𝐵 ∈ TopBases → ((𝑢 ∈ (topGen‘𝐵) ∧ 𝑣 ∈ (topGen‘𝐵)) → (𝑢𝑣) ∈ (topGen‘𝐵)))
7473ralrimivv 3178 . 2 (𝐵 ∈ TopBases → ∀𝑢 ∈ (topGen‘𝐵)∀𝑣 ∈ (topGen‘𝐵)(𝑢𝑣) ∈ (topGen‘𝐵))
75 fvex 6656 . . 3 (topGen‘𝐵) ∈ V
76 istopg 21478 . . 3 ((topGen‘𝐵) ∈ V → ((topGen‘𝐵) ∈ Top ↔ (∀𝑢(𝑢 ⊆ (topGen‘𝐵) → 𝑢 ∈ (topGen‘𝐵)) ∧ ∀𝑢 ∈ (topGen‘𝐵)∀𝑣 ∈ (topGen‘𝐵)(𝑢𝑣) ∈ (topGen‘𝐵))))
7775, 76ax-mp 5 . 2 ((topGen‘𝐵) ∈ Top ↔ (∀𝑢(𝑢 ⊆ (topGen‘𝐵) → 𝑢 ∈ (topGen‘𝐵)) ∧ ∀𝑢 ∈ (topGen‘𝐵)∀𝑣 ∈ (topGen‘𝐵)(𝑢𝑣) ∈ (topGen‘𝐵)))
7829, 74, 77sylanbrc 586 1 (𝐵 ∈ TopBases → (topGen‘𝐵) ∈ Top)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399  wal 1536   = wceq 1538  wcel 2115  wral 3126  wrex 3127  Vcvv 3471  cin 3909  wss 3910   cuni 4811  cfv 6328  topGenctg 16689  Topctop 21476  TopBasesctb 21528
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2178  ax-ext 2793  ax-sep 5176  ax-nul 5183  ax-pow 5239  ax-pr 5303  ax-un 7436
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2623  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2892  df-nfc 2960  df-ral 3131  df-rex 3132  df-rab 3135  df-v 3473  df-sbc 3750  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-nul 4267  df-if 4441  df-pw 4514  df-sn 4541  df-pr 4543  df-op 4547  df-uni 4812  df-br 5040  df-opab 5102  df-mpt 5120  df-id 5433  df-xp 5534  df-rel 5535  df-cnv 5536  df-co 5537  df-dm 5538  df-iota 6287  df-fun 6330  df-fv 6336  df-topgen 16695  df-top 21477  df-bases 21529
This theorem is referenced by:  tgclb  21553  tgtopon  21554  bastop  21564  elcls3  21666  resttop  21743  leordtval2  21795  tgcmp  21984  2ndctop  22030  2ndcsb  22032  2ndcsep  22042  txtop  22152  pttop  22165  xkotop  22171  alexsubALT  22634  retop  23345  onsuctop  33788  kelac2lem  39805
  Copyright terms: Public domain W3C validator