Theorem tgqtop 24061

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-1onto𝑌) → ((topGen‘𝐽) qTop 𝐹) = (topGen‘(𝐽 qTop 𝐹)))

Proof of Theorem tgqtop

Dummy variables 𝑥 𝑤 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		f1ocnv 6859	. . . . . . . . 9 ⊢ (𝐹:𝑋⟶1-1onto𝑌 → ◡𝐹:𝑌⟶1-1onto𝑋)
2		f1ofun 6848	. . . . . . . . 9 ⊢ (◡𝐹:𝑌⟶1-1onto𝑋 → Fun ◡𝐹)
3	1, 2	syl 18	. . . . . . . 8 ⊢ (𝐹:𝑋⟶1-1onto𝑌 → Fun ◡𝐹)
4	3	ad2antlr 740	. . . . . . 7 ⊢ (((𝐽 ∈ TopBases ∧ 𝐹:𝑋⟶1-1onto𝑌) ∧ 𝑥 ⊆ 𝑌) → Fun ◡𝐹)
5		simpr 490	. . . . . . . 8 ⊢ (((𝐽 ∈ TopBases ∧ 𝐹:𝑋⟶1-1onto𝑌) ∧ 𝑥 ⊆ 𝑌) → 𝑥 ⊆ 𝑌)
6		df-rn 5666	. . . . . . . . 9 ⊢ ran 𝐹 = dom ◡𝐹
7		f1ofo 6854	. . . . . . . . . . 11 ⊢ (𝐹:𝑋⟶1-1onto𝑌 → 𝐹:𝑋⟶onto𝑌)
8	7	ad2antlr 740	. . . . . . . . . 10 ⊢ (((𝐽 ∈ TopBases ∧ 𝐹:𝑋⟶1-1onto𝑌) ∧ 𝑥 ⊆ 𝑌) → 𝐹:𝑋⟶onto𝑌)
9		forn 6821	. . . . . . . . . 10 ⊢ (𝐹:𝑋⟶onto𝑌 → ran 𝐹 = 𝑌)
10	8, 9	syl 18	. . . . . . . . 9 ⊢ (((𝐽 ∈ TopBases ∧ 𝐹:𝑋⟶1-1onto𝑌) ∧ 𝑥 ⊆ 𝑌) → ran 𝐹 = 𝑌)
11	6, 10	eqtr3id 2812	. . . . . . . 8 ⊢ (((𝐽 ∈ TopBases ∧ 𝐹:𝑋⟶1-1onto𝑌) ∧ 𝑥 ⊆ 𝑌) → dom ◡𝐹 = 𝑌)
12	5, 11	sseqtrrd 3950	. . . . . . 7 ⊢ (((𝐽 ∈ TopBases ∧ 𝐹:𝑋⟶1-1onto𝑌) ∧ 𝑥 ⊆ 𝑌) → 𝑥 ⊆ dom ◡𝐹)
13		funimass4 6972	. . . . . . 7 ⊢ ((Fun ◡𝐹 ∧ 𝑥 ⊆ dom ◡𝐹) → ((◡𝐹 “ 𝑥) ⊆ ∪ (𝐽 ∩ 𝒫 (◡𝐹 “ 𝑥)) ↔ ∀𝑦 ∈ 𝑥 (◡𝐹‘𝑦) ∈ ∪ (𝐽 ∩ 𝒫 (◡𝐹 “ 𝑥))))
14	4, 12, 13	syl2anc 596	. . . . . 6 ⊢ (((𝐽 ∈ TopBases ∧ 𝐹:𝑋⟶1-1onto𝑌) ∧ 𝑥 ⊆ 𝑌) → ((◡𝐹 “ 𝑥) ⊆ ∪ (𝐽 ∩ 𝒫 (◡𝐹 “ 𝑥)) ↔ ∀𝑦 ∈ 𝑥 (◡𝐹‘𝑦) ∈ ∪ (𝐽 ∩ 𝒫 (◡𝐹 “ 𝑥))))
15		dfss3 3902	. . . . . . 7 ⊢ (𝑥 ⊆ ∪ ((𝐽 qTop 𝐹) ∩ 𝒫 𝑥) ↔ ∀𝑦 ∈ 𝑥 𝑦 ∈ ∪ ((𝐽 qTop 𝐹) ∩ 𝒫 𝑥))
16		simprl 783	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐽 ∈ TopBases ∧ 𝐹:𝑋⟶1-1onto𝑌) ∧ 𝑥 ⊆ 𝑌) ∧ 𝑦 ∈ 𝑥) ∧ (𝑧 ∈ ((𝐽 qTop 𝐹) ∩ 𝒫 𝑥) ∧ 𝑦 ∈ 𝑧)) → 𝑧 ∈ ((𝐽 qTop 𝐹) ∩ 𝒫 𝑥))
17	16	elin1d 4104	. . . . . . . . . . . . . . 15 ⊢ (((((𝐽 ∈ TopBases ∧ 𝐹:𝑋⟶1-1onto𝑌) ∧ 𝑥 ⊆ 𝑌) ∧ 𝑦 ∈ 𝑥) ∧ (𝑧 ∈ ((𝐽 qTop 𝐹) ∩ 𝒫 𝑥) ∧ 𝑦 ∈ 𝑧)) → 𝑧 ∈ (𝐽 qTop 𝐹))
18		qtopcmp.1	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑋 = ∪ 𝐽
19	18	elqtop2 24050	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐽 ∈ TopBases ∧ 𝐹:𝑋⟶onto𝑌) → (𝑧 ∈ (𝐽 qTop 𝐹) ↔ (𝑧 ⊆ 𝑌 ∧ (◡𝐹 “ 𝑧) ∈ 𝐽)))
20	7, 19	sylan2 605	. . . . . . . . . . . . . . . 16 ⊢ ((𝐽 ∈ TopBases ∧ 𝐹:𝑋⟶1-1onto𝑌) → (𝑧 ∈ (𝐽 qTop 𝐹) ↔ (𝑧 ⊆ 𝑌 ∧ (◡𝐹 “ 𝑧) ∈ 𝐽)))
21	20	ad3antrrr 743	. . . . . . . . . . . . . . 15 ⊢ (((((𝐽 ∈ TopBases ∧ 𝐹:𝑋⟶1-1onto𝑌) ∧ 𝑥 ⊆ 𝑌) ∧ 𝑦 ∈ 𝑥) ∧ (𝑧 ∈ ((𝐽 qTop 𝐹) ∩ 𝒫 𝑥) ∧ 𝑦 ∈ 𝑧)) → (𝑧 ∈ (𝐽 qTop 𝐹) ↔ (𝑧 ⊆ 𝑌 ∧ (◡𝐹 “ 𝑧) ∈ 𝐽)))
22	17, 21	mpbid 235	. . . . . . . . . . . . . 14 ⊢ (((((𝐽 ∈ TopBases ∧ 𝐹:𝑋⟶1-1onto𝑌) ∧ 𝑥 ⊆ 𝑌) ∧ 𝑦 ∈ 𝑥) ∧ (𝑧 ∈ ((𝐽 qTop 𝐹) ∩ 𝒫 𝑥) ∧ 𝑦 ∈ 𝑧)) → (𝑧 ⊆ 𝑌 ∧ (◡𝐹 “ 𝑧) ∈ 𝐽))
23	22	simprd 501	. . . . . . . . . . . . 13 ⊢ (((((𝐽 ∈ TopBases ∧ 𝐹:𝑋⟶1-1onto𝑌) ∧ 𝑥 ⊆ 𝑌) ∧ 𝑦 ∈ 𝑥) ∧ (𝑧 ∈ ((𝐽 qTop 𝐹) ∩ 𝒫 𝑥) ∧ 𝑦 ∈ 𝑧)) → (◡𝐹 “ 𝑧) ∈ 𝐽)
24	16	elin2d 4105	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐽 ∈ TopBases ∧ 𝐹:𝑋⟶1-1onto𝑌) ∧ 𝑥 ⊆ 𝑌) ∧ 𝑦 ∈ 𝑥) ∧ (𝑧 ∈ ((𝐽 qTop 𝐹) ∩ 𝒫 𝑥) ∧ 𝑦 ∈ 𝑧)) → 𝑧 ∈ 𝒫 𝑥)
25	24	elpwid 4569	. . . . . . . . . . . . . . 15 ⊢ (((((𝐽 ∈ TopBases ∧ 𝐹:𝑋⟶1-1onto𝑌) ∧ 𝑥 ⊆ 𝑌) ∧ 𝑦 ∈ 𝑥) ∧ (𝑧 ∈ ((𝐽 qTop 𝐹) ∩ 𝒫 𝑥) ∧ 𝑦 ∈ 𝑧)) → 𝑧 ⊆ 𝑥)
26		imass2 6067	. . . . . . . . . . . . . . 15 ⊢ (𝑧 ⊆ 𝑥 → (◡𝐹 “ 𝑧) ⊆ (◡𝐹 “ 𝑥))
27	25, 26	syl 18	. . . . . . . . . . . . . 14 ⊢ (((((𝐽 ∈ TopBases ∧ 𝐹:𝑋⟶1-1onto𝑌) ∧ 𝑥 ⊆ 𝑌) ∧ 𝑦 ∈ 𝑥) ∧ (𝑧 ∈ ((𝐽 qTop 𝐹) ∩ 𝒫 𝑥) ∧ 𝑦 ∈ 𝑧)) → (◡𝐹 “ 𝑧) ⊆ (◡𝐹 “ 𝑥))
28	23, 27	elpwd 4566	. . . . . . . . . . . . 13 ⊢ (((((𝐽 ∈ TopBases ∧ 𝐹:𝑋⟶1-1onto𝑌) ∧ 𝑥 ⊆ 𝑌) ∧ 𝑦 ∈ 𝑥) ∧ (𝑧 ∈ ((𝐽 qTop 𝐹) ∩ 𝒫 𝑥) ∧ 𝑦 ∈ 𝑧)) → (◡𝐹 “ 𝑧) ∈ 𝒫 (◡𝐹 “ 𝑥))
29	23, 28	elind 4100	. . . . . . . . . . . 12 ⊢ (((((𝐽 ∈ TopBases ∧ 𝐹:𝑋⟶1-1onto𝑌) ∧ 𝑥 ⊆ 𝑌) ∧ 𝑦 ∈ 𝑥) ∧ (𝑧 ∈ ((𝐽 qTop 𝐹) ∩ 𝒫 𝑥) ∧ 𝑦 ∈ 𝑧)) → (◡𝐹 “ 𝑧) ∈ (𝐽 ∩ 𝒫 (◡𝐹 “ 𝑥)))
30		simp-4r 796	. . . . . . . . . . . . . . 15 ⊢ (((((𝐽 ∈ TopBases ∧ 𝐹:𝑋⟶1-1onto𝑌) ∧ 𝑥 ⊆ 𝑌) ∧ 𝑦 ∈ 𝑥) ∧ (𝑧 ∈ ((𝐽 qTop 𝐹) ∩ 𝒫 𝑥) ∧ 𝑦 ∈ 𝑧)) → 𝐹:𝑋⟶1-1onto𝑌)
31	30, 1	syl 18	. . . . . . . . . . . . . 14 ⊢ (((((𝐽 ∈ TopBases ∧ 𝐹:𝑋⟶1-1onto𝑌) ∧ 𝑥 ⊆ 𝑌) ∧ 𝑦 ∈ 𝑥) ∧ (𝑧 ∈ ((𝐽 qTop 𝐹) ∩ 𝒫 𝑥) ∧ 𝑦 ∈ 𝑧)) → ◡𝐹:𝑌⟶1-1onto𝑋)
32		f1ofn 6847	. . . . . . . . . . . . . 14 ⊢ (◡𝐹:𝑌⟶1-1onto𝑋 → ◡𝐹 Fn 𝑌)
33	31, 32	syl 18	. . . . . . . . . . . . 13 ⊢ (((((𝐽 ∈ TopBases ∧ 𝐹:𝑋⟶1-1onto𝑌) ∧ 𝑥 ⊆ 𝑌) ∧ 𝑦 ∈ 𝑥) ∧ (𝑧 ∈ ((𝐽 qTop 𝐹) ∩ 𝒫 𝑥) ∧ 𝑦 ∈ 𝑧)) → ◡𝐹 Fn 𝑌)
34	5	ad2antrr 739	. . . . . . . . . . . . . 14 ⊢ (((((𝐽 ∈ TopBases ∧ 𝐹:𝑋⟶1-1onto𝑌) ∧ 𝑥 ⊆ 𝑌) ∧ 𝑦 ∈ 𝑥) ∧ (𝑧 ∈ ((𝐽 qTop 𝐹) ∩ 𝒫 𝑥) ∧ 𝑦 ∈ 𝑧)) → 𝑥 ⊆ 𝑌)
35	25, 34	sstrd 3923	. . . . . . . . . . . . 13 ⊢ (((((𝐽 ∈ TopBases ∧ 𝐹:𝑋⟶1-1onto𝑌) ∧ 𝑥 ⊆ 𝑌) ∧ 𝑦 ∈ 𝑥) ∧ (𝑧 ∈ ((𝐽 qTop 𝐹) ∩ 𝒫 𝑥) ∧ 𝑦 ∈ 𝑧)) → 𝑧 ⊆ 𝑌)
36		simprr 785	. . . . . . . . . . . . 13 ⊢ (((((𝐽 ∈ TopBases ∧ 𝐹:𝑋⟶1-1onto𝑌) ∧ 𝑥 ⊆ 𝑌) ∧ 𝑦 ∈ 𝑥) ∧ (𝑧 ∈ ((𝐽 qTop 𝐹) ∩ 𝒫 𝑥) ∧ 𝑦 ∈ 𝑧)) → 𝑦 ∈ 𝑧)
37		fnfvima 7262	. . . . . . . . . . . . 13 ⊢ ((◡𝐹 Fn 𝑌 ∧ 𝑧 ⊆ 𝑌 ∧ 𝑦 ∈ 𝑧) → (◡𝐹‘𝑦) ∈ (◡𝐹 “ 𝑧))
38	33, 35, 36, 37	syl3anc 1399	. . . . . . . . . . . 12 ⊢ (((((𝐽 ∈ TopBases ∧ 𝐹:𝑋⟶1-1onto𝑌) ∧ 𝑥 ⊆ 𝑌) ∧ 𝑦 ∈ 𝑥) ∧ (𝑧 ∈ ((𝐽 qTop 𝐹) ∩ 𝒫 𝑥) ∧ 𝑦 ∈ 𝑧)) → (◡𝐹‘𝑦) ∈ (◡𝐹 “ 𝑧))
39		eleq2 2853	. . . . . . . . . . . . 13 ⊢ (𝑤 = (◡𝐹 “ 𝑧) → ((◡𝐹‘𝑦) ∈ 𝑤 ↔ (◡𝐹‘𝑦) ∈ (◡𝐹 “ 𝑧)))
40	39	rspcev 3580	. . . . . . . . . . . 12 ⊢ (((◡𝐹 “ 𝑧) ∈ (𝐽 ∩ 𝒫 (◡𝐹 “ 𝑥)) ∧ (◡𝐹‘𝑦) ∈ (◡𝐹 “ 𝑧)) → ∃𝑤 ∈ (𝐽 ∩ 𝒫 (◡𝐹 “ 𝑥))(◡𝐹‘𝑦) ∈ 𝑤)
41	29, 38, 40	syl2anc 596	. . . . . . . . . . 11 ⊢ (((((𝐽 ∈ TopBases ∧ 𝐹:𝑋⟶1-1onto𝑌) ∧ 𝑥 ⊆ 𝑌) ∧ 𝑦 ∈ 𝑥) ∧ (𝑧 ∈ ((𝐽 qTop 𝐹) ∩ 𝒫 𝑥) ∧ 𝑦 ∈ 𝑧)) → ∃𝑤 ∈ (𝐽 ∩ 𝒫 (◡𝐹 “ 𝑥))(◡𝐹‘𝑦) ∈ 𝑤)
42	41	rexlimdvaa 3168	. . . . . . . . . 10 ⊢ ((((𝐽 ∈ TopBases ∧ 𝐹:𝑋⟶1-1onto𝑌) ∧ 𝑥 ⊆ 𝑌) ∧ 𝑦 ∈ 𝑥) → (∃𝑧 ∈ ((𝐽 qTop 𝐹) ∩ 𝒫 𝑥)𝑦 ∈ 𝑧 → ∃𝑤 ∈ (𝐽 ∩ 𝒫 (◡𝐹 “ 𝑥))(◡𝐹‘𝑦) ∈ 𝑤))
43		simp-4r 796	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐽 ∈ TopBases ∧ 𝐹:𝑋⟶1-1onto𝑌) ∧ 𝑥 ⊆ 𝑌) ∧ 𝑦 ∈ 𝑥) ∧ (𝑤 ∈ (𝐽 ∩ 𝒫 (◡𝐹 “ 𝑥)) ∧ (◡𝐹‘𝑦) ∈ 𝑤)) → 𝐹:𝑋⟶1-1onto𝑌)
44		f1ofun 6848	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹:𝑋⟶1-1onto𝑌 → Fun 𝐹)
45	43, 44	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐽 ∈ TopBases ∧ 𝐹:𝑋⟶1-1onto𝑌) ∧ 𝑥 ⊆ 𝑌) ∧ 𝑦 ∈ 𝑥) ∧ (𝑤 ∈ (𝐽 ∩ 𝒫 (◡𝐹 “ 𝑥)) ∧ (◡𝐹‘𝑦) ∈ 𝑤)) → Fun 𝐹)
46		simprl 783	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐽 ∈ TopBases ∧ 𝐹:𝑋⟶1-1onto𝑌) ∧ 𝑥 ⊆ 𝑌) ∧ 𝑦 ∈ 𝑥) ∧ (𝑤 ∈ (𝐽 ∩ 𝒫 (◡𝐹 “ 𝑥)) ∧ (◡𝐹‘𝑦) ∈ 𝑤)) → 𝑤 ∈ (𝐽 ∩ 𝒫 (◡𝐹 “ 𝑥)))
47	46	elin2d 4105	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐽 ∈ TopBases ∧ 𝐹:𝑋⟶1-1onto𝑌) ∧ 𝑥 ⊆ 𝑌) ∧ 𝑦 ∈ 𝑥) ∧ (𝑤 ∈ (𝐽 ∩ 𝒫 (◡𝐹 “ 𝑥)) ∧ (◡𝐹‘𝑦) ∈ 𝑤)) → 𝑤 ∈ 𝒫 (◡𝐹 “ 𝑥))
48	47	elpwid 4569	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐽 ∈ TopBases ∧ 𝐹:𝑋⟶1-1onto𝑌) ∧ 𝑥 ⊆ 𝑌) ∧ 𝑦 ∈ 𝑥) ∧ (𝑤 ∈ (𝐽 ∩ 𝒫 (◡𝐹 “ 𝑥)) ∧ (◡𝐹‘𝑦) ∈ 𝑤)) → 𝑤 ⊆ (◡𝐹 “ 𝑥))
49		funimass2 6645	. . . . . . . . . . . . . . . 16 ⊢ ((Fun 𝐹 ∧ 𝑤 ⊆ (◡𝐹 “ 𝑥)) → (𝐹 “ 𝑤) ⊆ 𝑥)
50	45, 48, 49	syl2anc 596	. . . . . . . . . . . . . . 15 ⊢ (((((𝐽 ∈ TopBases ∧ 𝐹:𝑋⟶1-1onto𝑌) ∧ 𝑥 ⊆ 𝑌) ∧ 𝑦 ∈ 𝑥) ∧ (𝑤 ∈ (𝐽 ∩ 𝒫 (◡𝐹 “ 𝑥)) ∧ (◡𝐹‘𝑦) ∈ 𝑤)) → (𝐹 “ 𝑤) ⊆ 𝑥)
51	5	ad2antrr 739	. . . . . . . . . . . . . . 15 ⊢ (((((𝐽 ∈ TopBases ∧ 𝐹:𝑋⟶1-1onto𝑌) ∧ 𝑥 ⊆ 𝑌) ∧ 𝑦 ∈ 𝑥) ∧ (𝑤 ∈ (𝐽 ∩ 𝒫 (◡𝐹 “ 𝑥)) ∧ (◡𝐹‘𝑦) ∈ 𝑤)) → 𝑥 ⊆ 𝑌)
52	50, 51	sstrd 3923	. . . . . . . . . . . . . 14 ⊢ (((((𝐽 ∈ TopBases ∧ 𝐹:𝑋⟶1-1onto𝑌) ∧ 𝑥 ⊆ 𝑌) ∧ 𝑦 ∈ 𝑥) ∧ (𝑤 ∈ (𝐽 ∩ 𝒫 (◡𝐹 “ 𝑥)) ∧ (◡𝐹‘𝑦) ∈ 𝑤)) → (𝐹 “ 𝑤) ⊆ 𝑌)
53		f1of1 6845	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹:𝑋⟶1-1onto𝑌 → 𝐹:𝑋⟶1-1𝑌)
54	43, 53	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐽 ∈ TopBases ∧ 𝐹:𝑋⟶1-1onto𝑌) ∧ 𝑥 ⊆ 𝑌) ∧ 𝑦 ∈ 𝑥) ∧ (𝑤 ∈ (𝐽 ∩ 𝒫 (◡𝐹 “ 𝑥)) ∧ (◡𝐹‘𝑦) ∈ 𝑤)) → 𝐹:𝑋⟶1-1𝑌)
55	46	elin1d 4104	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐽 ∈ TopBases ∧ 𝐹:𝑋⟶1-1onto𝑌) ∧ 𝑥 ⊆ 𝑌) ∧ 𝑦 ∈ 𝑥) ∧ (𝑤 ∈ (𝐽 ∩ 𝒫 (◡𝐹 “ 𝑥)) ∧ (◡𝐹‘𝑦) ∈ 𝑤)) → 𝑤 ∈ 𝐽)
56		elssuni 4902	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 ∈ 𝐽 → 𝑤 ⊆ ∪ 𝐽)
57	56, 18	sseqtrrdi 3954	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 ∈ 𝐽 → 𝑤 ⊆ 𝑋)
58	55, 57	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐽 ∈ TopBases ∧ 𝐹:𝑋⟶1-1onto𝑌) ∧ 𝑥 ⊆ 𝑌) ∧ 𝑦 ∈ 𝑥) ∧ (𝑤 ∈ (𝐽 ∩ 𝒫 (◡𝐹 “ 𝑥)) ∧ (◡𝐹‘𝑦) ∈ 𝑤)) → 𝑤 ⊆ 𝑋)
59		f1imacnv 6863	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹:𝑋⟶1-1𝑌 ∧ 𝑤 ⊆ 𝑋) → (◡𝐹 “ (𝐹 “ 𝑤)) = 𝑤)
60	54, 58, 59	syl2anc 596	. . . . . . . . . . . . . . 15 ⊢ (((((𝐽 ∈ TopBases ∧ 𝐹:𝑋⟶1-1onto𝑌) ∧ 𝑥 ⊆ 𝑌) ∧ 𝑦 ∈ 𝑥) ∧ (𝑤 ∈ (𝐽 ∩ 𝒫 (◡𝐹 “ 𝑥)) ∧ (◡𝐹‘𝑦) ∈ 𝑤)) → (◡𝐹 “ (𝐹 “ 𝑤)) = 𝑤)
61	60, 55	eqeltrd 2864	. . . . . . . . . . . . . 14 ⊢ (((((𝐽 ∈ TopBases ∧ 𝐹:𝑋⟶1-1onto𝑌) ∧ 𝑥 ⊆ 𝑌) ∧ 𝑦 ∈ 𝑥) ∧ (𝑤 ∈ (𝐽 ∩ 𝒫 (◡𝐹 “ 𝑥)) ∧ (◡𝐹‘𝑦) ∈ 𝑤)) → (◡𝐹 “ (𝐹 “ 𝑤)) ∈ 𝐽)
62	18	elqtop2 24050	. . . . . . . . . . . . . . . 16 ⊢ ((𝐽 ∈ TopBases ∧ 𝐹:𝑋⟶onto𝑌) → ((𝐹 “ 𝑤) ∈ (𝐽 qTop 𝐹) ↔ ((𝐹 “ 𝑤) ⊆ 𝑌 ∧ (◡𝐹 “ (𝐹 “ 𝑤)) ∈ 𝐽)))
63	7, 62	sylan2 605	. . . . . . . . . . . . . . 15 ⊢ ((𝐽 ∈ TopBases ∧ 𝐹:𝑋⟶1-1onto𝑌) → ((𝐹 “ 𝑤) ∈ (𝐽 qTop 𝐹) ↔ ((𝐹 “ 𝑤) ⊆ 𝑌 ∧ (◡𝐹 “ (𝐹 “ 𝑤)) ∈ 𝐽)))
64	63	ad3antrrr 743	. . . . . . . . . . . . . 14 ⊢ (((((𝐽 ∈ TopBases ∧ 𝐹:𝑋⟶1-1onto𝑌) ∧ 𝑥 ⊆ 𝑌) ∧ 𝑦 ∈ 𝑥) ∧ (𝑤 ∈ (𝐽 ∩ 𝒫 (◡𝐹 “ 𝑥)) ∧ (◡𝐹‘𝑦) ∈ 𝑤)) → ((𝐹 “ 𝑤) ∈ (𝐽 qTop 𝐹) ↔ ((𝐹 “ 𝑤) ⊆ 𝑌 ∧ (◡𝐹 “ (𝐹 “ 𝑤)) ∈ 𝐽)))
65	52, 61, 64	mpbir2and 726	. . . . . . . . . . . . 13 ⊢ (((((𝐽 ∈ TopBases ∧ 𝐹:𝑋⟶1-1onto𝑌) ∧ 𝑥 ⊆ 𝑌) ∧ 𝑦 ∈ 𝑥) ∧ (𝑤 ∈ (𝐽 ∩ 𝒫 (◡𝐹 “ 𝑥)) ∧ (◡𝐹‘𝑦) ∈ 𝑤)) → (𝐹 “ 𝑤) ∈ (𝐽 qTop 𝐹))
66		vex 3458	. . . . . . . . . . . . . . 15 ⊢ 𝑥 ∈ V
67	66	elpw2 5300	. . . . . . . . . . . . . 14 ⊢ ((𝐹 “ 𝑤) ∈ 𝒫 𝑥 ↔ (𝐹 “ 𝑤) ⊆ 𝑥)
68	50, 67	sylibr 237	. . . . . . . . . . . . 13 ⊢ (((((𝐽 ∈ TopBases ∧ 𝐹:𝑋⟶1-1onto𝑌) ∧ 𝑥 ⊆ 𝑌) ∧ 𝑦 ∈ 𝑥) ∧ (𝑤 ∈ (𝐽 ∩ 𝒫 (◡𝐹 “ 𝑥)) ∧ (◡𝐹‘𝑦) ∈ 𝑤)) → (𝐹 “ 𝑤) ∈ 𝒫 𝑥)
69	65, 68	elind 4100	. . . . . . . . . . . 12 ⊢ (((((𝐽 ∈ TopBases ∧ 𝐹:𝑋⟶1-1onto𝑌) ∧ 𝑥 ⊆ 𝑌) ∧ 𝑦 ∈ 𝑥) ∧ (𝑤 ∈ (𝐽 ∩ 𝒫 (◡𝐹 “ 𝑥)) ∧ (◡𝐹‘𝑦) ∈ 𝑤)) → (𝐹 “ 𝑤) ∈ ((𝐽 qTop 𝐹) ∩ 𝒫 𝑥))
70	5	sselda 3913	. . . . . . . . . . . . . . 15 ⊢ ((((𝐽 ∈ TopBases ∧ 𝐹:𝑋⟶1-1onto𝑌) ∧ 𝑥 ⊆ 𝑌) ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ 𝑌)
71	70	adantr 486	. . . . . . . . . . . . . 14 ⊢ (((((𝐽 ∈ TopBases ∧ 𝐹:𝑋⟶1-1onto𝑌) ∧ 𝑥 ⊆ 𝑌) ∧ 𝑦 ∈ 𝑥) ∧ (𝑤 ∈ (𝐽 ∩ 𝒫 (◡𝐹 “ 𝑥)) ∧ (◡𝐹‘𝑦) ∈ 𝑤)) → 𝑦 ∈ 𝑌)
72		f1ocnvfv2 7308	. . . . . . . . . . . . . 14 ⊢ ((𝐹:𝑋⟶1-1onto𝑌 ∧ 𝑦 ∈ 𝑌) → (𝐹‘(◡𝐹‘𝑦)) = 𝑦)
73	43, 71, 72	syl2anc 596	. . . . . . . . . . . . 13 ⊢ (((((𝐽 ∈ TopBases ∧ 𝐹:𝑋⟶1-1onto𝑌) ∧ 𝑥 ⊆ 𝑌) ∧ 𝑦 ∈ 𝑥) ∧ (𝑤 ∈ (𝐽 ∩ 𝒫 (◡𝐹 “ 𝑥)) ∧ (◡𝐹‘𝑦) ∈ 𝑤)) → (𝐹‘(◡𝐹‘𝑦)) = 𝑦)
74		f1ofn 6847	. . . . . . . . . . . . . . . 16 ⊢ (𝐹:𝑋⟶1-1onto𝑌 → 𝐹 Fn 𝑋)
75	74	adantl 487	. . . . . . . . . . . . . . 15 ⊢ ((𝐽 ∈ TopBases ∧ 𝐹:𝑋⟶1-1onto𝑌) → 𝐹 Fn 𝑋)
76	75	ad3antrrr 743	. . . . . . . . . . . . . 14 ⊢ (((((𝐽 ∈ TopBases ∧ 𝐹:𝑋⟶1-1onto𝑌) ∧ 𝑥 ⊆ 𝑌) ∧ 𝑦 ∈ 𝑥) ∧ (𝑤 ∈ (𝐽 ∩ 𝒫 (◡𝐹 “ 𝑥)) ∧ (◡𝐹‘𝑦) ∈ 𝑤)) → 𝐹 Fn 𝑋)
77		simprr 785	. . . . . . . . . . . . . 14 ⊢ (((((𝐽 ∈ TopBases ∧ 𝐹:𝑋⟶1-1onto𝑌) ∧ 𝑥 ⊆ 𝑌) ∧ 𝑦 ∈ 𝑥) ∧ (𝑤 ∈ (𝐽 ∩ 𝒫 (◡𝐹 “ 𝑥)) ∧ (◡𝐹‘𝑦) ∈ 𝑤)) → (◡𝐹‘𝑦) ∈ 𝑤)
78		fnfvima 7262	. . . . . . . . . . . . . 14 ⊢ ((𝐹 Fn 𝑋 ∧ 𝑤 ⊆ 𝑋 ∧ (◡𝐹‘𝑦) ∈ 𝑤) → (𝐹‘(◡𝐹‘𝑦)) ∈ (𝐹 “ 𝑤))
79	76, 58, 77, 78	syl3anc 1399	. . . . . . . . . . . . 13 ⊢ (((((𝐽 ∈ TopBases ∧ 𝐹:𝑋⟶1-1onto𝑌) ∧ 𝑥 ⊆ 𝑌) ∧ 𝑦 ∈ 𝑥) ∧ (𝑤 ∈ (𝐽 ∩ 𝒫 (◡𝐹 “ 𝑥)) ∧ (◡𝐹‘𝑦) ∈ 𝑤)) → (𝐹‘(◡𝐹‘𝑦)) ∈ (𝐹 “ 𝑤))
80	73, 79	eqeltrrd 2865	. . . . . . . . . . . 12 ⊢ (((((𝐽 ∈ TopBases ∧ 𝐹:𝑋⟶1-1onto𝑌) ∧ 𝑥 ⊆ 𝑌) ∧ 𝑦 ∈ 𝑥) ∧ (𝑤 ∈ (𝐽 ∩ 𝒫 (◡𝐹 “ 𝑥)) ∧ (◡𝐹‘𝑦) ∈ 𝑤)) → 𝑦 ∈ (𝐹 “ 𝑤))
81		eleq2 2853	. . . . . . . . . . . . 13 ⊢ (𝑧 = (𝐹 “ 𝑤) → (𝑦 ∈ 𝑧 ↔ 𝑦 ∈ (𝐹 “ 𝑤)))
82	81	rspcev 3580	. . . . . . . . . . . 12 ⊢ (((𝐹 “ 𝑤) ∈ ((𝐽 qTop 𝐹) ∩ 𝒫 𝑥) ∧ 𝑦 ∈ (𝐹 “ 𝑤)) → ∃𝑧 ∈ ((𝐽 qTop 𝐹) ∩ 𝒫 𝑥)𝑦 ∈ 𝑧)
83	69, 80, 82	syl2anc 596	. . . . . . . . . . 11 ⊢ (((((𝐽 ∈ TopBases ∧ 𝐹:𝑋⟶1-1onto𝑌) ∧ 𝑥 ⊆ 𝑌) ∧ 𝑦 ∈ 𝑥) ∧ (𝑤 ∈ (𝐽 ∩ 𝒫 (◡𝐹 “ 𝑥)) ∧ (◡𝐹‘𝑦) ∈ 𝑤)) → ∃𝑧 ∈ ((𝐽 qTop 𝐹) ∩ 𝒫 𝑥)𝑦 ∈ 𝑧)
84	83	rexlimdvaa 3168	. . . . . . . . . 10 ⊢ ((((𝐽 ∈ TopBases ∧ 𝐹:𝑋⟶1-1onto𝑌) ∧ 𝑥 ⊆ 𝑌) ∧ 𝑦 ∈ 𝑥) → (∃𝑤 ∈ (𝐽 ∩ 𝒫 (◡𝐹 “ 𝑥))(◡𝐹‘𝑦) ∈ 𝑤 → ∃𝑧 ∈ ((𝐽 qTop 𝐹) ∩ 𝒫 𝑥)𝑦 ∈ 𝑧))
85	42, 84	impbid 215	. . . . . . . . 9 ⊢ ((((𝐽 ∈ TopBases ∧ 𝐹:𝑋⟶1-1onto𝑌) ∧ 𝑥 ⊆ 𝑌) ∧ 𝑦 ∈ 𝑥) → (∃𝑧 ∈ ((𝐽 qTop 𝐹) ∩ 𝒫 𝑥)𝑦 ∈ 𝑧 ↔ ∃𝑤 ∈ (𝐽 ∩ 𝒫 (◡𝐹 “ 𝑥))(◡𝐹‘𝑦) ∈ 𝑤))
86		eluni2 4874	. . . . . . . . 9 ⊢ (𝑦 ∈ ∪ ((𝐽 qTop 𝐹) ∩ 𝒫 𝑥) ↔ ∃𝑧 ∈ ((𝐽 qTop 𝐹) ∩ 𝒫 𝑥)𝑦 ∈ 𝑧)
87		eluni2 4874	. . . . . . . . 9 ⊢ ((◡𝐹‘𝑦) ∈ ∪ (𝐽 ∩ 𝒫 (◡𝐹 “ 𝑥)) ↔ ∃𝑤 ∈ (𝐽 ∩ 𝒫 (◡𝐹 “ 𝑥))(◡𝐹‘𝑦) ∈ 𝑤)
88	85, 86, 87	3bitr4g 317	. . . . . . . 8 ⊢ ((((𝐽 ∈ TopBases ∧ 𝐹:𝑋⟶1-1onto𝑌) ∧ 𝑥 ⊆ 𝑌) ∧ 𝑦 ∈ 𝑥) → (𝑦 ∈ ∪ ((𝐽 qTop 𝐹) ∩ 𝒫 𝑥) ↔ (◡𝐹‘𝑦) ∈ ∪ (𝐽 ∩ 𝒫 (◡𝐹 “ 𝑥))))
89	88	ralbidva 3187	. . . . . . 7 ⊢ (((𝐽 ∈ TopBases ∧ 𝐹:𝑋⟶1-1onto𝑌) ∧ 𝑥 ⊆ 𝑌) → (∀𝑦 ∈ 𝑥 𝑦 ∈ ∪ ((𝐽 qTop 𝐹) ∩ 𝒫 𝑥) ↔ ∀𝑦 ∈ 𝑥 (◡𝐹‘𝑦) ∈ ∪ (𝐽 ∩ 𝒫 (◡𝐹 “ 𝑥))))
90	15, 89	bitrid 286	. . . . . 6 ⊢ (((𝐽 ∈ TopBases ∧ 𝐹:𝑋⟶1-1onto𝑌) ∧ 𝑥 ⊆ 𝑌) → (𝑥 ⊆ ∪ ((𝐽 qTop 𝐹) ∩ 𝒫 𝑥) ↔ ∀𝑦 ∈ 𝑥 (◡𝐹‘𝑦) ∈ ∪ (𝐽 ∩ 𝒫 (◡𝐹 “ 𝑥))))
91	14, 90	bitr4d 285	. . . . 5 ⊢ (((𝐽 ∈ TopBases ∧ 𝐹:𝑋⟶1-1onto𝑌) ∧ 𝑥 ⊆ 𝑌) → ((◡𝐹 “ 𝑥) ⊆ ∪ (𝐽 ∩ 𝒫 (◡𝐹 “ 𝑥)) ↔ 𝑥 ⊆ ∪ ((𝐽 qTop 𝐹) ∩ 𝒫 𝑥)))
92		eltg 23305	. . . . . 6 ⊢ (𝐽 ∈ TopBases → ((◡𝐹 “ 𝑥) ∈ (topGen‘𝐽) ↔ (◡𝐹 “ 𝑥) ⊆ ∪ (𝐽 ∩ 𝒫 (◡𝐹 “ 𝑥))))
93	92	ad2antrr 739	. . . . 5 ⊢ (((𝐽 ∈ TopBases ∧ 𝐹:𝑋⟶1-1onto𝑌) ∧ 𝑥 ⊆ 𝑌) → ((◡𝐹 “ 𝑥) ∈ (topGen‘𝐽) ↔ (◡𝐹 “ 𝑥) ⊆ ∪ (𝐽 ∩ 𝒫 (◡𝐹 “ 𝑥))))
94		ovex 7476	. . . . . 6 ⊢ (𝐽 qTop 𝐹) ∈ V
95		eltg 23305	. . . . . 6 ⊢ ((𝐽 qTop 𝐹) ∈ V → (𝑥 ∈ (topGen‘(𝐽 qTop 𝐹)) ↔ 𝑥 ⊆ ∪ ((𝐽 qTop 𝐹) ∩ 𝒫 𝑥)))
96	94, 95	mp1i 14	. . . . 5 ⊢ (((𝐽 ∈ TopBases ∧ 𝐹:𝑋⟶1-1onto𝑌) ∧ 𝑥 ⊆ 𝑌) → (𝑥 ∈ (topGen‘(𝐽 qTop 𝐹)) ↔ 𝑥 ⊆ ∪ ((𝐽 qTop 𝐹) ∩ 𝒫 𝑥)))
97	91, 93, 96	3bitr4d 314	. . . 4 ⊢ (((𝐽 ∈ TopBases ∧ 𝐹:𝑋⟶1-1onto𝑌) ∧ 𝑥 ⊆ 𝑌) → ((◡𝐹 “ 𝑥) ∈ (topGen‘𝐽) ↔ 𝑥 ∈ (topGen‘(𝐽 qTop 𝐹))))
98	97	pm5.32da 590	. . 3 ⊢ ((𝐽 ∈ TopBases ∧ 𝐹:𝑋⟶1-1onto𝑌) → ((𝑥 ⊆ 𝑌 ∧ (◡𝐹 “ 𝑥) ∈ (topGen‘𝐽)) ↔ (𝑥 ⊆ 𝑌 ∧ 𝑥 ∈ (topGen‘(𝐽 qTop 𝐹)))))
99		tgtopon 23319	. . . . . 6 ⊢ (𝐽 ∈ TopBases → (topGen‘𝐽) ∈ (TopOn‘∪ 𝐽))
100	99	adantr 486	. . . . 5 ⊢ ((𝐽 ∈ TopBases ∧ 𝐹:𝑋⟶1-1onto𝑌) → (topGen‘𝐽) ∈ (TopOn‘∪ 𝐽))
101	18	fveq2i 6911	. . . . 5 ⊢ (TopOn‘𝑋) = (TopOn‘∪ 𝐽)
102	100, 101	eleqtrrdi 2875	. . . 4 ⊢ ((𝐽 ∈ TopBases ∧ 𝐹:𝑋⟶1-1onto𝑌) → (topGen‘𝐽) ∈ (TopOn‘𝑋))
103	7	adantl 487	. . . 4 ⊢ ((𝐽 ∈ TopBases ∧ 𝐹:𝑋⟶1-1onto𝑌) → 𝐹:𝑋⟶onto𝑌)
104		elqtop3 24052	. . . 4 ⊢ (((topGen‘𝐽) ∈ (TopOn‘𝑋) ∧ 𝐹:𝑋⟶onto𝑌) → (𝑥 ∈ ((topGen‘𝐽) qTop 𝐹) ↔ (𝑥 ⊆ 𝑌 ∧ (◡𝐹 “ 𝑥) ∈ (topGen‘𝐽))))
105	102, 103, 104	syl2anc 596	. . 3 ⊢ ((𝐽 ∈ TopBases ∧ 𝐹:𝑋⟶1-1onto𝑌) → (𝑥 ∈ ((topGen‘𝐽) qTop 𝐹) ↔ (𝑥 ⊆ 𝑌 ∧ (◡𝐹 “ 𝑥) ∈ (topGen‘𝐽))))
106		unitg 23315	. . . . . . . . 9 ⊢ ((𝐽 qTop 𝐹) ∈ V → ∪ (topGen‘(𝐽 qTop 𝐹)) = ∪ (𝐽 qTop 𝐹))
107	94, 106	ax-mp 5	. . . . . . . 8 ⊢ ∪ (topGen‘(𝐽 qTop 𝐹)) = ∪ (𝐽 qTop 𝐹)
108	18	elqtop2 24050	. . . . . . . . . . . 12 ⊢ ((𝐽 ∈ TopBases ∧ 𝐹:𝑋⟶onto𝑌) → (𝑥 ∈ (𝐽 qTop 𝐹) ↔ (𝑥 ⊆ 𝑌 ∧ (◡𝐹 “ 𝑥) ∈ 𝐽)))
109	7, 108	sylan2 605	. . . . . . . . . . 11 ⊢ ((𝐽 ∈ TopBases ∧ 𝐹:𝑋⟶1-1onto𝑌) → (𝑥 ∈ (𝐽 qTop 𝐹) ↔ (𝑥 ⊆ 𝑌 ∧ (◡𝐹 “ 𝑥) ∈ 𝐽)))
110		velpw 4565	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ 𝒫 𝑌 ↔ 𝑥 ⊆ 𝑌)
111	110	biranri 511	. . . . . . . . . . 11 ⊢ ((𝑥 ⊆ 𝑌 ∧ (◡𝐹 “ 𝑥) ∈ 𝐽) → 𝑥 ∈ 𝒫 𝑌)
112	109, 111	biimtrdi 256	. . . . . . . . . 10 ⊢ ((𝐽 ∈ TopBases ∧ 𝐹:𝑋⟶1-1onto𝑌) → (𝑥 ∈ (𝐽 qTop 𝐹) → 𝑥 ∈ 𝒫 𝑌))
113	112	ssrdv 3919	. . . . . . . . 9 ⊢ ((𝐽 ∈ TopBases ∧ 𝐹:𝑋⟶1-1onto𝑌) → (𝐽 qTop 𝐹) ⊆ 𝒫 𝑌)
114		sspwuni 5063	. . . . . . . . 9 ⊢ ((𝐽 qTop 𝐹) ⊆ 𝒫 𝑌 ↔ ∪ (𝐽 qTop 𝐹) ⊆ 𝑌)
115	113, 114	sylib 221	. . . . . . . 8 ⊢ ((𝐽 ∈ TopBases ∧ 𝐹:𝑋⟶1-1onto𝑌) → ∪ (𝐽 qTop 𝐹) ⊆ 𝑌)
116	107, 115	eqsstrid 3951	. . . . . . 7 ⊢ ((𝐽 ∈ TopBases ∧ 𝐹:𝑋⟶1-1onto𝑌) → ∪ (topGen‘(𝐽 qTop 𝐹)) ⊆ 𝑌)
117		sspwuni 5063	. . . . . . 7 ⊢ ((topGen‘(𝐽 qTop 𝐹)) ⊆ 𝒫 𝑌 ↔ ∪ (topGen‘(𝐽 qTop 𝐹)) ⊆ 𝑌)
118	116, 117	sylibr 237	. . . . . 6 ⊢ ((𝐽 ∈ TopBases ∧ 𝐹:𝑋⟶1-1onto𝑌) → (topGen‘(𝐽 qTop 𝐹)) ⊆ 𝒫 𝑌)
119	118	sseld 3912	. . . . 5 ⊢ ((𝐽 ∈ TopBases ∧ 𝐹:𝑋⟶1-1onto𝑌) → (𝑥 ∈ (topGen‘(𝐽 qTop 𝐹)) → 𝑥 ∈ 𝒫 𝑌))
120	119, 110	imbitrdi 254	. . . 4 ⊢ ((𝐽 ∈ TopBases ∧ 𝐹:𝑋⟶1-1onto𝑌) → (𝑥 ∈ (topGen‘(𝐽 qTop 𝐹)) → 𝑥 ⊆ 𝑌))
121	120	pm4.71rd 572	. . 3 ⊢ ((𝐽 ∈ TopBases ∧ 𝐹:𝑋⟶1-1onto𝑌) → (𝑥 ∈ (topGen‘(𝐽 qTop 𝐹)) ↔ (𝑥 ⊆ 𝑌 ∧ 𝑥 ∈ (topGen‘(𝐽 qTop 𝐹)))))
122	98, 105, 121	3bitr4d 314	. 2 ⊢ ((𝐽 ∈ TopBases ∧ 𝐹:𝑋⟶1-1onto𝑌) → (𝑥 ∈ ((topGen‘𝐽) qTop 𝐹) ↔ 𝑥 ∈ (topGen‘(𝐽 qTop 𝐹))))
123	122	eqrdv 2761	1 ⊢ ((𝐽 ∈ TopBases ∧ 𝐹:𝑋⟶1-1onto𝑌) → ((topGen‘𝐽) qTop 𝐹) = (topGen‘(𝐽 qTop 𝐹)))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570   ∈ wcel 2147  ∀wral 3080  ∃wrex 3090  Vcvv 3454   ⊆ wss 3900   ∩ cin 4092  𝒫 cpw 4560  ∪ cuni 4870  ^◡ccnv 5654  dom cdm 5655  ran crn 5656   “ cima 5658  Fun wfun 6552   Fn wfn 6553  ⟶1-1wf1 6555  ⟶ontowfo 6556  ⟶1-1ontowf1o 6557  ‘cfv 6558  (class class class)co 7443  topGenctg 17637   qTop cqtop 17704  TopOnctopon 23258  TopBasesctb 23293

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-rep 5235  ax-sep 5252  ax-nul 5263  ax-pow 5331  ax-pr 5395  ax-un 7775

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3081  df-rex 3091  df-reu 3370  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-iun 4956  df-br 5107  df-opab 5171  df-mpt 5190  df-id 5550  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-iota 6512  df-fun 6560  df-fn 6561  df-f 6562  df-f1 6563  df-fo 6564  df-f1o 6565  df-fv 6566  df-ov 7446  df-oprab 7447  df-mpo 7448  df-topgen 17643  df-qtop 17708  df-top 23242  df-topon 23259  df-bases 23294

This theorem is used by:  imasf1oxms  24838