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