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

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 ⊢ 𝐵 = ( Base ‘ 𝑊 )
Assertion inftmrel ( 𝑊 ∈ 𝑉 → ( ⋘ ‘ 𝑊 ) ⊆ ( 𝐵 × 𝐵 ) )

Proof

Step Hyp Ref Expression
1 inftm.b ⊢ 𝐵 = ( Base ‘ 𝑊 )
2 elex ⊢ ( 𝑊 ∈ 𝑉 → 𝑊 ∈ V )
3 fveq2 ⊢ ( 𝑤 = 𝑊 → ( Base ‘ 𝑤 ) = ( Base ‘ 𝑊 ) )
4 3 1 eqtr4di ⊢ ( 𝑤 = 𝑊 → ( Base ‘ 𝑤 ) = 𝐵 )
5 4 eleq2d ⊢ ( 𝑤 = 𝑊 → ( 𝑥 ∈ ( Base ‘ 𝑤 ) ↔ 𝑥 ∈ 𝐵 ) )
6 4 eleq2d ⊢ ( 𝑤 = 𝑊 → ( 𝑦 ∈ ( Base ‘ 𝑤 ) ↔ 𝑦 ∈ 𝐵 ) )
7 5 6 anbi12d ⊢ ( 𝑤 = 𝑊 → ( ( 𝑥 ∈ ( Base ‘ 𝑤 ) ∧ 𝑦 ∈ ( Base ‘ 𝑤 ) ) ↔ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) )
8 fveq2 ⊢ ( 𝑤 = 𝑊 → ( 0g ‘ 𝑤 ) = ( 0g ‘ 𝑊 ) )
9 fveq2 ⊢ ( 𝑤 = 𝑊 → ( lt ‘ 𝑤 ) = ( lt ‘ 𝑊 ) )
10 eqidd ⊢ ( 𝑤 = 𝑊 → 𝑥 = 𝑥 )
11 8 9 10 breq123d ⊢ ( 𝑤 = 𝑊 → ( ( 0g ‘ 𝑤 ) ( lt ‘ 𝑤 ) 𝑥 ↔ ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 ) )
12 fveq2 ⊢ ( 𝑤 = 𝑊 → ( .g ‘ 𝑤 ) = ( .g ‘ 𝑊 ) )
13 12 oveqd ⊢ ( 𝑤 = 𝑊 → ( 𝑛 ( .g ‘ 𝑤 ) 𝑥 ) = ( 𝑛 ( .g ‘ 𝑊 ) 𝑥 ) )
14 eqidd ⊢ ( 𝑤 = 𝑊 → 𝑦 = 𝑦 )
15 13 9 14 breq123d ⊢ ( 𝑤 = 𝑊 → ( ( 𝑛 ( .g ‘ 𝑤 ) 𝑥 ) ( lt ‘ 𝑤 ) 𝑦 ↔ ( 𝑛 ( .g ‘ 𝑊 ) 𝑥 ) ( lt ‘ 𝑊 ) 𝑦 ) )
16 15 ralbidv ⊢ ( 𝑤 = 𝑊 → ( ∀ 𝑛 ∈ ℕ ( 𝑛 ( .g ‘ 𝑤 ) 𝑥 ) ( lt ‘ 𝑤 ) 𝑦 ↔ ∀ 𝑛 ∈ ℕ ( 𝑛 ( .g ‘ 𝑊 ) 𝑥 ) ( lt ‘ 𝑊 ) 𝑦 ) )
17 11 16 anbi12d ⊢ ( 𝑤 = 𝑊 → ( ( ( 0g ‘ 𝑤 ) ( lt ‘ 𝑤 ) 𝑥 ∧ ∀ 𝑛 ∈ ℕ ( 𝑛 ( .g ‘ 𝑤 ) 𝑥 ) ( lt ‘ 𝑤 ) 𝑦 ) ↔ ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 ∧ ∀ 𝑛 ∈ ℕ ( 𝑛 ( .g ‘ 𝑊 ) 𝑥 ) ( lt ‘ 𝑊 ) 𝑦 ) ) )
18 7 17 anbi12d ⊢ ( 𝑤 = 𝑊 → ( ( ( 𝑥 ∈ ( Base ‘ 𝑤 ) ∧ 𝑦 ∈ ( Base ‘ 𝑤 ) ) ∧ ( ( 0g ‘ 𝑤 ) ( lt ‘ 𝑤 ) 𝑥 ∧ ∀ 𝑛 ∈ ℕ ( 𝑛 ( .g ‘ 𝑤 ) 𝑥 ) ( lt ‘ 𝑤 ) 𝑦 ) ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 ∧ ∀ 𝑛 ∈ ℕ ( 𝑛 ( .g ‘ 𝑊 ) 𝑥 ) ( lt ‘ 𝑊 ) 𝑦 ) ) ) )
19 18 opabbidv ⊢ ( 𝑤 = 𝑊 → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( Base ‘ 𝑤 ) ∧ 𝑦 ∈ ( Base ‘ 𝑤 ) ) ∧ ( ( 0g ‘ 𝑤 ) ( lt ‘ 𝑤 ) 𝑥 ∧ ∀ 𝑛 ∈ ℕ ( 𝑛 ( .g ‘ 𝑤 ) 𝑥 ) ( lt ‘ 𝑤 ) 𝑦 ) ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 ∧ ∀ 𝑛 ∈ ℕ ( 𝑛 ( .g ‘ 𝑊 ) 𝑥 ) ( lt ‘ 𝑊 ) 𝑦 ) ) } )
20 df-inftm ⊢ ⋘ = ( 𝑤 ∈ V ↦ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( Base ‘ 𝑤 ) ∧ 𝑦 ∈ ( Base ‘ 𝑤 ) ) ∧ ( ( 0g ‘ 𝑤 ) ( lt ‘ 𝑤 ) 𝑥 ∧ ∀ 𝑛 ∈ ℕ ( 𝑛 ( .g ‘ 𝑤 ) 𝑥 ) ( lt ‘ 𝑤 ) 𝑦 ) ) } )
21 1 fvexi ⊢ 𝐵 ∈ V
22 21 21 xpex ⊢ ( 𝐵 × 𝐵 ) ∈ V
23 opabssxp ⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 ∧ ∀ 𝑛 ∈ ℕ ( 𝑛 ( .g ‘ 𝑊 ) 𝑥 ) ( lt ‘ 𝑊 ) 𝑦 ) ) } ⊆ ( 𝐵 × 𝐵 )
24 22 23 ssexi ⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 ∧ ∀ 𝑛 ∈ ℕ ( 𝑛 ( .g ‘ 𝑊 ) 𝑥 ) ( lt ‘ 𝑊 ) 𝑦 ) ) } ∈ V
25 19 20 24 fvmpt ⊢ ( 𝑊 ∈ V → ( ⋘ ‘ 𝑊 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 ∧ ∀ 𝑛 ∈ ℕ ( 𝑛 ( .g ‘ 𝑊 ) 𝑥 ) ( lt ‘ 𝑊 ) 𝑦 ) ) } )
26 2 25 syl ⊢ ( 𝑊 ∈ 𝑉 → ( ⋘ ‘ 𝑊 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ( ( 0g ‘ 𝑊 ) ( lt ‘ 𝑊 ) 𝑥 ∧ ∀ 𝑛 ∈ ℕ ( 𝑛 ( .g ‘ 𝑊 ) 𝑥 ) ( lt ‘ 𝑊 ) 𝑦 ) ) } )
27 26 23 eqsstrdi ⊢ ( 𝑊 ∈ 𝑉 → ( ⋘ ‘ 𝑊 ) ⊆ ( 𝐵 × 𝐵 ) )