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

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 ⊢ 𝐵 = ( Base ‘ 𝑊 )
inftm.0 ⊢ 0 = ( 0g ‘ 𝑊 )
inftm.x ⊢ · = ( .g ‘ 𝑊 )
inftm.l ⊢ < = ( lt ‘ 𝑊 )
Assertion isinftm ( ( 𝑊 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ( ⋘ ‘ 𝑊 ) 𝑌 ↔ ( 0 < 𝑋 ∧ ∀ 𝑛 ∈ ℕ ( 𝑛 · 𝑋 ) < 𝑌 ) ) )

Proof

Step Hyp Ref Expression
1 inftm.b ⊢ 𝐵 = ( Base ‘ 𝑊 )
2 inftm.0 ⊢ 0 = ( 0g ‘ 𝑊 )
3 inftm.x ⊢ · = ( .g ‘ 𝑊 )
4 inftm.l ⊢ < = ( lt ‘ 𝑊 )
5 eleq1 ⊢ ( 𝑥 = 𝑋 → ( 𝑥 ∈ 𝐵 ↔ 𝑋 ∈ 𝐵 ) )
6 eleq1 ⊢ ( 𝑦 = 𝑌 → ( 𝑦 ∈ 𝐵 ↔ 𝑌 ∈ 𝐵 ) )
7 5 6 bi2anan9 ⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) → ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ↔ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) )
8 simpl ⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) → 𝑥 = 𝑋 )
9 8 breq2d ⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) → ( 0 < 𝑥 ↔ 0 < 𝑋 ) )
10 8 oveq2d ⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) → ( 𝑛 · 𝑥 ) = ( 𝑛 · 𝑋 ) )
11 simpr ⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) → 𝑦 = 𝑌 )
12 10 11 breq12d ⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) → ( ( 𝑛 · 𝑥 ) < 𝑦 ↔ ( 𝑛 · 𝑋 ) < 𝑌 ) )
13 12 ralbidv ⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) → ( ∀ 𝑛 ∈ ℕ ( 𝑛 · 𝑥 ) < 𝑦 ↔ ∀ 𝑛 ∈ ℕ ( 𝑛 · 𝑋 ) < 𝑌 ) )
14 9 13 anbi12d ⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) → ( ( 0 < 𝑥 ∧ ∀ 𝑛 ∈ ℕ ( 𝑛 · 𝑥 ) < 𝑦 ) ↔ ( 0 < 𝑋 ∧ ∀ 𝑛 ∈ ℕ ( 𝑛 · 𝑋 ) < 𝑌 ) ) )
15 7 14 anbi12d ⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) → ( ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 0 < 𝑥 ∧ ∀ 𝑛 ∈ ℕ ( 𝑛 · 𝑥 ) < 𝑦 ) ) ↔ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 0 < 𝑋 ∧ ∀ 𝑛 ∈ ℕ ( 𝑛 · 𝑋 ) < 𝑌 ) ) ) )
16 eqid ⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 0 < 𝑥 ∧ ∀ 𝑛 ∈ ℕ ( 𝑛 · 𝑥 ) < 𝑦 ) ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 0 < 𝑥 ∧ ∀ 𝑛 ∈ ℕ ( 𝑛 · 𝑥 ) < 𝑦 ) ) }
17 15 16 brabga ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 0 < 𝑥 ∧ ∀ 𝑛 ∈ ℕ ( 𝑛 · 𝑥 ) < 𝑦 ) ) } 𝑌 ↔ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 0 < 𝑋 ∧ ∀ 𝑛 ∈ ℕ ( 𝑛 · 𝑋 ) < 𝑌 ) ) ) )
18 17 3adant1 ⊢ ( ( 𝑊 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 0 < 𝑥 ∧ ∀ 𝑛 ∈ ℕ ( 𝑛 · 𝑥 ) < 𝑦 ) ) } 𝑌 ↔ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 0 < 𝑋 ∧ ∀ 𝑛 ∈ ℕ ( 𝑛 · 𝑋 ) < 𝑌 ) ) ) )
19 elex ⊢ ( 𝑊 ∈ 𝑉 → 𝑊 ∈ V )
20 19 3ad2ant1 ⊢ ( ( 𝑊 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝑊 ∈ V )
21 fveq2 ⊢ ( 𝑤 = 𝑊 → ( Base ‘ 𝑤 ) = ( Base ‘ 𝑊 ) )
22 21 1 eqtr4di ⊢ ( 𝑤 = 𝑊 → ( Base ‘ 𝑤 ) = 𝐵 )
23 22 eleq2d ⊢ ( 𝑤 = 𝑊 → ( 𝑥 ∈ ( Base ‘ 𝑤 ) ↔ 𝑥 ∈ 𝐵 ) )
24 22 eleq2d ⊢ ( 𝑤 = 𝑊 → ( 𝑦 ∈ ( Base ‘ 𝑤 ) ↔ 𝑦 ∈ 𝐵 ) )
25 23 24 anbi12d ⊢ ( 𝑤 = 𝑊 → ( ( 𝑥 ∈ ( Base ‘ 𝑤 ) ∧ 𝑦 ∈ ( Base ‘ 𝑤 ) ) ↔ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) )
26 fveq2 ⊢ ( 𝑤 = 𝑊 → ( 0g ‘ 𝑤 ) = ( 0g ‘ 𝑊 ) )
27 26 2 eqtr4di ⊢ ( 𝑤 = 𝑊 → ( 0g ‘ 𝑤 ) = 0 )
28 fveq2 ⊢ ( 𝑤 = 𝑊 → ( lt ‘ 𝑤 ) = ( lt ‘ 𝑊 ) )
29 28 4 eqtr4di ⊢ ( 𝑤 = 𝑊 → ( lt ‘ 𝑤 ) = < )
30 eqidd ⊢ ( 𝑤 = 𝑊 → 𝑥 = 𝑥 )
31 27 29 30 breq123d ⊢ ( 𝑤 = 𝑊 → ( ( 0g ‘ 𝑤 ) ( lt ‘ 𝑤 ) 𝑥 ↔ 0 < 𝑥 ) )
32 fveq2 ⊢ ( 𝑤 = 𝑊 → ( .g ‘ 𝑤 ) = ( .g ‘ 𝑊 ) )
33 32 3 eqtr4di ⊢ ( 𝑤 = 𝑊 → ( .g ‘ 𝑤 ) = · )
34 33 oveqd ⊢ ( 𝑤 = 𝑊 → ( 𝑛 ( .g ‘ 𝑤 ) 𝑥 ) = ( 𝑛 · 𝑥 ) )
35 eqidd ⊢ ( 𝑤 = 𝑊 → 𝑦 = 𝑦 )
36 34 29 35 breq123d ⊢ ( 𝑤 = 𝑊 → ( ( 𝑛 ( .g ‘ 𝑤 ) 𝑥 ) ( lt ‘ 𝑤 ) 𝑦 ↔ ( 𝑛 · 𝑥 ) < 𝑦 ) )
37 36 ralbidv ⊢ ( 𝑤 = 𝑊 → ( ∀ 𝑛 ∈ ℕ ( 𝑛 ( .g ‘ 𝑤 ) 𝑥 ) ( lt ‘ 𝑤 ) 𝑦 ↔ ∀ 𝑛 ∈ ℕ ( 𝑛 · 𝑥 ) < 𝑦 ) )
38 31 37 anbi12d ⊢ ( 𝑤 = 𝑊 → ( ( ( 0g ‘ 𝑤 ) ( lt ‘ 𝑤 ) 𝑥 ∧ ∀ 𝑛 ∈ ℕ ( 𝑛 ( .g ‘ 𝑤 ) 𝑥 ) ( lt ‘ 𝑤 ) 𝑦 ) ↔ ( 0 < 𝑥 ∧ ∀ 𝑛 ∈ ℕ ( 𝑛 · 𝑥 ) < 𝑦 ) ) )
39 25 38 anbi12d ⊢ ( 𝑤 = 𝑊 → ( ( ( 𝑥 ∈ ( Base ‘ 𝑤 ) ∧ 𝑦 ∈ ( Base ‘ 𝑤 ) ) ∧ ( ( 0g ‘ 𝑤 ) ( lt ‘ 𝑤 ) 𝑥 ∧ ∀ 𝑛 ∈ ℕ ( 𝑛 ( .g ‘ 𝑤 ) 𝑥 ) ( lt ‘ 𝑤 ) 𝑦 ) ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 0 < 𝑥 ∧ ∀ 𝑛 ∈ ℕ ( 𝑛 · 𝑥 ) < 𝑦 ) ) ) )
40 39 opabbidv ⊢ ( 𝑤 = 𝑊 → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( Base ‘ 𝑤 ) ∧ 𝑦 ∈ ( Base ‘ 𝑤 ) ) ∧ ( ( 0g ‘ 𝑤 ) ( lt ‘ 𝑤 ) 𝑥 ∧ ∀ 𝑛 ∈ ℕ ( 𝑛 ( .g ‘ 𝑤 ) 𝑥 ) ( lt ‘ 𝑤 ) 𝑦 ) ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 0 < 𝑥 ∧ ∀ 𝑛 ∈ ℕ ( 𝑛 · 𝑥 ) < 𝑦 ) ) } )
41 df-inftm ⊢ ⋘ = ( 𝑤 ∈ V ↦ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( Base ‘ 𝑤 ) ∧ 𝑦 ∈ ( Base ‘ 𝑤 ) ) ∧ ( ( 0g ‘ 𝑤 ) ( lt ‘ 𝑤 ) 𝑥 ∧ ∀ 𝑛 ∈ ℕ ( 𝑛 ( .g ‘ 𝑤 ) 𝑥 ) ( lt ‘ 𝑤 ) 𝑦 ) ) } )
42 1 fvexi ⊢ 𝐵 ∈ V
43 42 42 xpex ⊢ ( 𝐵 × 𝐵 ) ∈ V
44 opabssxp ⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 0 < 𝑥 ∧ ∀ 𝑛 ∈ ℕ ( 𝑛 · 𝑥 ) < 𝑦 ) ) } ⊆ ( 𝐵 × 𝐵 )
45 43 44 ssexi ⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 0 < 𝑥 ∧ ∀ 𝑛 ∈ ℕ ( 𝑛 · 𝑥 ) < 𝑦 ) ) } ∈ V
46 40 41 45 fvmpt ⊢ ( 𝑊 ∈ V → ( ⋘ ‘ 𝑊 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 0 < 𝑥 ∧ ∀ 𝑛 ∈ ℕ ( 𝑛 · 𝑥 ) < 𝑦 ) ) } )
47 20 46 syl ⊢ ( ( 𝑊 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ⋘ ‘ 𝑊 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 0 < 𝑥 ∧ ∀ 𝑛 ∈ ℕ ( 𝑛 · 𝑥 ) < 𝑦 ) ) } )
48 47 breqd ⊢ ( ( 𝑊 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ( ⋘ ‘ 𝑊 ) 𝑌 ↔ 𝑋 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 0 < 𝑥 ∧ ∀ 𝑛 ∈ ℕ ( 𝑛 · 𝑥 ) < 𝑦 ) ) } 𝑌 ) )
49 3simpc ⊢ ( ( 𝑊 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) )
50 49 biantrurd ⊢ ( ( 𝑊 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 0 < 𝑋 ∧ ∀ 𝑛 ∈ ℕ ( 𝑛 · 𝑋 ) < 𝑌 ) ↔ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 0 < 𝑋 ∧ ∀ 𝑛 ∈ ℕ ( 𝑛 · 𝑋 ) < 𝑌 ) ) ) )
51 18 48 50 3bitr4d ⊢ ( ( 𝑊 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ( ⋘ ‘ 𝑊 ) 𝑌 ↔ ( 0 < 𝑋 ∧ ∀ 𝑛 ∈ ℕ ( 𝑛 · 𝑋 ) < 𝑌 ) ) )