This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝑋 = ∪ 𝐽
Assertion tgqtop ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) → ( ( topGen ‘ 𝐽 ) qTop 𝐹 ) = ( topGen ‘ ( 𝐽 qTop 𝐹 ) ) )

Proof

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