fcfval

Description: The set of cluster points of a function. (Contributed by Jeff Hankins, 24-Nov-2009) (Revised by Stefan O'Rear, 9-Aug-2015)

		Ref	Expression
	Assertion	fcfval	$⊢ (J \in TopOn (X) \land L \in Fil (Y) \land F : Y ⟶ X) \to (J fClusf L) (F) = J fClus (X FilMap F) (L)$

Proof

Step	Hyp	Ref	Expression
1		df-fcf	$⊢ fClusf = (j \in Top, f \in ⋃ ran Fil ⟼ (g \in ({⋃ j}^{⋃ f}) ⟼ j fClus (⋃ j FilMap g) (f)))$
2	1	a1i	$⊢ (J \in TopOn (X) \land L \in Fil (Y)) \to fClusf = (j \in Top, f \in ⋃ ran Fil ⟼ (g \in ({⋃ j}^{⋃ f}) ⟼ j fClus (⋃ j FilMap g) (f)))$
3		simprl	$⊢ ((J \in TopOn (X) \land L \in Fil (Y)) \land (j = J \land f = L)) \to j = J$
4	3	unieqd	$⊢ ((J \in TopOn (X) \land L \in Fil (Y)) \land (j = J \land f = L)) \to ⋃ j = ⋃ J$
5		toponuni	$⊢ J \in TopOn (X) \to X = ⋃ J$
6	5	ad2antrr	$⊢ ((J \in TopOn (X) \land L \in Fil (Y)) \land (j = J \land f = L)) \to X = ⋃ J$
7	4 6	eqtr4d	$⊢ ((J \in TopOn (X) \land L \in Fil (Y)) \land (j = J \land f = L)) \to ⋃ j = X$
8		unieq	$⊢ f = L \to ⋃ f = ⋃ L$
9	8	ad2antll	$⊢ ((J \in TopOn (X) \land L \in Fil (Y)) \land (j = J \land f = L)) \to ⋃ f = ⋃ L$
10		filunibas	$⊢ L \in Fil (Y) \to ⋃ L = Y$
11	10	ad2antlr	$⊢ ((J \in TopOn (X) \land L \in Fil (Y)) \land (j = J \land f = L)) \to ⋃ L = Y$
12	9 11	eqtrd	$⊢ ((J \in TopOn (X) \land L \in Fil (Y)) \land (j = J \land f = L)) \to ⋃ f = Y$
13	7 12	oveq12d	$⊢ ((J \in TopOn (X) \land L \in Fil (Y)) \land (j = J \land f = L)) \to {⋃ j}^{⋃ f} = X^{Y}$
14	7	oveq1d	$⊢ ((J \in TopOn (X) \land L \in Fil (Y)) \land (j = J \land f = L)) \to ⋃ j FilMap g = X FilMap g$
15		simprr	$⊢ ((J \in TopOn (X) \land L \in Fil (Y)) \land (j = J \land f = L)) \to f = L$
16	14 15	fveq12d	$⊢ ((J \in TopOn (X) \land L \in Fil (Y)) \land (j = J \land f = L)) \to (⋃ j FilMap g) (f) = (X FilMap g) (L)$
17	3 16	oveq12d	$⊢ ((J \in TopOn (X) \land L \in Fil (Y)) \land (j = J \land f = L)) \to j fClus (⋃ j FilMap g) (f) = J fClus (X FilMap g) (L)$
18	13 17	mpteq12dv	$⊢ ((J \in TopOn (X) \land L \in Fil (Y)) \land (j = J \land f = L)) \to (g \in ({⋃ j}^{⋃ f}) ⟼ j fClus (⋃ j FilMap g) (f)) = (g \in (X^{Y}) ⟼ J fClus (X FilMap g) (L))$
19		topontop	$⊢ J \in TopOn (X) \to J \in Top$
20	19	adantr	$⊢ (J \in TopOn (X) \land L \in Fil (Y)) \to J \in Top$
21		fvssunirn	$⊢ Fil (Y) \subseteq ⋃ ran Fil$
22	21	sseli	$⊢ L \in Fil (Y) \to L \in ⋃ ran Fil$
23	22	adantl	$⊢ (J \in TopOn (X) \land L \in Fil (Y)) \to L \in ⋃ ran Fil$
24		ovex	$⊢ X^{Y} \in V$
25	24	mptex	$⊢ (g \in (X^{Y}) ⟼ J fClus (X FilMap g) (L)) \in V$
26	25	a1i	$⊢ (J \in TopOn (X) \land L \in Fil (Y)) \to (g \in (X^{Y}) ⟼ J fClus (X FilMap g) (L)) \in V$
27	2 18 20 23 26	ovmpod	$⊢ (J \in TopOn (X) \land L \in Fil (Y)) \to J fClusf L = (g \in (X^{Y}) ⟼ J fClus (X FilMap g) (L))$
28	27	3adant3	$⊢ (J \in TopOn (X) \land L \in Fil (Y) \land F : Y ⟶ X) \to J fClusf L = (g \in (X^{Y}) ⟼ J fClus (X FilMap g) (L))$
29		simpr	$⊢ ((J \in TopOn (X) \land L \in Fil (Y) \land F : Y ⟶ X) \land g = F) \to g = F$
30	29	oveq2d	$⊢ ((J \in TopOn (X) \land L \in Fil (Y) \land F : Y ⟶ X) \land g = F) \to X FilMap g = X FilMap F$
31	30	fveq1d	$⊢ ((J \in TopOn (X) \land L \in Fil (Y) \land F : Y ⟶ X) \land g = F) \to (X FilMap g) (L) = (X FilMap F) (L)$
32	31	oveq2d	$⊢ ((J \in TopOn (X) \land L \in Fil (Y) \land F : Y ⟶ X) \land g = F) \to J fClus (X FilMap g) (L) = J fClus (X FilMap F) (L)$
33		toponmax	$⊢ J \in TopOn (X) \to X \in J$
34		filtop	$⊢ L \in Fil (Y) \to Y \in L$
35		elmapg	$⊢ (X \in J \land Y \in L) \to (F \in (X^{Y}) \leftrightarrow F : Y ⟶ X)$
36	33 34 35	syl2an	$⊢ (J \in TopOn (X) \land L \in Fil (Y)) \to (F \in (X^{Y}) \leftrightarrow F : Y ⟶ X)$
37	36	biimp3ar	$⊢ (J \in TopOn (X) \land L \in Fil (Y) \land F : Y ⟶ X) \to F \in (X^{Y})$
38		ovexd	$⊢ (J \in TopOn (X) \land L \in Fil (Y) \land F : Y ⟶ X) \to J fClus (X FilMap F) (L) \in V$
39	28 32 37 38	fvmptd	$⊢ (J \in TopOn (X) \land L \in Fil (Y) \land F : Y ⟶ X) \to (J fClusf L) (F) = J fClus (X FilMap F) (L)$

Metamath Proof Explorer

Theorem fcfval

Proof