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

Theorem tgcl 20697
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 4429 . . . . . . . 8 (𝑢 ⊆ (topGen‘𝐵) → 𝑢 (topGen‘𝐵))
21adantl 482 . . . . . . 7 ((𝐵 ∈ TopBases ∧ 𝑢 ⊆ (topGen‘𝐵)) → 𝑢 (topGen‘𝐵))
3 unitg 20695 . . . . . . . 8 (𝐵 ∈ TopBases → (topGen‘𝐵) = 𝐵)
43adantr 481 . . . . . . 7 ((𝐵 ∈ TopBases ∧ 𝑢 ⊆ (topGen‘𝐵)) → (topGen‘𝐵) = 𝐵)
52, 4sseqtrd 3625 . . . . . 6 ((𝐵 ∈ TopBases ∧ 𝑢 ⊆ (topGen‘𝐵)) → 𝑢 𝐵)
6 eluni2 4411 . . . . . . . 8 (𝑥 𝑢 ↔ ∃𝑡𝑢 𝑥𝑡)
7 ssel2 3582 . . . . . . . . . . . 12 ((𝑢 ⊆ (topGen‘𝐵) ∧ 𝑡𝑢) → 𝑡 ∈ (topGen‘𝐵))
8 eltg2b 20687 . . . . . . . . . . . . . . 15 (𝐵 ∈ TopBases → (𝑡 ∈ (topGen‘𝐵) ↔ ∀𝑥𝑡𝑦𝐵 (𝑥𝑦𝑦𝑡)))
9 rsp 2924 . . . . . . . . . . . . . . 15 (∀𝑥𝑡𝑦𝐵 (𝑥𝑦𝑦𝑡) → (𝑥𝑡 → ∃𝑦𝐵 (𝑥𝑦𝑦𝑡)))
108, 9syl6bi 243 . . . . . . . . . . . . . 14 (𝐵 ∈ TopBases → (𝑡 ∈ (topGen‘𝐵) → (𝑥𝑡 → ∃𝑦𝐵 (𝑥𝑦𝑦𝑡))))
1110imp31 448 . . . . . . . . . . . . 13 (((𝐵 ∈ TopBases ∧ 𝑡 ∈ (topGen‘𝐵)) ∧ 𝑥𝑡) → ∃𝑦𝐵 (𝑥𝑦𝑦𝑡))
1211an32s 845 . . . . . . . . . . . 12 (((𝐵 ∈ TopBases ∧ 𝑥𝑡) ∧ 𝑡 ∈ (topGen‘𝐵)) → ∃𝑦𝐵 (𝑥𝑦𝑦𝑡))
137, 12sylan2 491 . . . . . . . . . . 11 (((𝐵 ∈ TopBases ∧ 𝑥𝑡) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑡𝑢)) → ∃𝑦𝐵 (𝑥𝑦𝑦𝑡))
1413an42s 869 . . . . . . . . . 10 (((𝐵 ∈ TopBases ∧ 𝑢 ⊆ (topGen‘𝐵)) ∧ (𝑡𝑢𝑥𝑡)) → ∃𝑦𝐵 (𝑥𝑦𝑦𝑡))
15 elssuni 4438 . . . . . . . . . . . . . 14 (𝑡𝑢𝑡 𝑢)
16 sstr2 3594 . . . . . . . . . . . . . 14 (𝑦𝑡 → (𝑡 𝑢𝑦 𝑢))
1715, 16syl5com 31 . . . . . . . . . . . . 13 (𝑡𝑢 → (𝑦𝑡𝑦 𝑢))
1817anim2d 588 . . . . . . . . . . . 12 (𝑡𝑢 → ((𝑥𝑦𝑦𝑡) → (𝑥𝑦𝑦 𝑢)))
1918reximdv 3011 . . . . . . . . . . 11 (𝑡𝑢 → (∃𝑦𝐵 (𝑥𝑦𝑦𝑡) → ∃𝑦𝐵 (𝑥𝑦𝑦 𝑢)))
2019ad2antrl 763 . . . . . . . . . 10 (((𝐵 ∈ TopBases ∧ 𝑢 ⊆ (topGen‘𝐵)) ∧ (𝑡𝑢𝑥𝑡)) → (∃𝑦𝐵 (𝑥𝑦𝑦𝑡) → ∃𝑦𝐵 (𝑥𝑦𝑦 𝑢)))
2114, 20mpd 15 . . . . . . . . 9 (((𝐵 ∈ TopBases ∧ 𝑢 ⊆ (topGen‘𝐵)) ∧ (𝑡𝑢𝑥𝑡)) → ∃𝑦𝐵 (𝑥𝑦𝑦 𝑢))
2221rexlimdvaa 3026 . . . . . . . 8 ((𝐵 ∈ TopBases ∧ 𝑢 ⊆ (topGen‘𝐵)) → (∃𝑡𝑢 𝑥𝑡 → ∃𝑦𝐵 (𝑥𝑦𝑦 𝑢)))
236, 22syl5bi 232 . . . . . . 7 ((𝐵 ∈ TopBases ∧ 𝑢 ⊆ (topGen‘𝐵)) → (𝑥 𝑢 → ∃𝑦𝐵 (𝑥𝑦𝑦 𝑢)))
2423ralrimiv 2960 . . . . . 6 ((𝐵 ∈ TopBases ∧ 𝑢 ⊆ (topGen‘𝐵)) → ∀𝑥 𝑢𝑦𝐵 (𝑥𝑦𝑦 𝑢))
255, 24jca 554 . . . . 5 ((𝐵 ∈ TopBases ∧ 𝑢 ⊆ (topGen‘𝐵)) → ( 𝑢 𝐵 ∧ ∀𝑥 𝑢𝑦𝐵 (𝑥𝑦𝑦 𝑢)))
2625ex 450 . . . 4 (𝐵 ∈ TopBases → (𝑢 ⊆ (topGen‘𝐵) → ( 𝑢 𝐵 ∧ ∀𝑥 𝑢𝑦𝐵 (𝑥𝑦𝑦 𝑢))))
27 eltg2 20686 . . . 4 (𝐵 ∈ TopBases → ( 𝑢 ∈ (topGen‘𝐵) ↔ ( 𝑢 𝐵 ∧ ∀𝑥 𝑢𝑦𝐵 (𝑥𝑦𝑦 𝑢))))
2826, 27sylibrd 249 . . 3 (𝐵 ∈ TopBases → (𝑢 ⊆ (topGen‘𝐵) → 𝑢 ∈ (topGen‘𝐵)))
2928alrimiv 1852 . 2 (𝐵 ∈ TopBases → ∀𝑢(𝑢 ⊆ (topGen‘𝐵) → 𝑢 ∈ (topGen‘𝐵)))
30 inss1 3816 . . . . . . . 8 (𝑢𝑣) ⊆ 𝑢
31 tg1 20692 . . . . . . . 8 (𝑢 ∈ (topGen‘𝐵) → 𝑢 𝐵)
3230, 31syl5ss 3598 . . . . . . 7 (𝑢 ∈ (topGen‘𝐵) → (𝑢𝑣) ⊆ 𝐵)
3332ad2antrl 763 . . . . . 6 ((𝐵 ∈ TopBases ∧ (𝑢 ∈ (topGen‘𝐵) ∧ 𝑣 ∈ (topGen‘𝐵))) → (𝑢𝑣) ⊆ 𝐵)
34 eltg2 20686 . . . . . . . . . . . . 13 (𝐵 ∈ TopBases → (𝑢 ∈ (topGen‘𝐵) ↔ (𝑢 𝐵 ∧ ∀𝑥𝑢𝑧𝐵 (𝑥𝑧𝑧𝑢))))
3534simplbda 653 . . . . . . . . . . . 12 ((𝐵 ∈ TopBases ∧ 𝑢 ∈ (topGen‘𝐵)) → ∀𝑥𝑢𝑧𝐵 (𝑥𝑧𝑧𝑢))
36 rsp 2924 . . . . . . . . . . . 12 (∀𝑥𝑢𝑧𝐵 (𝑥𝑧𝑧𝑢) → (𝑥𝑢 → ∃𝑧𝐵 (𝑥𝑧𝑧𝑢)))
3735, 36syl 17 . . . . . . . . . . 11 ((𝐵 ∈ TopBases ∧ 𝑢 ∈ (topGen‘𝐵)) → (𝑥𝑢 → ∃𝑧𝐵 (𝑥𝑧𝑧𝑢)))
38 eltg2 20686 . . . . . . . . . . . . 13 (𝐵 ∈ TopBases → (𝑣 ∈ (topGen‘𝐵) ↔ (𝑣 𝐵 ∧ ∀𝑥𝑣𝑤𝐵 (𝑥𝑤𝑤𝑣))))
3938simplbda 653 . . . . . . . . . . . 12 ((𝐵 ∈ TopBases ∧ 𝑣 ∈ (topGen‘𝐵)) → ∀𝑥𝑣𝑤𝐵 (𝑥𝑤𝑤𝑣))
40 rsp 2924 . . . . . . . . . . . 12 (∀𝑥𝑣𝑤𝐵 (𝑥𝑤𝑤𝑣) → (𝑥𝑣 → ∃𝑤𝐵 (𝑥𝑤𝑤𝑣)))
4139, 40syl 17 . . . . . . . . . . 11 ((𝐵 ∈ TopBases ∧ 𝑣 ∈ (topGen‘𝐵)) → (𝑥𝑣 → ∃𝑤𝐵 (𝑥𝑤𝑤𝑣)))
4237, 41im2anan9 879 . . . . . . . . . 10 (((𝐵 ∈ TopBases ∧ 𝑢 ∈ (topGen‘𝐵)) ∧ (𝐵 ∈ TopBases ∧ 𝑣 ∈ (topGen‘𝐵))) → ((𝑥𝑢𝑥𝑣) → (∃𝑧𝐵 (𝑥𝑧𝑧𝑢) ∧ ∃𝑤𝐵 (𝑥𝑤𝑤𝑣))))
43 elin 3779 . . . . . . . . . 10 (𝑥 ∈ (𝑢𝑣) ↔ (𝑥𝑢𝑥𝑣))
44 reeanv 3100 . . . . . . . . . 10 (∃𝑧𝐵𝑤𝐵 ((𝑥𝑧𝑧𝑢) ∧ (𝑥𝑤𝑤𝑣)) ↔ (∃𝑧𝐵 (𝑥𝑧𝑧𝑢) ∧ ∃𝑤𝐵 (𝑥𝑤𝑤𝑣)))
4542, 43, 443imtr4g 285 . . . . . . . . 9 (((𝐵 ∈ TopBases ∧ 𝑢 ∈ (topGen‘𝐵)) ∧ (𝐵 ∈ TopBases ∧ 𝑣 ∈ (topGen‘𝐵))) → (𝑥 ∈ (𝑢𝑣) → ∃𝑧𝐵𝑤𝐵 ((𝑥𝑧𝑧𝑢) ∧ (𝑥𝑤𝑤𝑣))))
4645anandis 872 . . . . . . . 8 ((𝐵 ∈ TopBases ∧ (𝑢 ∈ (topGen‘𝐵) ∧ 𝑣 ∈ (topGen‘𝐵))) → (𝑥 ∈ (𝑢𝑣) → ∃𝑧𝐵𝑤𝐵 ((𝑥𝑧𝑧𝑢) ∧ (𝑥𝑤𝑤𝑣))))
47 elin 3779 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ (𝑧𝑤) ↔ (𝑥𝑧𝑥𝑤))
4847biimpri 218 . . . . . . . . . . . . . . . 16 ((𝑥𝑧𝑥𝑤) → 𝑥 ∈ (𝑧𝑤))
49 ss2in 3823 . . . . . . . . . . . . . . . 16 ((𝑧𝑢𝑤𝑣) → (𝑧𝑤) ⊆ (𝑢𝑣))
5048, 49anim12i 589 . . . . . . . . . . . . . . 15 (((𝑥𝑧𝑥𝑤) ∧ (𝑧𝑢𝑤𝑣)) → (𝑥 ∈ (𝑧𝑤) ∧ (𝑧𝑤) ⊆ (𝑢𝑣)))
5150an4s 868 . . . . . . . . . . . . . 14 (((𝑥𝑧𝑧𝑢) ∧ (𝑥𝑤𝑤𝑣)) → (𝑥 ∈ (𝑧𝑤) ∧ (𝑧𝑤) ⊆ (𝑢𝑣)))
52 basis2 20679 . . . . . . . . . . . . . . . . 17 (((𝐵 ∈ TopBases ∧ 𝑧𝐵) ∧ (𝑤𝐵𝑥 ∈ (𝑧𝑤))) → ∃𝑡𝐵 (𝑥𝑡𝑡 ⊆ (𝑧𝑤)))
5352adantllr 754 . . . . . . . . . . . . . . . 16 ((((𝐵 ∈ TopBases ∧ 𝑥 ∈ (𝑢𝑣)) ∧ 𝑧𝐵) ∧ (𝑤𝐵𝑥 ∈ (𝑧𝑤))) → ∃𝑡𝐵 (𝑥𝑡𝑡 ⊆ (𝑧𝑤)))
5453adantrrr 760 . . . . . . . . . . . . . . 15 ((((𝐵 ∈ TopBases ∧ 𝑥 ∈ (𝑢𝑣)) ∧ 𝑧𝐵) ∧ (𝑤𝐵 ∧ (𝑥 ∈ (𝑧𝑤) ∧ (𝑧𝑤) ⊆ (𝑢𝑣)))) → ∃𝑡𝐵 (𝑥𝑡𝑡 ⊆ (𝑧𝑤)))
55 sstr2 3594 . . . . . . . . . . . . . . . . . . . 20 (𝑡 ⊆ (𝑧𝑤) → ((𝑧𝑤) ⊆ (𝑢𝑣) → 𝑡 ⊆ (𝑢𝑣)))
5655com12 32 . . . . . . . . . . . . . . . . . . 19 ((𝑧𝑤) ⊆ (𝑢𝑣) → (𝑡 ⊆ (𝑧𝑤) → 𝑡 ⊆ (𝑢𝑣)))
5756anim2d 588 . . . . . . . . . . . . . . . . . 18 ((𝑧𝑤) ⊆ (𝑢𝑣) → ((𝑥𝑡𝑡 ⊆ (𝑧𝑤)) → (𝑥𝑡𝑡 ⊆ (𝑢𝑣))))
5857reximdv 3011 . . . . . . . . . . . . . . . . 17 ((𝑧𝑤) ⊆ (𝑢𝑣) → (∃𝑡𝐵 (𝑥𝑡𝑡 ⊆ (𝑧𝑤)) → ∃𝑡𝐵 (𝑥𝑡𝑡 ⊆ (𝑢𝑣))))
5958adantl 482 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ (𝑧𝑤) ∧ (𝑧𝑤) ⊆ (𝑢𝑣)) → (∃𝑡𝐵 (𝑥𝑡𝑡 ⊆ (𝑧𝑤)) → ∃𝑡𝐵 (𝑥𝑡𝑡 ⊆ (𝑢𝑣))))
6059ad2antll 764 . . . . . . . . . . . . . . 15 ((((𝐵 ∈ TopBases ∧ 𝑥 ∈ (𝑢𝑣)) ∧ 𝑧𝐵) ∧ (𝑤𝐵 ∧ (𝑥 ∈ (𝑧𝑤) ∧ (𝑧𝑤) ⊆ (𝑢𝑣)))) → (∃𝑡𝐵 (𝑥𝑡𝑡 ⊆ (𝑧𝑤)) → ∃𝑡𝐵 (𝑥𝑡𝑡 ⊆ (𝑢𝑣))))
6154, 60mpd 15 . . . . . . . . . . . . . 14 ((((𝐵 ∈ TopBases ∧ 𝑥 ∈ (𝑢𝑣)) ∧ 𝑧𝐵) ∧ (𝑤𝐵 ∧ (𝑥 ∈ (𝑧𝑤) ∧ (𝑧𝑤) ⊆ (𝑢𝑣)))) → ∃𝑡𝐵 (𝑥𝑡𝑡 ⊆ (𝑢𝑣)))
6251, 61sylanr2 684 . . . . . . . . . . . . 13 ((((𝐵 ∈ TopBases ∧ 𝑥 ∈ (𝑢𝑣)) ∧ 𝑧𝐵) ∧ (𝑤𝐵 ∧ ((𝑥𝑧𝑧𝑢) ∧ (𝑥𝑤𝑤𝑣)))) → ∃𝑡𝐵 (𝑥𝑡𝑡 ⊆ (𝑢𝑣)))
6362rexlimdvaa 3026 . . . . . . . . . . . 12 (((𝐵 ∈ TopBases ∧ 𝑥 ∈ (𝑢𝑣)) ∧ 𝑧𝐵) → (∃𝑤𝐵 ((𝑥𝑧𝑧𝑢) ∧ (𝑥𝑤𝑤𝑣)) → ∃𝑡𝐵 (𝑥𝑡𝑡 ⊆ (𝑢𝑣))))
6463rexlimdva 3025 . . . . . . . . . . 11 ((𝐵 ∈ TopBases ∧ 𝑥 ∈ (𝑢𝑣)) → (∃𝑧𝐵𝑤𝐵 ((𝑥𝑧𝑧𝑢) ∧ (𝑥𝑤𝑤𝑣)) → ∃𝑡𝐵 (𝑥𝑡𝑡 ⊆ (𝑢𝑣))))
6564ex 450 . . . . . . . . . 10 (𝐵 ∈ TopBases → (𝑥 ∈ (𝑢𝑣) → (∃𝑧𝐵𝑤𝐵 ((𝑥𝑧𝑧𝑢) ∧ (𝑥𝑤𝑤𝑣)) → ∃𝑡𝐵 (𝑥𝑡𝑡 ⊆ (𝑢𝑣)))))
6665a2d 29 . . . . . . . . 9 (𝐵 ∈ TopBases → ((𝑥 ∈ (𝑢𝑣) → ∃𝑧𝐵𝑤𝐵 ((𝑥𝑧𝑧𝑢) ∧ (𝑥𝑤𝑤𝑣))) → (𝑥 ∈ (𝑢𝑣) → ∃𝑡𝐵 (𝑥𝑡𝑡 ⊆ (𝑢𝑣)))))
6766imp 445 . . . . . . . 8 ((𝐵 ∈ TopBases ∧ (𝑥 ∈ (𝑢𝑣) → ∃𝑧𝐵𝑤𝐵 ((𝑥𝑧𝑧𝑢) ∧ (𝑥𝑤𝑤𝑣)))) → (𝑥 ∈ (𝑢𝑣) → ∃𝑡𝐵 (𝑥𝑡𝑡 ⊆ (𝑢𝑣))))
6846, 67syldan 487 . . . . . . 7 ((𝐵 ∈ TopBases ∧ (𝑢 ∈ (topGen‘𝐵) ∧ 𝑣 ∈ (topGen‘𝐵))) → (𝑥 ∈ (𝑢𝑣) → ∃𝑡𝐵 (𝑥𝑡𝑡 ⊆ (𝑢𝑣))))
6968ralrimiv 2960 . . . . . 6 ((𝐵 ∈ TopBases ∧ (𝑢 ∈ (topGen‘𝐵) ∧ 𝑣 ∈ (topGen‘𝐵))) → ∀𝑥 ∈ (𝑢𝑣)∃𝑡𝐵 (𝑥𝑡𝑡 ⊆ (𝑢𝑣)))
7033, 69jca 554 . . . . 5 ((𝐵 ∈ TopBases ∧ (𝑢 ∈ (topGen‘𝐵) ∧ 𝑣 ∈ (topGen‘𝐵))) → ((𝑢𝑣) ⊆ 𝐵 ∧ ∀𝑥 ∈ (𝑢𝑣)∃𝑡𝐵 (𝑥𝑡𝑡 ⊆ (𝑢𝑣))))
7170ex 450 . . . 4 (𝐵 ∈ TopBases → ((𝑢 ∈ (topGen‘𝐵) ∧ 𝑣 ∈ (topGen‘𝐵)) → ((𝑢𝑣) ⊆ 𝐵 ∧ ∀𝑥 ∈ (𝑢𝑣)∃𝑡𝐵 (𝑥𝑡𝑡 ⊆ (𝑢𝑣)))))
72 eltg2 20686 . . . 4 (𝐵 ∈ TopBases → ((𝑢𝑣) ∈ (topGen‘𝐵) ↔ ((𝑢𝑣) ⊆ 𝐵 ∧ ∀𝑥 ∈ (𝑢𝑣)∃𝑡𝐵 (𝑥𝑡𝑡 ⊆ (𝑢𝑣)))))
7371, 72sylibrd 249 . . 3 (𝐵 ∈ TopBases → ((𝑢 ∈ (topGen‘𝐵) ∧ 𝑣 ∈ (topGen‘𝐵)) → (𝑢𝑣) ∈ (topGen‘𝐵)))
7473ralrimivv 2965 . 2 (𝐵 ∈ TopBases → ∀𝑢 ∈ (topGen‘𝐵)∀𝑣 ∈ (topGen‘𝐵)(𝑢𝑣) ∈ (topGen‘𝐵))
75 fvex 6163 . . 3 (topGen‘𝐵) ∈ V
76 istopg 20632 . . 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 697 1 (𝐵 ∈ TopBases → (topGen‘𝐵) ∈ Top)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384  wal 1478   = wceq 1480  wcel 1987  wral 2907  wrex 2908  Vcvv 3189  cin 3558  wss 3559   cuni 4407  cfv 5852  topGenctg 16030  Topctop 20630  TopBasesctb 20673
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4746  ax-nul 4754  ax-pow 4808  ax-pr 4872  ax-un 6909
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-ral 2912  df-rex 2913  df-rab 2916  df-v 3191  df-sbc 3422  df-dif 3562  df-un 3564  df-in 3566  df-ss 3573  df-nul 3897  df-if 4064  df-pw 4137  df-sn 4154  df-pr 4156  df-op 4160  df-uni 4408  df-br 4619  df-opab 4679  df-mpt 4680  df-id 4994  df-xp 5085  df-rel 5086  df-cnv 5087  df-co 5088  df-dm 5089  df-iota 5815  df-fun 5854  df-fv 5860  df-topgen 16036  df-top 20631  df-bases 20674
This theorem is referenced by:  tgclb  20698  tgtopon  20699  bastop  20709  elcls3  20810  resttop  20887  leordtval2  20939  tgcmp  21127  2ndctop  21173  2ndcsb  21175  2ndcsep  21185  txtop  21295  pttop  21308  xkotop  21314  alexsubALT  21778  retop  22488  onsuctop  32109  kelac2lem  37149
  Copyright terms: Public domain W3C validator