This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-inftm

Description: Define the relation " x is infinitesimal with respect to y " for a structure w . (Contributed by Thierry Arnoux, 30-Jan-2018)

Ref Expression
Assertion df-inftm ⋘ = ( 𝑤 ∈ V ↦ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( Base ‘ 𝑤 ) ∧ 𝑦 ∈ ( Base ‘ 𝑤 ) ) ∧ ( ( 0g ‘ 𝑤 ) ( lt ‘ 𝑤 ) 𝑥 ∧ ∀ 𝑛 ∈ ℕ ( 𝑛 ( .g ‘ 𝑤 ) 𝑥 ) ( lt ‘ 𝑤 ) 𝑦 ) ) } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cinftm ⊢ ⋘
1 vw ⊢ 𝑤
2 cvv ⊢ V
3 vx ⊢ 𝑥
4 vy ⊢ 𝑦
5 3 cv ⊢ 𝑥
6 cbs ⊢ Base
7 1 cv ⊢ 𝑤
8 7 6 cfv ⊢ ( Base ‘ 𝑤 )
9 5 8 wcel ⊢ 𝑥 ∈ ( Base ‘ 𝑤 )
10 4 cv ⊢ 𝑦
11 10 8 wcel ⊢ 𝑦 ∈ ( Base ‘ 𝑤 )
12 9 11 wa ⊢ ( 𝑥 ∈ ( Base ‘ 𝑤 ) ∧ 𝑦 ∈ ( Base ‘ 𝑤 ) )
13 c0g ⊢ 0g
14 7 13 cfv ⊢ ( 0g ‘ 𝑤 )
15 cplt ⊢ lt
16 7 15 cfv ⊢ ( lt ‘ 𝑤 )
17 14 5 16 wbr ⊢ ( 0g ‘ 𝑤 ) ( lt ‘ 𝑤 ) 𝑥
18 vn ⊢ 𝑛
19 cn ⊢ ℕ
20 18 cv ⊢ 𝑛
21 cmg ⊢ .g
22 7 21 cfv ⊢ ( .g ‘ 𝑤 )
23 20 5 22 co ⊢ ( 𝑛 ( .g ‘ 𝑤 ) 𝑥 )
24 23 10 16 wbr ⊢ ( 𝑛 ( .g ‘ 𝑤 ) 𝑥 ) ( lt ‘ 𝑤 ) 𝑦
25 24 18 19 wral ⊢ ∀ 𝑛 ∈ ℕ ( 𝑛 ( .g ‘ 𝑤 ) 𝑥 ) ( lt ‘ 𝑤 ) 𝑦
26 17 25 wa ⊢ ( ( 0g ‘ 𝑤 ) ( lt ‘ 𝑤 ) 𝑥 ∧ ∀ 𝑛 ∈ ℕ ( 𝑛 ( .g ‘ 𝑤 ) 𝑥 ) ( lt ‘ 𝑤 ) 𝑦 )
27 12 26 wa ⊢ ( ( 𝑥 ∈ ( Base ‘ 𝑤 ) ∧ 𝑦 ∈ ( Base ‘ 𝑤 ) ) ∧ ( ( 0g ‘ 𝑤 ) ( lt ‘ 𝑤 ) 𝑥 ∧ ∀ 𝑛 ∈ ℕ ( 𝑛 ( .g ‘ 𝑤 ) 𝑥 ) ( lt ‘ 𝑤 ) 𝑦 ) )
28 27 3 4 copab ⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( Base ‘ 𝑤 ) ∧ 𝑦 ∈ ( Base ‘ 𝑤 ) ) ∧ ( ( 0g ‘ 𝑤 ) ( lt ‘ 𝑤 ) 𝑥 ∧ ∀ 𝑛 ∈ ℕ ( 𝑛 ( .g ‘ 𝑤 ) 𝑥 ) ( lt ‘ 𝑤 ) 𝑦 ) ) }
29 1 2 28 cmpt ⊢ ( 𝑤 ∈ V ↦ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( Base ‘ 𝑤 ) ∧ 𝑦 ∈ ( Base ‘ 𝑤 ) ) ∧ ( ( 0g ‘ 𝑤 ) ( lt ‘ 𝑤 ) 𝑥 ∧ ∀ 𝑛 ∈ ℕ ( 𝑛 ( .g ‘ 𝑤 ) 𝑥 ) ( lt ‘ 𝑤 ) 𝑦 ) ) } )
30 0 29 wceq ⊢ ⋘ = ( 𝑤 ∈ V ↦ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( Base ‘ 𝑤 ) ∧ 𝑦 ∈ ( Base ‘ 𝑤 ) ) ∧ ( ( 0g ‘ 𝑤 ) ( lt ‘ 𝑤 ) 𝑥 ∧ ∀ 𝑛 ∈ ℕ ( 𝑛 ( .g ‘ 𝑤 ) 𝑥 ) ( lt ‘ 𝑤 ) 𝑦 ) ) } )