Metamath Proof Explorer


Theorem lmbr3v

Description: Express the binary relation "sequence F converges to point P " in a metric space using an arbitrary upper set of integers. (Contributed by Glauco Siliprandi, 5-Feb-2022)

Ref Expression
Hypothesis lmbr3v.1 φ J TopOn X
Assertion lmbr3v φ F t J P F X 𝑝𝑚 P X u J P u j k j k dom F F k u

Proof

Step Hyp Ref Expression
1 lmbr3v.1 φ J TopOn X
2 eqid 0 = 0
3 0zd φ 0
4 1 2 3 lmbr2 φ F t J P F X 𝑝𝑚 P X u J P u j 0 k j k dom F F k u
5 0z 0
6 2 rexuz3 0 j 0 k j k dom F F k u j k j k dom F F k u
7 5 6 ax-mp j 0 k j k dom F F k u j k j k dom F F k u
8 7 imbi2i P u j 0 k j k dom F F k u P u j k j k dom F F k u
9 8 ralbii u J P u j 0 k j k dom F F k u u J P u j k j k dom F F k u
10 9 3anbi3i F X 𝑝𝑚 P X u J P u j 0 k j k dom F F k u F X 𝑝𝑚 P X u J P u j k j k dom F F k u
11 4 10 bitrdi φ F t J P F X 𝑝𝑚 P X u J P u j k j k dom F F k u