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=BaseW
Assertion inftmrel ⊢W∈V→⋘⁡W⊆B×B

Proof

Step Hyp Ref Expression
1 inftm.b ⊢B=BaseW
2 elex ⊢W∈V→W∈V
3 fveq2 ⊢w=W→Basew=BaseW
4 3 1 eqtr4di ⊢w=W→Basew=B
5 4 eleq2d ⊢w=W→x∈Basew↔x∈B
6 4 eleq2d ⊢w=W→y∈Basew↔y∈B
7 5 6 anbi12d ⊢w=W→x∈Basew∧y∈Basew↔x∈B∧y∈B
8 fveq2 ⊢w=W→0w=0W
9 fveq2 ⊢w=W→<w=<W
10 eqidd ⊢w=W→x=x
11 8 9 10 breq123d ⊢w=W→0w<wx↔0W<Wx
12 fveq2 ⊢w=W→⋅w=⋅W
13 12 oveqd ⊢w=W→n⋅wx=n⋅Wx
14 eqidd ⊢w=W→y=y
15 13 9 14 breq123d ⊢w=W→n⋅wx<wy↔n⋅Wx<Wy
16 15 ralbidv ⊢w=W→∀n∈ℕn⋅wx<wy↔∀n∈ℕn⋅Wx<Wy
17 11 16 anbi12d ⊢w=W→0w<wx∧∀n∈ℕn⋅wx<wy↔0W<Wx∧∀n∈ℕn⋅Wx<Wy
18 7 17 anbi12d ⊢w=W→x∈Basew∧y∈Basew∧0w<wx∧∀n∈ℕn⋅wx<wy↔x∈B∧y∈B∧0W<Wx∧∀n∈ℕn⋅Wx<Wy
19 18 opabbidv ⊢w=W→xy|x∈Basew∧y∈Basew∧0w<wx∧∀n∈ℕn⋅wx<wy=xy|x∈B∧y∈B∧0W<Wx∧∀n∈ℕn⋅Wx<Wy
20 df-inftm ⊢⋘=w∈V⟼xy|x∈Basew∧y∈Basew∧0w<wx∧∀n∈ℕn⋅wx<wy
21 1 fvexi ⊢B∈V
22 21 21 xpex ⊢B×B∈V
23 opabssxp ⊢xy|x∈B∧y∈B∧0W<Wx∧∀n∈ℕn⋅Wx<Wy⊆B×B
24 22 23 ssexi ⊢xy|x∈B∧y∈B∧0W<Wx∧∀n∈ℕn⋅Wx<Wy∈V
25 19 20 24 fvmpt ⊢W∈V→⋘⁡W=xy|x∈B∧y∈B∧0W<Wx∧∀n∈ℕn⋅Wx<Wy
26 2 25 syl ⊢W∈V→⋘⁡W=xy|x∈B∧y∈B∧0W<Wx∧∀n∈ℕn⋅Wx<Wy
27 26 23 eqsstrdi ⊢W∈V→⋘⁡W⊆B×B