fcluscnplem - Mathbox for Jeff Hankins

Mathbox for Jeff Hankins

< Previous Next >
Related theorems
GIF version

Theorem fcluscnplem 11729

Description: Lemma for fcluscnp 11730. If a function is continuous at a point, it respects clustering there.

**Hypotheses**
Ref	Expression
fcluscnp.1	⊢ X = ∪J
fcluscnp.2	⊢ Y = ∪K

**Assertion**
Ref	Expression
fcluscnplem	⊢ (((J ∈ Top ⋀ K ∈ Top ⋀ F:X–→Y) ⋀ A ∈ X) → (∀g ∈ Fil ((X = ∪g ⋀ A ∈ ((fLim1 ‘J) ‘g)) → (F ‘A) ∈ ((fLim1 ‘K) ‘((Y FilMap g) ‘F))) → ∀f ∈ Fil ((X = ∪f ⋀ A ∈ ((fClus ‘J) ‘f)) → (F ‘A) ∈ ((fClus ‘K) ‘((Y FilMap f) ‘F)))))

Distinct variable groups: f,g,A f,F,g f,J,g f,K,g f,X,g f,Y,g

**Proof of Theorem fcluscnplem**
Step	Hyp	Ref	Expression
1		unieq 2576	. . . . . . . . . . . . . . . . 17 ⊢ (g = h → ∪g = ∪h)
2	1	eqeq2d 1529	. . . . . . . . . . . . . . . 16 ⊢ (g = h → (X = ∪g ↔ X = ∪h))
3		fveq2 3835	. . . . . . . . . . . . . . . . 17 ⊢ (g = h → ((fLim1 ‘J) ‘g) = ((fLim1 ‘J) ‘h))
4	3	eleq2d 1584	. . . . . . . . . . . . . . . 16 ⊢ (g = h → (A ∈ ((fLim1 ‘J) ‘g) ↔ A ∈ ((fLim1 ‘J) ‘h)))
5	2, 4	anbi12d 631	. . . . . . . . . . . . . . 15 ⊢ (g = h → ((X = ∪g ⋀ A ∈ ((fLim1 ‘J) ‘g)) ↔ (X = ∪h ⋀ A ∈ ((fLim1 ‘J) ‘h))))
6		opreq2 4027	. . . . . . . . . . . . . . . . . 18 ⊢ (g = h → (Y FilMap g) = (Y FilMap h))
7	6	fveq1d 3837	. . . . . . . . . . . . . . . . 17 ⊢ (g = h → ((Y FilMap g) ‘F) = ((Y FilMap h) ‘F))
8	7	fveq2d 3839	. . . . . . . . . . . . . . . 16 ⊢ (g = h → ((fLim1 ‘K) ‘((Y FilMap g) ‘F)) = ((fLim1 ‘K) ‘((Y FilMap h) ‘F)))
9	8	eleq2d 1584	. . . . . . . . . . . . . . 15 ⊢ (g = h → ((F ‘A) ∈ ((fLim1 ‘K) ‘((Y FilMap g) ‘F)) ↔ (F ‘A) ∈ ((fLim1 ‘K) ‘((Y FilMap h) ‘F))))
10	5, 9	imbi12d 629	. . . . . . . . . . . . . 14 ⊢ (g = h → (((X = ∪g ⋀ A ∈ ((fLim1 ‘J) ‘g)) → (F ‘A) ∈ ((fLim1 ‘K) ‘((Y FilMap g) ‘F))) ↔ ((X = ∪h ⋀ A ∈ ((fLim1 ‘J) ‘h)) → (F ‘A) ∈ ((fLim1 ‘K) ‘((Y FilMap h) ‘F)))))
11	10	rcla4v 1919	. . . . . . . . . . . . 13 ⊢ (h ∈ Fil → (∀g ∈ Fil ((X = ∪g ⋀ A ∈ ((fLim1 ‘J) ‘g)) → (F ‘A) ∈ ((fLim1 ‘K) ‘((Y FilMap g) ‘F))) → ((X = ∪h ⋀ A ∈ ((fLim1 ‘J) ‘h)) → (F ‘A) ∈ ((fLim1 ‘K) ‘((Y FilMap h) ‘F)))))
12	11	ad2antlr 405	. . . . . . . . . . . 12 ⊢ (((((J ∈ Top ⋀ K ∈ Top ⋀ F:X–→Y) ⋀ A ∈ X) ⋀ h ∈ Fil) ⋀ ((X = ∪h ⋀ f ⊆ h ⋀ A ∈ ((fLim1 ‘J) ‘h)) ⋀ (f ∈ Fil ⋀ X = ∪f))) → (∀g ∈ Fil ((X = ∪g ⋀ A ∈ ((fLim1 ‘J) ‘g)) → (F ‘A) ∈ ((fLim1 ‘K) ‘((Y FilMap g) ‘F))) → ((X = ∪h ⋀ A ∈ ((fLim1 ‘J) ‘h)) → (F ‘A) ∈ ((fLim1 ‘K) ‘((Y FilMap h) ‘F)))))
13		3simpb 792	. . . . . . . . . . . . . 14 ⊢ ((X = ∪h ⋀ f ⊆ h ⋀ A ∈ ((fLim1 ‘J) ‘h)) → (X = ∪h ⋀ A ∈ ((fLim1 ‘J) ‘h)))
14	13	ad2antrl 406	. . . . . . . . . . . . 13 ⊢ (((((J ∈ Top ⋀ K ∈ Top ⋀ F:X–→Y) ⋀ A ∈ X) ⋀ h ∈ Fil) ⋀ ((X = ∪h ⋀ f ⊆ h ⋀ A ∈ ((fLim1 ‘J) ‘h)) ⋀ (f ∈ Fil ⋀ X = ∪f))) → (X = ∪h ⋀ A ∈ ((fLim1 ‘J) ‘h)))
15		unieq 2576	. . . . . . . . . . . . . . . . . . 19 ⊢ (k = ((Y FilMap h) ‘F) → ∪k = ∪((Y FilMap h) ‘F))
16	15	eqeq2d 1529	. . . . . . . . . . . . . . . . . 18 ⊢ (k = ((Y FilMap h) ‘F) → (Y = ∪k ↔ Y = ∪((Y FilMap h) ‘F)))
17		sseq2 2135	. . . . . . . . . . . . . . . . . 18 ⊢ (k = ((Y FilMap h) ‘F) → (((Y FilMap f) ‘F) ⊆ k ↔ ((Y FilMap f) ‘F) ⊆ ((Y FilMap h) ‘F)))
18		fveq2 3835	. . . . . . . . . . . . . . . . . . 19 ⊢ (k = ((Y FilMap h) ‘F) → ((fLim1 ‘K) ‘k) = ((fLim1 ‘K) ‘((Y FilMap h) ‘F)))
19	18	eleq2d 1584	. . . . . . . . . . . . . . . . . 18 ⊢ (k = ((Y FilMap h) ‘F) → ((F ‘A) ∈ ((fLim1 ‘K) ‘k) ↔ (F ‘A) ∈ ((fLim1 ‘K) ‘((Y FilMap h) ‘F))))
20	16, 17, 19	3anbi123d 899	. . . . . . . . . . . . . . . . 17 ⊢ (k = ((Y FilMap h) ‘F) → ((Y = ∪k ⋀ ((Y FilMap f) ‘F) ⊆ k ⋀ (F ‘A) ∈ ((fLim1 ‘K) ‘k)) ↔ (Y = ∪((Y FilMap h) ‘F) ⋀ ((Y FilMap f) ‘F) ⊆ ((Y FilMap h) ‘F) ⋀ (F ‘A) ∈ ((fLim1 ‘K) ‘((Y FilMap h) ‘F)))))
21	20	rcla4ev 1923	. . . . . . . . . . . . . . . 16 ⊢ ((((Y FilMap h) ‘F) ∈ Fil ⋀ (Y = ∪((Y FilMap h) ‘F) ⋀ ((Y FilMap f) ‘F) ⊆ ((Y FilMap h) ‘F) ⋀ (F ‘A) ∈ ((fLim1 ‘K) ‘((Y FilMap h) ‘F)))) → ∃k ∈ Fil (Y = ∪k ⋀ ((Y FilMap f) ‘F) ⊆ k ⋀ (F ‘A) ∈ ((fLim1 ‘K) ‘k)))
22		eqid 1518	. . . . . . . . . . . . . . . . . 18 ⊢ ∪h = ∪h
23	22	fmf 11693	. . . . . . . . . . . . . . . . 17 ⊢ ((Y ∈ V ⋀ h ∈ fBas ⋀ F:∪h–→Y) → ((Y FilMap h) ‘F) ∈ Fil)
24		uniexg 3094	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (K ∈ Top → ∪K ∈ V)
25		fcluscnp.2	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Y = ∪K
26	24, 25	syl5eqel 1595	. . . . . . . . . . . . . . . . . . . 20 ⊢ (K ∈ Top → Y ∈ V)
27	26	3ad2ant2 807	. . . . . . . . . . . . . . . . . . 19 ⊢ ((J ∈ Top ⋀ K ∈ Top ⋀ F:X–→Y) → Y ∈ V)
28	27	ad2antrr 404	. . . . . . . . . . . . . . . . . 18 ⊢ ((((J ∈ Top ⋀ K ∈ Top ⋀ F:X–→Y) ⋀ A ∈ X) ⋀ h ∈ Fil) → Y ∈ V)
29	28	ad2antrr 404	. . . . . . . . . . . . . . . . 17 ⊢ ((((((J ∈ Top ⋀ K ∈ Top ⋀ F:X–→Y) ⋀ A ∈ X) ⋀ h ∈ Fil) ⋀ ((X = ∪h ⋀ f ⊆ h ⋀ A ∈ ((fLim1 ‘J) ‘h)) ⋀ (f ∈ Fil ⋀ X = ∪f))) ⋀ (F ‘A) ∈ ((fLim1 ‘K) ‘((Y FilMap h) ‘F))) → Y ∈ V)
30		filfbas 11628	. . . . . . . . . . . . . . . . . . 19 ⊢ (h ∈ Fil → h ∈ fBas)
31	30	adantl 388	. . . . . . . . . . . . . . . . . 18 ⊢ ((((J ∈ Top ⋀ K ∈ Top ⋀ F:X–→Y) ⋀ A ∈ X) ⋀ h ∈ Fil) → h ∈ fBas)
32	31	ad2antrr 404	. . . . . . . . . . . . . . . . 17 ⊢ ((((((J ∈ Top ⋀ K ∈ Top ⋀ F:X–→Y) ⋀ A ∈ X) ⋀ h ∈ Fil) ⋀ ((X = ∪h ⋀ f ⊆ h ⋀ A ∈ ((fLim1 ‘J) ‘h)) ⋀ (f ∈ Fil ⋀ X = ∪f))) ⋀ (F ‘A) ∈ ((fLim1 ‘K) ‘((Y FilMap h) ‘F))) → h ∈ fBas)
33		feq2 3728	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (X = ∪h → (F:X–→Y ↔ F:∪h–→Y))
34	33	biimpac 418	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((F:X–→Y ⋀ X = ∪h) → F:∪h–→Y)
35	34	3ad2antl3 817	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((J ∈ Top ⋀ K ∈ Top ⋀ F:X–→Y) ⋀ X = ∪h) → F:∪h–→Y)
36	35	adantlr 393	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((J ∈ Top ⋀ K ∈ Top ⋀ F:X–→Y) ⋀ A ∈ X) ⋀ X = ∪h) → F:∪h–→Y)
37	36	adantlr 393	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((J ∈ Top ⋀ K ∈ Top ⋀ F:X–→Y) ⋀ A ∈ X) ⋀ h ∈ Fil) ⋀ X = ∪h) → F:∪h–→Y)
38	37	3ad2antr1 818	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((J ∈ Top ⋀ K ∈ Top ⋀ F:X–→Y) ⋀ A ∈ X) ⋀ h ∈ Fil) ⋀ (X = ∪h ⋀ f ⊆ h ⋀ A ∈ ((fLim1 ‘J) ‘h))) → F:∪h–→Y)
39	38	adantrr 395	. . . . . . . . . . . . . . . . . 18 ⊢ (((((J ∈ Top ⋀ K ∈ Top ⋀ F:X–→Y) ⋀ A ∈ X) ⋀ h ∈ Fil) ⋀ ((X = ∪h ⋀ f ⊆ h ⋀ A ∈ ((fLim1 ‘J) ‘h)) ⋀ (f ∈ Fil ⋀ X = ∪f))) → F:∪h–→Y)
40	39	adantr 389	. . . . . . . . . . . . . . . . 17 ⊢ ((((((J ∈ Top ⋀ K ∈ Top ⋀ F:X–→Y) ⋀ A ∈ X) ⋀ h ∈ Fil) ⋀ ((X = ∪h ⋀ f ⊆ h ⋀ A ∈ ((fLim1 ‘J) ‘h)) ⋀ (f ∈ Fil ⋀ X = ∪f))) ⋀ (F ‘A) ∈ ((fLim1 ‘K) ‘((Y FilMap h) ‘F))) → F:∪h–→Y)
41	23, 29, 32, 40	syl3anc 864	. . . . . . . . . . . . . . . 16 ⊢ ((((((J ∈ Top ⋀ K ∈ Top ⋀ F:X–→Y) ⋀ A ∈ X) ⋀ h ∈ Fil) ⋀ ((X = ∪h ⋀ f ⊆ h ⋀ A ∈ ((fLim1 ‘J) ‘h)) ⋀ (f ∈ Fil ⋀ X = ∪f))) ⋀ (F ‘A) ∈ ((fLim1 ‘K) ‘((Y FilMap h) ‘F))) → ((Y FilMap h) ‘F) ∈ Fil)
42	22	fmbas 11694	. . . . . . . . . . . . . . . . . . 19 ⊢ ((Y ∈ V ⋀ h ∈ fBas ⋀ F:∪h–→Y) → ∪((Y FilMap h) ‘F) = Y)
43	42, 29, 32, 40	syl3anc 864	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((J ∈ Top ⋀ K ∈ Top ⋀ F:X–→Y) ⋀ A ∈ X) ⋀ h ∈ Fil) ⋀ ((X = ∪h ⋀ f ⊆ h ⋀ A ∈ ((fLim1 ‘J) ‘h)) ⋀ (f ∈ Fil ⋀ X = ∪f))) ⋀ (F ‘A) ∈ ((fLim1 ‘K) ‘((Y FilMap h) ‘F))) → ∪((Y FilMap h) ‘F) = Y)
44	43	eqcomd 1523	. . . . . . . . . . . . . . . . 17 ⊢ ((((((J ∈ Top ⋀ K ∈ Top ⋀ F:X–→Y) ⋀ A ∈ X) ⋀ h ∈ Fil) ⋀ ((X = ∪h ⋀ f ⊆ h ⋀ A ∈ ((fLim1 ‘J) ‘h)) ⋀ (f ∈ Fil ⋀ X = ∪f))) ⋀ (F ‘A) ∈ ((fLim1 ‘K) ‘((Y FilMap h) ‘F))) → Y = ∪((Y FilMap h) ‘F))
45		fgss 11634	. . . . . . . . . . . . . . . . . . 19 ⊢ ((({x∣∃y ∈ f x = (F “ y)} ∪ {Y}) ∈ fBas ⋀ ({x∣∃y ∈ h x = (F “ y)} ∪ {Y}) ∈ fBas ⋀ ({x∣∃y ∈ f x = (F “ y)} ∪ {Y}) ⊆ ({x∣∃y ∈ h x = (F “ y)} ∪ {Y})) → (filGen ‘({x∣∃y ∈ f x = (F “ y)} ∪ {Y})) ⊆ (filGen ‘({x∣∃y ∈ h x = (F “ y)} ∪ {Y})))
46		eqid 1518	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ∪{x∣∃y ∈ f x = (F “ y)} = ∪{x∣∃y ∈ f x = (F “ y)}
47	46	extbas1 11641	. . . . . . . . . . . . . . . . . . . 20 ⊢ (({x∣∃y ∈ f x = (F “ y)} ∈ fBas ⋀ ∪{x∣∃y ∈ f x = (F “ y)} ⊆ Y) → ({x∣∃y ∈ f x = (F “ y)} ∪ {Y}) ∈ fBas)
48		eqid 1518	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ∪f = ∪f
49		eqid 1518	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ {x∣∃y ∈ f x = (F “ y)} = {x∣∃y ∈ f x = (F “ y)}
50	48, 49	filrn 11643	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((f ∈ fBas ⋀ F Fn ∪f) → {x∣∃y ∈ f x = (F “ y)} ∈ fBas)
51		filfbas 11628	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (f ∈ Fil → f ∈ fBas)
52	51	ad2antrl 406	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((X = ∪h ⋀ f ⊆ h ⋀ A ∈ ((fLim1 ‘J) ‘h)) ⋀ (f ∈ Fil ⋀ X = ∪f)) → f ∈ fBas)
53	52	ad2antlr 405	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((J ∈ Top ⋀ K ∈ Top ⋀ F:X–→Y) ⋀ A ∈ X) ⋀ h ∈ Fil) ⋀ ((X = ∪h ⋀ f ⊆ h ⋀ A ∈ ((fLim1 ‘J) ‘h)) ⋀ (f ∈ Fil ⋀ X = ∪f))) ⋀ (F ‘A) ∈ ((fLim1 ‘K) ‘((Y FilMap h) ‘F))) → f ∈ fBas)
54		ffn 3734	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (F:X–→Y → F Fn X)
55	54	3ad2ant3 808	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((J ∈ Top ⋀ K ∈ Top ⋀ F:X–→Y) → F Fn X)
56	55	adantr 389	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((J ∈ Top ⋀ K ∈ Top ⋀ F:X–→Y) ⋀ A ∈ X) → F Fn X)
57	56	ad2antrr 404	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((J ∈ Top ⋀ K ∈ Top ⋀ F:X–→Y) ⋀ A ∈ X) ⋀ h ∈ Fil) ⋀ ((X = ∪h ⋀ f ⊆ h ⋀ A ∈ ((fLim1 ‘J) ‘h)) ⋀ (f ∈ Fil ⋀ X = ∪f))) → F Fn X)
58		fneq2 3689	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (X = ∪f → (F Fn X ↔ F Fn ∪f))
59	58	adantl 388	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((f ∈ Fil ⋀ X = ∪f) → (F Fn X ↔ F Fn ∪f))
60	59	ad2antll 407	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((J ∈ Top ⋀ K ∈ Top ⋀ F:X–→Y) ⋀ A ∈ X) ⋀ h ∈ Fil) ⋀ ((X = ∪h ⋀ f ⊆ h ⋀ A ∈ ((fLim1 ‘J) ‘h)) ⋀ (f ∈ Fil ⋀ X = ∪f))) → (F Fn X ↔ F Fn ∪f))
61	57, 60	mpbid 193	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((J ∈ Top ⋀ K ∈ Top ⋀ F:X–→Y) ⋀ A ∈ X) ⋀ h ∈ Fil) ⋀ ((X = ∪h ⋀ f ⊆ h ⋀ A ∈ ((fLim1 ‘J) ‘h)) ⋀ (f ∈ Fil ⋀ X = ∪f))) → F Fn ∪f)
62	61	adantr 389	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((J ∈ Top ⋀ K ∈ Top ⋀ F:X–→Y) ⋀ A ∈ X) ⋀ h ∈ Fil) ⋀ ((X = ∪h ⋀ f ⊆ h ⋀ A ∈ ((fLim1 ‘J) ‘h)) ⋀ (f ∈ Fil ⋀ X = ∪f))) ⋀ (F ‘A) ∈ ((fLim1 ‘K) ‘((Y FilMap h) ‘F))) → F Fn ∪f)
63	50, 53, 62	sylanc 473	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((J ∈ Top ⋀ K ∈ Top ⋀ F:X–→Y) ⋀ A ∈ X) ⋀ h ∈ Fil) ⋀ ((X = ∪h ⋀ f ⊆ h ⋀ A ∈ ((fLim1 ‘J) ‘h)) ⋀ (f ∈ Fil ⋀ X = ∪f))) ⋀ (F ‘A) ∈ ((fLim1 ‘K) ‘((Y FilMap h) ‘F))) → {x∣∃y ∈ f x = (F “ y)} ∈ fBas)
64		sseq1 2134	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (t = (F “ y) → (t ⊆ Y ↔ (F “ y) ⊆ Y))
65		imassrn 3507	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (F “ y) ⊆ ran F
66	65	a1i 8	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (F:X–→Y → (F “ y) ⊆ ran F)
67		frn 3740	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (F:X–→Y → ran F ⊆ Y)
68	66, 67	sstrd 2126	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (F:X–→Y → (F “ y) ⊆ Y)
69	68	3ad2ant3 808	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((J ∈ Top ⋀ K ∈ Top ⋀ F:X–→Y) → (F “ y) ⊆ Y)
70	69	ad2antrr 404	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((J ∈ Top ⋀ K ∈ Top ⋀ F:X–→Y) ⋀ A ∈ X) ⋀ h ∈ Fil) → (F “ y) ⊆ Y)
71	70	ad2antrr 404	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((((J ∈ Top ⋀ K ∈ Top ⋀ F:X–→Y) ⋀ A ∈ X) ⋀ h ∈ Fil) ⋀ ((X = ∪h ⋀ f ⊆ h ⋀ A ∈ ((fLim1 ‘J) ‘h)) ⋀ (f ∈ Fil ⋀ X = ∪f))) ⋀ (F ‘A) ∈ ((fLim1 ‘K) ‘((Y FilMap h) ‘F))) → (F “ y) ⊆ Y)
72	64, 71	syl5cbir 209	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((J ∈ Top ⋀ K ∈ Top ⋀ F:X–→Y) ⋀ A ∈ X) ⋀ h ∈ Fil) ⋀ ((X = ∪h ⋀ f ⊆ h ⋀ A ∈ ((fLim1 ‘J) ‘h)) ⋀ (f ∈ Fil ⋀ X = ∪f))) ⋀ (F ‘A) ∈ ((fLim1 ‘K) ‘((Y FilMap h) ‘F))) → (t = (F “ y) → t ⊆ Y))
73	72	a1d 12	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((J ∈ Top ⋀ K ∈ Top ⋀ F:X–→Y) ⋀ A ∈ X) ⋀ h ∈ Fil) ⋀ ((X = ∪h ⋀ f ⊆ h ⋀ A ∈ ((fLim1 ‘J) ‘h)) ⋀ (f ∈ Fil ⋀ X = ∪f))) ⋀ (F ‘A) ∈ ((fLim1 ‘K) ‘((Y FilMap h) ‘F))) → (y ∈ f → (t = (F “ y) → t ⊆ Y)))
74	73	r19.23adv 1792	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((J ∈ Top ⋀ K ∈ Top ⋀ F:X–→Y) ⋀ A ∈ X) ⋀ h ∈ Fil) ⋀ ((X = ∪h ⋀ f ⊆ h ⋀ A ∈ ((fLim1 ‘J) ‘h)) ⋀ (f ∈ Fil ⋀ X = ∪f))) ⋀ (F ‘A) ∈ ((fLim1 ‘K) ‘((Y FilMap h) ‘F))) → (∃y ∈ f t = (F “ y) → t ⊆ Y))
75		visset 1859	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ t ∈ V
76		eqeq1 1524	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (x = t → (x = (F “ y) ↔ t = (F “ y)))
77	76	rexbidv 1710	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (x = t → (∃y ∈ f x = (F “ y) ↔ ∃y ∈ f t = (F “ y)))
78	75, 77	elab 1943	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (t ∈ {x∣∃y ∈ f x = (F “ y)} ↔ ∃y ∈ f t = (F “ y))
79	74, 78	syl5ib 204	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((J ∈ Top ⋀ K ∈ Top ⋀ F:X–→Y) ⋀ A ∈ X) ⋀ h ∈ Fil) ⋀ ((X = ∪h ⋀ f ⊆ h ⋀ A ∈ ((fLim1 ‘J) ‘h)) ⋀ (f ∈ Fil ⋀ X = ∪f))) ⋀ (F ‘A) ∈ ((fLim1 ‘K) ‘((Y FilMap h) ‘F))) → (t ∈ {x∣∃y ∈ f x = (F “ y)} → t ⊆ Y))
80	79	r19.21aiv 1759	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((J ∈ Top ⋀ K ∈ Top ⋀ F:X–→Y) ⋀ A ∈ X) ⋀ h ∈ Fil) ⋀ ((X = ∪h ⋀ f ⊆ h ⋀ A ∈ ((fLim1 ‘J) ‘h)) ⋀ (f ∈ Fil ⋀ X = ∪f))) ⋀ (F ‘A) ∈ ((fLim1 ‘K) ‘((Y FilMap h) ‘F))) → ∀t ∈ {x∣∃y ∈ f x = (F “ y)}t ⊆ Y)
81		unissb 2595	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∪{x∣∃y ∈ f x = (F “ y)} ⊆ Y ↔ ∀t ∈ {x∣∃y ∈ f x = (F “ y)}t ⊆ Y)
82	80, 81	sylibr 198	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((J ∈ Top ⋀ K ∈ Top ⋀ F:X–→Y) ⋀ A ∈ X) ⋀ h ∈ Fil) ⋀ ((X = ∪h ⋀ f ⊆ h ⋀ A ∈ ((fLim1 ‘J) ‘h)) ⋀ (f ∈ Fil ⋀ X = ∪f))) ⋀ (F ‘A) ∈ ((fLim1 ‘K) ‘((Y FilMap h) ‘F))) → ∪{x∣∃y ∈ f x = (F “ y)} ⊆ Y)
83	47, 63, 82	sylanc 473	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((J ∈ Top ⋀ K ∈ Top ⋀ F:X–→Y) ⋀ A ∈ X) ⋀ h ∈ Fil) ⋀ ((X = ∪h ⋀ f ⊆ h ⋀ A ∈ ((fLim1 ‘J) ‘h)) ⋀ (f ∈ Fil ⋀ X = ∪f))) ⋀ (F ‘A) ∈ ((fLim1 ‘K) ‘((Y FilMap h) ‘F))) → ({x∣∃y ∈ f x = (F “ y)} ∪ {Y}) ∈ fBas)
84		eqid 1518	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ∪{x∣∃y ∈ h x = (F “ y)} = ∪{x∣∃y ∈ h x = (F “ y)}
85	84	extbas1 11641	. . . . . . . . . . . . . . . . . . . 20 ⊢ (({x∣∃y ∈ h x = (F “ y)} ∈ fBas ⋀ ∪{x∣∃y ∈ h x = (F “ y)} ⊆ Y) → ({x∣∃y ∈ h x = (F “ y)} ∪ {Y}) ∈ fBas)
86		eqid 1518	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ {x∣∃y ∈ h x = (F “ y)} = {x∣∃y ∈ h x = (F “ y)}
87	22, 86	filrn 11643	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((h ∈ fBas ⋀ F Fn ∪h) → {x∣∃y ∈ h x = (F “ y)} ∈ fBas)
88	55	ad2antrr 404	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((J ∈ Top ⋀ K ∈ Top ⋀ F:X–→Y) ⋀ A ∈ X) ⋀ h ∈ Fil) → F Fn X)
89	88	ad2antrr 404	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((J ∈ Top ⋀ K ∈ Top ⋀ F:X–→Y) ⋀ A ∈ X) ⋀ h ∈ Fil) ⋀ ((X = ∪h ⋀ f ⊆ h ⋀ A ∈ ((fLim1 ‘J) ‘h)) ⋀ (f ∈ Fil ⋀ X = ∪f))) ⋀ (F ‘A) ∈ ((fLim1 ‘K) ‘((Y FilMap h) ‘F))) → F Fn X)
90		fneq2 3689	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (X = ∪h → (F Fn X ↔ F Fn ∪h))
91	90	3ad2ant1 806	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((X = ∪h ⋀ f ⊆ h ⋀ A ∈ ((fLim1 ‘J) ‘h)) → (F Fn X ↔ F Fn ∪h))
92	91	adantr 389	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((X = ∪h ⋀ f ⊆ h ⋀ A ∈ ((fLim1 ‘J) ‘h)) ⋀ (f ∈ Fil ⋀ X = ∪f)) → (F Fn X ↔ F Fn ∪h))
93	92	ad2antlr 405	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((J ∈ Top ⋀ K ∈ Top ⋀ F:X–→Y) ⋀ A ∈ X) ⋀ h ∈ Fil) ⋀ ((X = ∪h ⋀ f ⊆ h ⋀ A ∈ ((fLim1 ‘J) ‘h)) ⋀ (f ∈ Fil ⋀ X = ∪f))) ⋀ (F ‘A) ∈ ((fLim1 ‘K) ‘((Y FilMap h) ‘F))) → (F Fn X ↔ F Fn ∪h))
94	89, 93	mpbid 193	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((J ∈ Top ⋀ K ∈ Top ⋀ F:X–→Y) ⋀ A ∈ X) ⋀ h ∈ Fil) ⋀ ((X = ∪h ⋀ f ⊆ h ⋀ A ∈ ((fLim1 ‘J) ‘h)) ⋀ (f ∈ Fil ⋀ X = ∪f))) ⋀ (F ‘A) ∈ ((fLim1 ‘K) ‘((Y FilMap h) ‘F))) → F Fn ∪h)
95	87, 32, 94	sylanc 473	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((J ∈ Top ⋀ K ∈ Top ⋀ F:X–→Y) ⋀ A ∈ X) ⋀ h ∈ Fil) ⋀ ((X = ∪h ⋀ f ⊆ h ⋀ A ∈ ((fLim1 ‘J) ‘h)) ⋀ (f ∈ Fil ⋀ X = ∪f))) ⋀ (F ‘A) ∈ ((fLim1 ‘K) ‘((Y FilMap h) ‘F))) → {x∣∃y ∈ h x = (F “ y)} ∈ fBas)
96	64, 68	syl5cbir 209	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (F:X–→Y → (t = (F “ y) → t ⊆ Y))
97	96	3ad2ant3 808	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((J ∈ Top ⋀ K ∈ Top ⋀ F:X–→Y) → (t = (F “ y) → t ⊆ Y))
98	97	ad2antrr 404	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((J ∈ Top ⋀ K ∈ Top ⋀ F:X–→Y) ⋀ A ∈ X) ⋀ h ∈ Fil) → (t = (F “ y) → t ⊆ Y))
99	98	ad2antrr 404	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((J ∈ Top ⋀ K ∈ Top ⋀ F:X–→Y) ⋀ A ∈ X) ⋀ h ∈ Fil) ⋀ ((X = ∪h ⋀ f ⊆ h ⋀ A ∈ ((fLim1 ‘J) ‘h)) ⋀ (f ∈ Fil ⋀ X = ∪f))) ⋀ (F ‘A) ∈ ((fLim1 ‘K) ‘((Y FilMap h) ‘F))) → (t = (F “ y) → t ⊆ Y))
100	99	a1d 12	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((J ∈ Top ⋀ K ∈ Top ⋀ F:X–→Y) ⋀ A ∈ X) ⋀ h ∈ Fil) ⋀ ((X = ∪h ⋀ f ⊆ h ⋀ A ∈ ((fLim1 ‘J) ‘h)) ⋀ (f ∈ Fil ⋀ X = ∪f))) ⋀ (F ‘A) ∈ ((fLim1 ‘K) ‘((Y FilMap h) ‘F))) → (y ∈ h → (t = (F “ y) → t ⊆ Y)))
101	100	r19.23adv 1792	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((J ∈ Top ⋀ K ∈ Top ⋀ F:X–→Y) ⋀ A ∈ X) ⋀ h ∈ Fil) ⋀ ((X = ∪h ⋀ f ⊆ h ⋀ A ∈ ((fLim1 ‘J) ‘h)) ⋀ (f ∈ Fil ⋀ X = ∪f))) ⋀ (F ‘A) ∈ ((fLim1 ‘K) ‘((Y FilMap h) ‘F))) → (∃y ∈ h t = (F “ y) → t ⊆ Y))
102	76	rexbidv 1710	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (x = t → (∃y ∈ h x = (F “ y) ↔ ∃y ∈ h t = (F “ y)))
103	75, 102	elab 1943	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (t ∈ {x∣∃y ∈ h x = (F “ y)} ↔ ∃y ∈ h t = (F “ y))
104	101, 103	syl5ib 204	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((J ∈ Top ⋀ K ∈ Top ⋀ F:X–→Y) ⋀ A ∈ X) ⋀ h ∈ Fil) ⋀ ((X = ∪h ⋀ f ⊆ h ⋀ A ∈ ((fLim1 ‘J) ‘h)) ⋀ (f ∈ Fil ⋀ X = ∪f))) ⋀ (F ‘A) ∈ ((fLim1 ‘K) ‘((Y FilMap h) ‘F))) → (t ∈ {x∣∃y ∈ h x = (F “ y)} → t ⊆ Y))
105	104	r19.21aiv 1759	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((J ∈ Top ⋀ K ∈ Top ⋀ F:X–→Y) ⋀ A ∈ X) ⋀ h ∈ Fil) ⋀ ((X = ∪h ⋀ f ⊆ h ⋀ A ∈ ((fLim1 ‘J) ‘h)) ⋀ (f ∈ Fil ⋀ X = ∪f))) ⋀ (F ‘A) ∈ ((fLim1 ‘K) ‘((Y FilMap h) ‘F))) → ∀t ∈ {x∣∃y ∈ h x = (F “ y)}t ⊆ Y)
106		unissb 2595	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∪{x∣∃y ∈ h x = (F “ y)} ⊆ Y ↔ ∀t ∈ {x∣∃y ∈ h x = (F “ y)}t ⊆ Y)
107	105, 106	sylibr 198	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((J ∈ Top ⋀ K ∈ Top ⋀ F:X–→Y) ⋀ A ∈ X) ⋀ h ∈ Fil) ⋀ ((X = ∪h ⋀ f ⊆ h ⋀ A ∈ ((fLim1 ‘J) ‘h)) ⋀ (f ∈ Fil ⋀ X = ∪f))) ⋀ (F ‘A) ∈ ((fLim1 ‘K) ‘((Y FilMap h) ‘F))) → ∪{x∣∃y ∈ h x = (F “ y)} ⊆ Y)
108	85, 95, 107	sylanc 473	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((J ∈ Top ⋀ K ∈ Top ⋀ F:X–→Y) ⋀ A ∈ X) ⋀ h ∈ Fil) ⋀ ((X = ∪h ⋀ f ⊆ h ⋀ A ∈ ((fLim1 ‘J) ‘h)) ⋀ (f ∈ Fil ⋀ X = ∪f))) ⋀ (F ‘A) ∈ ((fLim1 ‘K) ‘((Y FilMap h) ‘F))) → ({x∣∃y ∈ h x = (F “ y)} ∪ {Y}) ∈ fBas)
109		ssrexv 2167	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (f ⊆ h → (∃y ∈ f x = (F “ y) → ∃y ∈ h x = (F “ y)))
110	109	3ad2ant2 807	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((X = ∪h ⋀ f ⊆ h ⋀ A ∈ ((fLim1 ‘J) ‘h)) → (∃y ∈ f x = (F “ y) → ∃y ∈ h x = (F “ y)))
111	110	adantr 389	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((X = ∪h ⋀ f ⊆ h ⋀ A ∈ ((fLim1 ‘J) ‘h)) ⋀ (f ∈ Fil ⋀ X = ∪f)) → (∃y ∈ f x = (F “ y) → ∃y ∈ h x = (F “ y)))
112	111	ad2antlr 405	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((J ∈ Top ⋀ K ∈ Top ⋀ F:X–→Y) ⋀ A ∈ X) ⋀ h ∈ Fil) ⋀ ((X = ∪h ⋀ f ⊆ h ⋀ A ∈ ((fLim1 ‘J) ‘h)) ⋀ (f ∈ Fil ⋀ X = ∪f))) ⋀ (F ‘A) ∈ ((fLim1 ‘K) ‘((Y FilMap h) ‘F))) → (∃y ∈ f x = (F “ y) → ∃y ∈ h x = (F “ y)))
113	112	19.21aiv 1324	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((J ∈ Top ⋀ K ∈ Top ⋀ F:X–→Y) ⋀ A ∈ X) ⋀ h ∈ Fil) ⋀ ((X = ∪h ⋀ f ⊆ h ⋀ A ∈ ((fLim1 ‘J) ‘h)) ⋀ (f ∈ Fil ⋀ X = ∪f))) ⋀ (F ‘A) ∈ ((fLim1 ‘K) ‘((Y FilMap h) ‘F))) → ∀x(∃y ∈ f x = (F “ y) → ∃y ∈ h x = (F “ y)))
114		ss2ab 2168	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ({x∣∃y ∈ f x = (F “ y)} ⊆ {x∣∃y ∈ h x = (F “ y)} ↔ ∀x(∃y ∈ f x = (F “ y) → ∃y ∈ h x = (F “ y)))
115		unss1 2251	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ({x∣∃y ∈ f x = (F “ y)} ⊆ {x∣∃y ∈ h x = (F “ y)} → ({x∣∃y ∈ f x = (F “ y)} ∪ {Y}) ⊆ ({x∣∃y ∈ h x = (F “ y)} ∪ {Y}))
116	114, 115	sylbir 199	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∀x(∃y ∈ f x = (F “ y) → ∃y ∈ h x = (F “ y)) → ({x∣∃y ∈ f x = (F “ y)} ∪ {Y}) ⊆ ({x∣∃y ∈ h x = (F “ y)} ∪ {Y}))
117	113, 116	syl 10	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((J ∈ Top ⋀ K ∈ Top ⋀ F:X–→Y) ⋀ A ∈ X) ⋀ h ∈ Fil) ⋀ ((X = ∪h ⋀ f ⊆ h ⋀ A ∈ ((fLim1 ‘J) ‘h)) ⋀ (f ∈ Fil ⋀ X = ∪f))) ⋀ (F ‘A) ∈ ((fLim1 ‘K) ‘((Y FilMap h) ‘F))) → ({x∣∃y ∈ f x = (F “ y)} ∪ {Y}) ⊆ ({x∣∃y ∈ h x = (F “ y)} ∪ {Y}))
118	45, 83, 108, 117	syl3anc 864	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((J ∈ Top ⋀ K ∈ Top ⋀ F:X–→Y) ⋀ A ∈ X) ⋀ h ∈ Fil) ⋀ ((X = ∪h ⋀ f ⊆ h ⋀ A ∈ ((fLim1 ‘J) ‘h)) ⋀ (f ∈ Fil ⋀ X = ∪f))) ⋀ (F ‘A) ∈ ((fLim1 ‘K) ‘((Y FilMap h) ‘F))) → (filGen ‘({x∣∃y ∈ f x = (F “ y)} ∪ {Y})) ⊆ (filGen ‘({x∣∃y ∈ h x = (F “ y)} ∪ {Y})))
119	48	isfilmap 11689	. . . . . . . . . . . . . . . . . . 19 ⊢ ((Y ∈ V ⋀ f ∈ fBas ⋀ F:∪f–→Y) → ((Y FilMap f) ‘F) = (filGen ‘({x∣∃y ∈ f x = (F “ y)} ∪ {Y})))
120		feq2 3728	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (X = ∪f → (F:X–→Y ↔ F:∪f–→Y))
121	120	biimpac 418	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((F:X–→Y ⋀ X = ∪f) → F:∪f–→Y)
122	121	3ad2antl3 817	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((J ∈ Top ⋀ K ∈ Top ⋀ F:X–→Y) ⋀ X = ∪f) → F:∪f–→Y)
123	122	adantlr 393	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((J ∈ Top ⋀ K ∈ Top ⋀ F:X–→Y) ⋀ A ∈ X) ⋀ X = ∪f) → F:∪f–→Y)
124	123	ad2ant2rl 411	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((J ∈ Top ⋀ K ∈ Top ⋀ F:X–→Y) ⋀ A ∈ X) ⋀ h ∈ Fil) ⋀ ((X = ∪h ⋀ f ⊆ h ⋀ A ∈ ((fLim1 ‘J) ‘h)) ⋀ X = ∪f)) → F:∪f–→Y)
125	124	adantrrl 402	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((J ∈ Top ⋀ K ∈ Top ⋀ F:X–→Y) ⋀ A ∈ X) ⋀ h ∈ Fil) ⋀ ((X = ∪h ⋀ f ⊆ h ⋀ A ∈ ((fLim1 ‘J) ‘h)) ⋀ (f ∈ Fil ⋀ X = ∪f))) → F:∪f–→Y)
126	125	adantr 389	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((J ∈ Top ⋀ K ∈ Top ⋀ F:X–→Y) ⋀ A ∈ X) ⋀ h ∈ Fil) ⋀ ((X = ∪h ⋀ f ⊆ h ⋀ A ∈ ((fLim1 ‘J) ‘h)) ⋀ (f ∈ Fil ⋀ X = ∪f))) ⋀ (F ‘A) ∈ ((fLim1 ‘K) ‘((Y FilMap h) ‘F))) → F:∪f–→Y)
127	119, 29, 53, 126	syl3anc 864	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((J ∈ Top ⋀ K ∈ Top ⋀ F:X–→Y) ⋀ A ∈ X) ⋀ h ∈ Fil) ⋀ ((X = ∪h ⋀ f ⊆ h ⋀ A ∈ ((fLim1 ‘J) ‘h)) ⋀ (f ∈ Fil ⋀ X = ∪f))) ⋀ (F ‘A) ∈ ((fLim1 ‘K) ‘((Y FilMap h) ‘F))) → ((Y FilMap f) ‘F) = (filGen ‘({x∣∃y ∈ f x = (F “ y)} ∪ {Y})))
128	22	isfilmap 11689	. . . . . . . . . . . . . . . . . . 19 ⊢ ((Y ∈ V ⋀ h ∈ fBas ⋀ F:∪h–→Y) → ((Y FilMap h) ‘F) = (filGen ‘({x∣∃y ∈ h x = (F “ y)} ∪ {Y})))
129	128, 29, 32, 40	syl3anc 864	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((J ∈ Top ⋀ K ∈ Top ⋀ F:X–→Y) ⋀ A ∈ X) ⋀ h ∈ Fil) ⋀ ((X = ∪h ⋀ f ⊆ h ⋀ A ∈ ((fLim1 ‘J) ‘h)) ⋀ (f ∈ Fil ⋀ X = ∪f))) ⋀ (F ‘A) ∈ ((fLim1 ‘K) ‘((Y FilMap h) ‘F))) → ((Y FilMap h) ‘F) = (filGen ‘({x∣∃y ∈ h x = (F “ y)} ∪ {Y})))
130	118, 127, 129	3sstr4d 2156	. . . . . . . . . . . . . . . . 17 ⊢ ((((((J ∈ Top ⋀ K ∈ Top ⋀ F:X–→Y) ⋀ A ∈ X) ⋀ h ∈ Fil) ⋀ ((X = ∪h ⋀ f ⊆ h ⋀ A ∈ ((fLim1 ‘J) ‘h)) ⋀ (f ∈ Fil ⋀ X = ∪f))) ⋀ (F ‘A) ∈ ((fLim1 ‘K) ‘((Y FilMap h) ‘F))) → ((Y FilMap f) ‘F) ⊆ ((Y FilMap h) ‘F))
131		pm3.27 321	. . . . . . . . . . . . . . . . 17 ⊢ ((((((J ∈ Top ⋀ K ∈ Top ⋀ F:X–→Y) ⋀ A ∈ X) ⋀ h ∈ Fil) ⋀ ((X = ∪h ⋀ f ⊆ h ⋀ A ∈ ((fLim1 ‘J) ‘h)) ⋀ (f ∈ Fil ⋀ X = ∪f))) ⋀ (F ‘A) ∈ ((fLim1 ‘K) ‘((Y FilMap h) ‘F))) → (F ‘A) ∈ ((fLim1 ‘K) ‘((Y FilMap h) ‘F)))
132	44, 130, 131	3jca 825	. . . . . . . . . . . . . . . 16 ⊢ ((((((J ∈ Top ⋀ K ∈ Top ⋀ F:X–→Y) ⋀ A ∈ X) ⋀ h ∈ Fil) ⋀ ((X = ∪h ⋀ f ⊆ h ⋀ A ∈ ((fLim1 ‘J) ‘h)) ⋀ (f ∈ Fil ⋀ X = ∪f))) ⋀ (F ‘A) ∈ ((fLim1 ‘K) ‘((Y FilMap h) ‘F))) → (Y = ∪((Y FilMap h) ‘F) ⋀ ((Y FilMap f) ‘F) ⊆ ((Y FilMap h) ‘F) ⋀ (F ‘A) ∈ ((fLim1 ‘K) ‘((Y FilMap h) ‘F))))
133	21, 41, 132	sylanc 473	. . . . . . . . . . . . . . 15 ⊢ ((((((J ∈ Top ⋀ K ∈ Top ⋀ F:X–→Y) ⋀ A ∈ X) ⋀ h ∈ Fil) ⋀ ((X = ∪h ⋀ f ⊆ h ⋀ A ∈ ((fLim1 ‘J) ‘h)) ⋀ (f ∈ Fil ⋀ X = ∪f))) ⋀ (F ‘A) ∈ ((fLim1 ‘K) ‘((Y FilMap h) ‘F))) → ∃k ∈ Fil (Y = ∪k ⋀ ((Y FilMap f) ‘F) ⊆ k ⋀ (F ‘A) ∈ ((fLim1 ‘K) ‘k)))
134	133	ex 371	. . . . . . . . . . . . . 14 ⊢ (((((J ∈ Top ⋀ K ∈ Top ⋀ F:X–→Y) ⋀ A ∈ X) ⋀ h ∈ Fil) ⋀ ((X = ∪h ⋀ f ⊆ h ⋀ A ∈ ((fLim1 ‘J) ‘h)) ⋀ (f ∈ Fil ⋀ X = ∪f))) → ((F ‘A) ∈ ((fLim1 ‘K) ‘((Y FilMap h) ‘F)) → ∃k ∈ Fil (Y = ∪k ⋀ ((Y FilMap f) ‘F) ⊆ k ⋀ (F ‘A) ∈ ((fLim1 ‘K) ‘k))))
135	134	imim2d 25	. . . . . . . . . . . . 13 ⊢ (((((J ∈ Top ⋀ K ∈ Top ⋀ F:X–→Y) ⋀ A ∈ X) ⋀ h ∈ Fil) ⋀ ((X = ∪h ⋀ f ⊆ h ⋀ A ∈ ((fLim1 ‘J) ‘h)) ⋀ (f ∈ Fil ⋀ X = ∪f))) → (((X = ∪h ⋀ A ∈ ((fLim1 ‘J) ‘h)) → (F ‘A) ∈ ((fLim1 ‘K) ‘((Y FilMap h) ‘F))) → ((X = ∪h ⋀ A ∈ ((fLim1 ‘J) ‘h)) → ∃k ∈ Fil (Y = ∪k ⋀ ((Y FilMap f) ‘F) ⊆ k ⋀ (F ‘A) ∈ ((fLim1 ‘K) ‘k)))))
136	14, 135	mpid 47	. . . . . . . . . . . 12 ⊢ (((((J ∈ Top ⋀ K ∈ Top ⋀ F:X–→Y) ⋀ A ∈ X) ⋀ h ∈ Fil) ⋀ ((X = ∪h ⋀ f ⊆ h ⋀ A ∈ ((fLim1 ‘J) ‘h)) ⋀ (f ∈ Fil ⋀ X = ∪f))) → (((X = ∪h ⋀ A ∈ ((fLim1 ‘J) ‘h)) → (F ‘A) ∈ ((fLim1 ‘K) ‘((Y FilMap h) ‘F))) → ∃k ∈ Fil (Y = ∪k ⋀ ((Y FilMap f) ‘F) ⊆ k ⋀ (F ‘A) ∈ ((fLim1 ‘K) ‘k))))
137	12, 136	syld 27	. . . . . . . . . . 11 ⊢ (((((J ∈ Top ⋀ K ∈ Top ⋀ F:X–→Y) ⋀ A ∈ X) ⋀ h ∈ Fil) ⋀ ((X = ∪h ⋀ f ⊆ h ⋀ A ∈ ((fLim1 ‘J) ‘h)) ⋀ (f ∈ Fil ⋀ X = ∪f))) → (∀g ∈ Fil ((X = ∪g ⋀ A ∈ ((fLim1 ‘J) ‘g)) → (F ‘A) ∈ ((fLim1 ‘K) ‘((Y FilMap g) ‘F))) → ∃k ∈ Fil (Y = ∪k ⋀ ((Y FilMap f) ‘F) ⊆ k ⋀ (F ‘A) ∈ ((fLim1 ‘K) ‘k))))
138	137	exp43 384	. . . . . . . . . 10 ⊢ (((J ∈ Top ⋀ K ∈ Top ⋀ F:X–→Y) ⋀ A ∈ X) → (h ∈ Fil → ((X = ∪h ⋀ f ⊆ h ⋀ A ∈ ((fLim1 ‘J) ‘h)) → ((f ∈ Fil ⋀ X = ∪f) → (∀g ∈ Fil ((X = ∪g ⋀ A ∈ ((fLim1 ‘J) ‘g)) → (F ‘A) ∈ ((fLim1 ‘K) ‘((Y FilMap g) ‘F))) → ∃k ∈ Fil (Y = ∪k ⋀ ((Y FilMap f) ‘F) ⊆ k ⋀ (F ‘A) ∈ ((fLim1 ‘K) ‘k)))))))
139	138	com45 11325	. . . . . . . . 9 ⊢ (((J ∈ Top ⋀ K ∈ Top ⋀ F:X–→Y) ⋀ A ∈ X) → (h ∈ Fil → ((X = ∪h ⋀ f ⊆ h ⋀ A ∈ ((fLim1 ‘J) ‘h)) → (∀g ∈ Fil ((X = ∪g ⋀ A ∈ ((fLim1 ‘J) ‘g)) → (F ‘A) ∈ ((fLim1 ‘K) ‘((Y FilMap g) ‘F))) → ((f ∈ Fil ⋀ X = ∪f) → ∃k ∈ Fil (Y = ∪k ⋀ ((Y FilMap f) ‘F) ⊆ k ⋀ (F ‘A) ∈ ((fLim1 ‘K) ‘k)))))))
140	139	com35 11326	. . . . . . . 8 ⊢ (((J ∈ Top ⋀ K ∈ Top ⋀ F:X–→Y) ⋀ A ∈ X) → (h ∈ Fil → ((f ∈ Fil ⋀ X = ∪f) → (∀g ∈ Fil ((X = ∪g ⋀ A ∈ ((fLim1 ‘J) ‘g)) → (F ‘A) ∈ ((fLim1 ‘K) ‘((Y FilMap g) ‘F))) → ((X = ∪h ⋀ f ⊆ h ⋀ A ∈ ((fLim1 ‘J) ‘h)) → ∃k ∈ Fil (Y = ∪k ⋀ ((Y FilMap f) ‘F) ⊆ k ⋀ (F ‘A) ∈ ((fLim1 ‘K) ‘k)))))))
141	140	com24 37	. . . . . . 7 ⊢ (((J ∈ Top ⋀ K ∈ Top ⋀ F:X–→Y) ⋀ A ∈ X) → (∀g ∈ Fil ((X = ∪g ⋀ A ∈ ((fLim1 ‘J) ‘g)) → (F ‘A) ∈ ((fLim1 ‘K) ‘((Y FilMap g) ‘F))) → ((f ∈ Fil ⋀ X = ∪f) → (h ∈ Fil → ((X = ∪h ⋀ f ⊆ h ⋀ A ∈ ((fLim1 ‘J) ‘h)) → ∃k ∈ Fil (Y = ∪k ⋀ ((Y FilMap f) ‘F) ⊆ k ⋀ (F ‘A) ∈ ((fLim1 ‘K) ‘k)))))))
142	141	imp32 361	. . . . . 6 ⊢ ((((J ∈ Top ⋀ K ∈ Top ⋀ F:X–→Y) ⋀ A ∈ X) ⋀ (∀g ∈ Fil ((X = ∪g ⋀ A ∈ ((fLim1 ‘J) ‘g)) → (F ‘A) ∈ ((fLim1 ‘K) ‘((Y FilMap g) ‘F))) ⋀ (f ∈ Fil ⋀ X = ∪f))) → (h ∈ Fil → ((X = ∪h ⋀ f ⊆ h ⋀ A ∈ ((fLim1 ‘J) ‘h)) → ∃k ∈ Fil (Y = ∪k ⋀ ((Y FilMap f) ‘F) ⊆ k ⋀ (F ‘A) ∈ ((fLim1 ‘K) ‘k)))))
143	142	r19.23adv 1792	. . . . 5 ⊢ ((((J ∈ Top ⋀ K ∈ Top ⋀ F:X–→Y) ⋀ A ∈ X) ⋀ (∀g ∈ Fil ((X = ∪g ⋀ A ∈ ((fLim1 ‘J) ‘g)) → (F ‘A) ∈ ((fLim1 ‘K) ‘((Y FilMap g) ‘F))) ⋀ (f ∈ Fil ⋀ X = ∪f))) → (∃h ∈ Fil (X = ∪h ⋀ f ⊆ h ⋀ A ∈ ((fLim1 ‘J) ‘h)) → ∃k ∈ Fil (Y = ∪k ⋀ ((Y FilMap f) ‘F) ⊆ k ⋀ (F ‘A) ∈ ((fLim1 ‘K) ‘k))))
144		fcluscnp.1	. . . . . . 7 ⊢ X = ∪J
145	144, 48	fclsfnflim 11726	. . . . . 6 ⊢ ((J ∈ Top ⋀ f ∈ Fil ⋀ X = ∪f) → (A ∈ ((fClus ‘J) ‘f) ↔ ∃h ∈ Fil (X = ∪h ⋀ f ⊆ h ⋀ A ∈ ((fLim1 ‘J) ‘h))))
146		3simp1 794	. . . . . . 7 ⊢ ((J ∈ Top ⋀ K ∈ Top ⋀ F:X–→Y) → J ∈ Top)
147	146	ad2antrr 404	. . . . . 6 ⊢ ((((J ∈ Top ⋀ K ∈ Top ⋀ F:X–→Y) ⋀ A ∈ X) ⋀ (∀g ∈ Fil ((X = ∪g ⋀ A ∈ ((fLim1 ‘J) ‘g)) → (F ‘A) ∈ ((fLim1 ‘K) ‘((Y FilMap g) ‘F))) ⋀ (f ∈ Fil ⋀ X = ∪f))) → J ∈ Top)
148		simprrl 11368	. . . . . 6 ⊢ ((((J ∈ Top ⋀ K ∈ Top ⋀ F:X–→Y) ⋀ A ∈ X) ⋀ (∀g ∈ Fil ((X = ∪g ⋀ A ∈ ((fLim1 ‘J) ‘g)) → (F ‘A) ∈ ((fLim1 ‘K) ‘((Y FilMap g) ‘F))) ⋀ (f ∈ Fil ⋀ X = ∪f))) → f ∈ Fil)
149		simprrr 11369	. . . . . 6 ⊢ ((((J ∈ Top ⋀ K ∈ Top ⋀ F:X–→Y) ⋀ A ∈ X) ⋀ (∀g ∈ Fil ((X = ∪g ⋀ A ∈ ((fLim1 ‘J) ‘g)) → (F ‘A) ∈ ((fLim1 ‘K) ‘((Y FilMap g) ‘F))) ⋀ (f ∈ Fil ⋀ X = ∪f))) → X = ∪f)
150	145, 147, 148, 149	syl3anc 864	. . . . 5 ⊢ ((((J ∈ Top ⋀ K ∈ Top ⋀ F:X–→Y) ⋀ A ∈ X) ⋀ (∀g ∈ Fil ((X = ∪g ⋀ A ∈ ((fLim1 ‘J) ‘g)) → (F ‘A) ∈ ((fLim1 ‘K) ‘((Y FilMap g) ‘F))) ⋀ (f ∈ Fil ⋀ X = ∪f))) → (A ∈ ((fClus ‘J) ‘f) ↔ ∃h ∈ Fil (X = ∪h ⋀ f ⊆ h ⋀ A ∈ ((fLim1 ‘J) ‘h))))
151		eqid 1518	. . . . . . 7 ⊢ ∪((Y FilMap f) ‘F) = ∪((Y FilMap f) ‘F)
152	25, 151	fclsfnflim 11726	. . . . . 6 ⊢ ((K ∈ Top ⋀ ((Y FilMap f) ‘F) ∈ Fil ⋀ Y = ∪((Y FilMap f) ‘F)) → ((F ‘A) ∈ ((fClus ‘K) ‘((Y FilMap f) ‘F)) ↔ ∃k ∈ Fil (Y = ∪k ⋀ ((Y FilMap f) ‘F) ⊆ k ⋀ (F ‘A) ∈ ((fLim1 ‘K) ‘k))))
153		3simp2 795	. . . . . . 7 ⊢ ((J ∈ Top ⋀ K ∈ Top ⋀ F:X–→Y) → K ∈ Top)
154	153	ad2antrr 404	. . . . . 6 ⊢ ((((J ∈ Top ⋀ K ∈ Top ⋀ F:X–→Y) ⋀ A ∈ X) ⋀ (∀g ∈ Fil ((X = ∪g ⋀ A ∈ ((fLim1 ‘J) ‘g)) → (F ‘A) ∈ ((fLim1 ‘K) ‘((Y FilMap g) ‘F))) ⋀ (f ∈ Fil ⋀ X = ∪f))) → K ∈ Top)
155	48	fmf 11693	. . . . . . 7 ⊢ ((Y ∈ V ⋀ f ∈ fBas ⋀ F:∪f–→Y) → ((Y FilMap f) ‘F) ∈ Fil)
156	27	ad2antrr 404	. . . . . . 7 ⊢ ((((J ∈ Top ⋀ K ∈ Top ⋀ F:X–→Y) ⋀ A ∈ X) ⋀ (∀g ∈ Fil ((X = ∪g ⋀ A ∈ ((fLim1 ‘J) ‘g)) → (F ‘A) ∈ ((fLim1 ‘K) ‘((Y FilMap g) ‘F))) ⋀ (f ∈ Fil ⋀ X = ∪f))) → Y ∈ V)
157	51	adantr 389	. . . . . . . 8 ⊢ ((f ∈ Fil ⋀ X = ∪f) → f ∈ fBas)
158	157	ad2antll 407	. . . . . . 7 ⊢ ((((J ∈ Top ⋀ K ∈ Top ⋀ F:X–→Y) ⋀ A ∈ X) ⋀ (∀g ∈ Fil ((X = ∪g ⋀ A ∈ ((fLim1 ‘J) ‘g)) → (F ‘A) ∈ ((fLim1 ‘K) ‘((Y FilMap g) ‘F))) ⋀ (f ∈ Fil ⋀ X = ∪f))) → f ∈ fBas)
159		3simp3 796	. . . . . . . . 9 ⊢ ((J ∈ Top ⋀ K ∈ Top ⋀ F:X–→Y) → F:X–→Y)
160	159	ad2antrr 404	. . . . . . . 8 ⊢ ((((J ∈ Top ⋀ K ∈ Top ⋀ F:X–→Y) ⋀ A ∈ X) ⋀ (∀g ∈ Fil ((X = ∪g ⋀ A ∈ ((fLim1 ‘J) ‘g)) → (F ‘A) ∈ ((fLim1 ‘K) ‘((Y FilMap g) ‘F))) ⋀ (f ∈ Fil ⋀ X = ∪f))) → F:X–→Y)
161	120	adantl 388	. . . . . . . . 9 ⊢ ((f ∈ Fil ⋀ X = ∪f) → (F:X–→Y ↔ F:∪f–→Y))
162	161	ad2antll 407	. . . . . . . 8 ⊢ ((((J ∈ Top ⋀ K ∈ Top ⋀ F:X–→Y) ⋀ A ∈ X) ⋀ (∀g ∈ Fil ((X = ∪g ⋀ A ∈ ((fLim1 ‘J) ‘g)) → (F ‘A) ∈ ((fLim1 ‘K) ‘((Y FilMap g) ‘F))) ⋀ (f ∈ Fil ⋀ X = ∪f))) → (F:X–→Y ↔ F:∪f–→Y))
163	160, 162	mpbid 193	. . . . . . 7 ⊢ ((((J ∈ Top ⋀ K ∈ Top ⋀ F:X–→Y) ⋀ A ∈ X) ⋀ (∀g ∈ Fil ((X = ∪g ⋀ A ∈ ((fLim1 ‘J) ‘g)) → (F ‘A) ∈ ((fLim1 ‘K) ‘((Y FilMap g) ‘F))) ⋀ (f ∈ Fil ⋀ X = ∪f))) → F:∪f–→Y)
164	155, 156, 158, 163	syl3anc 864	. . . . . 6 ⊢ ((((J ∈ Top ⋀ K ∈ Top ⋀ F:X–→Y) ⋀ A ∈ X) ⋀ (∀g ∈ Fil ((X = ∪g ⋀ A ∈ ((fLim1 ‘J) ‘g)) → (F ‘A) ∈ ((fLim1 ‘K) ‘((Y FilMap g) ‘F))) ⋀ (f ∈ Fil ⋀ X = ∪f))) → ((Y FilMap f) ‘F) ∈ Fil)
165	48	fmbas 11694	. . . . . . . 8 ⊢ ((Y ∈ V ⋀ f ∈ fBas ⋀ F:∪f–→Y) → ∪((Y FilMap f) ‘F) = Y)
166	165, 156, 158, 163	syl3anc 864	. . . . . . 7 ⊢ ((((J ∈ Top ⋀ K ∈ Top ⋀ F:X–→Y) ⋀ A ∈ X) ⋀ (∀g ∈ Fil ((X = ∪g ⋀ A ∈ ((fLim1 ‘J) ‘g)) → (F ‘A) ∈ ((fLim1 ‘K) ‘((Y FilMap g) ‘F))) ⋀ (f ∈ Fil ⋀ X = ∪f))) → ∪((Y FilMap f) ‘F) = Y)
167	166	eqcomd 1523	. . . . . 6 ⊢ ((((J ∈ Top ⋀ K ∈ Top ⋀ F:X–→Y) ⋀ A ∈ X) ⋀ (∀g ∈ Fil ((X = ∪g ⋀ A ∈ ((fLim1 ‘J) ‘g)) → (F ‘A) ∈ ((fLim1 ‘K) ‘((Y FilMap g) ‘F))) ⋀ (f ∈ Fil ⋀ X = ∪f))) → Y = ∪((Y FilMap f) ‘F))
168	152, 154, 164, 167	syl3anc 864	. . . . 5 ⊢ ((((J ∈ Top ⋀ K ∈ Top ⋀ F:X–→Y) ⋀ A ∈ X) ⋀ (∀g ∈ Fil ((X = ∪g ⋀ A ∈ ((fLim1 ‘J) ‘g)) → (F ‘A) ∈ ((fLim1 ‘K) ‘((Y FilMap g) ‘F))) ⋀ (f ∈ Fil ⋀ X = ∪f))) → ((F ‘A) ∈ ((fClus ‘K) ‘((Y FilMap f) ‘F)) ↔ ∃k ∈ Fil (Y = ∪k ⋀ ((Y FilMap f) ‘F) ⊆ k ⋀ (F ‘A) ∈ ((fLim1 ‘K) ‘k))))
169	143, 150, 168	3imtr4d 546	. . . 4 ⊢ ((((J ∈ Top ⋀ K ∈ Top ⋀ F:X–→Y) ⋀ A ∈ X) ⋀ (∀g ∈ Fil ((X = ∪g ⋀ A ∈ ((fLim1 ‘J) ‘g)) → (F ‘A) ∈ ((fLim1 ‘K) ‘((Y FilMap g) ‘F))) ⋀ (f ∈ Fil ⋀ X = ∪f))) → (A ∈ ((fClus ‘J) ‘f) → (F ‘A) ∈ ((fClus ‘K) ‘((Y FilMap f) ‘F))))
170	169	exp45 386	. . 3 ⊢ (((J ∈ Top ⋀ K ∈ Top ⋀ F:X–→Y) ⋀ A ∈ X) → (∀g ∈ Fil ((X = ∪g ⋀ A ∈ ((fLim1 ‘J) ‘g)) → (F ‘A) ∈ ((fLim1 ‘K) ‘((Y FilMap g) ‘F))) → (f ∈ Fil → (X = ∪f → (A ∈ ((fClus ‘J) ‘f) → (F ‘A) ∈ ((fClus ‘K) ‘((Y FilMap f) ‘F)))))))
171	170	imp5a 11342	. 2 ⊢ (((J ∈ Top ⋀ K ∈ Top ⋀ F:X–→Y) ⋀ A ∈ X) → (∀g ∈ Fil ((X = ∪g ⋀ A ∈ ((fLim1 ‘J) ‘g)) → (F ‘A) ∈ ((fLim1 ‘K) ‘((Y FilMap g) ‘F))) → (f ∈ Fil → ((X = ∪f ⋀ A ∈ ((fClus ‘J) ‘f)) → (F ‘A) ∈ ((fClus ‘K) ‘((Y FilMap f) ‘F))))))
172	171	r19.21adv 1764	1 ⊢ (((J ∈ Top ⋀ K ∈ Top ⋀ F:X–→Y) ⋀ A ∈ X) → (∀g ∈ Fil ((X = ∪g ⋀ A ∈ ((fLim1 ‘J) ‘g)) → (F ‘A) ∈ ((fLim1 ‘K) ‘((Y FilMap g) ‘F))) → ∀f ∈ Fil ((X = ∪f ⋀ A ∈ ((fClus ‘J) ‘f)) → (F ‘A) ∈ ((fClus ‘K) ‘((Y FilMap f) ‘F)))))

Colors of variables: wff set class

Syntax hints: → wi 3 ↔ wb 144 ⋀ wa 221 ⋀ w3a 781 ∀wal 990 = wceq 992 ∈ wcel 994 {cab 1505 ∀wral 1691 ∃wrex 1692 Vcvv 1857 ∪ cun 2097 ⊆ wss 2099 {csn 2467 ∪cuni 2569 ran crn 3252 “ cima 3254 Fn wfn 3258 –→wf 3259 ‘cfv 3263 (class class class)co 4021 Topctop 7800 Filcfil 11069 fLim1cflim1 11096 fBascfbas 11617 filGencfg 11618 FilMap cfilmap 11667 fCluscfclus 11669

This theorem is referenced by: fcluscnp 11730

This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-7 998 ax-gen 999 ax-8 1000 ax-9 1001 ax-10 1002 ax-11 1003 ax-12 1004 ax-13 1005 ax-14 1006 ax-17 1007 ax-4 1009 ax-5o 1011 ax-6o 1014 ax-9o 1159 ax-10o 1177 ax-16 1247 ax-11o 1255 ax-ext 1500 ax-rep 2767 ax-sep 2777 ax-nul 2784 ax-pow 2818 ax-pr 2855 ax-un 3089

This theorem depends on definitions: df-bi 145 df-or 222 df-an 223 df-3or 782 df-3an 783 df-ex 1017 df-sb 1209 df-eu 1421 df-mo 1422 df-clab 1506 df-cleq 1511 df-clel 1514 df-ne 1630 df-nel 1631 df-ral 1695 df-rex 1696 df-reu 1697 df-rab 1698 df-v 1858 df-sbc 1987 df-csb 2052 df-dif 2101 df-un 2102 df-in 2103 df-ss 2105 df-pss 2107 df-nul 2333 df-if 2416 df-pw 2459 df-sn 2470 df-pr 2471 df-tp 2473 df-op 2474 df-uni 2570 df-int 2601 df-iun 2635 df-iin 2636 df-br 2693 df-opab 2741 df-tr 2755 df-eprel 2910 df-id 2913 df-po 2918 df-so 2929 df-fr 2947 df-we 2962 df-ord 2978 df-on 2979 df-lim 2980 df-suc 2981 df-om 3219 df-xp 3265 df-rel 3266 df-cnv 3267 df-co 3268 df-dm 3269 df-rn 3270 df-res 3271 df-ima 3272 df-fun 3273 df-fn 3274 df-f 3275 df-f1 3276 df-fo 3277 df-f1o 3278 df-fv 3279 df-opr 4023 df-oprab 4024 df-rdg 4233 df-1o 4269 df-oadd 4271 df-er 4401 df-map 4465 df-en 4509 df-fin 4512 df-top 7804 df-cld 7873 df-ntr 7874 df-cls 7875 df-nei 7923 df-fi 10848 df-fil 11070 df-flim1 11098 df-fbas 11619 df-fg 11620 df-filmap 11671 df-fclus 11673