Metamath Proof Explorer


Theorem toprntopon

Description: A topology is the same thing as a topology on a set (variable-free version). (Contributed by BJ, 27-Apr-2021)

Ref Expression
Assertion toprntopon Top = ran TopOn

Proof

Step Hyp Ref Expression
1 toptopon2 x Top x TopOn x
2 fvex TopOn x V
3 eleq2 y = TopOn x x y x TopOn x
4 eleq1 y = TopOn x y ran TopOn TopOn x ran TopOn
5 3 4 anbi12d y = TopOn x x y y ran TopOn x TopOn x TopOn x ran TopOn
6 simpl x TopOn x TopOn x ran TopOn x TopOn x
7 fntopon TopOn Fn V
8 vuniex x V
9 fnfvelrn TopOn Fn V x V TopOn x ran TopOn
10 7 8 9 mp2an TopOn x ran TopOn
11 10 jctr x TopOn x x TopOn x TopOn x ran TopOn
12 6 11 impbii x TopOn x TopOn x ran TopOn x TopOn x
13 5 12 bitrdi y = TopOn x x y y ran TopOn x TopOn x
14 2 13 spcev x TopOn x y x y y ran TopOn
15 1 14 sylbi x Top y x y y ran TopOn
16 funtopon Fun TopOn
17 elrnrexdm Fun TopOn y ran TopOn z dom TopOn y = TopOn z
18 16 17 ax-mp y ran TopOn z dom TopOn y = TopOn z
19 rexex z dom TopOn y = TopOn z z y = TopOn z
20 18 19 syl y ran TopOn z y = TopOn z
21 19.42v z x y y = TopOn z x y z y = TopOn z
22 eqimss y = TopOn z y TopOn z
23 22 sseld y = TopOn z x y x TopOn z
24 23 impcom x y y = TopOn z x TopOn z
25 24 eximi z x y y = TopOn z z x TopOn z
26 21 25 sylbir x y z y = TopOn z z x TopOn z
27 20 26 sylan2 x y y ran TopOn z x TopOn z
28 topontop x TopOn z x Top
29 28 exlimiv z x TopOn z x Top
30 27 29 syl x y y ran TopOn x Top
31 30 exlimiv y x y y ran TopOn x Top
32 15 31 impbii x Top y x y y ran TopOn
33 eluni x ran TopOn y x y y ran TopOn
34 32 33 bitr4i x Top x ran TopOn
35 34 eqriv Top = ran TopOn