Metamath Proof Explorer


Theorem lmbr

Description: Express the binary relation "sequence F converges to point P " in a topological space. Definition 1.4-1 of Kreyszig p. 25. The condition F C_ ( CC X. X ) allows us to use objects more general than sequences when convenient; see the comment in df-lm . (Contributed by Mario Carneiro, 14-Nov-2013)

Ref Expression
Hypothesis lmbr.2 φ J TopOn X
Assertion lmbr φ F t J P F X 𝑝𝑚 P X u J P u y ran F y : y u

Proof

Step Hyp Ref Expression
1 lmbr.2 φ J TopOn X
2 lmfval J TopOn X t J = f x | f X 𝑝𝑚 x X u J x u y ran f y : y u
3 1 2 syl φ t J = f x | f X 𝑝𝑚 x X u J x u y ran f y : y u
4 3 breqd φ F t J P F f x | f X 𝑝𝑚 x X u J x u y ran f y : y u P
5 reseq1 f = F f y = F y
6 5 feq1d f = F f y : y u F y : y u
7 6 rexbidv f = F y ran f y : y u y ran F y : y u
8 7 imbi2d f = F x u y ran f y : y u x u y ran F y : y u
9 8 ralbidv f = F u J x u y ran f y : y u u J x u y ran F y : y u
10 eleq1 x = P x u P u
11 10 imbi1d x = P x u y ran F y : y u P u y ran F y : y u
12 11 ralbidv x = P u J x u y ran F y : y u u J P u y ran F y : y u
13 9 12 sylan9bb f = F x = P u J x u y ran f y : y u u J P u y ran F y : y u
14 df-3an f X 𝑝𝑚 x X u J x u y ran f y : y u f X 𝑝𝑚 x X u J x u y ran f y : y u
15 14 opabbii f x | f X 𝑝𝑚 x X u J x u y ran f y : y u = f x | f X 𝑝𝑚 x X u J x u y ran f y : y u
16 13 15 brab2a F f x | f X 𝑝𝑚 x X u J x u y ran f y : y u P F X 𝑝𝑚 P X u J P u y ran F y : y u
17 df-3an F X 𝑝𝑚 P X u J P u y ran F y : y u F X 𝑝𝑚 P X u J P u y ran F y : y u
18 16 17 bitr4i F f x | f X 𝑝𝑚 x X u J x u y ran f y : y u P F X 𝑝𝑚 P X u J P u y ran F y : y u
19 4 18 bitrdi φ F t J P F X 𝑝𝑚 P X u J P u y ran F y : y u