# 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}={\mathrm{Base}}_{{W}}$
Assertion inftmrel ${⊢}{W}\in {V}\to ⋘\left({W}\right)\subseteq {B}×{B}$

### Proof

Step Hyp Ref Expression
1 inftm.b ${⊢}{B}={\mathrm{Base}}_{{W}}$
2 elex ${⊢}{W}\in {V}\to {W}\in \mathrm{V}$
3 fveq2 ${⊢}{w}={W}\to {\mathrm{Base}}_{{w}}={\mathrm{Base}}_{{W}}$
4 3 1 syl6eqr ${⊢}{w}={W}\to {\mathrm{Base}}_{{w}}={B}$
5 4 eleq2d ${⊢}{w}={W}\to \left({x}\in {\mathrm{Base}}_{{w}}↔{x}\in {B}\right)$
6 4 eleq2d ${⊢}{w}={W}\to \left({y}\in {\mathrm{Base}}_{{w}}↔{y}\in {B}\right)$
7 5 6 anbi12d ${⊢}{w}={W}\to \left(\left({x}\in {\mathrm{Base}}_{{w}}\wedge {y}\in {\mathrm{Base}}_{{w}}\right)↔\left({x}\in {B}\wedge {y}\in {B}\right)\right)$
8 fveq2 ${⊢}{w}={W}\to {0}_{{w}}={0}_{{W}}$
9 fveq2 ${⊢}{w}={W}\to {<}_{{w}}={<}_{{W}}$
10 eqidd ${⊢}{w}={W}\to {x}={x}$
11 8 9 10 breq123d ${⊢}{w}={W}\to \left({0}_{{w}}{<}_{{w}}{x}↔{0}_{{W}}{<}_{{W}}{x}\right)$
12 fveq2 ${⊢}{w}={W}\to {\cdot }_{{w}}={\cdot }_{{W}}$
13 12 oveqd ${⊢}{w}={W}\to {n}{\cdot }_{{w}}{x}={n}{\cdot }_{{W}}{x}$
14 eqidd ${⊢}{w}={W}\to {y}={y}$
15 13 9 14 breq123d ${⊢}{w}={W}\to \left(\left({n}{\cdot }_{{w}}{x}\right){<}_{{w}}{y}↔\left({n}{\cdot }_{{W}}{x}\right){<}_{{W}}{y}\right)$
16 15 ralbidv ${⊢}{w}={W}\to \left(\forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left({n}{\cdot }_{{w}}{x}\right){<}_{{w}}{y}↔\forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left({n}{\cdot }_{{W}}{x}\right){<}_{{W}}{y}\right)$
17 11 16 anbi12d ${⊢}{w}={W}\to \left(\left({0}_{{w}}{<}_{{w}}{x}\wedge \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left({n}{\cdot }_{{w}}{x}\right){<}_{{w}}{y}\right)↔\left({0}_{{W}}{<}_{{W}}{x}\wedge \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left({n}{\cdot }_{{W}}{x}\right){<}_{{W}}{y}\right)\right)$
18 7 17 anbi12d ${⊢}{w}={W}\to \left(\left(\left({x}\in {\mathrm{Base}}_{{w}}\wedge {y}\in {\mathrm{Base}}_{{w}}\right)\wedge \left({0}_{{w}}{<}_{{w}}{x}\wedge \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left({n}{\cdot }_{{w}}{x}\right){<}_{{w}}{y}\right)\right)↔\left(\left({x}\in {B}\wedge {y}\in {B}\right)\wedge \left({0}_{{W}}{<}_{{W}}{x}\wedge \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left({n}{\cdot }_{{W}}{x}\right){<}_{{W}}{y}\right)\right)\right)$
19 18 opabbidv ${⊢}{w}={W}\to \left\{⟨{x},{y}⟩|\left(\left({x}\in {\mathrm{Base}}_{{w}}\wedge {y}\in {\mathrm{Base}}_{{w}}\right)\wedge \left({0}_{{w}}{<}_{{w}}{x}\wedge \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left({n}{\cdot }_{{w}}{x}\right){<}_{{w}}{y}\right)\right)\right\}=\left\{⟨{x},{y}⟩|\left(\left({x}\in {B}\wedge {y}\in {B}\right)\wedge \left({0}_{{W}}{<}_{{W}}{x}\wedge \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left({n}{\cdot }_{{W}}{x}\right){<}_{{W}}{y}\right)\right)\right\}$
20 df-inftm ${⊢}⋘=\left({w}\in \mathrm{V}⟼\left\{⟨{x},{y}⟩|\left(\left({x}\in {\mathrm{Base}}_{{w}}\wedge {y}\in {\mathrm{Base}}_{{w}}\right)\wedge \left({0}_{{w}}{<}_{{w}}{x}\wedge \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left({n}{\cdot }_{{w}}{x}\right){<}_{{w}}{y}\right)\right)\right\}\right)$
21 1 fvexi ${⊢}{B}\in \mathrm{V}$
22 21 21 xpex ${⊢}{B}×{B}\in \mathrm{V}$
23 opabssxp ${⊢}\left\{⟨{x},{y}⟩|\left(\left({x}\in {B}\wedge {y}\in {B}\right)\wedge \left({0}_{{W}}{<}_{{W}}{x}\wedge \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left({n}{\cdot }_{{W}}{x}\right){<}_{{W}}{y}\right)\right)\right\}\subseteq {B}×{B}$
24 22 23 ssexi ${⊢}\left\{⟨{x},{y}⟩|\left(\left({x}\in {B}\wedge {y}\in {B}\right)\wedge \left({0}_{{W}}{<}_{{W}}{x}\wedge \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left({n}{\cdot }_{{W}}{x}\right){<}_{{W}}{y}\right)\right)\right\}\in \mathrm{V}$
25 19 20 24 fvmpt ${⊢}{W}\in \mathrm{V}\to ⋘\left({W}\right)=\left\{⟨{x},{y}⟩|\left(\left({x}\in {B}\wedge {y}\in {B}\right)\wedge \left({0}_{{W}}{<}_{{W}}{x}\wedge \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left({n}{\cdot }_{{W}}{x}\right){<}_{{W}}{y}\right)\right)\right\}$
26 2 25 syl ${⊢}{W}\in {V}\to ⋘\left({W}\right)=\left\{⟨{x},{y}⟩|\left(\left({x}\in {B}\wedge {y}\in {B}\right)\wedge \left({0}_{{W}}{<}_{{W}}{x}\wedge \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left({n}{\cdot }_{{W}}{x}\right){<}_{{W}}{y}\right)\right)\right\}$
27 26 23 eqsstrdi ${⊢}{W}\in {V}\to ⋘\left({W}\right)\subseteq {B}×{B}$