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 = J
Assertion tgqtop J TopBases F : X 1-1 onto Y topGen J qTop F = topGen J qTop F

Proof

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