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

Theorem tgcl 12160
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 3727 . . . . . . . 8 (𝑢 ⊆ (topGen‘𝐵) → 𝑢 (topGen‘𝐵))
21adantl 275 . . . . . . 7 ((𝐵 ∈ TopBases ∧ 𝑢 ⊆ (topGen‘𝐵)) → 𝑢 (topGen‘𝐵))
3 unitg 12158 . . . . . . . 8 (𝐵 ∈ TopBases → (topGen‘𝐵) = 𝐵)
43adantr 274 . . . . . . 7 ((𝐵 ∈ TopBases ∧ 𝑢 ⊆ (topGen‘𝐵)) → (topGen‘𝐵) = 𝐵)
52, 4sseqtrd 3105 . . . . . 6 ((𝐵 ∈ TopBases ∧ 𝑢 ⊆ (topGen‘𝐵)) → 𝑢 𝐵)
6 eluni2 3710 . . . . . . . 8 (𝑥 𝑢 ↔ ∃𝑡𝑢 𝑥𝑡)
7 ssel2 3062 . . . . . . . . . . . 12 ((𝑢 ⊆ (topGen‘𝐵) ∧ 𝑡𝑢) → 𝑡 ∈ (topGen‘𝐵))
8 eltg2b 12150 . . . . . . . . . . . . . . 15 (𝐵 ∈ TopBases → (𝑡 ∈ (topGen‘𝐵) ↔ ∀𝑥𝑡𝑦𝐵 (𝑥𝑦𝑦𝑡)))
9 rsp 2457 . . . . . . . . . . . . . . 15 (∀𝑥𝑡𝑦𝐵 (𝑥𝑦𝑦𝑡) → (𝑥𝑡 → ∃𝑦𝐵 (𝑥𝑦𝑦𝑡)))
108, 9syl6bi 162 . . . . . . . . . . . . . 14 (𝐵 ∈ TopBases → (𝑡 ∈ (topGen‘𝐵) → (𝑥𝑡 → ∃𝑦𝐵 (𝑥𝑦𝑦𝑡))))
1110imp31 254 . . . . . . . . . . . . 13 (((𝐵 ∈ TopBases ∧ 𝑡 ∈ (topGen‘𝐵)) ∧ 𝑥𝑡) → ∃𝑦𝐵 (𝑥𝑦𝑦𝑡))
1211an32s 542 . . . . . . . . . . . 12 (((𝐵 ∈ TopBases ∧ 𝑥𝑡) ∧ 𝑡 ∈ (topGen‘𝐵)) → ∃𝑦𝐵 (𝑥𝑦𝑦𝑡))
137, 12sylan2 284 . . . . . . . . . . 11 (((𝐵 ∈ TopBases ∧ 𝑥𝑡) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑡𝑢)) → ∃𝑦𝐵 (𝑥𝑦𝑦𝑡))
1413an42s 563 . . . . . . . . . 10 (((𝐵 ∈ TopBases ∧ 𝑢 ⊆ (topGen‘𝐵)) ∧ (𝑡𝑢𝑥𝑡)) → ∃𝑦𝐵 (𝑥𝑦𝑦𝑡))
15 elssuni 3734 . . . . . . . . . . . . . 14 (𝑡𝑢𝑡 𝑢)
16 sstr2 3074 . . . . . . . . . . . . . 14 (𝑦𝑡 → (𝑡 𝑢𝑦 𝑢))
1715, 16syl5com 29 . . . . . . . . . . . . 13 (𝑡𝑢 → (𝑦𝑡𝑦 𝑢))
1817anim2d 335 . . . . . . . . . . . 12 (𝑡𝑢 → ((𝑥𝑦𝑦𝑡) → (𝑥𝑦𝑦 𝑢)))
1918reximdv 2510 . . . . . . . . . . 11 (𝑡𝑢 → (∃𝑦𝐵 (𝑥𝑦𝑦𝑡) → ∃𝑦𝐵 (𝑥𝑦𝑦 𝑢)))
2019ad2antrl 481 . . . . . . . . . 10 (((𝐵 ∈ TopBases ∧ 𝑢 ⊆ (topGen‘𝐵)) ∧ (𝑡𝑢𝑥𝑡)) → (∃𝑦𝐵 (𝑥𝑦𝑦𝑡) → ∃𝑦𝐵 (𝑥𝑦𝑦 𝑢)))
2114, 20mpd 13 . . . . . . . . 9 (((𝐵 ∈ TopBases ∧ 𝑢 ⊆ (topGen‘𝐵)) ∧ (𝑡𝑢𝑥𝑡)) → ∃𝑦𝐵 (𝑥𝑦𝑦 𝑢))
2221rexlimdvaa 2527 . . . . . . . 8 ((𝐵 ∈ TopBases ∧ 𝑢 ⊆ (topGen‘𝐵)) → (∃𝑡𝑢 𝑥𝑡 → ∃𝑦𝐵 (𝑥𝑦𝑦 𝑢)))
236, 22syl5bi 151 . . . . . . 7 ((𝐵 ∈ TopBases ∧ 𝑢 ⊆ (topGen‘𝐵)) → (𝑥 𝑢 → ∃𝑦𝐵 (𝑥𝑦𝑦 𝑢)))
2423ralrimiv 2481 . . . . . 6 ((𝐵 ∈ TopBases ∧ 𝑢 ⊆ (topGen‘𝐵)) → ∀𝑥 𝑢𝑦𝐵 (𝑥𝑦𝑦 𝑢))
255, 24jca 304 . . . . 5 ((𝐵 ∈ TopBases ∧ 𝑢 ⊆ (topGen‘𝐵)) → ( 𝑢 𝐵 ∧ ∀𝑥 𝑢𝑦𝐵 (𝑥𝑦𝑦 𝑢)))
2625ex 114 . . . 4 (𝐵 ∈ TopBases → (𝑢 ⊆ (topGen‘𝐵) → ( 𝑢 𝐵 ∧ ∀𝑥 𝑢𝑦𝐵 (𝑥𝑦𝑦 𝑢))))
27 eltg2 12149 . . . 4 (𝐵 ∈ TopBases → ( 𝑢 ∈ (topGen‘𝐵) ↔ ( 𝑢 𝐵 ∧ ∀𝑥 𝑢𝑦𝐵 (𝑥𝑦𝑦 𝑢))))
2826, 27sylibrd 168 . . 3 (𝐵 ∈ TopBases → (𝑢 ⊆ (topGen‘𝐵) → 𝑢 ∈ (topGen‘𝐵)))
2928alrimiv 1830 . 2 (𝐵 ∈ TopBases → ∀𝑢(𝑢 ⊆ (topGen‘𝐵) → 𝑢 ∈ (topGen‘𝐵)))
30 inss1 3266 . . . . . . . 8 (𝑢𝑣) ⊆ 𝑢
31 tg1 12155 . . . . . . . 8 (𝑢 ∈ (topGen‘𝐵) → 𝑢 𝐵)
3230, 31sstrid 3078 . . . . . . 7 (𝑢 ∈ (topGen‘𝐵) → (𝑢𝑣) ⊆ 𝐵)
3332ad2antrl 481 . . . . . 6 ((𝐵 ∈ TopBases ∧ (𝑢 ∈ (topGen‘𝐵) ∧ 𝑣 ∈ (topGen‘𝐵))) → (𝑢𝑣) ⊆ 𝐵)
34 eltg2 12149 . . . . . . . . . . . . 13 (𝐵 ∈ TopBases → (𝑢 ∈ (topGen‘𝐵) ↔ (𝑢 𝐵 ∧ ∀𝑥𝑢𝑧𝐵 (𝑥𝑧𝑧𝑢))))
3534simplbda 381 . . . . . . . . . . . 12 ((𝐵 ∈ TopBases ∧ 𝑢 ∈ (topGen‘𝐵)) → ∀𝑥𝑢𝑧𝐵 (𝑥𝑧𝑧𝑢))
36 rsp 2457 . . . . . . . . . . . 12 (∀𝑥𝑢𝑧𝐵 (𝑥𝑧𝑧𝑢) → (𝑥𝑢 → ∃𝑧𝐵 (𝑥𝑧𝑧𝑢)))
3735, 36syl 14 . . . . . . . . . . 11 ((𝐵 ∈ TopBases ∧ 𝑢 ∈ (topGen‘𝐵)) → (𝑥𝑢 → ∃𝑧𝐵 (𝑥𝑧𝑧𝑢)))
38 eltg2 12149 . . . . . . . . . . . . 13 (𝐵 ∈ TopBases → (𝑣 ∈ (topGen‘𝐵) ↔ (𝑣 𝐵 ∧ ∀𝑥𝑣𝑤𝐵 (𝑥𝑤𝑤𝑣))))
3938simplbda 381 . . . . . . . . . . . 12 ((𝐵 ∈ TopBases ∧ 𝑣 ∈ (topGen‘𝐵)) → ∀𝑥𝑣𝑤𝐵 (𝑥𝑤𝑤𝑣))
40 rsp 2457 . . . . . . . . . . . 12 (∀𝑥𝑣𝑤𝐵 (𝑥𝑤𝑤𝑣) → (𝑥𝑣 → ∃𝑤𝐵 (𝑥𝑤𝑤𝑣)))
4139, 40syl 14 . . . . . . . . . . 11 ((𝐵 ∈ TopBases ∧ 𝑣 ∈ (topGen‘𝐵)) → (𝑥𝑣 → ∃𝑤𝐵 (𝑥𝑤𝑤𝑣)))
4237, 41im2anan9 572 . . . . . . . . . 10 (((𝐵 ∈ TopBases ∧ 𝑢 ∈ (topGen‘𝐵)) ∧ (𝐵 ∈ TopBases ∧ 𝑣 ∈ (topGen‘𝐵))) → ((𝑥𝑢𝑥𝑣) → (∃𝑧𝐵 (𝑥𝑧𝑧𝑢) ∧ ∃𝑤𝐵 (𝑥𝑤𝑤𝑣))))
43 elin 3229 . . . . . . . . . 10 (𝑥 ∈ (𝑢𝑣) ↔ (𝑥𝑢𝑥𝑣))
44 reeanv 2577 . . . . . . . . . 10 (∃𝑧𝐵𝑤𝐵 ((𝑥𝑧𝑧𝑢) ∧ (𝑥𝑤𝑤𝑣)) ↔ (∃𝑧𝐵 (𝑥𝑧𝑧𝑢) ∧ ∃𝑤𝐵 (𝑥𝑤𝑤𝑣)))
4542, 43, 443imtr4g 204 . . . . . . . . 9 (((𝐵 ∈ TopBases ∧ 𝑢 ∈ (topGen‘𝐵)) ∧ (𝐵 ∈ TopBases ∧ 𝑣 ∈ (topGen‘𝐵))) → (𝑥 ∈ (𝑢𝑣) → ∃𝑧𝐵𝑤𝐵 ((𝑥𝑧𝑧𝑢) ∧ (𝑥𝑤𝑤𝑣))))
4645anandis 566 . . . . . . . 8 ((𝐵 ∈ TopBases ∧ (𝑢 ∈ (topGen‘𝐵) ∧ 𝑣 ∈ (topGen‘𝐵))) → (𝑥 ∈ (𝑢𝑣) → ∃𝑧𝐵𝑤𝐵 ((𝑥𝑧𝑧𝑢) ∧ (𝑥𝑤𝑤𝑣))))
47 elin 3229 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ (𝑧𝑤) ↔ (𝑥𝑧𝑥𝑤))
4847biimpri 132 . . . . . . . . . . . . . . . 16 ((𝑥𝑧𝑥𝑤) → 𝑥 ∈ (𝑧𝑤))
49 ss2in 3274 . . . . . . . . . . . . . . . 16 ((𝑧𝑢𝑤𝑣) → (𝑧𝑤) ⊆ (𝑢𝑣))
5048, 49anim12i 336 . . . . . . . . . . . . . . 15 (((𝑥𝑧𝑥𝑤) ∧ (𝑧𝑢𝑤𝑣)) → (𝑥 ∈ (𝑧𝑤) ∧ (𝑧𝑤) ⊆ (𝑢𝑣)))
5150an4s 562 . . . . . . . . . . . . . 14 (((𝑥𝑧𝑧𝑢) ∧ (𝑥𝑤𝑤𝑣)) → (𝑥 ∈ (𝑧𝑤) ∧ (𝑧𝑤) ⊆ (𝑢𝑣)))
52 basis2 12142 . . . . . . . . . . . . . . . . 17 (((𝐵 ∈ TopBases ∧ 𝑧𝐵) ∧ (𝑤𝐵𝑥 ∈ (𝑧𝑤))) → ∃𝑡𝐵 (𝑥𝑡𝑡 ⊆ (𝑧𝑤)))
5352adantllr 472 . . . . . . . . . . . . . . . 16 ((((𝐵 ∈ TopBases ∧ 𝑥 ∈ (𝑢𝑣)) ∧ 𝑧𝐵) ∧ (𝑤𝐵𝑥 ∈ (𝑧𝑤))) → ∃𝑡𝐵 (𝑥𝑡𝑡 ⊆ (𝑧𝑤)))
5453adantrrr 478 . . . . . . . . . . . . . . 15 ((((𝐵 ∈ TopBases ∧ 𝑥 ∈ (𝑢𝑣)) ∧ 𝑧𝐵) ∧ (𝑤𝐵 ∧ (𝑥 ∈ (𝑧𝑤) ∧ (𝑧𝑤) ⊆ (𝑢𝑣)))) → ∃𝑡𝐵 (𝑥𝑡𝑡 ⊆ (𝑧𝑤)))
55 sstr2 3074 . . . . . . . . . . . . . . . . . . . 20 (𝑡 ⊆ (𝑧𝑤) → ((𝑧𝑤) ⊆ (𝑢𝑣) → 𝑡 ⊆ (𝑢𝑣)))
5655com12 30 . . . . . . . . . . . . . . . . . . 19 ((𝑧𝑤) ⊆ (𝑢𝑣) → (𝑡 ⊆ (𝑧𝑤) → 𝑡 ⊆ (𝑢𝑣)))
5756anim2d 335 . . . . . . . . . . . . . . . . . 18 ((𝑧𝑤) ⊆ (𝑢𝑣) → ((𝑥𝑡𝑡 ⊆ (𝑧𝑤)) → (𝑥𝑡𝑡 ⊆ (𝑢𝑣))))
5857reximdv 2510 . . . . . . . . . . . . . . . . 17 ((𝑧𝑤) ⊆ (𝑢𝑣) → (∃𝑡𝐵 (𝑥𝑡𝑡 ⊆ (𝑧𝑤)) → ∃𝑡𝐵 (𝑥𝑡𝑡 ⊆ (𝑢𝑣))))
5958adantl 275 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ (𝑧𝑤) ∧ (𝑧𝑤) ⊆ (𝑢𝑣)) → (∃𝑡𝐵 (𝑥𝑡𝑡 ⊆ (𝑧𝑤)) → ∃𝑡𝐵 (𝑥𝑡𝑡 ⊆ (𝑢𝑣))))
6059ad2antll 482 . . . . . . . . . . . . . . 15 ((((𝐵 ∈ TopBases ∧ 𝑥 ∈ (𝑢𝑣)) ∧ 𝑧𝐵) ∧ (𝑤𝐵 ∧ (𝑥 ∈ (𝑧𝑤) ∧ (𝑧𝑤) ⊆ (𝑢𝑣)))) → (∃𝑡𝐵 (𝑥𝑡𝑡 ⊆ (𝑧𝑤)) → ∃𝑡𝐵 (𝑥𝑡𝑡 ⊆ (𝑢𝑣))))
6154, 60mpd 13 . . . . . . . . . . . . . 14 ((((𝐵 ∈ TopBases ∧ 𝑥 ∈ (𝑢𝑣)) ∧ 𝑧𝐵) ∧ (𝑤𝐵 ∧ (𝑥 ∈ (𝑧𝑤) ∧ (𝑧𝑤) ⊆ (𝑢𝑣)))) → ∃𝑡𝐵 (𝑥𝑡𝑡 ⊆ (𝑢𝑣)))
6251, 61sylanr2 402 . . . . . . . . . . . . 13 ((((𝐵 ∈ TopBases ∧ 𝑥 ∈ (𝑢𝑣)) ∧ 𝑧𝐵) ∧ (𝑤𝐵 ∧ ((𝑥𝑧𝑧𝑢) ∧ (𝑥𝑤𝑤𝑣)))) → ∃𝑡𝐵 (𝑥𝑡𝑡 ⊆ (𝑢𝑣)))
6362rexlimdvaa 2527 . . . . . . . . . . . 12 (((𝐵 ∈ TopBases ∧ 𝑥 ∈ (𝑢𝑣)) ∧ 𝑧𝐵) → (∃𝑤𝐵 ((𝑥𝑧𝑧𝑢) ∧ (𝑥𝑤𝑤𝑣)) → ∃𝑡𝐵 (𝑥𝑡𝑡 ⊆ (𝑢𝑣))))
6463rexlimdva 2526 . . . . . . . . . . 11 ((𝐵 ∈ TopBases ∧ 𝑥 ∈ (𝑢𝑣)) → (∃𝑧𝐵𝑤𝐵 ((𝑥𝑧𝑧𝑢) ∧ (𝑥𝑤𝑤𝑣)) → ∃𝑡𝐵 (𝑥𝑡𝑡 ⊆ (𝑢𝑣))))
6564ex 114 . . . . . . . . . 10 (𝐵 ∈ TopBases → (𝑥 ∈ (𝑢𝑣) → (∃𝑧𝐵𝑤𝐵 ((𝑥𝑧𝑧𝑢) ∧ (𝑥𝑤𝑤𝑣)) → ∃𝑡𝐵 (𝑥𝑡𝑡 ⊆ (𝑢𝑣)))))
6665a2d 26 . . . . . . . . 9 (𝐵 ∈ TopBases → ((𝑥 ∈ (𝑢𝑣) → ∃𝑧𝐵𝑤𝐵 ((𝑥𝑧𝑧𝑢) ∧ (𝑥𝑤𝑤𝑣))) → (𝑥 ∈ (𝑢𝑣) → ∃𝑡𝐵 (𝑥𝑡𝑡 ⊆ (𝑢𝑣)))))
6766imp 123 . . . . . . . 8 ((𝐵 ∈ TopBases ∧ (𝑥 ∈ (𝑢𝑣) → ∃𝑧𝐵𝑤𝐵 ((𝑥𝑧𝑧𝑢) ∧ (𝑥𝑤𝑤𝑣)))) → (𝑥 ∈ (𝑢𝑣) → ∃𝑡𝐵 (𝑥𝑡𝑡 ⊆ (𝑢𝑣))))
6846, 67syldan 280 . . . . . . 7 ((𝐵 ∈ TopBases ∧ (𝑢 ∈ (topGen‘𝐵) ∧ 𝑣 ∈ (topGen‘𝐵))) → (𝑥 ∈ (𝑢𝑣) → ∃𝑡𝐵 (𝑥𝑡𝑡 ⊆ (𝑢𝑣))))
6968ralrimiv 2481 . . . . . 6 ((𝐵 ∈ TopBases ∧ (𝑢 ∈ (topGen‘𝐵) ∧ 𝑣 ∈ (topGen‘𝐵))) → ∀𝑥 ∈ (𝑢𝑣)∃𝑡𝐵 (𝑥𝑡𝑡 ⊆ (𝑢𝑣)))
7033, 69jca 304 . . . . 5 ((𝐵 ∈ TopBases ∧ (𝑢 ∈ (topGen‘𝐵) ∧ 𝑣 ∈ (topGen‘𝐵))) → ((𝑢𝑣) ⊆ 𝐵 ∧ ∀𝑥 ∈ (𝑢𝑣)∃𝑡𝐵 (𝑥𝑡𝑡 ⊆ (𝑢𝑣))))
7170ex 114 . . . 4 (𝐵 ∈ TopBases → ((𝑢 ∈ (topGen‘𝐵) ∧ 𝑣 ∈ (topGen‘𝐵)) → ((𝑢𝑣) ⊆ 𝐵 ∧ ∀𝑥 ∈ (𝑢𝑣)∃𝑡𝐵 (𝑥𝑡𝑡 ⊆ (𝑢𝑣)))))
72 eltg2 12149 . . . 4 (𝐵 ∈ TopBases → ((𝑢𝑣) ∈ (topGen‘𝐵) ↔ ((𝑢𝑣) ⊆ 𝐵 ∧ ∀𝑥 ∈ (𝑢𝑣)∃𝑡𝐵 (𝑥𝑡𝑡 ⊆ (𝑢𝑣)))))
7371, 72sylibrd 168 . . 3 (𝐵 ∈ TopBases → ((𝑢 ∈ (topGen‘𝐵) ∧ 𝑣 ∈ (topGen‘𝐵)) → (𝑢𝑣) ∈ (topGen‘𝐵)))
7473ralrimivv 2490 . 2 (𝐵 ∈ TopBases → ∀𝑢 ∈ (topGen‘𝐵)∀𝑣 ∈ (topGen‘𝐵)(𝑢𝑣) ∈ (topGen‘𝐵))
75 tgvalex 12146 . . 3 (𝐵 ∈ TopBases → (topGen‘𝐵) ∈ V)
76 istopg 12093 . . 3 ((topGen‘𝐵) ∈ V → ((topGen‘𝐵) ∈ Top ↔ (∀𝑢(𝑢 ⊆ (topGen‘𝐵) → 𝑢 ∈ (topGen‘𝐵)) ∧ ∀𝑢 ∈ (topGen‘𝐵)∀𝑣 ∈ (topGen‘𝐵)(𝑢𝑣) ∈ (topGen‘𝐵))))
7775, 76syl 14 . 2 (𝐵 ∈ TopBases → ((topGen‘𝐵) ∈ Top ↔ (∀𝑢(𝑢 ⊆ (topGen‘𝐵) → 𝑢 ∈ (topGen‘𝐵)) ∧ ∀𝑢 ∈ (topGen‘𝐵)∀𝑣 ∈ (topGen‘𝐵)(𝑢𝑣) ∈ (topGen‘𝐵))))
7829, 74, 77mpbir2and 913 1 (𝐵 ∈ TopBases → (topGen‘𝐵) ∈ Top)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  wb 104  wal 1314   = wceq 1316  wcel 1465  wral 2393  wrex 2394  Vcvv 2660  cin 3040  wss 3041   cuni 3706  cfv 5093  topGenctg 12062  Topctop 12091  TopBasesctb 12136
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 683  ax-5 1408  ax-7 1409  ax-gen 1410  ax-ie1 1454  ax-ie2 1455  ax-8 1467  ax-10 1468  ax-11 1469  ax-i12 1470  ax-bndl 1471  ax-4 1472  ax-13 1476  ax-14 1477  ax-17 1491  ax-i9 1495  ax-ial 1499  ax-i5r 1500  ax-ext 2099  ax-sep 4016  ax-pow 4068  ax-pr 4101  ax-un 4325
This theorem depends on definitions:  df-bi 116  df-3an 949  df-tru 1319  df-nf 1422  df-sb 1721  df-eu 1980  df-mo 1981  df-clab 2104  df-cleq 2110  df-clel 2113  df-nfc 2247  df-ral 2398  df-rex 2399  df-v 2662  df-sbc 2883  df-un 3045  df-in 3047  df-ss 3054  df-pw 3482  df-sn 3503  df-pr 3504  df-op 3506  df-uni 3707  df-br 3900  df-opab 3960  df-mpt 3961  df-id 4185  df-xp 4515  df-rel 4516  df-cnv 4517  df-co 4518  df-dm 4519  df-iota 5058  df-fun 5095  df-fv 5101  df-topgen 12068  df-top 12092  df-bases 12137
This theorem is referenced by:  tgclb  12161  tgtopon  12162  bastop  12171  resttop  12266  txtop  12356  mopnval  12538  retop  12620
  Copyright terms: Public domain W3C validator