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 = U. ran TopOn

Proof

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