# Metamath Proof Explorer

## Theorem isinftm

Description: Express x is infinitesimal with respect to y for a structure W . (Contributed by Thierry Arnoux, 30-Jan-2018)

Ref Expression
Hypotheses inftm.b ${⊢}{B}={\mathrm{Base}}_{{W}}$
inftm.0
inftm.x
inftm.l
Assertion isinftm

### Proof

Step Hyp Ref Expression
1 inftm.b ${⊢}{B}={\mathrm{Base}}_{{W}}$
2 inftm.0
3 inftm.x
4 inftm.l
5 eleq1 ${⊢}{x}={X}\to \left({x}\in {B}↔{X}\in {B}\right)$
6 eleq1 ${⊢}{y}={Y}\to \left({y}\in {B}↔{Y}\in {B}\right)$
7 5 6 bi2anan9 ${⊢}\left({x}={X}\wedge {y}={Y}\right)\to \left(\left({x}\in {B}\wedge {y}\in {B}\right)↔\left({X}\in {B}\wedge {Y}\in {B}\right)\right)$
8 simpl ${⊢}\left({x}={X}\wedge {y}={Y}\right)\to {x}={X}$
9 8 breq2d
10 8 oveq2d
11 simpr ${⊢}\left({x}={X}\wedge {y}={Y}\right)\to {y}={Y}$
12 10 11 breq12d
13 12 ralbidv
14 9 13 anbi12d
15 7 14 anbi12d
16 eqid
17 15 16 brabga
19 elex ${⊢}{W}\in {V}\to {W}\in \mathrm{V}$
20 19 3ad2ant1 ${⊢}\left({W}\in {V}\wedge {X}\in {B}\wedge {Y}\in {B}\right)\to {W}\in \mathrm{V}$
21 fveq2 ${⊢}{w}={W}\to {\mathrm{Base}}_{{w}}={\mathrm{Base}}_{{W}}$
22 21 1 syl6eqr ${⊢}{w}={W}\to {\mathrm{Base}}_{{w}}={B}$
23 22 eleq2d ${⊢}{w}={W}\to \left({x}\in {\mathrm{Base}}_{{w}}↔{x}\in {B}\right)$
24 22 eleq2d ${⊢}{w}={W}\to \left({y}\in {\mathrm{Base}}_{{w}}↔{y}\in {B}\right)$
25 23 24 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)$
26 fveq2 ${⊢}{w}={W}\to {0}_{{w}}={0}_{{W}}$
27 26 2 syl6eqr
28 fveq2 ${⊢}{w}={W}\to {<}_{{w}}={<}_{{W}}$
29 28 4 syl6eqr
30 eqidd ${⊢}{w}={W}\to {x}={x}$
31 27 29 30 breq123d
32 fveq2 ${⊢}{w}={W}\to {\cdot }_{{w}}={\cdot }_{{W}}$
33 32 3 syl6eqr
34 33 oveqd
35 eqidd ${⊢}{w}={W}\to {y}={y}$
36 34 29 35 breq123d
37 36 ralbidv
38 31 37 anbi12d
39 25 38 anbi12d
40 39 opabbidv
41 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)$
42 1 fvexi ${⊢}{B}\in \mathrm{V}$
43 42 42 xpex ${⊢}{B}×{B}\in \mathrm{V}$
44 opabssxp
45 43 44 ssexi
46 40 41 45 fvmpt
47 20 46 syl
48 47 breqd
49 3simpc ${⊢}\left({W}\in {V}\wedge {X}\in {B}\wedge {Y}\in {B}\right)\to \left({X}\in {B}\wedge {Y}\in {B}\right)$
50 49 biantrurd
51 18 48 50 3bitr4d