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 bitrid 
 |-  ( ( ( 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 biimtrdi 
 |-  ( ( 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 imbitrdi 
 |-  ( ( 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 ) ) )