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

Theorem tgcl 20995
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 4596 . . . . . . . 8 (𝑢 ⊆ (topGen‘𝐵) → 𝑢 (topGen‘𝐵))
21adantl 467 . . . . . . 7 ((𝐵 ∈ TopBases ∧ 𝑢 ⊆ (topGen‘𝐵)) → 𝑢 (topGen‘𝐵))
3 unitg 20993 . . . . . . . 8 (𝐵 ∈ TopBases → (topGen‘𝐵) = 𝐵)
43adantr 466 . . . . . . 7 ((𝐵 ∈ TopBases ∧ 𝑢 ⊆ (topGen‘𝐵)) → (topGen‘𝐵) = 𝐵)
52, 4sseqtrd 3791 . . . . . 6 ((𝐵 ∈ TopBases ∧ 𝑢 ⊆ (topGen‘𝐵)) → 𝑢 𝐵)
6 eluni2 4579 . . . . . . . 8 (𝑥 𝑢 ↔ ∃𝑡𝑢 𝑥𝑡)
7 ssel2 3748 . . . . . . . . . . . 12 ((𝑢 ⊆ (topGen‘𝐵) ∧ 𝑡𝑢) → 𝑡 ∈ (topGen‘𝐵))
8 eltg2b 20985 . . . . . . . . . . . . . . 15 (𝐵 ∈ TopBases → (𝑡 ∈ (topGen‘𝐵) ↔ ∀𝑥𝑡𝑦𝐵 (𝑥𝑦𝑦𝑡)))
9 rsp 3078 . . . . . . . . . . . . . . 15 (∀𝑥𝑡𝑦𝐵 (𝑥𝑦𝑦𝑡) → (𝑥𝑡 → ∃𝑦𝐵 (𝑥𝑦𝑦𝑡)))
108, 9syl6bi 243 . . . . . . . . . . . . . 14 (𝐵 ∈ TopBases → (𝑡 ∈ (topGen‘𝐵) → (𝑥𝑡 → ∃𝑦𝐵 (𝑥𝑦𝑦𝑡))))
1110imp31 404 . . . . . . . . . . . . 13 (((𝐵 ∈ TopBases ∧ 𝑡 ∈ (topGen‘𝐵)) ∧ 𝑥𝑡) → ∃𝑦𝐵 (𝑥𝑦𝑦𝑡))
1211an32s 625 . . . . . . . . . . . 12 (((𝐵 ∈ TopBases ∧ 𝑥𝑡) ∧ 𝑡 ∈ (topGen‘𝐵)) → ∃𝑦𝐵 (𝑥𝑦𝑦𝑡))
137, 12sylan2 574 . . . . . . . . . . 11 (((𝐵 ∈ TopBases ∧ 𝑥𝑡) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑡𝑢)) → ∃𝑦𝐵 (𝑥𝑦𝑦𝑡))
1413an42s 634 . . . . . . . . . 10 (((𝐵 ∈ TopBases ∧ 𝑢 ⊆ (topGen‘𝐵)) ∧ (𝑡𝑢𝑥𝑡)) → ∃𝑦𝐵 (𝑥𝑦𝑦𝑡))
15 elssuni 4604 . . . . . . . . . . . . . 14 (𝑡𝑢𝑡 𝑢)
16 sstr2 3760 . . . . . . . . . . . . . 14 (𝑦𝑡 → (𝑡 𝑢𝑦 𝑢))
1715, 16syl5com 31 . . . . . . . . . . . . 13 (𝑡𝑢 → (𝑦𝑡𝑦 𝑢))
1817anim2d 593 . . . . . . . . . . . 12 (𝑡𝑢 → ((𝑥𝑦𝑦𝑡) → (𝑥𝑦𝑦 𝑢)))
1918reximdv 3164 . . . . . . . . . . 11 (𝑡𝑢 → (∃𝑦𝐵 (𝑥𝑦𝑦𝑡) → ∃𝑦𝐵 (𝑥𝑦𝑦 𝑢)))
2019ad2antrl 701 . . . . . . . . . 10 (((𝐵 ∈ TopBases ∧ 𝑢 ⊆ (topGen‘𝐵)) ∧ (𝑡𝑢𝑥𝑡)) → (∃𝑦𝐵 (𝑥𝑦𝑦𝑡) → ∃𝑦𝐵 (𝑥𝑦𝑦 𝑢)))
2114, 20mpd 15 . . . . . . . . 9 (((𝐵 ∈ TopBases ∧ 𝑢 ⊆ (topGen‘𝐵)) ∧ (𝑡𝑢𝑥𝑡)) → ∃𝑦𝐵 (𝑥𝑦𝑦 𝑢))
2221rexlimdvaa 3180 . . . . . . . 8 ((𝐵 ∈ TopBases ∧ 𝑢 ⊆ (topGen‘𝐵)) → (∃𝑡𝑢 𝑥𝑡 → ∃𝑦𝐵 (𝑥𝑦𝑦 𝑢)))
236, 22syl5bi 232 . . . . . . 7 ((𝐵 ∈ TopBases ∧ 𝑢 ⊆ (topGen‘𝐵)) → (𝑥 𝑢 → ∃𝑦𝐵 (𝑥𝑦𝑦 𝑢)))
2423ralrimiv 3114 . . . . . 6 ((𝐵 ∈ TopBases ∧ 𝑢 ⊆ (topGen‘𝐵)) → ∀𝑥 𝑢𝑦𝐵 (𝑥𝑦𝑦 𝑢))
255, 24jca 497 . . . . 5 ((𝐵 ∈ TopBases ∧ 𝑢 ⊆ (topGen‘𝐵)) → ( 𝑢 𝐵 ∧ ∀𝑥 𝑢𝑦𝐵 (𝑥𝑦𝑦 𝑢)))
2625ex 397 . . . 4 (𝐵 ∈ TopBases → (𝑢 ⊆ (topGen‘𝐵) → ( 𝑢 𝐵 ∧ ∀𝑥 𝑢𝑦𝐵 (𝑥𝑦𝑦 𝑢))))
27 eltg2 20984 . . . 4 (𝐵 ∈ TopBases → ( 𝑢 ∈ (topGen‘𝐵) ↔ ( 𝑢 𝐵 ∧ ∀𝑥 𝑢𝑦𝐵 (𝑥𝑦𝑦 𝑢))))
2826, 27sylibrd 249 . . 3 (𝐵 ∈ TopBases → (𝑢 ⊆ (topGen‘𝐵) → 𝑢 ∈ (topGen‘𝐵)))
2928alrimiv 2007 . 2 (𝐵 ∈ TopBases → ∀𝑢(𝑢 ⊆ (topGen‘𝐵) → 𝑢 ∈ (topGen‘𝐵)))
30 inss1 3982 . . . . . . . 8 (𝑢𝑣) ⊆ 𝑢
31 tg1 20990 . . . . . . . 8 (𝑢 ∈ (topGen‘𝐵) → 𝑢 𝐵)
3230, 31syl5ss 3764 . . . . . . 7 (𝑢 ∈ (topGen‘𝐵) → (𝑢𝑣) ⊆ 𝐵)
3332ad2antrl 701 . . . . . 6 ((𝐵 ∈ TopBases ∧ (𝑢 ∈ (topGen‘𝐵) ∧ 𝑣 ∈ (topGen‘𝐵))) → (𝑢𝑣) ⊆ 𝐵)
34 eltg2 20984 . . . . . . . . . . . . 13 (𝐵 ∈ TopBases → (𝑢 ∈ (topGen‘𝐵) ↔ (𝑢 𝐵 ∧ ∀𝑥𝑢𝑧𝐵 (𝑥𝑧𝑧𝑢))))
3534simplbda 483 . . . . . . . . . . . 12 ((𝐵 ∈ TopBases ∧ 𝑢 ∈ (topGen‘𝐵)) → ∀𝑥𝑢𝑧𝐵 (𝑥𝑧𝑧𝑢))
36 rsp 3078 . . . . . . . . . . . 12 (∀𝑥𝑢𝑧𝐵 (𝑥𝑧𝑧𝑢) → (𝑥𝑢 → ∃𝑧𝐵 (𝑥𝑧𝑧𝑢)))
3735, 36syl 17 . . . . . . . . . . 11 ((𝐵 ∈ TopBases ∧ 𝑢 ∈ (topGen‘𝐵)) → (𝑥𝑢 → ∃𝑧𝐵 (𝑥𝑧𝑧𝑢)))
38 eltg2 20984 . . . . . . . . . . . . 13 (𝐵 ∈ TopBases → (𝑣 ∈ (topGen‘𝐵) ↔ (𝑣 𝐵 ∧ ∀𝑥𝑣𝑤𝐵 (𝑥𝑤𝑤𝑣))))
3938simplbda 483 . . . . . . . . . . . 12 ((𝐵 ∈ TopBases ∧ 𝑣 ∈ (topGen‘𝐵)) → ∀𝑥𝑣𝑤𝐵 (𝑥𝑤𝑤𝑣))
40 rsp 3078 . . . . . . . . . . . 12 (∀𝑥𝑣𝑤𝐵 (𝑥𝑤𝑤𝑣) → (𝑥𝑣 → ∃𝑤𝐵 (𝑥𝑤𝑤𝑣)))
4139, 40syl 17 . . . . . . . . . . 11 ((𝐵 ∈ TopBases ∧ 𝑣 ∈ (topGen‘𝐵)) → (𝑥𝑣 → ∃𝑤𝐵 (𝑥𝑤𝑤𝑣)))
4237, 41im2anan9 600 . . . . . . . . . 10 (((𝐵 ∈ TopBases ∧ 𝑢 ∈ (topGen‘𝐵)) ∧ (𝐵 ∈ TopBases ∧ 𝑣 ∈ (topGen‘𝐵))) → ((𝑥𝑢𝑥𝑣) → (∃𝑧𝐵 (𝑥𝑧𝑧𝑢) ∧ ∃𝑤𝐵 (𝑥𝑤𝑤𝑣))))
43 elin 3948 . . . . . . . . . 10 (𝑥 ∈ (𝑢𝑣) ↔ (𝑥𝑢𝑥𝑣))
44 reeanv 3255 . . . . . . . . . 10 (∃𝑧𝐵𝑤𝐵 ((𝑥𝑧𝑧𝑢) ∧ (𝑥𝑤𝑤𝑣)) ↔ (∃𝑧𝐵 (𝑥𝑧𝑧𝑢) ∧ ∃𝑤𝐵 (𝑥𝑤𝑤𝑣)))
4542, 43, 443imtr4g 285 . . . . . . . . 9 (((𝐵 ∈ TopBases ∧ 𝑢 ∈ (topGen‘𝐵)) ∧ (𝐵 ∈ TopBases ∧ 𝑣 ∈ (topGen‘𝐵))) → (𝑥 ∈ (𝑢𝑣) → ∃𝑧𝐵𝑤𝐵 ((𝑥𝑧𝑧𝑢) ∧ (𝑥𝑤𝑤𝑣))))
4645anandis 651 . . . . . . . 8 ((𝐵 ∈ TopBases ∧ (𝑢 ∈ (topGen‘𝐵) ∧ 𝑣 ∈ (topGen‘𝐵))) → (𝑥 ∈ (𝑢𝑣) → ∃𝑧𝐵𝑤𝐵 ((𝑥𝑧𝑧𝑢) ∧ (𝑥𝑤𝑤𝑣))))
47 elin 3948 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ (𝑧𝑤) ↔ (𝑥𝑧𝑥𝑤))
4847biimpri 218 . . . . . . . . . . . . . . . 16 ((𝑥𝑧𝑥𝑤) → 𝑥 ∈ (𝑧𝑤))
49 ss2in 3990 . . . . . . . . . . . . . . . 16 ((𝑧𝑢𝑤𝑣) → (𝑧𝑤) ⊆ (𝑢𝑣))
5048, 49anim12i 594 . . . . . . . . . . . . . . 15 (((𝑥𝑧𝑥𝑤) ∧ (𝑧𝑢𝑤𝑣)) → (𝑥 ∈ (𝑧𝑤) ∧ (𝑧𝑤) ⊆ (𝑢𝑣)))
5150an4s 633 . . . . . . . . . . . . . 14 (((𝑥𝑧𝑧𝑢) ∧ (𝑥𝑤𝑤𝑣)) → (𝑥 ∈ (𝑧𝑤) ∧ (𝑧𝑤) ⊆ (𝑢𝑣)))
52 basis2 20977 . . . . . . . . . . . . . . . . 17 (((𝐵 ∈ TopBases ∧ 𝑧𝐵) ∧ (𝑤𝐵𝑥 ∈ (𝑧𝑤))) → ∃𝑡𝐵 (𝑥𝑡𝑡 ⊆ (𝑧𝑤)))
5352adantllr 692 . . . . . . . . . . . . . . . 16 ((((𝐵 ∈ TopBases ∧ 𝑥 ∈ (𝑢𝑣)) ∧ 𝑧𝐵) ∧ (𝑤𝐵𝑥 ∈ (𝑧𝑤))) → ∃𝑡𝐵 (𝑥𝑡𝑡 ⊆ (𝑧𝑤)))
5453adantrrr 698 . . . . . . . . . . . . . . 15 ((((𝐵 ∈ TopBases ∧ 𝑥 ∈ (𝑢𝑣)) ∧ 𝑧𝐵) ∧ (𝑤𝐵 ∧ (𝑥 ∈ (𝑧𝑤) ∧ (𝑧𝑤) ⊆ (𝑢𝑣)))) → ∃𝑡𝐵 (𝑥𝑡𝑡 ⊆ (𝑧𝑤)))
55 sstr2 3760 . . . . . . . . . . . . . . . . . . . 20 (𝑡 ⊆ (𝑧𝑤) → ((𝑧𝑤) ⊆ (𝑢𝑣) → 𝑡 ⊆ (𝑢𝑣)))
5655com12 32 . . . . . . . . . . . . . . . . . . 19 ((𝑧𝑤) ⊆ (𝑢𝑣) → (𝑡 ⊆ (𝑧𝑤) → 𝑡 ⊆ (𝑢𝑣)))
5756anim2d 593 . . . . . . . . . . . . . . . . . 18 ((𝑧𝑤) ⊆ (𝑢𝑣) → ((𝑥𝑡𝑡 ⊆ (𝑧𝑤)) → (𝑥𝑡𝑡 ⊆ (𝑢𝑣))))
5857reximdv 3164 . . . . . . . . . . . . . . . . 17 ((𝑧𝑤) ⊆ (𝑢𝑣) → (∃𝑡𝐵 (𝑥𝑡𝑡 ⊆ (𝑧𝑤)) → ∃𝑡𝐵 (𝑥𝑡𝑡 ⊆ (𝑢𝑣))))
5958adantl 467 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ (𝑧𝑤) ∧ (𝑧𝑤) ⊆ (𝑢𝑣)) → (∃𝑡𝐵 (𝑥𝑡𝑡 ⊆ (𝑧𝑤)) → ∃𝑡𝐵 (𝑥𝑡𝑡 ⊆ (𝑢𝑣))))
6059ad2antll 702 . . . . . . . . . . . . . . 15 ((((𝐵 ∈ TopBases ∧ 𝑥 ∈ (𝑢𝑣)) ∧ 𝑧𝐵) ∧ (𝑤𝐵 ∧ (𝑥 ∈ (𝑧𝑤) ∧ (𝑧𝑤) ⊆ (𝑢𝑣)))) → (∃𝑡𝐵 (𝑥𝑡𝑡 ⊆ (𝑧𝑤)) → ∃𝑡𝐵 (𝑥𝑡𝑡 ⊆ (𝑢𝑣))))
6154, 60mpd 15 . . . . . . . . . . . . . 14 ((((𝐵 ∈ TopBases ∧ 𝑥 ∈ (𝑢𝑣)) ∧ 𝑧𝐵) ∧ (𝑤𝐵 ∧ (𝑥 ∈ (𝑧𝑤) ∧ (𝑧𝑤) ⊆ (𝑢𝑣)))) → ∃𝑡𝐵 (𝑥𝑡𝑡 ⊆ (𝑢𝑣)))
6251, 61sylanr2 656 . . . . . . . . . . . . 13 ((((𝐵 ∈ TopBases ∧ 𝑥 ∈ (𝑢𝑣)) ∧ 𝑧𝐵) ∧ (𝑤𝐵 ∧ ((𝑥𝑧𝑧𝑢) ∧ (𝑥𝑤𝑤𝑣)))) → ∃𝑡𝐵 (𝑥𝑡𝑡 ⊆ (𝑢𝑣)))
6362rexlimdvaa 3180 . . . . . . . . . . . 12 (((𝐵 ∈ TopBases ∧ 𝑥 ∈ (𝑢𝑣)) ∧ 𝑧𝐵) → (∃𝑤𝐵 ((𝑥𝑧𝑧𝑢) ∧ (𝑥𝑤𝑤𝑣)) → ∃𝑡𝐵 (𝑥𝑡𝑡 ⊆ (𝑢𝑣))))
6463rexlimdva 3179 . . . . . . . . . . 11 ((𝐵 ∈ TopBases ∧ 𝑥 ∈ (𝑢𝑣)) → (∃𝑧𝐵𝑤𝐵 ((𝑥𝑧𝑧𝑢) ∧ (𝑥𝑤𝑤𝑣)) → ∃𝑡𝐵 (𝑥𝑡𝑡 ⊆ (𝑢𝑣))))
6564ex 397 . . . . . . . . . 10 (𝐵 ∈ TopBases → (𝑥 ∈ (𝑢𝑣) → (∃𝑧𝐵𝑤𝐵 ((𝑥𝑧𝑧𝑢) ∧ (𝑥𝑤𝑤𝑣)) → ∃𝑡𝐵 (𝑥𝑡𝑡 ⊆ (𝑢𝑣)))))
6665a2d 29 . . . . . . . . 9 (𝐵 ∈ TopBases → ((𝑥 ∈ (𝑢𝑣) → ∃𝑧𝐵𝑤𝐵 ((𝑥𝑧𝑧𝑢) ∧ (𝑥𝑤𝑤𝑣))) → (𝑥 ∈ (𝑢𝑣) → ∃𝑡𝐵 (𝑥𝑡𝑡 ⊆ (𝑢𝑣)))))
6766imp 393 . . . . . . . 8 ((𝐵 ∈ TopBases ∧ (𝑥 ∈ (𝑢𝑣) → ∃𝑧𝐵𝑤𝐵 ((𝑥𝑧𝑧𝑢) ∧ (𝑥𝑤𝑤𝑣)))) → (𝑥 ∈ (𝑢𝑣) → ∃𝑡𝐵 (𝑥𝑡𝑡 ⊆ (𝑢𝑣))))
6846, 67syldan 573 . . . . . . 7 ((𝐵 ∈ TopBases ∧ (𝑢 ∈ (topGen‘𝐵) ∧ 𝑣 ∈ (topGen‘𝐵))) → (𝑥 ∈ (𝑢𝑣) → ∃𝑡𝐵 (𝑥𝑡𝑡 ⊆ (𝑢𝑣))))
6968ralrimiv 3114 . . . . . 6 ((𝐵 ∈ TopBases ∧ (𝑢 ∈ (topGen‘𝐵) ∧ 𝑣 ∈ (topGen‘𝐵))) → ∀𝑥 ∈ (𝑢𝑣)∃𝑡𝐵 (𝑥𝑡𝑡 ⊆ (𝑢𝑣)))
7033, 69jca 497 . . . . 5 ((𝐵 ∈ TopBases ∧ (𝑢 ∈ (topGen‘𝐵) ∧ 𝑣 ∈ (topGen‘𝐵))) → ((𝑢𝑣) ⊆ 𝐵 ∧ ∀𝑥 ∈ (𝑢𝑣)∃𝑡𝐵 (𝑥𝑡𝑡 ⊆ (𝑢𝑣))))
7170ex 397 . . . 4 (𝐵 ∈ TopBases → ((𝑢 ∈ (topGen‘𝐵) ∧ 𝑣 ∈ (topGen‘𝐵)) → ((𝑢𝑣) ⊆ 𝐵 ∧ ∀𝑥 ∈ (𝑢𝑣)∃𝑡𝐵 (𝑥𝑡𝑡 ⊆ (𝑢𝑣)))))
72 eltg2 20984 . . . 4 (𝐵 ∈ TopBases → ((𝑢𝑣) ∈ (topGen‘𝐵) ↔ ((𝑢𝑣) ⊆ 𝐵 ∧ ∀𝑥 ∈ (𝑢𝑣)∃𝑡𝐵 (𝑥𝑡𝑡 ⊆ (𝑢𝑣)))))
7371, 72sylibrd 249 . . 3 (𝐵 ∈ TopBases → ((𝑢 ∈ (topGen‘𝐵) ∧ 𝑣 ∈ (topGen‘𝐵)) → (𝑢𝑣) ∈ (topGen‘𝐵)))
7473ralrimivv 3119 . 2 (𝐵 ∈ TopBases → ∀𝑢 ∈ (topGen‘𝐵)∀𝑣 ∈ (topGen‘𝐵)(𝑢𝑣) ∈ (topGen‘𝐵))
75 fvex 6343 . . 3 (topGen‘𝐵) ∈ V
76 istopg 20921 . . 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 566 1 (𝐵 ∈ TopBases → (topGen‘𝐵) ∈ Top)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 382  wal 1629   = wceq 1631  wcel 2145  wral 3061  wrex 3062  Vcvv 3351  cin 3723  wss 3724   cuni 4575  cfv 6032  topGenctg 16307  Topctop 20919  TopBasesctb 20971
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-sep 4916  ax-nul 4924  ax-pow 4975  ax-pr 5035  ax-un 7097
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 829  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3353  df-sbc 3589  df-dif 3727  df-un 3729  df-in 3731  df-ss 3738  df-nul 4065  df-if 4227  df-pw 4300  df-sn 4318  df-pr 4320  df-op 4324  df-uni 4576  df-br 4788  df-opab 4848  df-mpt 4865  df-id 5158  df-xp 5256  df-rel 5257  df-cnv 5258  df-co 5259  df-dm 5260  df-iota 5995  df-fun 6034  df-fv 6040  df-topgen 16313  df-top 20920  df-bases 20972
This theorem is referenced by:  tgclb  20996  tgtopon  20997  bastop  21007  elcls3  21109  resttop  21186  leordtval2  21238  tgcmp  21426  2ndctop  21472  2ndcsb  21474  2ndcsep  21484  txtop  21594  pttop  21607  xkotop  21613  alexsubALT  22076  retop  22786  onsuctop  32770  kelac2lem  38161
  Copyright terms: Public domain W3C validator