Metamath Proof Explorer


Theorem inftmrel

Description: The infinitesimal relation for a structure W . (Contributed by Thierry Arnoux, 30-Jan-2018)

Ref Expression
Hypothesis inftm.b B = Base W
Assertion inftmrel W V W B × B

Proof

Step Hyp Ref Expression
1 inftm.b B = Base W
2 elex W V W V
3 fveq2 w = W Base w = Base W
4 3 1 syl6eqr w = W Base w = B
5 4 eleq2d w = W x Base w x B
6 4 eleq2d w = W y Base w y B
7 5 6 anbi12d w = W x Base w y Base w x B y B
8 fveq2 w = W 0 w = 0 W
9 fveq2 w = W < w = < W
10 eqidd w = W x = x
11 8 9 10 breq123d w = W 0 w < w x 0 W < W x
12 fveq2 w = W w = W
13 12 oveqd w = W n w x = n W x
14 eqidd w = W y = y
15 13 9 14 breq123d w = W n w x < w y n W x < W y
16 15 ralbidv w = W n n w x < w y n n W x < W y
17 11 16 anbi12d w = W 0 w < w x n n w x < w y 0 W < W x n n W x < W y
18 7 17 anbi12d w = W x Base w y Base w 0 w < w x n n w x < w y x B y B 0 W < W x n n W x < W y
19 18 opabbidv w = W x y | x Base w y Base w 0 w < w x n n w x < w y = x y | x B y B 0 W < W x n n W x < W y
20 df-inftm = w V x y | x Base w y Base w 0 w < w x n n w x < w y
21 1 fvexi B V
22 21 21 xpex B × B V
23 opabssxp x y | x B y B 0 W < W x n n W x < W y B × B
24 22 23 ssexi x y | x B y B 0 W < W x n n W x < W y V
25 19 20 24 fvmpt W V W = x y | x B y B 0 W < W x n n W x < W y
26 2 25 syl W V W = x y | x B y B 0 W < W x n n W x < W y
27 26 23 eqsstrdi W V W B × B