This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( 𝐽 ∈ ( TopOn ‘ 𝐵 ) ↔ ( 𝐽 ∈ Top ∧ 𝐵 = ∪ 𝐽 ) )

Proof

Step Hyp Ref Expression
1 elfvex ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝐵 ) → 𝐵 ∈ V )
2 uniexg ⊢ ( 𝐽 ∈ Top → ∪ 𝐽 ∈ V )
3 eleq1 ⊢ ( 𝐵 = ∪ 𝐽 → ( 𝐵 ∈ V ↔ ∪ 𝐽 ∈ V ) )
4 2 3 syl5ibrcom ⊢ ( 𝐽 ∈ Top → ( 𝐵 = ∪ 𝐽 → 𝐵 ∈ V ) )
5 4 imp ⊢ ( ( 𝐽 ∈ Top ∧ 𝐵 = ∪ 𝐽 ) → 𝐵 ∈ V )
6 eqeq1 ⊢ ( 𝑏 = 𝐵 → ( 𝑏 = ∪ 𝑗 ↔ 𝐵 = ∪ 𝑗 ) )
7 6 rabbidv ⊢ ( 𝑏 = 𝐵 → { 𝑗 ∈ Top ∣ 𝑏 = ∪ 𝑗 } = { 𝑗 ∈ Top ∣ 𝐵 = ∪ 𝑗 } )
8 df-topon ⊢ TopOn = ( 𝑏 ∈ V ↦ { 𝑗 ∈ Top ∣ 𝑏 = ∪ 𝑗 } )
9 vpwex ⊢ 𝒫 𝑏 ∈ V
10 9 pwex ⊢ 𝒫 𝒫 𝑏 ∈ V
11 rabss ⊢ ( { 𝑗 ∈ Top ∣ 𝑏 = ∪ 𝑗 } ⊆ 𝒫 𝒫 𝑏 ↔ ∀ 𝑗 ∈ Top ( 𝑏 = ∪ 𝑗 → 𝑗 ∈ 𝒫 𝒫 𝑏 ) )
12 pwuni ⊢ 𝑗 ⊆ 𝒫 ∪ 𝑗
13 pweq ⊢ ( 𝑏 = ∪ 𝑗 → 𝒫 𝑏 = 𝒫 ∪ 𝑗 )
14 12 13 sseqtrrid ⊢ ( 𝑏 = ∪ 𝑗 → 𝑗 ⊆ 𝒫 𝑏 )
15 velpw ⊢ ( 𝑗 ∈ 𝒫 𝒫 𝑏 ↔ 𝑗 ⊆ 𝒫 𝑏 )
16 14 15 sylibr ⊢ ( 𝑏 = ∪ 𝑗 → 𝑗 ∈ 𝒫 𝒫 𝑏 )
17 16 a1i ⊢ ( 𝑗 ∈ Top → ( 𝑏 = ∪ 𝑗 → 𝑗 ∈ 𝒫 𝒫 𝑏 ) )
18 11 17 mprgbir ⊢ { 𝑗 ∈ Top ∣ 𝑏 = ∪ 𝑗 } ⊆ 𝒫 𝒫 𝑏
19 10 18 ssexi ⊢ { 𝑗 ∈ Top ∣ 𝑏 = ∪ 𝑗 } ∈ V
20 7 8 19 fvmpt3i ⊢ ( 𝐵 ∈ V → ( TopOn ‘ 𝐵 ) = { 𝑗 ∈ Top ∣ 𝐵 = ∪ 𝑗 } )
21 20 eleq2d ⊢ ( 𝐵 ∈ V → ( 𝐽 ∈ ( TopOn ‘ 𝐵 ) ↔ 𝐽 ∈ { 𝑗 ∈ Top ∣ 𝐵 = ∪ 𝑗 } ) )
22 unieq ⊢ ( 𝑗 = 𝐽 → ∪ 𝑗 = ∪ 𝐽 )
23 22 eqeq2d ⊢ ( 𝑗 = 𝐽 → ( 𝐵 = ∪ 𝑗 ↔ 𝐵 = ∪ 𝐽 ) )
24 23 elrab ⊢ ( 𝐽 ∈ { 𝑗 ∈ Top ∣ 𝐵 = ∪ 𝑗 } ↔ ( 𝐽 ∈ Top ∧ 𝐵 = ∪ 𝐽 ) )
25 21 24 bitrdi ⊢ ( 𝐵 ∈ V → ( 𝐽 ∈ ( TopOn ‘ 𝐵 ) ↔ ( 𝐽 ∈ Top ∧ 𝐵 = ∪ 𝐽 ) ) )
26 1 5 25 pm5.21nii ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝐵 ) ↔ ( 𝐽 ∈ Top ∧ 𝐵 = ∪ 𝐽 ) )