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 ‘ 𝑤 ) 𝑦 ) ) } )