MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  tgqtop Structured version   Visualization version   GIF version

Theorem tgqtop 23216
Description: An injection maps generated topologies to each other. (Contributed by Mario Carneiro, 27-Aug-2015.)
Hypothesis
Ref Expression
qtopcmp.1 𝑋 = βˆͺ 𝐽
Assertion
Ref Expression
tgqtop ((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-ontoβ†’π‘Œ) β†’ ((topGenβ€˜π½) qTop 𝐹) = (topGenβ€˜(𝐽 qTop 𝐹)))

Proof of Theorem tgqtop
Dummy variables π‘₯ 𝑀 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 f1ocnv 6846 . . . . . . . . 9 (𝐹:𝑋–1-1-ontoβ†’π‘Œ β†’ ◑𝐹:π‘Œβ€“1-1-onto→𝑋)
2 f1ofun 6836 . . . . . . . . 9 (◑𝐹:π‘Œβ€“1-1-onto→𝑋 β†’ Fun ◑𝐹)
31, 2syl 17 . . . . . . . 8 (𝐹:𝑋–1-1-ontoβ†’π‘Œ β†’ Fun ◑𝐹)
43ad2antlr 726 . . . . . . 7 (((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-ontoβ†’π‘Œ) ∧ π‘₯ βŠ† π‘Œ) β†’ Fun ◑𝐹)
5 simpr 486 . . . . . . . 8 (((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-ontoβ†’π‘Œ) ∧ π‘₯ βŠ† π‘Œ) β†’ π‘₯ βŠ† π‘Œ)
6 df-rn 5688 . . . . . . . . 9 ran 𝐹 = dom ◑𝐹
7 f1ofo 6841 . . . . . . . . . . 11 (𝐹:𝑋–1-1-ontoβ†’π‘Œ β†’ 𝐹:𝑋–ontoβ†’π‘Œ)
87ad2antlr 726 . . . . . . . . . 10 (((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-ontoβ†’π‘Œ) ∧ π‘₯ βŠ† π‘Œ) β†’ 𝐹:𝑋–ontoβ†’π‘Œ)
9 forn 6809 . . . . . . . . . 10 (𝐹:𝑋–ontoβ†’π‘Œ β†’ ran 𝐹 = π‘Œ)
108, 9syl 17 . . . . . . . . 9 (((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-ontoβ†’π‘Œ) ∧ π‘₯ βŠ† π‘Œ) β†’ ran 𝐹 = π‘Œ)
116, 10eqtr3id 2787 . . . . . . . 8 (((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-ontoβ†’π‘Œ) ∧ π‘₯ βŠ† π‘Œ) β†’ dom ◑𝐹 = π‘Œ)
125, 11sseqtrrd 4024 . . . . . . 7 (((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-ontoβ†’π‘Œ) ∧ π‘₯ βŠ† π‘Œ) β†’ π‘₯ βŠ† dom ◑𝐹)
13 funimass4 6957 . . . . . . 7 ((Fun ◑𝐹 ∧ π‘₯ βŠ† dom ◑𝐹) β†’ ((◑𝐹 β€œ π‘₯) βŠ† βˆͺ (𝐽 ∩ 𝒫 (◑𝐹 β€œ π‘₯)) ↔ βˆ€π‘¦ ∈ π‘₯ (β—‘πΉβ€˜π‘¦) ∈ βˆͺ (𝐽 ∩ 𝒫 (◑𝐹 β€œ π‘₯))))
144, 12, 13syl2anc 585 . . . . . 6 (((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-ontoβ†’π‘Œ) ∧ π‘₯ βŠ† π‘Œ) β†’ ((◑𝐹 β€œ π‘₯) βŠ† βˆͺ (𝐽 ∩ 𝒫 (◑𝐹 β€œ π‘₯)) ↔ βˆ€π‘¦ ∈ π‘₯ (β—‘πΉβ€˜π‘¦) ∈ βˆͺ (𝐽 ∩ 𝒫 (◑𝐹 β€œ π‘₯))))
15 dfss3 3971 . . . . . . 7 (π‘₯ βŠ† βˆͺ ((𝐽 qTop 𝐹) ∩ 𝒫 π‘₯) ↔ βˆ€π‘¦ ∈ π‘₯ 𝑦 ∈ βˆͺ ((𝐽 qTop 𝐹) ∩ 𝒫 π‘₯))
16 simprl 770 . . . . . . . . . . . . . . . 16 (((((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-ontoβ†’π‘Œ) ∧ π‘₯ βŠ† π‘Œ) ∧ 𝑦 ∈ π‘₯) ∧ (𝑧 ∈ ((𝐽 qTop 𝐹) ∩ 𝒫 π‘₯) ∧ 𝑦 ∈ 𝑧)) β†’ 𝑧 ∈ ((𝐽 qTop 𝐹) ∩ 𝒫 π‘₯))
1716elin1d 4199 . . . . . . . . . . . . . . 15 (((((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-ontoβ†’π‘Œ) ∧ π‘₯ βŠ† π‘Œ) ∧ 𝑦 ∈ π‘₯) ∧ (𝑧 ∈ ((𝐽 qTop 𝐹) ∩ 𝒫 π‘₯) ∧ 𝑦 ∈ 𝑧)) β†’ 𝑧 ∈ (𝐽 qTop 𝐹))
18 qtopcmp.1 . . . . . . . . . . . . . . . . . 18 𝑋 = βˆͺ 𝐽
1918elqtop2 23205 . . . . . . . . . . . . . . . . 17 ((𝐽 ∈ TopBases ∧ 𝐹:𝑋–ontoβ†’π‘Œ) β†’ (𝑧 ∈ (𝐽 qTop 𝐹) ↔ (𝑧 βŠ† π‘Œ ∧ (◑𝐹 β€œ 𝑧) ∈ 𝐽)))
207, 19sylan2 594 . . . . . . . . . . . . . . . 16 ((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-ontoβ†’π‘Œ) β†’ (𝑧 ∈ (𝐽 qTop 𝐹) ↔ (𝑧 βŠ† π‘Œ ∧ (◑𝐹 β€œ 𝑧) ∈ 𝐽)))
2120ad3antrrr 729 . . . . . . . . . . . . . . 15 (((((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-ontoβ†’π‘Œ) ∧ π‘₯ βŠ† π‘Œ) ∧ 𝑦 ∈ π‘₯) ∧ (𝑧 ∈ ((𝐽 qTop 𝐹) ∩ 𝒫 π‘₯) ∧ 𝑦 ∈ 𝑧)) β†’ (𝑧 ∈ (𝐽 qTop 𝐹) ↔ (𝑧 βŠ† π‘Œ ∧ (◑𝐹 β€œ 𝑧) ∈ 𝐽)))
2217, 21mpbid 231 . . . . . . . . . . . . . 14 (((((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-ontoβ†’π‘Œ) ∧ π‘₯ βŠ† π‘Œ) ∧ 𝑦 ∈ π‘₯) ∧ (𝑧 ∈ ((𝐽 qTop 𝐹) ∩ 𝒫 π‘₯) ∧ 𝑦 ∈ 𝑧)) β†’ (𝑧 βŠ† π‘Œ ∧ (◑𝐹 β€œ 𝑧) ∈ 𝐽))
2322simprd 497 . . . . . . . . . . . . 13 (((((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-ontoβ†’π‘Œ) ∧ π‘₯ βŠ† π‘Œ) ∧ 𝑦 ∈ π‘₯) ∧ (𝑧 ∈ ((𝐽 qTop 𝐹) ∩ 𝒫 π‘₯) ∧ 𝑦 ∈ 𝑧)) β†’ (◑𝐹 β€œ 𝑧) ∈ 𝐽)
2416elin2d 4200 . . . . . . . . . . . . . . . 16 (((((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-ontoβ†’π‘Œ) ∧ π‘₯ βŠ† π‘Œ) ∧ 𝑦 ∈ π‘₯) ∧ (𝑧 ∈ ((𝐽 qTop 𝐹) ∩ 𝒫 π‘₯) ∧ 𝑦 ∈ 𝑧)) β†’ 𝑧 ∈ 𝒫 π‘₯)
2524elpwid 4612 . . . . . . . . . . . . . . 15 (((((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-ontoβ†’π‘Œ) ∧ π‘₯ βŠ† π‘Œ) ∧ 𝑦 ∈ π‘₯) ∧ (𝑧 ∈ ((𝐽 qTop 𝐹) ∩ 𝒫 π‘₯) ∧ 𝑦 ∈ 𝑧)) β†’ 𝑧 βŠ† π‘₯)
26 imass2 6102 . . . . . . . . . . . . . . 15 (𝑧 βŠ† π‘₯ β†’ (◑𝐹 β€œ 𝑧) βŠ† (◑𝐹 β€œ π‘₯))
2725, 26syl 17 . . . . . . . . . . . . . 14 (((((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-ontoβ†’π‘Œ) ∧ π‘₯ βŠ† π‘Œ) ∧ 𝑦 ∈ π‘₯) ∧ (𝑧 ∈ ((𝐽 qTop 𝐹) ∩ 𝒫 π‘₯) ∧ 𝑦 ∈ 𝑧)) β†’ (◑𝐹 β€œ 𝑧) βŠ† (◑𝐹 β€œ π‘₯))
2823, 27elpwd 4609 . . . . . . . . . . . . 13 (((((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-ontoβ†’π‘Œ) ∧ π‘₯ βŠ† π‘Œ) ∧ 𝑦 ∈ π‘₯) ∧ (𝑧 ∈ ((𝐽 qTop 𝐹) ∩ 𝒫 π‘₯) ∧ 𝑦 ∈ 𝑧)) β†’ (◑𝐹 β€œ 𝑧) ∈ 𝒫 (◑𝐹 β€œ π‘₯))
2923, 28elind 4195 . . . . . . . . . . . 12 (((((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-ontoβ†’π‘Œ) ∧ π‘₯ βŠ† π‘Œ) ∧ 𝑦 ∈ π‘₯) ∧ (𝑧 ∈ ((𝐽 qTop 𝐹) ∩ 𝒫 π‘₯) ∧ 𝑦 ∈ 𝑧)) β†’ (◑𝐹 β€œ 𝑧) ∈ (𝐽 ∩ 𝒫 (◑𝐹 β€œ π‘₯)))
30 simp-4r 783 . . . . . . . . . . . . . . 15 (((((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-ontoβ†’π‘Œ) ∧ π‘₯ βŠ† π‘Œ) ∧ 𝑦 ∈ π‘₯) ∧ (𝑧 ∈ ((𝐽 qTop 𝐹) ∩ 𝒫 π‘₯) ∧ 𝑦 ∈ 𝑧)) β†’ 𝐹:𝑋–1-1-ontoβ†’π‘Œ)
3130, 1syl 17 . . . . . . . . . . . . . 14 (((((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-ontoβ†’π‘Œ) ∧ π‘₯ βŠ† π‘Œ) ∧ 𝑦 ∈ π‘₯) ∧ (𝑧 ∈ ((𝐽 qTop 𝐹) ∩ 𝒫 π‘₯) ∧ 𝑦 ∈ 𝑧)) β†’ ◑𝐹:π‘Œβ€“1-1-onto→𝑋)
32 f1ofn 6835 . . . . . . . . . . . . . 14 (◑𝐹:π‘Œβ€“1-1-onto→𝑋 β†’ ◑𝐹 Fn π‘Œ)
3331, 32syl 17 . . . . . . . . . . . . 13 (((((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-ontoβ†’π‘Œ) ∧ π‘₯ βŠ† π‘Œ) ∧ 𝑦 ∈ π‘₯) ∧ (𝑧 ∈ ((𝐽 qTop 𝐹) ∩ 𝒫 π‘₯) ∧ 𝑦 ∈ 𝑧)) β†’ ◑𝐹 Fn π‘Œ)
345ad2antrr 725 . . . . . . . . . . . . . 14 (((((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-ontoβ†’π‘Œ) ∧ π‘₯ βŠ† π‘Œ) ∧ 𝑦 ∈ π‘₯) ∧ (𝑧 ∈ ((𝐽 qTop 𝐹) ∩ 𝒫 π‘₯) ∧ 𝑦 ∈ 𝑧)) β†’ π‘₯ βŠ† π‘Œ)
3525, 34sstrd 3993 . . . . . . . . . . . . 13 (((((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-ontoβ†’π‘Œ) ∧ π‘₯ βŠ† π‘Œ) ∧ 𝑦 ∈ π‘₯) ∧ (𝑧 ∈ ((𝐽 qTop 𝐹) ∩ 𝒫 π‘₯) ∧ 𝑦 ∈ 𝑧)) β†’ 𝑧 βŠ† π‘Œ)
36 simprr 772 . . . . . . . . . . . . 13 (((((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-ontoβ†’π‘Œ) ∧ π‘₯ βŠ† π‘Œ) ∧ 𝑦 ∈ π‘₯) ∧ (𝑧 ∈ ((𝐽 qTop 𝐹) ∩ 𝒫 π‘₯) ∧ 𝑦 ∈ 𝑧)) β†’ 𝑦 ∈ 𝑧)
37 fnfvima 7235 . . . . . . . . . . . . 13 ((◑𝐹 Fn π‘Œ ∧ 𝑧 βŠ† π‘Œ ∧ 𝑦 ∈ 𝑧) β†’ (β—‘πΉβ€˜π‘¦) ∈ (◑𝐹 β€œ 𝑧))
3833, 35, 36, 37syl3anc 1372 . . . . . . . . . . . 12 (((((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-ontoβ†’π‘Œ) ∧ π‘₯ βŠ† π‘Œ) ∧ 𝑦 ∈ π‘₯) ∧ (𝑧 ∈ ((𝐽 qTop 𝐹) ∩ 𝒫 π‘₯) ∧ 𝑦 ∈ 𝑧)) β†’ (β—‘πΉβ€˜π‘¦) ∈ (◑𝐹 β€œ 𝑧))
39 eleq2 2823 . . . . . . . . . . . . 13 (𝑀 = (◑𝐹 β€œ 𝑧) β†’ ((β—‘πΉβ€˜π‘¦) ∈ 𝑀 ↔ (β—‘πΉβ€˜π‘¦) ∈ (◑𝐹 β€œ 𝑧)))
4039rspcev 3613 . . . . . . . . . . . 12 (((◑𝐹 β€œ 𝑧) ∈ (𝐽 ∩ 𝒫 (◑𝐹 β€œ π‘₯)) ∧ (β—‘πΉβ€˜π‘¦) ∈ (◑𝐹 β€œ 𝑧)) β†’ βˆƒπ‘€ ∈ (𝐽 ∩ 𝒫 (◑𝐹 β€œ π‘₯))(β—‘πΉβ€˜π‘¦) ∈ 𝑀)
4129, 38, 40syl2anc 585 . . . . . . . . . . 11 (((((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-ontoβ†’π‘Œ) ∧ π‘₯ βŠ† π‘Œ) ∧ 𝑦 ∈ π‘₯) ∧ (𝑧 ∈ ((𝐽 qTop 𝐹) ∩ 𝒫 π‘₯) ∧ 𝑦 ∈ 𝑧)) β†’ βˆƒπ‘€ ∈ (𝐽 ∩ 𝒫 (◑𝐹 β€œ π‘₯))(β—‘πΉβ€˜π‘¦) ∈ 𝑀)
4241rexlimdvaa 3157 . . . . . . . . . 10 ((((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-ontoβ†’π‘Œ) ∧ π‘₯ βŠ† π‘Œ) ∧ 𝑦 ∈ π‘₯) β†’ (βˆƒπ‘§ ∈ ((𝐽 qTop 𝐹) ∩ 𝒫 π‘₯)𝑦 ∈ 𝑧 β†’ βˆƒπ‘€ ∈ (𝐽 ∩ 𝒫 (◑𝐹 β€œ π‘₯))(β—‘πΉβ€˜π‘¦) ∈ 𝑀))
43 simp-4r 783 . . . . . . . . . . . . . . . . 17 (((((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-ontoβ†’π‘Œ) ∧ π‘₯ βŠ† π‘Œ) ∧ 𝑦 ∈ π‘₯) ∧ (𝑀 ∈ (𝐽 ∩ 𝒫 (◑𝐹 β€œ π‘₯)) ∧ (β—‘πΉβ€˜π‘¦) ∈ 𝑀)) β†’ 𝐹:𝑋–1-1-ontoβ†’π‘Œ)
44 f1ofun 6836 . . . . . . . . . . . . . . . . 17 (𝐹:𝑋–1-1-ontoβ†’π‘Œ β†’ Fun 𝐹)
4543, 44syl 17 . . . . . . . . . . . . . . . 16 (((((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-ontoβ†’π‘Œ) ∧ π‘₯ βŠ† π‘Œ) ∧ 𝑦 ∈ π‘₯) ∧ (𝑀 ∈ (𝐽 ∩ 𝒫 (◑𝐹 β€œ π‘₯)) ∧ (β—‘πΉβ€˜π‘¦) ∈ 𝑀)) β†’ Fun 𝐹)
46 simprl 770 . . . . . . . . . . . . . . . . . 18 (((((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-ontoβ†’π‘Œ) ∧ π‘₯ βŠ† π‘Œ) ∧ 𝑦 ∈ π‘₯) ∧ (𝑀 ∈ (𝐽 ∩ 𝒫 (◑𝐹 β€œ π‘₯)) ∧ (β—‘πΉβ€˜π‘¦) ∈ 𝑀)) β†’ 𝑀 ∈ (𝐽 ∩ 𝒫 (◑𝐹 β€œ π‘₯)))
4746elin2d 4200 . . . . . . . . . . . . . . . . 17 (((((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-ontoβ†’π‘Œ) ∧ π‘₯ βŠ† π‘Œ) ∧ 𝑦 ∈ π‘₯) ∧ (𝑀 ∈ (𝐽 ∩ 𝒫 (◑𝐹 β€œ π‘₯)) ∧ (β—‘πΉβ€˜π‘¦) ∈ 𝑀)) β†’ 𝑀 ∈ 𝒫 (◑𝐹 β€œ π‘₯))
4847elpwid 4612 . . . . . . . . . . . . . . . 16 (((((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-ontoβ†’π‘Œ) ∧ π‘₯ βŠ† π‘Œ) ∧ 𝑦 ∈ π‘₯) ∧ (𝑀 ∈ (𝐽 ∩ 𝒫 (◑𝐹 β€œ π‘₯)) ∧ (β—‘πΉβ€˜π‘¦) ∈ 𝑀)) β†’ 𝑀 βŠ† (◑𝐹 β€œ π‘₯))
49 funimass2 6632 . . . . . . . . . . . . . . . 16 ((Fun 𝐹 ∧ 𝑀 βŠ† (◑𝐹 β€œ π‘₯)) β†’ (𝐹 β€œ 𝑀) βŠ† π‘₯)
5045, 48, 49syl2anc 585 . . . . . . . . . . . . . . 15 (((((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-ontoβ†’π‘Œ) ∧ π‘₯ βŠ† π‘Œ) ∧ 𝑦 ∈ π‘₯) ∧ (𝑀 ∈ (𝐽 ∩ 𝒫 (◑𝐹 β€œ π‘₯)) ∧ (β—‘πΉβ€˜π‘¦) ∈ 𝑀)) β†’ (𝐹 β€œ 𝑀) βŠ† π‘₯)
515ad2antrr 725 . . . . . . . . . . . . . . 15 (((((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-ontoβ†’π‘Œ) ∧ π‘₯ βŠ† π‘Œ) ∧ 𝑦 ∈ π‘₯) ∧ (𝑀 ∈ (𝐽 ∩ 𝒫 (◑𝐹 β€œ π‘₯)) ∧ (β—‘πΉβ€˜π‘¦) ∈ 𝑀)) β†’ π‘₯ βŠ† π‘Œ)
5250, 51sstrd 3993 . . . . . . . . . . . . . 14 (((((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-ontoβ†’π‘Œ) ∧ π‘₯ βŠ† π‘Œ) ∧ 𝑦 ∈ π‘₯) ∧ (𝑀 ∈ (𝐽 ∩ 𝒫 (◑𝐹 β€œ π‘₯)) ∧ (β—‘πΉβ€˜π‘¦) ∈ 𝑀)) β†’ (𝐹 β€œ 𝑀) βŠ† π‘Œ)
53 f1of1 6833 . . . . . . . . . . . . . . . . 17 (𝐹:𝑋–1-1-ontoβ†’π‘Œ β†’ 𝐹:𝑋–1-1β†’π‘Œ)
5443, 53syl 17 . . . . . . . . . . . . . . . 16 (((((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-ontoβ†’π‘Œ) ∧ π‘₯ βŠ† π‘Œ) ∧ 𝑦 ∈ π‘₯) ∧ (𝑀 ∈ (𝐽 ∩ 𝒫 (◑𝐹 β€œ π‘₯)) ∧ (β—‘πΉβ€˜π‘¦) ∈ 𝑀)) β†’ 𝐹:𝑋–1-1β†’π‘Œ)
5546elin1d 4199 . . . . . . . . . . . . . . . . 17 (((((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-ontoβ†’π‘Œ) ∧ π‘₯ βŠ† π‘Œ) ∧ 𝑦 ∈ π‘₯) ∧ (𝑀 ∈ (𝐽 ∩ 𝒫 (◑𝐹 β€œ π‘₯)) ∧ (β—‘πΉβ€˜π‘¦) ∈ 𝑀)) β†’ 𝑀 ∈ 𝐽)
56 elssuni 4942 . . . . . . . . . . . . . . . . . 18 (𝑀 ∈ 𝐽 β†’ 𝑀 βŠ† βˆͺ 𝐽)
5756, 18sseqtrrdi 4034 . . . . . . . . . . . . . . . . 17 (𝑀 ∈ 𝐽 β†’ 𝑀 βŠ† 𝑋)
5855, 57syl 17 . . . . . . . . . . . . . . . 16 (((((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-ontoβ†’π‘Œ) ∧ π‘₯ βŠ† π‘Œ) ∧ 𝑦 ∈ π‘₯) ∧ (𝑀 ∈ (𝐽 ∩ 𝒫 (◑𝐹 β€œ π‘₯)) ∧ (β—‘πΉβ€˜π‘¦) ∈ 𝑀)) β†’ 𝑀 βŠ† 𝑋)
59 f1imacnv 6850 . . . . . . . . . . . . . . . 16 ((𝐹:𝑋–1-1β†’π‘Œ ∧ 𝑀 βŠ† 𝑋) β†’ (◑𝐹 β€œ (𝐹 β€œ 𝑀)) = 𝑀)
6054, 58, 59syl2anc 585 . . . . . . . . . . . . . . 15 (((((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-ontoβ†’π‘Œ) ∧ π‘₯ βŠ† π‘Œ) ∧ 𝑦 ∈ π‘₯) ∧ (𝑀 ∈ (𝐽 ∩ 𝒫 (◑𝐹 β€œ π‘₯)) ∧ (β—‘πΉβ€˜π‘¦) ∈ 𝑀)) β†’ (◑𝐹 β€œ (𝐹 β€œ 𝑀)) = 𝑀)
6160, 55eqeltrd 2834 . . . . . . . . . . . . . 14 (((((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-ontoβ†’π‘Œ) ∧ π‘₯ βŠ† π‘Œ) ∧ 𝑦 ∈ π‘₯) ∧ (𝑀 ∈ (𝐽 ∩ 𝒫 (◑𝐹 β€œ π‘₯)) ∧ (β—‘πΉβ€˜π‘¦) ∈ 𝑀)) β†’ (◑𝐹 β€œ (𝐹 β€œ 𝑀)) ∈ 𝐽)
6218elqtop2 23205 . . . . . . . . . . . . . . . 16 ((𝐽 ∈ TopBases ∧ 𝐹:𝑋–ontoβ†’π‘Œ) β†’ ((𝐹 β€œ 𝑀) ∈ (𝐽 qTop 𝐹) ↔ ((𝐹 β€œ 𝑀) βŠ† π‘Œ ∧ (◑𝐹 β€œ (𝐹 β€œ 𝑀)) ∈ 𝐽)))
637, 62sylan2 594 . . . . . . . . . . . . . . 15 ((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-ontoβ†’π‘Œ) β†’ ((𝐹 β€œ 𝑀) ∈ (𝐽 qTop 𝐹) ↔ ((𝐹 β€œ 𝑀) βŠ† π‘Œ ∧ (◑𝐹 β€œ (𝐹 β€œ 𝑀)) ∈ 𝐽)))
6463ad3antrrr 729 . . . . . . . . . . . . . 14 (((((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-ontoβ†’π‘Œ) ∧ π‘₯ βŠ† π‘Œ) ∧ 𝑦 ∈ π‘₯) ∧ (𝑀 ∈ (𝐽 ∩ 𝒫 (◑𝐹 β€œ π‘₯)) ∧ (β—‘πΉβ€˜π‘¦) ∈ 𝑀)) β†’ ((𝐹 β€œ 𝑀) ∈ (𝐽 qTop 𝐹) ↔ ((𝐹 β€œ 𝑀) βŠ† π‘Œ ∧ (◑𝐹 β€œ (𝐹 β€œ 𝑀)) ∈ 𝐽)))
6552, 61, 64mpbir2and 712 . . . . . . . . . . . . 13 (((((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-ontoβ†’π‘Œ) ∧ π‘₯ βŠ† π‘Œ) ∧ 𝑦 ∈ π‘₯) ∧ (𝑀 ∈ (𝐽 ∩ 𝒫 (◑𝐹 β€œ π‘₯)) ∧ (β—‘πΉβ€˜π‘¦) ∈ 𝑀)) β†’ (𝐹 β€œ 𝑀) ∈ (𝐽 qTop 𝐹))
66 vex 3479 . . . . . . . . . . . . . . 15 π‘₯ ∈ V
6766elpw2 5346 . . . . . . . . . . . . . 14 ((𝐹 β€œ 𝑀) ∈ 𝒫 π‘₯ ↔ (𝐹 β€œ 𝑀) βŠ† π‘₯)
6850, 67sylibr 233 . . . . . . . . . . . . 13 (((((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-ontoβ†’π‘Œ) ∧ π‘₯ βŠ† π‘Œ) ∧ 𝑦 ∈ π‘₯) ∧ (𝑀 ∈ (𝐽 ∩ 𝒫 (◑𝐹 β€œ π‘₯)) ∧ (β—‘πΉβ€˜π‘¦) ∈ 𝑀)) β†’ (𝐹 β€œ 𝑀) ∈ 𝒫 π‘₯)
6965, 68elind 4195 . . . . . . . . . . . 12 (((((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-ontoβ†’π‘Œ) ∧ π‘₯ βŠ† π‘Œ) ∧ 𝑦 ∈ π‘₯) ∧ (𝑀 ∈ (𝐽 ∩ 𝒫 (◑𝐹 β€œ π‘₯)) ∧ (β—‘πΉβ€˜π‘¦) ∈ 𝑀)) β†’ (𝐹 β€œ 𝑀) ∈ ((𝐽 qTop 𝐹) ∩ 𝒫 π‘₯))
705sselda 3983 . . . . . . . . . . . . . . 15 ((((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-ontoβ†’π‘Œ) ∧ π‘₯ βŠ† π‘Œ) ∧ 𝑦 ∈ π‘₯) β†’ 𝑦 ∈ π‘Œ)
7170adantr 482 . . . . . . . . . . . . . 14 (((((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-ontoβ†’π‘Œ) ∧ π‘₯ βŠ† π‘Œ) ∧ 𝑦 ∈ π‘₯) ∧ (𝑀 ∈ (𝐽 ∩ 𝒫 (◑𝐹 β€œ π‘₯)) ∧ (β—‘πΉβ€˜π‘¦) ∈ 𝑀)) β†’ 𝑦 ∈ π‘Œ)
72 f1ocnvfv2 7275 . . . . . . . . . . . . . 14 ((𝐹:𝑋–1-1-ontoβ†’π‘Œ ∧ 𝑦 ∈ π‘Œ) β†’ (πΉβ€˜(β—‘πΉβ€˜π‘¦)) = 𝑦)
7343, 71, 72syl2anc 585 . . . . . . . . . . . . 13 (((((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-ontoβ†’π‘Œ) ∧ π‘₯ βŠ† π‘Œ) ∧ 𝑦 ∈ π‘₯) ∧ (𝑀 ∈ (𝐽 ∩ 𝒫 (◑𝐹 β€œ π‘₯)) ∧ (β—‘πΉβ€˜π‘¦) ∈ 𝑀)) β†’ (πΉβ€˜(β—‘πΉβ€˜π‘¦)) = 𝑦)
74 f1ofn 6835 . . . . . . . . . . . . . . . 16 (𝐹:𝑋–1-1-ontoβ†’π‘Œ β†’ 𝐹 Fn 𝑋)
7574adantl 483 . . . . . . . . . . . . . . 15 ((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-ontoβ†’π‘Œ) β†’ 𝐹 Fn 𝑋)
7675ad3antrrr 729 . . . . . . . . . . . . . 14 (((((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-ontoβ†’π‘Œ) ∧ π‘₯ βŠ† π‘Œ) ∧ 𝑦 ∈ π‘₯) ∧ (𝑀 ∈ (𝐽 ∩ 𝒫 (◑𝐹 β€œ π‘₯)) ∧ (β—‘πΉβ€˜π‘¦) ∈ 𝑀)) β†’ 𝐹 Fn 𝑋)
77 simprr 772 . . . . . . . . . . . . . 14 (((((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-ontoβ†’π‘Œ) ∧ π‘₯ βŠ† π‘Œ) ∧ 𝑦 ∈ π‘₯) ∧ (𝑀 ∈ (𝐽 ∩ 𝒫 (◑𝐹 β€œ π‘₯)) ∧ (β—‘πΉβ€˜π‘¦) ∈ 𝑀)) β†’ (β—‘πΉβ€˜π‘¦) ∈ 𝑀)
78 fnfvima 7235 . . . . . . . . . . . . . 14 ((𝐹 Fn 𝑋 ∧ 𝑀 βŠ† 𝑋 ∧ (β—‘πΉβ€˜π‘¦) ∈ 𝑀) β†’ (πΉβ€˜(β—‘πΉβ€˜π‘¦)) ∈ (𝐹 β€œ 𝑀))
7976, 58, 77, 78syl3anc 1372 . . . . . . . . . . . . 13 (((((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-ontoβ†’π‘Œ) ∧ π‘₯ βŠ† π‘Œ) ∧ 𝑦 ∈ π‘₯) ∧ (𝑀 ∈ (𝐽 ∩ 𝒫 (◑𝐹 β€œ π‘₯)) ∧ (β—‘πΉβ€˜π‘¦) ∈ 𝑀)) β†’ (πΉβ€˜(β—‘πΉβ€˜π‘¦)) ∈ (𝐹 β€œ 𝑀))
8073, 79eqeltrrd 2835 . . . . . . . . . . . 12 (((((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-ontoβ†’π‘Œ) ∧ π‘₯ βŠ† π‘Œ) ∧ 𝑦 ∈ π‘₯) ∧ (𝑀 ∈ (𝐽 ∩ 𝒫 (◑𝐹 β€œ π‘₯)) ∧ (β—‘πΉβ€˜π‘¦) ∈ 𝑀)) β†’ 𝑦 ∈ (𝐹 β€œ 𝑀))
81 eleq2 2823 . . . . . . . . . . . . 13 (𝑧 = (𝐹 β€œ 𝑀) β†’ (𝑦 ∈ 𝑧 ↔ 𝑦 ∈ (𝐹 β€œ 𝑀)))
8281rspcev 3613 . . . . . . . . . . . 12 (((𝐹 β€œ 𝑀) ∈ ((𝐽 qTop 𝐹) ∩ 𝒫 π‘₯) ∧ 𝑦 ∈ (𝐹 β€œ 𝑀)) β†’ βˆƒπ‘§ ∈ ((𝐽 qTop 𝐹) ∩ 𝒫 π‘₯)𝑦 ∈ 𝑧)
8369, 80, 82syl2anc 585 . . . . . . . . . . 11 (((((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-ontoβ†’π‘Œ) ∧ π‘₯ βŠ† π‘Œ) ∧ 𝑦 ∈ π‘₯) ∧ (𝑀 ∈ (𝐽 ∩ 𝒫 (◑𝐹 β€œ π‘₯)) ∧ (β—‘πΉβ€˜π‘¦) ∈ 𝑀)) β†’ βˆƒπ‘§ ∈ ((𝐽 qTop 𝐹) ∩ 𝒫 π‘₯)𝑦 ∈ 𝑧)
8483rexlimdvaa 3157 . . . . . . . . . 10 ((((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-ontoβ†’π‘Œ) ∧ π‘₯ βŠ† π‘Œ) ∧ 𝑦 ∈ π‘₯) β†’ (βˆƒπ‘€ ∈ (𝐽 ∩ 𝒫 (◑𝐹 β€œ π‘₯))(β—‘πΉβ€˜π‘¦) ∈ 𝑀 β†’ βˆƒπ‘§ ∈ ((𝐽 qTop 𝐹) ∩ 𝒫 π‘₯)𝑦 ∈ 𝑧))
8542, 84impbid 211 . . . . . . . . 9 ((((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-ontoβ†’π‘Œ) ∧ π‘₯ βŠ† π‘Œ) ∧ 𝑦 ∈ π‘₯) β†’ (βˆƒπ‘§ ∈ ((𝐽 qTop 𝐹) ∩ 𝒫 π‘₯)𝑦 ∈ 𝑧 ↔ βˆƒπ‘€ ∈ (𝐽 ∩ 𝒫 (◑𝐹 β€œ π‘₯))(β—‘πΉβ€˜π‘¦) ∈ 𝑀))
86 eluni2 4913 . . . . . . . . 9 (𝑦 ∈ βˆͺ ((𝐽 qTop 𝐹) ∩ 𝒫 π‘₯) ↔ βˆƒπ‘§ ∈ ((𝐽 qTop 𝐹) ∩ 𝒫 π‘₯)𝑦 ∈ 𝑧)
87 eluni2 4913 . . . . . . . . 9 ((β—‘πΉβ€˜π‘¦) ∈ βˆͺ (𝐽 ∩ 𝒫 (◑𝐹 β€œ π‘₯)) ↔ βˆƒπ‘€ ∈ (𝐽 ∩ 𝒫 (◑𝐹 β€œ π‘₯))(β—‘πΉβ€˜π‘¦) ∈ 𝑀)
8885, 86, 873bitr4g 314 . . . . . . . 8 ((((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-ontoβ†’π‘Œ) ∧ π‘₯ βŠ† π‘Œ) ∧ 𝑦 ∈ π‘₯) β†’ (𝑦 ∈ βˆͺ ((𝐽 qTop 𝐹) ∩ 𝒫 π‘₯) ↔ (β—‘πΉβ€˜π‘¦) ∈ βˆͺ (𝐽 ∩ 𝒫 (◑𝐹 β€œ π‘₯))))
8988ralbidva 3176 . . . . . . 7 (((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-ontoβ†’π‘Œ) ∧ π‘₯ βŠ† π‘Œ) β†’ (βˆ€π‘¦ ∈ π‘₯ 𝑦 ∈ βˆͺ ((𝐽 qTop 𝐹) ∩ 𝒫 π‘₯) ↔ βˆ€π‘¦ ∈ π‘₯ (β—‘πΉβ€˜π‘¦) ∈ βˆͺ (𝐽 ∩ 𝒫 (◑𝐹 β€œ π‘₯))))
9015, 89bitrid 283 . . . . . 6 (((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-ontoβ†’π‘Œ) ∧ π‘₯ βŠ† π‘Œ) β†’ (π‘₯ βŠ† βˆͺ ((𝐽 qTop 𝐹) ∩ 𝒫 π‘₯) ↔ βˆ€π‘¦ ∈ π‘₯ (β—‘πΉβ€˜π‘¦) ∈ βˆͺ (𝐽 ∩ 𝒫 (◑𝐹 β€œ π‘₯))))
9114, 90bitr4d 282 . . . . 5 (((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-ontoβ†’π‘Œ) ∧ π‘₯ βŠ† π‘Œ) β†’ ((◑𝐹 β€œ π‘₯) βŠ† βˆͺ (𝐽 ∩ 𝒫 (◑𝐹 β€œ π‘₯)) ↔ π‘₯ βŠ† βˆͺ ((𝐽 qTop 𝐹) ∩ 𝒫 π‘₯)))
92 eltg 22460 . . . . . 6 (𝐽 ∈ TopBases β†’ ((◑𝐹 β€œ π‘₯) ∈ (topGenβ€˜π½) ↔ (◑𝐹 β€œ π‘₯) βŠ† βˆͺ (𝐽 ∩ 𝒫 (◑𝐹 β€œ π‘₯))))
9392ad2antrr 725 . . . . 5 (((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-ontoβ†’π‘Œ) ∧ π‘₯ βŠ† π‘Œ) β†’ ((◑𝐹 β€œ π‘₯) ∈ (topGenβ€˜π½) ↔ (◑𝐹 β€œ π‘₯) βŠ† βˆͺ (𝐽 ∩ 𝒫 (◑𝐹 β€œ π‘₯))))
94 ovex 7442 . . . . . 6 (𝐽 qTop 𝐹) ∈ V
95 eltg 22460 . . . . . 6 ((𝐽 qTop 𝐹) ∈ V β†’ (π‘₯ ∈ (topGenβ€˜(𝐽 qTop 𝐹)) ↔ π‘₯ βŠ† βˆͺ ((𝐽 qTop 𝐹) ∩ 𝒫 π‘₯)))
9694, 95mp1i 13 . . . . 5 (((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-ontoβ†’π‘Œ) ∧ π‘₯ βŠ† π‘Œ) β†’ (π‘₯ ∈ (topGenβ€˜(𝐽 qTop 𝐹)) ↔ π‘₯ βŠ† βˆͺ ((𝐽 qTop 𝐹) ∩ 𝒫 π‘₯)))
9791, 93, 963bitr4d 311 . . . 4 (((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-ontoβ†’π‘Œ) ∧ π‘₯ βŠ† π‘Œ) β†’ ((◑𝐹 β€œ π‘₯) ∈ (topGenβ€˜π½) ↔ π‘₯ ∈ (topGenβ€˜(𝐽 qTop 𝐹))))
9897pm5.32da 580 . . 3 ((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-ontoβ†’π‘Œ) β†’ ((π‘₯ βŠ† π‘Œ ∧ (◑𝐹 β€œ π‘₯) ∈ (topGenβ€˜π½)) ↔ (π‘₯ βŠ† π‘Œ ∧ π‘₯ ∈ (topGenβ€˜(𝐽 qTop 𝐹)))))
99 tgtopon 22474 . . . . . 6 (𝐽 ∈ TopBases β†’ (topGenβ€˜π½) ∈ (TopOnβ€˜βˆͺ 𝐽))
10099adantr 482 . . . . 5 ((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-ontoβ†’π‘Œ) β†’ (topGenβ€˜π½) ∈ (TopOnβ€˜βˆͺ 𝐽))
10118fveq2i 6895 . . . . 5 (TopOnβ€˜π‘‹) = (TopOnβ€˜βˆͺ 𝐽)
102100, 101eleqtrrdi 2845 . . . 4 ((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-ontoβ†’π‘Œ) β†’ (topGenβ€˜π½) ∈ (TopOnβ€˜π‘‹))
1037adantl 483 . . . 4 ((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-ontoβ†’π‘Œ) β†’ 𝐹:𝑋–ontoβ†’π‘Œ)
104 elqtop3 23207 . . . 4 (((topGenβ€˜π½) ∈ (TopOnβ€˜π‘‹) ∧ 𝐹:𝑋–ontoβ†’π‘Œ) β†’ (π‘₯ ∈ ((topGenβ€˜π½) qTop 𝐹) ↔ (π‘₯ βŠ† π‘Œ ∧ (◑𝐹 β€œ π‘₯) ∈ (topGenβ€˜π½))))
105102, 103, 104syl2anc 585 . . 3 ((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-ontoβ†’π‘Œ) β†’ (π‘₯ ∈ ((topGenβ€˜π½) qTop 𝐹) ↔ (π‘₯ βŠ† π‘Œ ∧ (◑𝐹 β€œ π‘₯) ∈ (topGenβ€˜π½))))
106 unitg 22470 . . . . . . . . 9 ((𝐽 qTop 𝐹) ∈ V β†’ βˆͺ (topGenβ€˜(𝐽 qTop 𝐹)) = βˆͺ (𝐽 qTop 𝐹))
10794, 106ax-mp 5 . . . . . . . 8 βˆͺ (topGenβ€˜(𝐽 qTop 𝐹)) = βˆͺ (𝐽 qTop 𝐹)
10818elqtop2 23205 . . . . . . . . . . . 12 ((𝐽 ∈ TopBases ∧ 𝐹:𝑋–ontoβ†’π‘Œ) β†’ (π‘₯ ∈ (𝐽 qTop 𝐹) ↔ (π‘₯ βŠ† π‘Œ ∧ (◑𝐹 β€œ π‘₯) ∈ 𝐽)))
1097, 108sylan2 594 . . . . . . . . . . 11 ((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-ontoβ†’π‘Œ) β†’ (π‘₯ ∈ (𝐽 qTop 𝐹) ↔ (π‘₯ βŠ† π‘Œ ∧ (◑𝐹 β€œ π‘₯) ∈ 𝐽)))
110 simpl 484 . . . . . . . . . . . 12 ((π‘₯ βŠ† π‘Œ ∧ (◑𝐹 β€œ π‘₯) ∈ 𝐽) β†’ π‘₯ βŠ† π‘Œ)
111 velpw 4608 . . . . . . . . . . . 12 (π‘₯ ∈ 𝒫 π‘Œ ↔ π‘₯ βŠ† π‘Œ)
112110, 111sylibr 233 . . . . . . . . . . 11 ((π‘₯ βŠ† π‘Œ ∧ (◑𝐹 β€œ π‘₯) ∈ 𝐽) β†’ π‘₯ ∈ 𝒫 π‘Œ)
113109, 112syl6bi 253 . . . . . . . . . 10 ((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-ontoβ†’π‘Œ) β†’ (π‘₯ ∈ (𝐽 qTop 𝐹) β†’ π‘₯ ∈ 𝒫 π‘Œ))
114113ssrdv 3989 . . . . . . . . 9 ((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-ontoβ†’π‘Œ) β†’ (𝐽 qTop 𝐹) βŠ† 𝒫 π‘Œ)
115 sspwuni 5104 . . . . . . . . 9 ((𝐽 qTop 𝐹) βŠ† 𝒫 π‘Œ ↔ βˆͺ (𝐽 qTop 𝐹) βŠ† π‘Œ)
116114, 115sylib 217 . . . . . . . 8 ((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-ontoβ†’π‘Œ) β†’ βˆͺ (𝐽 qTop 𝐹) βŠ† π‘Œ)
117107, 116eqsstrid 4031 . . . . . . 7 ((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-ontoβ†’π‘Œ) β†’ βˆͺ (topGenβ€˜(𝐽 qTop 𝐹)) βŠ† π‘Œ)
118 sspwuni 5104 . . . . . . 7 ((topGenβ€˜(𝐽 qTop 𝐹)) βŠ† 𝒫 π‘Œ ↔ βˆͺ (topGenβ€˜(𝐽 qTop 𝐹)) βŠ† π‘Œ)
119117, 118sylibr 233 . . . . . 6 ((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-ontoβ†’π‘Œ) β†’ (topGenβ€˜(𝐽 qTop 𝐹)) βŠ† 𝒫 π‘Œ)
120119sseld 3982 . . . . 5 ((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-ontoβ†’π‘Œ) β†’ (π‘₯ ∈ (topGenβ€˜(𝐽 qTop 𝐹)) β†’ π‘₯ ∈ 𝒫 π‘Œ))
121120, 111imbitrdi 250 . . . 4 ((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-ontoβ†’π‘Œ) β†’ (π‘₯ ∈ (topGenβ€˜(𝐽 qTop 𝐹)) β†’ π‘₯ βŠ† π‘Œ))
122121pm4.71rd 564 . . 3 ((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-ontoβ†’π‘Œ) β†’ (π‘₯ ∈ (topGenβ€˜(𝐽 qTop 𝐹)) ↔ (π‘₯ βŠ† π‘Œ ∧ π‘₯ ∈ (topGenβ€˜(𝐽 qTop 𝐹)))))
12398, 105, 1223bitr4d 311 . 2 ((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-ontoβ†’π‘Œ) β†’ (π‘₯ ∈ ((topGenβ€˜π½) qTop 𝐹) ↔ π‘₯ ∈ (topGenβ€˜(𝐽 qTop 𝐹))))
124123eqrdv 2731 1 ((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-ontoβ†’π‘Œ) β†’ ((topGenβ€˜π½) qTop 𝐹) = (topGenβ€˜(𝐽 qTop 𝐹)))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 397   = wceq 1542   ∈ wcel 2107  βˆ€wral 3062  βˆƒwrex 3071  Vcvv 3475   ∩ cin 3948   βŠ† wss 3949  π’« cpw 4603  βˆͺ cuni 4909  β—‘ccnv 5676  dom cdm 5677  ran crn 5678   β€œ cima 5680  Fun wfun 6538   Fn wfn 6539  β€“1-1β†’wf1 6541  β€“ontoβ†’wfo 6542  β€“1-1-ontoβ†’wf1o 6543  β€˜cfv 6544  (class class class)co 7409  topGenctg 17383   qTop cqtop 17449  TopOnctopon 22412  TopBasesctb 22448
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5286  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7725
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-ral 3063  df-rex 3072  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-iun 5000  df-br 5150  df-opab 5212  df-mpt 5233  df-id 5575  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-ov 7412  df-oprab 7413  df-mpo 7414  df-topgen 17389  df-qtop 17453  df-top 22396  df-topon 22413  df-bases 22449
This theorem is referenced by:  imasf1oxms  23998
  Copyright terms: Public domain W3C validator