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 )