Description: The convergence relation is function-like in a Hausdorff space. (Contributed by Mario Carneiro, 26-Dec-2013)
Ref | Expression | ||
---|---|---|---|
Assertion | lmfun | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | lmrel | |
|
2 | 1 | a1i | |
3 | simpl | |
|
4 | simprl | |
|
5 | simprr | |
|
6 | 3 4 5 | lmmo | |
7 | 6 | ex | |
8 | 7 | alrimiv | |
9 | 8 | alrimiv | |
10 | 9 | alrimiv | |
11 | dffun2 | |
|
12 | 2 10 11 | sylanbrc | |