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

Definition df-flim 17959
 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 17954 . 2
2 vj . . 3
3 vf . . 3
4 ctop 16946 . . 3
5 cfil 17865 . . . . 5
65crn 4870 . . . 4
76cuni 4007 . . 3
8 vx . . . . . . . . 9
98cv 1651 . . . . . . . 8
109csn 3806 . . . . . . 7
112cv 1651 . . . . . . . 8
12 cnei 17149 . . . . . . . 8
1311, 12cfv 5445 . . . . . . 7
1410, 13cfv 5445 . . . . . 6
153cv 1651 . . . . . 6
1614, 15wss 3312 . . . . 5
1711cuni 4007 . . . . . . 7
1817cpw 3791 . . . . . 6
1915, 18wss 3312 . . . . 5
2016, 19wa 359 . . . 4
2120, 8, 17crab 2701 . . 3
222, 3, 4, 7, 21cmpt2 6074 . 2
231, 22wceq 1652 1
 Colors of variables: wff set class This definition is referenced by:  flimval  17983  elflim2  17984
 Copyright terms: Public domain W3C validator