Metamath Proof Explorer

Theorem istopon

Description: Property of being a topology with a given base set. (Contributed by Stefan O'Rear, 31-Jan-2015) (Revised by Mario Carneiro, 13-Aug-2015)

Ref Expression
Assertion istopon ⊢J∈TopOn⁡B↔J∈Top∧B=⋃J

Proof

Step Hyp Ref Expression
1 elfvex ⊢J∈TopOn⁡B→B∈V
2 uniexg ⊢J∈Top→⋃J∈V
3 eleq1 ⊢B=⋃J→B∈V↔⋃J∈V
4 2 3 syl5ibrcom ⊢J∈Top→B=⋃J→B∈V
5 4 imp ⊢J∈Top∧B=⋃J→B∈V
6 eqeq1 ⊢b=B→b=⋃j↔B=⋃j
7 6 rabbidv ⊢b=B→j∈Top|b=⋃j=j∈Top|B=⋃j
8 df-topon ⊢TopOn=b∈V⟼j∈Top|b=⋃j
9 vpwex ⊢𝒫b∈V
10 9 pwex ⊢𝒫𝒫b∈V
11 rabss ⊢j∈Top|b=⋃j⊆𝒫𝒫b↔∀j∈Topb=⋃j→j∈𝒫𝒫b
12 pwuni ⊢j⊆𝒫⋃j
13 pweq ⊢b=⋃j→𝒫b=𝒫⋃j
14 12 13 sseqtrrid ⊢b=⋃j→j⊆𝒫b
15 velpw ⊢j∈𝒫𝒫b↔j⊆𝒫b
16 14 15 sylibr ⊢b=⋃j→j∈𝒫𝒫b
17 16 a1i ⊢j∈Top→b=⋃j→j∈𝒫𝒫b
18 11 17 mprgbir ⊢j∈Top|b=⋃j⊆𝒫𝒫b
19 10 18 ssexi ⊢j∈Top|b=⋃j∈V
20 7 8 19 fvmpt3i ⊢B∈V→TopOn⁡B=j∈Top|B=⋃j
21 20 eleq2d ⊢B∈V→J∈TopOn⁡B↔J∈j∈Top|B=⋃j
22 unieq ⊢j=J→⋃j=⋃J
23 22 eqeq2d ⊢j=J→B=⋃j↔B=⋃J
24 23 elrab ⊢J∈j∈Top|B=⋃j↔J∈Top∧B=⋃J
25 21 24 bitrdi ⊢B∈V→J∈TopOn⁡B↔J∈Top∧B=⋃J
26 1 5 25 pm5.21nii ⊢J∈TopOn⁡B↔J∈Top∧B=⋃J