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

Metamath Proof Explorer

Theorem basqtop

Description: An injection maps bases to bases. (Contributed by Mario Carneiro, 27-Aug-2015)

Ref Expression
Hypothesis qtopcmp.1 ⊢ 𝑋 = ∪ 𝐽
Assertion basqtop ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) → ( 𝐽 qTop 𝐹 ) ∈ TopBases )

Proof

Step Hyp Ref Expression
1 qtopcmp.1 ⊢ 𝑋 = ∪ 𝐽
2 f1ofo ⊢ ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 → 𝐹 : 𝑋 –onto→ 𝑌 )
3 1 elqtop2 ⊢ ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –onto→ 𝑌 ) → ( 𝑥 ∈ ( 𝐽 qTop 𝐹 ) ↔ ( 𝑥 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ) ) )
4 1 elqtop2 ⊢ ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –onto→ 𝑌 ) → ( 𝑦 ∈ ( 𝐽 qTop 𝐹 ) ↔ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) )
5 3 4 anbi12d ⊢ ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –onto→ 𝑌 ) → ( ( 𝑥 ∈ ( 𝐽 qTop 𝐹 ) ∧ 𝑦 ∈ ( 𝐽 qTop 𝐹 ) ) ↔ ( ( 𝑥 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ) ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) ) )
6 2 5 sylan2 ⊢ ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) → ( ( 𝑥 ∈ ( 𝐽 qTop 𝐹 ) ∧ 𝑦 ∈ ( 𝐽 qTop 𝐹 ) ) ↔ ( ( 𝑥 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ) ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) ) )
7 simpl1l ⊢ ( ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ ( 𝑥 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ) ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) ∧ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ) → 𝐽 ∈ TopBases )
8 simpl2r ⊢ ( ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ ( 𝑥 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ) ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) ∧ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ) → ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 )
9 simpl3r ⊢ ( ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ ( 𝑥 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ) ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) ∧ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ) → ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 )
10 simpl1r ⊢ ( ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ ( 𝑥 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ) ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) ∧ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ) → 𝐹 : 𝑋 –1-1-onto→ 𝑌 )
11 f1ocnv ⊢ ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 → ◡ 𝐹 : 𝑌 –1-1-onto→ 𝑋 )
12 f1ofn ⊢ ( ◡ 𝐹 : 𝑌 –1-1-onto→ 𝑋 → ◡ 𝐹 Fn 𝑌 )
13 10 11 12 3syl ⊢ ( ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ ( 𝑥 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ) ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) ∧ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ) → ◡ 𝐹 Fn 𝑌 )
14 simpl2l ⊢ ( ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ ( 𝑥 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ) ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) ∧ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ) → 𝑥 ⊆ 𝑌 )
15 simpr ⊢ ( ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ ( 𝑥 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ) ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) ∧ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ) → 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) )
16 15 elin1d ⊢ ( ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ ( 𝑥 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ) ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) ∧ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ) → 𝑧 ∈ 𝑥 )
17 fnfvima ⊢ ( ( ◡ 𝐹 Fn 𝑌 ∧ 𝑥 ⊆ 𝑌 ∧ 𝑧 ∈ 𝑥 ) → ( ◡ 𝐹 ‘ 𝑧 ) ∈ ( ◡ 𝐹 “ 𝑥 ) )
18 13 14 16 17 syl3anc ⊢ ( ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ ( 𝑥 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ) ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) ∧ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ) → ( ◡ 𝐹 ‘ 𝑧 ) ∈ ( ◡ 𝐹 “ 𝑥 ) )
19 simpl3l ⊢ ( ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ ( 𝑥 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ) ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) ∧ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ) → 𝑦 ⊆ 𝑌 )
20 15 elin2d ⊢ ( ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ ( 𝑥 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ) ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) ∧ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ) → 𝑧 ∈ 𝑦 )
21 fnfvima ⊢ ( ( ◡ 𝐹 Fn 𝑌 ∧ 𝑦 ⊆ 𝑌 ∧ 𝑧 ∈ 𝑦 ) → ( ◡ 𝐹 ‘ 𝑧 ) ∈ ( ◡ 𝐹 “ 𝑦 ) )
22 13 19 20 21 syl3anc ⊢ ( ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ ( 𝑥 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ) ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) ∧ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ) → ( ◡ 𝐹 ‘ 𝑧 ) ∈ ( ◡ 𝐹 “ 𝑦 ) )
23 18 22 elind ⊢ ( ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ ( 𝑥 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ) ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) ∧ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ) → ( ◡ 𝐹 ‘ 𝑧 ) ∈ ( ( ◡ 𝐹 “ 𝑥 ) ∩ ( ◡ 𝐹 “ 𝑦 ) ) )
24 basis2 ⊢ ( ( ( 𝐽 ∈ TopBases ∧ ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ) ∧ ( ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ∧ ( ◡ 𝐹 ‘ 𝑧 ) ∈ ( ( ◡ 𝐹 “ 𝑥 ) ∩ ( ◡ 𝐹 “ 𝑦 ) ) ) ) → ∃ 𝑤 ∈ 𝐽 ( ( ◡ 𝐹 ‘ 𝑧 ) ∈ 𝑤 ∧ 𝑤 ⊆ ( ( ◡ 𝐹 “ 𝑥 ) ∩ ( ◡ 𝐹 “ 𝑦 ) ) ) )
25 7 8 9 23 24 syl22anc ⊢ ( ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ ( 𝑥 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ) ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) ∧ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ) → ∃ 𝑤 ∈ 𝐽 ( ( ◡ 𝐹 ‘ 𝑧 ) ∈ 𝑤 ∧ 𝑤 ⊆ ( ( ◡ 𝐹 “ 𝑥 ) ∩ ( ◡ 𝐹 “ 𝑦 ) ) ) )
26 10 adantr ⊢ ( ( ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ ( 𝑥 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ) ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) ∧ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ) ∧ ( 𝑤 ∈ 𝐽 ∧ ( ( ◡ 𝐹 ‘ 𝑧 ) ∈ 𝑤 ∧ 𝑤 ⊆ ( ( ◡ 𝐹 “ 𝑥 ) ∩ ( ◡ 𝐹 “ 𝑦 ) ) ) ) ) → 𝐹 : 𝑋 –1-1-onto→ 𝑌 )
27 inss1 ⊢ ( 𝑥 ∩ 𝑦 ) ⊆ 𝑥
28 simp2l ⊢ ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ ( 𝑥 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ) ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) → 𝑥 ⊆ 𝑌 )
29 27 28 sstrid ⊢ ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ ( 𝑥 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ) ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) → ( 𝑥 ∩ 𝑦 ) ⊆ 𝑌 )
30 29 sselda ⊢ ( ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ ( 𝑥 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ) ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) ∧ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ) → 𝑧 ∈ 𝑌 )
31 30 adantr ⊢ ( ( ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ ( 𝑥 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ) ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) ∧ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ) ∧ ( 𝑤 ∈ 𝐽 ∧ ( ( ◡ 𝐹 ‘ 𝑧 ) ∈ 𝑤 ∧ 𝑤 ⊆ ( ( ◡ 𝐹 “ 𝑥 ) ∩ ( ◡ 𝐹 “ 𝑦 ) ) ) ) ) → 𝑧 ∈ 𝑌 )
32 f1ocnvfv2 ⊢ ( ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 ∧ 𝑧 ∈ 𝑌 ) → ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑧 ) ) = 𝑧 )
33 26 31 32 syl2anc ⊢ ( ( ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ ( 𝑥 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ) ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) ∧ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ) ∧ ( 𝑤 ∈ 𝐽 ∧ ( ( ◡ 𝐹 ‘ 𝑧 ) ∈ 𝑤 ∧ 𝑤 ⊆ ( ( ◡ 𝐹 “ 𝑥 ) ∩ ( ◡ 𝐹 “ 𝑦 ) ) ) ) ) → ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑧 ) ) = 𝑧 )
34 f1ofn ⊢ ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 → 𝐹 Fn 𝑋 )
35 26 34 syl ⊢ ( ( ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ ( 𝑥 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ) ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) ∧ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ) ∧ ( 𝑤 ∈ 𝐽 ∧ ( ( ◡ 𝐹 ‘ 𝑧 ) ∈ 𝑤 ∧ 𝑤 ⊆ ( ( ◡ 𝐹 “ 𝑥 ) ∩ ( ◡ 𝐹 “ 𝑦 ) ) ) ) ) → 𝐹 Fn 𝑋 )
36 simprrr ⊢ ( ( ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ ( 𝑥 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ) ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) ∧ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ) ∧ ( 𝑤 ∈ 𝐽 ∧ ( ( ◡ 𝐹 ‘ 𝑧 ) ∈ 𝑤 ∧ 𝑤 ⊆ ( ( ◡ 𝐹 “ 𝑥 ) ∩ ( ◡ 𝐹 “ 𝑦 ) ) ) ) ) → 𝑤 ⊆ ( ( ◡ 𝐹 “ 𝑥 ) ∩ ( ◡ 𝐹 “ 𝑦 ) ) )
37 inss1 ⊢ ( ( ◡ 𝐹 “ 𝑥 ) ∩ ( ◡ 𝐹 “ 𝑦 ) ) ⊆ ( ◡ 𝐹 “ 𝑥 )
38 36 37 sstrdi ⊢ ( ( ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ ( 𝑥 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ) ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) ∧ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ) ∧ ( 𝑤 ∈ 𝐽 ∧ ( ( ◡ 𝐹 ‘ 𝑧 ) ∈ 𝑤 ∧ 𝑤 ⊆ ( ( ◡ 𝐹 “ 𝑥 ) ∩ ( ◡ 𝐹 “ 𝑦 ) ) ) ) ) → 𝑤 ⊆ ( ◡ 𝐹 “ 𝑥 ) )
39 cnvimass ⊢ ( ◡ 𝐹 “ 𝑥 ) ⊆ dom 𝐹
40 f1odm ⊢ ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 → dom 𝐹 = 𝑋 )
41 26 40 syl ⊢ ( ( ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ ( 𝑥 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ) ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) ∧ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ) ∧ ( 𝑤 ∈ 𝐽 ∧ ( ( ◡ 𝐹 ‘ 𝑧 ) ∈ 𝑤 ∧ 𝑤 ⊆ ( ( ◡ 𝐹 “ 𝑥 ) ∩ ( ◡ 𝐹 “ 𝑦 ) ) ) ) ) → dom 𝐹 = 𝑋 )
42 39 41 sseqtrid ⊢ ( ( ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ ( 𝑥 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ) ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) ∧ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ) ∧ ( 𝑤 ∈ 𝐽 ∧ ( ( ◡ 𝐹 ‘ 𝑧 ) ∈ 𝑤 ∧ 𝑤 ⊆ ( ( ◡ 𝐹 “ 𝑥 ) ∩ ( ◡ 𝐹 “ 𝑦 ) ) ) ) ) → ( ◡ 𝐹 “ 𝑥 ) ⊆ 𝑋 )
43 38 42 sstrd ⊢ ( ( ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ ( 𝑥 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ) ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) ∧ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ) ∧ ( 𝑤 ∈ 𝐽 ∧ ( ( ◡ 𝐹 ‘ 𝑧 ) ∈ 𝑤 ∧ 𝑤 ⊆ ( ( ◡ 𝐹 “ 𝑥 ) ∩ ( ◡ 𝐹 “ 𝑦 ) ) ) ) ) → 𝑤 ⊆ 𝑋 )
44 simprrl ⊢ ( ( ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ ( 𝑥 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ) ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) ∧ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ) ∧ ( 𝑤 ∈ 𝐽 ∧ ( ( ◡ 𝐹 ‘ 𝑧 ) ∈ 𝑤 ∧ 𝑤 ⊆ ( ( ◡ 𝐹 “ 𝑥 ) ∩ ( ◡ 𝐹 “ 𝑦 ) ) ) ) ) → ( ◡ 𝐹 ‘ 𝑧 ) ∈ 𝑤 )
45 fnfvima ⊢ ( ( 𝐹 Fn 𝑋 ∧ 𝑤 ⊆ 𝑋 ∧ ( ◡ 𝐹 ‘ 𝑧 ) ∈ 𝑤 ) → ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑧 ) ) ∈ ( 𝐹 “ 𝑤 ) )
46 35 43 44 45 syl3anc ⊢ ( ( ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ ( 𝑥 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ) ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) ∧ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ) ∧ ( 𝑤 ∈ 𝐽 ∧ ( ( ◡ 𝐹 ‘ 𝑧 ) ∈ 𝑤 ∧ 𝑤 ⊆ ( ( ◡ 𝐹 “ 𝑥 ) ∩ ( ◡ 𝐹 “ 𝑦 ) ) ) ) ) → ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑧 ) ) ∈ ( 𝐹 “ 𝑤 ) )
47 33 46 eqeltrrd ⊢ ( ( ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ ( 𝑥 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ) ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) ∧ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ) ∧ ( 𝑤 ∈ 𝐽 ∧ ( ( ◡ 𝐹 ‘ 𝑧 ) ∈ 𝑤 ∧ 𝑤 ⊆ ( ( ◡ 𝐹 “ 𝑥 ) ∩ ( ◡ 𝐹 “ 𝑦 ) ) ) ) ) → 𝑧 ∈ ( 𝐹 “ 𝑤 ) )
48 imassrn ⊢ ( 𝐹 “ 𝑤 ) ⊆ ran 𝐹
49 26 2 syl ⊢ ( ( ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ ( 𝑥 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ) ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) ∧ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ) ∧ ( 𝑤 ∈ 𝐽 ∧ ( ( ◡ 𝐹 ‘ 𝑧 ) ∈ 𝑤 ∧ 𝑤 ⊆ ( ( ◡ 𝐹 “ 𝑥 ) ∩ ( ◡ 𝐹 “ 𝑦 ) ) ) ) ) → 𝐹 : 𝑋 –onto→ 𝑌 )
50 forn ⊢ ( 𝐹 : 𝑋 –onto→ 𝑌 → ran 𝐹 = 𝑌 )
51 49 50 syl ⊢ ( ( ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ ( 𝑥 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ) ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) ∧ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ) ∧ ( 𝑤 ∈ 𝐽 ∧ ( ( ◡ 𝐹 ‘ 𝑧 ) ∈ 𝑤 ∧ 𝑤 ⊆ ( ( ◡ 𝐹 “ 𝑥 ) ∩ ( ◡ 𝐹 “ 𝑦 ) ) ) ) ) → ran 𝐹 = 𝑌 )
52 48 51 sseqtrid ⊢ ( ( ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ ( 𝑥 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ) ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) ∧ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ) ∧ ( 𝑤 ∈ 𝐽 ∧ ( ( ◡ 𝐹 ‘ 𝑧 ) ∈ 𝑤 ∧ 𝑤 ⊆ ( ( ◡ 𝐹 “ 𝑥 ) ∩ ( ◡ 𝐹 “ 𝑦 ) ) ) ) ) → ( 𝐹 “ 𝑤 ) ⊆ 𝑌 )
53 f1of1 ⊢ ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 → 𝐹 : 𝑋 –1-1→ 𝑌 )
54 26 53 syl ⊢ ( ( ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ ( 𝑥 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ) ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) ∧ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ) ∧ ( 𝑤 ∈ 𝐽 ∧ ( ( ◡ 𝐹 ‘ 𝑧 ) ∈ 𝑤 ∧ 𝑤 ⊆ ( ( ◡ 𝐹 “ 𝑥 ) ∩ ( ◡ 𝐹 “ 𝑦 ) ) ) ) ) → 𝐹 : 𝑋 –1-1→ 𝑌 )
55 f1imacnv ⊢ ( ( 𝐹 : 𝑋 –1-1→ 𝑌 ∧ 𝑤 ⊆ 𝑋 ) → ( ◡ 𝐹 “ ( 𝐹 “ 𝑤 ) ) = 𝑤 )
56 54 43 55 syl2anc ⊢ ( ( ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ ( 𝑥 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ) ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) ∧ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ) ∧ ( 𝑤 ∈ 𝐽 ∧ ( ( ◡ 𝐹 ‘ 𝑧 ) ∈ 𝑤 ∧ 𝑤 ⊆ ( ( ◡ 𝐹 “ 𝑥 ) ∩ ( ◡ 𝐹 “ 𝑦 ) ) ) ) ) → ( ◡ 𝐹 “ ( 𝐹 “ 𝑤 ) ) = 𝑤 )
57 simprl ⊢ ( ( ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ ( 𝑥 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ) ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) ∧ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ) ∧ ( 𝑤 ∈ 𝐽 ∧ ( ( ◡ 𝐹 ‘ 𝑧 ) ∈ 𝑤 ∧ 𝑤 ⊆ ( ( ◡ 𝐹 “ 𝑥 ) ∩ ( ◡ 𝐹 “ 𝑦 ) ) ) ) ) → 𝑤 ∈ 𝐽 )
58 56 57 eqeltrd ⊢ ( ( ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ ( 𝑥 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ) ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) ∧ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ) ∧ ( 𝑤 ∈ 𝐽 ∧ ( ( ◡ 𝐹 ‘ 𝑧 ) ∈ 𝑤 ∧ 𝑤 ⊆ ( ( ◡ 𝐹 “ 𝑥 ) ∩ ( ◡ 𝐹 “ 𝑦 ) ) ) ) ) → ( ◡ 𝐹 “ ( 𝐹 “ 𝑤 ) ) ∈ 𝐽 )
59 7 adantr ⊢ ( ( ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ ( 𝑥 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ) ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) ∧ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ) ∧ ( 𝑤 ∈ 𝐽 ∧ ( ( ◡ 𝐹 ‘ 𝑧 ) ∈ 𝑤 ∧ 𝑤 ⊆ ( ( ◡ 𝐹 “ 𝑥 ) ∩ ( ◡ 𝐹 “ 𝑦 ) ) ) ) ) → 𝐽 ∈ TopBases )
60 1 elqtop2 ⊢ ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –onto→ 𝑌 ) → ( ( 𝐹 “ 𝑤 ) ∈ ( 𝐽 qTop 𝐹 ) ↔ ( ( 𝐹 “ 𝑤 ) ⊆ 𝑌 ∧ ( ◡ 𝐹 “ ( 𝐹 “ 𝑤 ) ) ∈ 𝐽 ) ) )
61 59 49 60 syl2anc ⊢ ( ( ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ ( 𝑥 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ) ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) ∧ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ) ∧ ( 𝑤 ∈ 𝐽 ∧ ( ( ◡ 𝐹 ‘ 𝑧 ) ∈ 𝑤 ∧ 𝑤 ⊆ ( ( ◡ 𝐹 “ 𝑥 ) ∩ ( ◡ 𝐹 “ 𝑦 ) ) ) ) ) → ( ( 𝐹 “ 𝑤 ) ∈ ( 𝐽 qTop 𝐹 ) ↔ ( ( 𝐹 “ 𝑤 ) ⊆ 𝑌 ∧ ( ◡ 𝐹 “ ( 𝐹 “ 𝑤 ) ) ∈ 𝐽 ) ) )
62 52 58 61 mpbir2and ⊢ ( ( ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ ( 𝑥 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ) ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) ∧ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ) ∧ ( 𝑤 ∈ 𝐽 ∧ ( ( ◡ 𝐹 ‘ 𝑧 ) ∈ 𝑤 ∧ 𝑤 ⊆ ( ( ◡ 𝐹 “ 𝑥 ) ∩ ( ◡ 𝐹 “ 𝑦 ) ) ) ) ) → ( 𝐹 “ 𝑤 ) ∈ ( 𝐽 qTop 𝐹 ) )
63 fnfun ⊢ ( 𝐹 Fn 𝑋 → Fun 𝐹 )
64 inpreima ⊢ ( Fun 𝐹 → ( ◡ 𝐹 “ ( 𝑥 ∩ 𝑦 ) ) = ( ( ◡ 𝐹 “ 𝑥 ) ∩ ( ◡ 𝐹 “ 𝑦 ) ) )
65 35 63 64 3syl ⊢ ( ( ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ ( 𝑥 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ) ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) ∧ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ) ∧ ( 𝑤 ∈ 𝐽 ∧ ( ( ◡ 𝐹 ‘ 𝑧 ) ∈ 𝑤 ∧ 𝑤 ⊆ ( ( ◡ 𝐹 “ 𝑥 ) ∩ ( ◡ 𝐹 “ 𝑦 ) ) ) ) ) → ( ◡ 𝐹 “ ( 𝑥 ∩ 𝑦 ) ) = ( ( ◡ 𝐹 “ 𝑥 ) ∩ ( ◡ 𝐹 “ 𝑦 ) ) )
66 36 65 sseqtrrd ⊢ ( ( ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ ( 𝑥 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ) ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) ∧ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ) ∧ ( 𝑤 ∈ 𝐽 ∧ ( ( ◡ 𝐹 ‘ 𝑧 ) ∈ 𝑤 ∧ 𝑤 ⊆ ( ( ◡ 𝐹 “ 𝑥 ) ∩ ( ◡ 𝐹 “ 𝑦 ) ) ) ) ) → 𝑤 ⊆ ( ◡ 𝐹 “ ( 𝑥 ∩ 𝑦 ) ) )
67 35 63 syl ⊢ ( ( ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ ( 𝑥 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ) ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) ∧ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ) ∧ ( 𝑤 ∈ 𝐽 ∧ ( ( ◡ 𝐹 ‘ 𝑧 ) ∈ 𝑤 ∧ 𝑤 ⊆ ( ( ◡ 𝐹 “ 𝑥 ) ∩ ( ◡ 𝐹 “ 𝑦 ) ) ) ) ) → Fun 𝐹 )
68 38 39 sstrdi ⊢ ( ( ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ ( 𝑥 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ) ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) ∧ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ) ∧ ( 𝑤 ∈ 𝐽 ∧ ( ( ◡ 𝐹 ‘ 𝑧 ) ∈ 𝑤 ∧ 𝑤 ⊆ ( ( ◡ 𝐹 “ 𝑥 ) ∩ ( ◡ 𝐹 “ 𝑦 ) ) ) ) ) → 𝑤 ⊆ dom 𝐹 )
69 funimass3 ⊢ ( ( Fun 𝐹 ∧ 𝑤 ⊆ dom 𝐹 ) → ( ( 𝐹 “ 𝑤 ) ⊆ ( 𝑥 ∩ 𝑦 ) ↔ 𝑤 ⊆ ( ◡ 𝐹 “ ( 𝑥 ∩ 𝑦 ) ) ) )
70 67 68 69 syl2anc ⊢ ( ( ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ ( 𝑥 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ) ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) ∧ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ) ∧ ( 𝑤 ∈ 𝐽 ∧ ( ( ◡ 𝐹 ‘ 𝑧 ) ∈ 𝑤 ∧ 𝑤 ⊆ ( ( ◡ 𝐹 “ 𝑥 ) ∩ ( ◡ 𝐹 “ 𝑦 ) ) ) ) ) → ( ( 𝐹 “ 𝑤 ) ⊆ ( 𝑥 ∩ 𝑦 ) ↔ 𝑤 ⊆ ( ◡ 𝐹 “ ( 𝑥 ∩ 𝑦 ) ) ) )
71 66 70 mpbird ⊢ ( ( ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ ( 𝑥 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ) ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) ∧ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ) ∧ ( 𝑤 ∈ 𝐽 ∧ ( ( ◡ 𝐹 ‘ 𝑧 ) ∈ 𝑤 ∧ 𝑤 ⊆ ( ( ◡ 𝐹 “ 𝑥 ) ∩ ( ◡ 𝐹 “ 𝑦 ) ) ) ) ) → ( 𝐹 “ 𝑤 ) ⊆ ( 𝑥 ∩ 𝑦 ) )
72 vex ⊢ 𝑥 ∈ V
73 72 inex1 ⊢ ( 𝑥 ∩ 𝑦 ) ∈ V
74 73 elpw2 ⊢ ( ( 𝐹 “ 𝑤 ) ∈ 𝒫 ( 𝑥 ∩ 𝑦 ) ↔ ( 𝐹 “ 𝑤 ) ⊆ ( 𝑥 ∩ 𝑦 ) )
75 71 74 sylibr ⊢ ( ( ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ ( 𝑥 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ) ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) ∧ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ) ∧ ( 𝑤 ∈ 𝐽 ∧ ( ( ◡ 𝐹 ‘ 𝑧 ) ∈ 𝑤 ∧ 𝑤 ⊆ ( ( ◡ 𝐹 “ 𝑥 ) ∩ ( ◡ 𝐹 “ 𝑦 ) ) ) ) ) → ( 𝐹 “ 𝑤 ) ∈ 𝒫 ( 𝑥 ∩ 𝑦 ) )
76 62 75 elind ⊢ ( ( ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ ( 𝑥 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ) ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) ∧ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ) ∧ ( 𝑤 ∈ 𝐽 ∧ ( ( ◡ 𝐹 ‘ 𝑧 ) ∈ 𝑤 ∧ 𝑤 ⊆ ( ( ◡ 𝐹 “ 𝑥 ) ∩ ( ◡ 𝐹 “ 𝑦 ) ) ) ) ) → ( 𝐹 “ 𝑤 ) ∈ ( ( 𝐽 qTop 𝐹 ) ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) )
77 elunii ⊢ ( ( 𝑧 ∈ ( 𝐹 “ 𝑤 ) ∧ ( 𝐹 “ 𝑤 ) ∈ ( ( 𝐽 qTop 𝐹 ) ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ) → 𝑧 ∈ ∪ ( ( 𝐽 qTop 𝐹 ) ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) )
78 47 76 77 syl2anc ⊢ ( ( ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ ( 𝑥 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ) ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) ∧ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ) ∧ ( 𝑤 ∈ 𝐽 ∧ ( ( ◡ 𝐹 ‘ 𝑧 ) ∈ 𝑤 ∧ 𝑤 ⊆ ( ( ◡ 𝐹 “ 𝑥 ) ∩ ( ◡ 𝐹 “ 𝑦 ) ) ) ) ) → 𝑧 ∈ ∪ ( ( 𝐽 qTop 𝐹 ) ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) )
79 25 78 rexlimddv ⊢ ( ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ ( 𝑥 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ) ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) ∧ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ) → 𝑧 ∈ ∪ ( ( 𝐽 qTop 𝐹 ) ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) )
80 79 ex ⊢ ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ ( 𝑥 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ) ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) → ( 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) → 𝑧 ∈ ∪ ( ( 𝐽 qTop 𝐹 ) ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ) )
81 80 ssrdv ⊢ ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ ( 𝑥 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ) ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) → ( 𝑥 ∩ 𝑦 ) ⊆ ∪ ( ( 𝐽 qTop 𝐹 ) ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) )
82 81 3expib ⊢ ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) → ( ( ( 𝑥 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ) ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) → ( 𝑥 ∩ 𝑦 ) ⊆ ∪ ( ( 𝐽 qTop 𝐹 ) ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ) )
83 6 82 sylbid ⊢ ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) → ( ( 𝑥 ∈ ( 𝐽 qTop 𝐹 ) ∧ 𝑦 ∈ ( 𝐽 qTop 𝐹 ) ) → ( 𝑥 ∩ 𝑦 ) ⊆ ∪ ( ( 𝐽 qTop 𝐹 ) ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ) )
84 83 ralrimivv ⊢ ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) → ∀ 𝑥 ∈ ( 𝐽 qTop 𝐹 ) ∀ 𝑦 ∈ ( 𝐽 qTop 𝐹 ) ( 𝑥 ∩ 𝑦 ) ⊆ ∪ ( ( 𝐽 qTop 𝐹 ) ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) )
85 ovex ⊢ ( 𝐽 qTop 𝐹 ) ∈ V
86 isbasisg ⊢ ( ( 𝐽 qTop 𝐹 ) ∈ V → ( ( 𝐽 qTop 𝐹 ) ∈ TopBases ↔ ∀ 𝑥 ∈ ( 𝐽 qTop 𝐹 ) ∀ 𝑦 ∈ ( 𝐽 qTop 𝐹 ) ( 𝑥 ∩ 𝑦 ) ⊆ ∪ ( ( 𝐽 qTop 𝐹 ) ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ) )
87 85 86 ax-mp ⊢ ( ( 𝐽 qTop 𝐹 ) ∈ TopBases ↔ ∀ 𝑥 ∈ ( 𝐽 qTop 𝐹 ) ∀ 𝑦 ∈ ( 𝐽 qTop 𝐹 ) ( 𝑥 ∩ 𝑦 ) ⊆ ∪ ( ( 𝐽 qTop 𝐹 ) ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) )
88 84 87 sylibr ⊢ ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) → ( 𝐽 qTop 𝐹 ) ∈ TopBases )