Metamath Proof Explorer


Theorem tgqtop

Description: An injection maps generated topologies to each other. (Contributed by Mario Carneiro, 27-Aug-2015)

Ref Expression
Hypothesis qtopcmp.1
|- X = U. J
Assertion tgqtop
|- ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) -> ( ( topGen ` J ) qTop F ) = ( topGen ` ( J qTop F ) ) )

Proof

Step Hyp Ref Expression
1 qtopcmp.1
 |-  X = U. J
2 f1ocnv
 |-  ( F : X -1-1-onto-> Y -> `' F : Y -1-1-onto-> X )
3 f1ofun
 |-  ( `' F : Y -1-1-onto-> X -> Fun `' F )
4 2 3 syl
 |-  ( F : X -1-1-onto-> Y -> Fun `' F )
5 4 ad2antlr
 |-  ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ x C_ Y ) -> Fun `' F )
6 simpr
 |-  ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ x C_ Y ) -> x C_ Y )
7 df-rn
 |-  ran F = dom `' F
8 f1ofo
 |-  ( F : X -1-1-onto-> Y -> F : X -onto-> Y )
9 8 ad2antlr
 |-  ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ x C_ Y ) -> F : X -onto-> Y )
10 forn
 |-  ( F : X -onto-> Y -> ran F = Y )
11 9 10 syl
 |-  ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ x C_ Y ) -> ran F = Y )
12 7 11 eqtr3id
 |-  ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ x C_ Y ) -> dom `' F = Y )
13 6 12 sseqtrrd
 |-  ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ x C_ Y ) -> x C_ dom `' F )
14 funimass4
 |-  ( ( Fun `' F /\ x C_ dom `' F ) -> ( ( `' F " x ) C_ U. ( J i^i ~P ( `' F " x ) ) <-> A. y e. x ( `' F ` y ) e. U. ( J i^i ~P ( `' F " x ) ) ) )
15 5 13 14 syl2anc
 |-  ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ x C_ Y ) -> ( ( `' F " x ) C_ U. ( J i^i ~P ( `' F " x ) ) <-> A. y e. x ( `' F ` y ) e. U. ( J i^i ~P ( `' F " x ) ) ) )
16 dfss3
 |-  ( x C_ U. ( ( J qTop F ) i^i ~P x ) <-> A. y e. x y e. U. ( ( J qTop F ) i^i ~P x ) )
17 simprl
 |-  ( ( ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ x C_ Y ) /\ y e. x ) /\ ( z e. ( ( J qTop F ) i^i ~P x ) /\ y e. z ) ) -> z e. ( ( J qTop F ) i^i ~P x ) )
18 17 elin1d
 |-  ( ( ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ x C_ Y ) /\ y e. x ) /\ ( z e. ( ( J qTop F ) i^i ~P x ) /\ y e. z ) ) -> z e. ( J qTop F ) )
19 1 elqtop2
 |-  ( ( J e. TopBases /\ F : X -onto-> Y ) -> ( z e. ( J qTop F ) <-> ( z C_ Y /\ ( `' F " z ) e. J ) ) )
20 8 19 sylan2
 |-  ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) -> ( z e. ( J qTop F ) <-> ( z C_ Y /\ ( `' F " z ) e. J ) ) )
21 20 ad3antrrr
 |-  ( ( ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ x C_ Y ) /\ y e. x ) /\ ( z e. ( ( J qTop F ) i^i ~P x ) /\ y e. z ) ) -> ( z e. ( J qTop F ) <-> ( z C_ Y /\ ( `' F " z ) e. J ) ) )
22 18 21 mpbid
 |-  ( ( ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ x C_ Y ) /\ y e. x ) /\ ( z e. ( ( J qTop F ) i^i ~P x ) /\ y e. z ) ) -> ( z C_ Y /\ ( `' F " z ) e. J ) )
23 22 simprd
 |-  ( ( ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ x C_ Y ) /\ y e. x ) /\ ( z e. ( ( J qTop F ) i^i ~P x ) /\ y e. z ) ) -> ( `' F " z ) e. J )
24 17 elin2d
 |-  ( ( ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ x C_ Y ) /\ y e. x ) /\ ( z e. ( ( J qTop F ) i^i ~P x ) /\ y e. z ) ) -> z e. ~P x )
25 24 elpwid
 |-  ( ( ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ x C_ Y ) /\ y e. x ) /\ ( z e. ( ( J qTop F ) i^i ~P x ) /\ y e. z ) ) -> z C_ x )
26 imass2
 |-  ( z C_ x -> ( `' F " z ) C_ ( `' F " x ) )
27 25 26 syl
 |-  ( ( ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ x C_ Y ) /\ y e. x ) /\ ( z e. ( ( J qTop F ) i^i ~P x ) /\ y e. z ) ) -> ( `' F " z ) C_ ( `' F " x ) )
28 23 27 elpwd
 |-  ( ( ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ x C_ Y ) /\ y e. x ) /\ ( z e. ( ( J qTop F ) i^i ~P x ) /\ y e. z ) ) -> ( `' F " z ) e. ~P ( `' F " x ) )
29 23 28 elind
 |-  ( ( ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ x C_ Y ) /\ y e. x ) /\ ( z e. ( ( J qTop F ) i^i ~P x ) /\ y e. z ) ) -> ( `' F " z ) e. ( J i^i ~P ( `' F " x ) ) )
30 simp-4r
 |-  ( ( ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ x C_ Y ) /\ y e. x ) /\ ( z e. ( ( J qTop F ) i^i ~P x ) /\ y e. z ) ) -> F : X -1-1-onto-> Y )
31 30 2 syl
 |-  ( ( ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ x C_ Y ) /\ y e. x ) /\ ( z e. ( ( J qTop F ) i^i ~P x ) /\ y e. z ) ) -> `' F : Y -1-1-onto-> X )
32 f1ofn
 |-  ( `' F : Y -1-1-onto-> X -> `' F Fn Y )
33 31 32 syl
 |-  ( ( ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ x C_ Y ) /\ y e. x ) /\ ( z e. ( ( J qTop F ) i^i ~P x ) /\ y e. z ) ) -> `' F Fn Y )
34 6 ad2antrr
 |-  ( ( ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ x C_ Y ) /\ y e. x ) /\ ( z e. ( ( J qTop F ) i^i ~P x ) /\ y e. z ) ) -> x C_ Y )
35 25 34 sstrd
 |-  ( ( ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ x C_ Y ) /\ y e. x ) /\ ( z e. ( ( J qTop F ) i^i ~P x ) /\ y e. z ) ) -> z C_ Y )
36 simprr
 |-  ( ( ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ x C_ Y ) /\ y e. x ) /\ ( z e. ( ( J qTop F ) i^i ~P x ) /\ y e. z ) ) -> y e. z )
37 fnfvima
 |-  ( ( `' F Fn Y /\ z C_ Y /\ y e. z ) -> ( `' F ` y ) e. ( `' F " z ) )
38 33 35 36 37 syl3anc
 |-  ( ( ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ x C_ Y ) /\ y e. x ) /\ ( z e. ( ( J qTop F ) i^i ~P x ) /\ y e. z ) ) -> ( `' F ` y ) e. ( `' F " z ) )
39 eleq2
 |-  ( w = ( `' F " z ) -> ( ( `' F ` y ) e. w <-> ( `' F ` y ) e. ( `' F " z ) ) )
40 39 rspcev
 |-  ( ( ( `' F " z ) e. ( J i^i ~P ( `' F " x ) ) /\ ( `' F ` y ) e. ( `' F " z ) ) -> E. w e. ( J i^i ~P ( `' F " x ) ) ( `' F ` y ) e. w )
41 29 38 40 syl2anc
 |-  ( ( ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ x C_ Y ) /\ y e. x ) /\ ( z e. ( ( J qTop F ) i^i ~P x ) /\ y e. z ) ) -> E. w e. ( J i^i ~P ( `' F " x ) ) ( `' F ` y ) e. w )
42 41 rexlimdvaa
 |-  ( ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ x C_ Y ) /\ y e. x ) -> ( E. z e. ( ( J qTop F ) i^i ~P x ) y e. z -> E. w e. ( J i^i ~P ( `' F " x ) ) ( `' F ` y ) e. w ) )
43 simp-4r
 |-  ( ( ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ x C_ Y ) /\ y e. x ) /\ ( w e. ( J i^i ~P ( `' F " x ) ) /\ ( `' F ` y ) e. w ) ) -> F : X -1-1-onto-> Y )
44 f1ofun
 |-  ( F : X -1-1-onto-> Y -> Fun F )
45 43 44 syl
 |-  ( ( ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ x C_ Y ) /\ y e. x ) /\ ( w e. ( J i^i ~P ( `' F " x ) ) /\ ( `' F ` y ) e. w ) ) -> Fun F )
46 simprl
 |-  ( ( ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ x C_ Y ) /\ y e. x ) /\ ( w e. ( J i^i ~P ( `' F " x ) ) /\ ( `' F ` y ) e. w ) ) -> w e. ( J i^i ~P ( `' F " x ) ) )
47 46 elin2d
 |-  ( ( ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ x C_ Y ) /\ y e. x ) /\ ( w e. ( J i^i ~P ( `' F " x ) ) /\ ( `' F ` y ) e. w ) ) -> w e. ~P ( `' F " x ) )
48 47 elpwid
 |-  ( ( ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ x C_ Y ) /\ y e. x ) /\ ( w e. ( J i^i ~P ( `' F " x ) ) /\ ( `' F ` y ) e. w ) ) -> w C_ ( `' F " x ) )
49 funimass2
 |-  ( ( Fun F /\ w C_ ( `' F " x ) ) -> ( F " w ) C_ x )
50 45 48 49 syl2anc
 |-  ( ( ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ x C_ Y ) /\ y e. x ) /\ ( w e. ( J i^i ~P ( `' F " x ) ) /\ ( `' F ` y ) e. w ) ) -> ( F " w ) C_ x )
51 6 ad2antrr
 |-  ( ( ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ x C_ Y ) /\ y e. x ) /\ ( w e. ( J i^i ~P ( `' F " x ) ) /\ ( `' F ` y ) e. w ) ) -> x C_ Y )
52 50 51 sstrd
 |-  ( ( ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ x C_ Y ) /\ y e. x ) /\ ( w e. ( J i^i ~P ( `' F " x ) ) /\ ( `' F ` y ) e. w ) ) -> ( F " w ) C_ Y )
53 f1of1
 |-  ( F : X -1-1-onto-> Y -> F : X -1-1-> Y )
54 43 53 syl
 |-  ( ( ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ x C_ Y ) /\ y e. x ) /\ ( w e. ( J i^i ~P ( `' F " x ) ) /\ ( `' F ` y ) e. w ) ) -> F : X -1-1-> Y )
55 46 elin1d
 |-  ( ( ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ x C_ Y ) /\ y e. x ) /\ ( w e. ( J i^i ~P ( `' F " x ) ) /\ ( `' F ` y ) e. w ) ) -> w e. J )
56 elssuni
 |-  ( w e. J -> w C_ U. J )
57 56 1 sseqtrrdi
 |-  ( w e. J -> w C_ X )
58 55 57 syl
 |-  ( ( ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ x C_ Y ) /\ y e. x ) /\ ( w e. ( J i^i ~P ( `' F " x ) ) /\ ( `' F ` y ) e. w ) ) -> w C_ X )
59 f1imacnv
 |-  ( ( F : X -1-1-> Y /\ w C_ X ) -> ( `' F " ( F " w ) ) = w )
60 54 58 59 syl2anc
 |-  ( ( ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ x C_ Y ) /\ y e. x ) /\ ( w e. ( J i^i ~P ( `' F " x ) ) /\ ( `' F ` y ) e. w ) ) -> ( `' F " ( F " w ) ) = w )
61 60 55 eqeltrd
 |-  ( ( ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ x C_ Y ) /\ y e. x ) /\ ( w e. ( J i^i ~P ( `' F " x ) ) /\ ( `' F ` y ) e. w ) ) -> ( `' F " ( F " w ) ) e. J )
62 1 elqtop2
 |-  ( ( J e. TopBases /\ F : X -onto-> Y ) -> ( ( F " w ) e. ( J qTop F ) <-> ( ( F " w ) C_ Y /\ ( `' F " ( F " w ) ) e. J ) ) )
63 8 62 sylan2
 |-  ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) -> ( ( F " w ) e. ( J qTop F ) <-> ( ( F " w ) C_ Y /\ ( `' F " ( F " w ) ) e. J ) ) )
64 63 ad3antrrr
 |-  ( ( ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ x C_ Y ) /\ y e. x ) /\ ( w e. ( J i^i ~P ( `' F " x ) ) /\ ( `' F ` y ) e. w ) ) -> ( ( F " w ) e. ( J qTop F ) <-> ( ( F " w ) C_ Y /\ ( `' F " ( F " w ) ) e. J ) ) )
65 52 61 64 mpbir2and
 |-  ( ( ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ x C_ Y ) /\ y e. x ) /\ ( w e. ( J i^i ~P ( `' F " x ) ) /\ ( `' F ` y ) e. w ) ) -> ( F " w ) e. ( J qTop F ) )
66 vex
 |-  x e. _V
67 66 elpw2
 |-  ( ( F " w ) e. ~P x <-> ( F " w ) C_ x )
68 50 67 sylibr
 |-  ( ( ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ x C_ Y ) /\ y e. x ) /\ ( w e. ( J i^i ~P ( `' F " x ) ) /\ ( `' F ` y ) e. w ) ) -> ( F " w ) e. ~P x )
69 65 68 elind
 |-  ( ( ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ x C_ Y ) /\ y e. x ) /\ ( w e. ( J i^i ~P ( `' F " x ) ) /\ ( `' F ` y ) e. w ) ) -> ( F " w ) e. ( ( J qTop F ) i^i ~P x ) )
70 6 sselda
 |-  ( ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ x C_ Y ) /\ y e. x ) -> y e. Y )
71 70 adantr
 |-  ( ( ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ x C_ Y ) /\ y e. x ) /\ ( w e. ( J i^i ~P ( `' F " x ) ) /\ ( `' F ` y ) e. w ) ) -> y e. Y )
72 f1ocnvfv2
 |-  ( ( F : X -1-1-onto-> Y /\ y e. Y ) -> ( F ` ( `' F ` y ) ) = y )
73 43 71 72 syl2anc
 |-  ( ( ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ x C_ Y ) /\ y e. x ) /\ ( w e. ( J i^i ~P ( `' F " x ) ) /\ ( `' F ` y ) e. w ) ) -> ( F ` ( `' F ` y ) ) = y )
74 f1ofn
 |-  ( F : X -1-1-onto-> Y -> F Fn X )
75 74 adantl
 |-  ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) -> F Fn X )
76 75 ad3antrrr
 |-  ( ( ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ x C_ Y ) /\ y e. x ) /\ ( w e. ( J i^i ~P ( `' F " x ) ) /\ ( `' F ` y ) e. w ) ) -> F Fn X )
77 simprr
 |-  ( ( ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ x C_ Y ) /\ y e. x ) /\ ( w e. ( J i^i ~P ( `' F " x ) ) /\ ( `' F ` y ) e. w ) ) -> ( `' F ` y ) e. w )
78 fnfvima
 |-  ( ( F Fn X /\ w C_ X /\ ( `' F ` y ) e. w ) -> ( F ` ( `' F ` y ) ) e. ( F " w ) )
79 76 58 77 78 syl3anc
 |-  ( ( ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ x C_ Y ) /\ y e. x ) /\ ( w e. ( J i^i ~P ( `' F " x ) ) /\ ( `' F ` y ) e. w ) ) -> ( F ` ( `' F ` y ) ) e. ( F " w ) )
80 73 79 eqeltrrd
 |-  ( ( ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ x C_ Y ) /\ y e. x ) /\ ( w e. ( J i^i ~P ( `' F " x ) ) /\ ( `' F ` y ) e. w ) ) -> y e. ( F " w ) )
81 eleq2
 |-  ( z = ( F " w ) -> ( y e. z <-> y e. ( F " w ) ) )
82 81 rspcev
 |-  ( ( ( F " w ) e. ( ( J qTop F ) i^i ~P x ) /\ y e. ( F " w ) ) -> E. z e. ( ( J qTop F ) i^i ~P x ) y e. z )
83 69 80 82 syl2anc
 |-  ( ( ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ x C_ Y ) /\ y e. x ) /\ ( w e. ( J i^i ~P ( `' F " x ) ) /\ ( `' F ` y ) e. w ) ) -> E. z e. ( ( J qTop F ) i^i ~P x ) y e. z )
84 83 rexlimdvaa
 |-  ( ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ x C_ Y ) /\ y e. x ) -> ( E. w e. ( J i^i ~P ( `' F " x ) ) ( `' F ` y ) e. w -> E. z e. ( ( J qTop F ) i^i ~P x ) y e. z ) )
85 42 84 impbid
 |-  ( ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ x C_ Y ) /\ y e. x ) -> ( E. z e. ( ( J qTop F ) i^i ~P x ) y e. z <-> E. w e. ( J i^i ~P ( `' F " x ) ) ( `' F ` y ) e. w ) )
86 eluni2
 |-  ( y e. U. ( ( J qTop F ) i^i ~P x ) <-> E. z e. ( ( J qTop F ) i^i ~P x ) y e. z )
87 eluni2
 |-  ( ( `' F ` y ) e. U. ( J i^i ~P ( `' F " x ) ) <-> E. w e. ( J i^i ~P ( `' F " x ) ) ( `' F ` y ) e. w )
88 85 86 87 3bitr4g
 |-  ( ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ x C_ Y ) /\ y e. x ) -> ( y e. U. ( ( J qTop F ) i^i ~P x ) <-> ( `' F ` y ) e. U. ( J i^i ~P ( `' F " x ) ) ) )
89 88 ralbidva
 |-  ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ x C_ Y ) -> ( A. y e. x y e. U. ( ( J qTop F ) i^i ~P x ) <-> A. y e. x ( `' F ` y ) e. U. ( J i^i ~P ( `' F " x ) ) ) )
90 16 89 syl5bb
 |-  ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ x C_ Y ) -> ( x C_ U. ( ( J qTop F ) i^i ~P x ) <-> A. y e. x ( `' F ` y ) e. U. ( J i^i ~P ( `' F " x ) ) ) )
91 15 90 bitr4d
 |-  ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ x C_ Y ) -> ( ( `' F " x ) C_ U. ( J i^i ~P ( `' F " x ) ) <-> x C_ U. ( ( J qTop F ) i^i ~P x ) ) )
92 eltg
 |-  ( J e. TopBases -> ( ( `' F " x ) e. ( topGen ` J ) <-> ( `' F " x ) C_ U. ( J i^i ~P ( `' F " x ) ) ) )
93 92 ad2antrr
 |-  ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ x C_ Y ) -> ( ( `' F " x ) e. ( topGen ` J ) <-> ( `' F " x ) C_ U. ( J i^i ~P ( `' F " x ) ) ) )
94 ovex
 |-  ( J qTop F ) e. _V
95 eltg
 |-  ( ( J qTop F ) e. _V -> ( x e. ( topGen ` ( J qTop F ) ) <-> x C_ U. ( ( J qTop F ) i^i ~P x ) ) )
96 94 95 mp1i
 |-  ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ x C_ Y ) -> ( x e. ( topGen ` ( J qTop F ) ) <-> x C_ U. ( ( J qTop F ) i^i ~P x ) ) )
97 91 93 96 3bitr4d
 |-  ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ x C_ Y ) -> ( ( `' F " x ) e. ( topGen ` J ) <-> x e. ( topGen ` ( J qTop F ) ) ) )
98 97 pm5.32da
 |-  ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) -> ( ( x C_ Y /\ ( `' F " x ) e. ( topGen ` J ) ) <-> ( x C_ Y /\ x e. ( topGen ` ( J qTop F ) ) ) ) )
99 tgtopon
 |-  ( J e. TopBases -> ( topGen ` J ) e. ( TopOn ` U. J ) )
100 99 adantr
 |-  ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) -> ( topGen ` J ) e. ( TopOn ` U. J ) )
101 1 fveq2i
 |-  ( TopOn ` X ) = ( TopOn ` U. J )
102 100 101 eleqtrrdi
 |-  ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) -> ( topGen ` J ) e. ( TopOn ` X ) )
103 8 adantl
 |-  ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) -> F : X -onto-> Y )
104 elqtop3
 |-  ( ( ( topGen ` J ) e. ( TopOn ` X ) /\ F : X -onto-> Y ) -> ( x e. ( ( topGen ` J ) qTop F ) <-> ( x C_ Y /\ ( `' F " x ) e. ( topGen ` J ) ) ) )
105 102 103 104 syl2anc
 |-  ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) -> ( x e. ( ( topGen ` J ) qTop F ) <-> ( x C_ Y /\ ( `' F " x ) e. ( topGen ` J ) ) ) )
106 unitg
 |-  ( ( J qTop F ) e. _V -> U. ( topGen ` ( J qTop F ) ) = U. ( J qTop F ) )
107 94 106 ax-mp
 |-  U. ( topGen ` ( J qTop F ) ) = U. ( J qTop F )
108 1 elqtop2
 |-  ( ( J e. TopBases /\ F : X -onto-> Y ) -> ( x e. ( J qTop F ) <-> ( x C_ Y /\ ( `' F " x ) e. J ) ) )
109 8 108 sylan2
 |-  ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) -> ( x e. ( J qTop F ) <-> ( x C_ Y /\ ( `' F " x ) e. J ) ) )
110 simpl
 |-  ( ( x C_ Y /\ ( `' F " x ) e. J ) -> x C_ Y )
111 velpw
 |-  ( x e. ~P Y <-> x C_ Y )
112 110 111 sylibr
 |-  ( ( x C_ Y /\ ( `' F " x ) e. J ) -> x e. ~P Y )
113 109 112 syl6bi
 |-  ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) -> ( x e. ( J qTop F ) -> x e. ~P Y ) )
114 113 ssrdv
 |-  ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) -> ( J qTop F ) C_ ~P Y )
115 sspwuni
 |-  ( ( J qTop F ) C_ ~P Y <-> U. ( J qTop F ) C_ Y )
116 114 115 sylib
 |-  ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) -> U. ( J qTop F ) C_ Y )
117 107 116 eqsstrid
 |-  ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) -> U. ( topGen ` ( J qTop F ) ) C_ Y )
118 sspwuni
 |-  ( ( topGen ` ( J qTop F ) ) C_ ~P Y <-> U. ( topGen ` ( J qTop F ) ) C_ Y )
119 117 118 sylibr
 |-  ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) -> ( topGen ` ( J qTop F ) ) C_ ~P Y )
120 119 sseld
 |-  ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) -> ( x e. ( topGen ` ( J qTop F ) ) -> x e. ~P Y ) )
121 120 111 syl6ib
 |-  ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) -> ( x e. ( topGen ` ( J qTop F ) ) -> x C_ Y ) )
122 121 pm4.71rd
 |-  ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) -> ( x e. ( topGen ` ( J qTop F ) ) <-> ( x C_ Y /\ x e. ( topGen ` ( J qTop F ) ) ) ) )
123 98 105 122 3bitr4d
 |-  ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) -> ( x e. ( ( topGen ` J ) qTop F ) <-> x e. ( topGen ` ( J qTop F ) ) ) )
124 123 eqrdv
 |-  ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) -> ( ( topGen ` J ) qTop F ) = ( topGen ` ( J qTop F ) ) )