Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-flim Structured version   Unicode version

Definition df-flim 17973
 Description: Define a function (indexed by a topology ) whose value is the limits of a filter . (Contributed by Jeff Hankins, 4-Sep-2009.)
Assertion
Ref Expression
df-flim
Distinct variable group:   ,,

Detailed syntax breakdown of Definition df-flim
StepHypRef Expression
1 cflim 17968 . 2
2 vj . . 3
3 vf . . 3
4 ctop 16960 . . 3
5 cfil 17879 . . . . 5
65crn 4881 . . . 4
76cuni 4017 . . 3
8 vx . . . . . . . . 9
98cv 1652 . . . . . . . 8
109csn 3816 . . . . . . 7
112cv 1652 . . . . . . . 8
12 cnei 17163 . . . . . . . 8
1311, 12cfv 5456 . . . . . . 7
1410, 13cfv 5456 . . . . . 6
153cv 1652 . . . . . 6
1614, 15wss 3322 . . . . 5
1711cuni 4017 . . . . . . 7
1817cpw 3801 . . . . . 6
1915, 18wss 3322 . . . . 5
2016, 19wa 360 . . . 4
2120, 8, 17crab 2711 . . 3
222, 3, 4, 7, 21cmpt2 6085 . 2
231, 22wceq 1653 1
 Colors of variables: wff set class This definition is referenced by:  flimval  17997  elflim2  17998
 Copyright terms: Public domain W3C validator