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