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 ∈ Top b = ⋃ 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 syl6bb ⊢ B ∈ V → J ∈ TopOn ⁡ B ↔ J ∈ Top ∧ B = ⋃ J
26 1 5 25 pm5.21nii ⊢ J ∈ TopOn ⁡ B ↔ J ∈ Top ∧ B = ⋃ J