Theorem fclsval

Description: The set of all cluster points of a filter. (Contributed by Jeff Hankins, 10-Nov-2009) (Revised by Stefan O'Rear, 8-Aug-2015)

	Ref	Expression
Hypothesis	fclsval.x	⊢ 𝑋 = ∪ 𝐽
Assertion	fclsval	⊢ ( ( 𝐽 ∈ Top ∧ 𝐹 ∈ ( Fil ‘ 𝑌 ) ) → ( 𝐽 fClus 𝐹 ) = if ( 𝑋 = 𝑌 , ∩ 𝑡 ∈ 𝐹 ( ( cls ‘ 𝐽 ) ‘ 𝑡 ) , ∅ ) )

Proof

Step	Hyp	Ref	Expression
1		fclsval.x	⊢ 𝑋 = ∪ 𝐽
2		simpl	⊢ ( ( 𝐽 ∈ Top ∧ 𝐹 ∈ ( Fil ‘ 𝑌 ) ) → 𝐽 ∈ Top )
3		fvssunirn	⊢ ( Fil ‘ 𝑌 ) ⊆ ∪ ran Fil
4	3	sseli	⊢ ( 𝐹 ∈ ( Fil ‘ 𝑌 ) → 𝐹 ∈ ∪ ran Fil )
5	4	adantl	⊢ ( ( 𝐽 ∈ Top ∧ 𝐹 ∈ ( Fil ‘ 𝑌 ) ) → 𝐹 ∈ ∪ ran Fil )
6		filn0	⊢ ( 𝐹 ∈ ( Fil ‘ 𝑌 ) → 𝐹 ≠ ∅ )
7	6	adantl	⊢ ( ( 𝐽 ∈ Top ∧ 𝐹 ∈ ( Fil ‘ 𝑌 ) ) → 𝐹 ≠ ∅ )
8		fvex	⊢ ( ( cls ‘ 𝐽 ) ‘ 𝑡 ) ∈ V
9	8	rgenw	⊢ ∀ 𝑡 ∈ 𝐹 ( ( cls ‘ 𝐽 ) ‘ 𝑡 ) ∈ V
10		iinexg	⊢ ( ( 𝐹 ≠ ∅ ∧ ∀ 𝑡 ∈ 𝐹 ( ( cls ‘ 𝐽 ) ‘ 𝑡 ) ∈ V ) → ∩ 𝑡 ∈ 𝐹 ( ( cls ‘ 𝐽 ) ‘ 𝑡 ) ∈ V )
11	7 9 10	sylancl	⊢ ( ( 𝐽 ∈ Top ∧ 𝐹 ∈ ( Fil ‘ 𝑌 ) ) → ∩ 𝑡 ∈ 𝐹 ( ( cls ‘ 𝐽 ) ‘ 𝑡 ) ∈ V )
12		0ex	⊢ ∅ ∈ V
13		ifcl	⊢ ( ( ∩ 𝑡 ∈ 𝐹 ( ( cls ‘ 𝐽 ) ‘ 𝑡 ) ∈ V ∧ ∅ ∈ V ) → if ( 𝑋 = ∪ 𝐹 , ∩ 𝑡 ∈ 𝐹 ( ( cls ‘ 𝐽 ) ‘ 𝑡 ) , ∅ ) ∈ V )
14	11 12 13	sylancl	⊢ ( ( 𝐽 ∈ Top ∧ 𝐹 ∈ ( Fil ‘ 𝑌 ) ) → if ( 𝑋 = ∪ 𝐹 , ∩ 𝑡 ∈ 𝐹 ( ( cls ‘ 𝐽 ) ‘ 𝑡 ) , ∅ ) ∈ V )
15		unieq	⊢ ( 𝑗 = 𝐽 → ∪ 𝑗 = ∪ 𝐽 )
16	15 1	eqtr4di	⊢ ( 𝑗 = 𝐽 → ∪ 𝑗 = 𝑋 )
17		unieq	⊢ ( 𝑓 = 𝐹 → ∪ 𝑓 = ∪ 𝐹 )
18	16 17	eqeqan12d	⊢ ( ( 𝑗 = 𝐽 ∧ 𝑓 = 𝐹 ) → ( ∪ 𝑗 = ∪ 𝑓 ↔ 𝑋 = ∪ 𝐹 ) )
19		iineq1	⊢ ( 𝑓 = 𝐹 → ∩ 𝑡 ∈ 𝑓 ( ( cls ‘ 𝑗 ) ‘ 𝑡 ) = ∩ 𝑡 ∈ 𝐹 ( ( cls ‘ 𝑗 ) ‘ 𝑡 ) )
20	19	adantl	⊢ ( ( 𝑗 = 𝐽 ∧ 𝑓 = 𝐹 ) → ∩ 𝑡 ∈ 𝑓 ( ( cls ‘ 𝑗 ) ‘ 𝑡 ) = ∩ 𝑡 ∈ 𝐹 ( ( cls ‘ 𝑗 ) ‘ 𝑡 ) )
21		simpll	⊢ ( ( ( 𝑗 = 𝐽 ∧ 𝑓 = 𝐹 ) ∧ 𝑡 ∈ 𝐹 ) → 𝑗 = 𝐽 )
22	21	fveq2d	⊢ ( ( ( 𝑗 = 𝐽 ∧ 𝑓 = 𝐹 ) ∧ 𝑡 ∈ 𝐹 ) → ( cls ‘ 𝑗 ) = ( cls ‘ 𝐽 ) )
23	22	fveq1d	⊢ ( ( ( 𝑗 = 𝐽 ∧ 𝑓 = 𝐹 ) ∧ 𝑡 ∈ 𝐹 ) → ( ( cls ‘ 𝑗 ) ‘ 𝑡 ) = ( ( cls ‘ 𝐽 ) ‘ 𝑡 ) )
24	23	iineq2dv	⊢ ( ( 𝑗 = 𝐽 ∧ 𝑓 = 𝐹 ) → ∩ 𝑡 ∈ 𝐹 ( ( cls ‘ 𝑗 ) ‘ 𝑡 ) = ∩ 𝑡 ∈ 𝐹 ( ( cls ‘ 𝐽 ) ‘ 𝑡 ) )
25	20 24	eqtrd	⊢ ( ( 𝑗 = 𝐽 ∧ 𝑓 = 𝐹 ) → ∩ 𝑡 ∈ 𝑓 ( ( cls ‘ 𝑗 ) ‘ 𝑡 ) = ∩ 𝑡 ∈ 𝐹 ( ( cls ‘ 𝐽 ) ‘ 𝑡 ) )
26	18 25	ifbieq1d	⊢ ( ( 𝑗 = 𝐽 ∧ 𝑓 = 𝐹 ) → if ( ∪ 𝑗 = ∪ 𝑓 , ∩ 𝑡 ∈ 𝑓 ( ( cls ‘ 𝑗 ) ‘ 𝑡 ) , ∅ ) = if ( 𝑋 = ∪ 𝐹 , ∩ 𝑡 ∈ 𝐹 ( ( cls ‘ 𝐽 ) ‘ 𝑡 ) , ∅ ) )
27		df-fcls	⊢ fClus = ( 𝑗 ∈ Top , 𝑓 ∈ ∪ ran Fil ↦ if ( ∪ 𝑗 = ∪ 𝑓 , ∩ 𝑡 ∈ 𝑓 ( ( cls ‘ 𝑗 ) ‘ 𝑡 ) , ∅ ) )
28	26 27	ovmpoga	⊢ ( ( 𝐽 ∈ Top ∧ 𝐹 ∈ ∪ ran Fil ∧ if ( 𝑋 = ∪ 𝐹 , ∩ 𝑡 ∈ 𝐹 ( ( cls ‘ 𝐽 ) ‘ 𝑡 ) , ∅ ) ∈ V ) → ( 𝐽 fClus 𝐹 ) = if ( 𝑋 = ∪ 𝐹 , ∩ 𝑡 ∈ 𝐹 ( ( cls ‘ 𝐽 ) ‘ 𝑡 ) , ∅ ) )
29	2 5 14 28	syl3anc	⊢ ( ( 𝐽 ∈ Top ∧ 𝐹 ∈ ( Fil ‘ 𝑌 ) ) → ( 𝐽 fClus 𝐹 ) = if ( 𝑋 = ∪ 𝐹 , ∩ 𝑡 ∈ 𝐹 ( ( cls ‘ 𝐽 ) ‘ 𝑡 ) , ∅ ) )
30		filunibas	⊢ ( 𝐹 ∈ ( Fil ‘ 𝑌 ) → ∪ 𝐹 = 𝑌 )
31	30	eqeq2d	⊢ ( 𝐹 ∈ ( Fil ‘ 𝑌 ) → ( 𝑋 = ∪ 𝐹 ↔ 𝑋 = 𝑌 ) )
32	31	adantl	⊢ ( ( 𝐽 ∈ Top ∧ 𝐹 ∈ ( Fil ‘ 𝑌 ) ) → ( 𝑋 = ∪ 𝐹 ↔ 𝑋 = 𝑌 ) )
33	32	ifbid	⊢ ( ( 𝐽 ∈ Top ∧ 𝐹 ∈ ( Fil ‘ 𝑌 ) ) → if ( 𝑋 = ∪ 𝐹 , ∩ 𝑡 ∈ 𝐹 ( ( cls ‘ 𝐽 ) ‘ 𝑡 ) , ∅ ) = if ( 𝑋 = 𝑌 , ∩ 𝑡 ∈ 𝐹 ( ( cls ‘ 𝐽 ) ‘ 𝑡 ) , ∅ ) )
34	29 33	eqtrd	⊢ ( ( 𝐽 ∈ Top ∧ 𝐹 ∈ ( Fil ‘ 𝑌 ) ) → ( 𝐽 fClus 𝐹 ) = if ( 𝑋 = 𝑌 , ∩ 𝑡 ∈ 𝐹 ( ( cls ‘ 𝐽 ) ‘ 𝑡 ) , ∅ ) )