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 bitrdi B V J TopOn B J Top B = J
26 1 5 25 pm5.21nii J TopOn B J Top B = J