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 syl6bb ( 𝐵 ∈ V → ( 𝐽 ∈ ( TopOn ‘ 𝐵 ) ↔ ( 𝐽 ∈ Top ∧ 𝐵 = 𝐽 ) ) )
26 1 5 25 pm5.21nii ( 𝐽 ∈ ( TopOn ‘ 𝐵 ) ↔ ( 𝐽 ∈ Top ∧ 𝐵 = 𝐽 ) )