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 eqtr4di ⊢ 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