imasds

Description: The distance function of an image structure. (Contributed by Mario Carneiro, 23-Feb-2015) (Revised by Mario Carneiro, 11-Jul-2015) (Revised by Thierry Arnoux, 16-Jun-2019) (Revised by AV, 6-Oct-2020)

	Ref	Expression
Hypotheses	imasbas.u	⊢ ( 𝜑 → 𝑈 = ( 𝐹 “_s 𝑅 ) )
	imasbas.v	⊢ ( 𝜑 → 𝑉 = ( Base ‘ 𝑅 ) )
	imasbas.f	⊢ ( 𝜑 → 𝐹 : 𝑉 –onto→ 𝐵 )
	imasbas.r	⊢ ( 𝜑 → 𝑅 ∈ 𝑍 )
	imasds.e	⊢ 𝐸 = ( dist ‘ 𝑅 )
	imasds.d	⊢ 𝐷 = ( dist ‘ 𝑈 )
Assertion	imasds	⊢ ( 𝜑 → 𝐷 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ inf ( ∪ 𝑛 ∈ ℕ ran ( 𝑔 ∈ { ℎ ∈ ( ( 𝑉 × 𝑉 ) ↑_m ( 1 ... 𝑛 ) ) ∣ ( ( 𝐹 ‘ ( 1^st ‘ ( ℎ ‘ 1 ) ) ) = 𝑥 ∧ ( 𝐹 ‘ ( 2^nd ‘ ( ℎ ‘ 𝑛 ) ) ) = 𝑦 ∧ ∀ 𝑖 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 𝐹 ‘ ( 2^nd ‘ ( ℎ ‘ 𝑖 ) ) ) = ( 𝐹 ‘ ( 1^st ‘ ( ℎ ‘ ( 𝑖 + 1 ) ) ) ) ) } ↦ ( ℝ^_𝑠 Σ_g ( 𝐸 ∘ 𝑔 ) ) ) , ℝ^ , < ) ) )

Proof

Step	Hyp	Ref	Expression
1		imasbas.u	⊢ ( 𝜑 → 𝑈 = ( 𝐹 “_s 𝑅 ) )
2		imasbas.v	⊢ ( 𝜑 → 𝑉 = ( Base ‘ 𝑅 ) )
3		imasbas.f	⊢ ( 𝜑 → 𝐹 : 𝑉 –onto→ 𝐵 )
4		imasbas.r	⊢ ( 𝜑 → 𝑅 ∈ 𝑍 )
5		imasds.e	⊢ 𝐸 = ( dist ‘ 𝑅 )
6		imasds.d	⊢ 𝐷 = ( dist ‘ 𝑈 )
7		eqid	⊢ ( +_g ‘ 𝑅 ) = ( +_g ‘ 𝑅 )
8		eqid	⊢ ( ._r ‘ 𝑅 ) = ( ._r ‘ 𝑅 )
9		eqid	⊢ ( Scalar ‘ 𝑅 ) = ( Scalar ‘ 𝑅 )
10		eqid	⊢ ( Base ‘ ( Scalar ‘ 𝑅 ) ) = ( Base ‘ ( Scalar ‘ 𝑅 ) )
11		eqid	⊢ ( ·_𝑠 ‘ 𝑅 ) = ( ·_𝑠 ‘ 𝑅 )
12		eqid	⊢ ( ·_𝑖 ‘ 𝑅 ) = ( ·_𝑖 ‘ 𝑅 )
13		eqid	⊢ ( TopOpen ‘ 𝑅 ) = ( TopOpen ‘ 𝑅 )
14		eqid	⊢ ( le ‘ 𝑅 ) = ( le ‘ 𝑅 )
15		eqidd	⊢ ( 𝜑 → ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 { ⟨ ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ , ( 𝐹 ‘ ( 𝑝 ( +_g ‘ 𝑅 ) 𝑞 ) ) ⟩ } = ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 { ⟨ ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ , ( 𝐹 ‘ ( 𝑝 ( +_g ‘ 𝑅 ) 𝑞 ) ) ⟩ } )
16		eqidd	⊢ ( 𝜑 → ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 { ⟨ ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ , ( 𝐹 ‘ ( 𝑝 ( ._r ‘ 𝑅 ) 𝑞 ) ) ⟩ } = ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 { ⟨ ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ , ( 𝐹 ‘ ( 𝑝 ( ._r ‘ 𝑅 ) 𝑞 ) ) ⟩ } )
17		eqidd	⊢ ( 𝜑 → ∪ 𝑞 ∈ 𝑉 ( 𝑝 ∈ ( Base ‘ ( Scalar ‘ 𝑅 ) ) , 𝑥 ∈ { ( 𝐹 ‘ 𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 ( ·_𝑠 ‘ 𝑅 ) 𝑞 ) ) ) = ∪ 𝑞 ∈ 𝑉 ( 𝑝 ∈ ( Base ‘ ( Scalar ‘ 𝑅 ) ) , 𝑥 ∈ { ( 𝐹 ‘ 𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 ( ·_𝑠 ‘ 𝑅 ) 𝑞 ) ) ) )
18		eqidd	⊢ ( 𝜑 → ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 { ⟨ ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ , ( 𝑝 ( ·_𝑖 ‘ 𝑅 ) 𝑞 ) ⟩ } = ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 { ⟨ ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ , ( 𝑝 ( ·_𝑖 ‘ 𝑅 ) 𝑞 ) ⟩ } )
19		eqidd	⊢ ( 𝜑 → ( ( TopOpen ‘ 𝑅 ) qTop 𝐹 ) = ( ( TopOpen ‘ 𝑅 ) qTop 𝐹 ) )
20		eqidd	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ inf ( ∪ 𝑛 ∈ ℕ ran ( 𝑔 ∈ { ℎ ∈ ( ( 𝑉 × 𝑉 ) ↑_m ( 1 ... 𝑛 ) ) ∣ ( ( 𝐹 ‘ ( 1^st ‘ ( ℎ ‘ 1 ) ) ) = 𝑥 ∧ ( 𝐹 ‘ ( 2^nd ‘ ( ℎ ‘ 𝑛 ) ) ) = 𝑦 ∧ ∀ 𝑖 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 𝐹 ‘ ( 2^nd ‘ ( ℎ ‘ 𝑖 ) ) ) = ( 𝐹 ‘ ( 1^st ‘ ( ℎ ‘ ( 𝑖 + 1 ) ) ) ) ) } ↦ ( ℝ^_𝑠 Σ_g ( 𝐸 ∘ 𝑔 ) ) ) , ℝ^ , < ) ) = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ inf ( ∪ 𝑛 ∈ ℕ ran ( 𝑔 ∈ { ℎ ∈ ( ( 𝑉 × 𝑉 ) ↑_m ( 1 ... 𝑛 ) ) ∣ ( ( 𝐹 ‘ ( 1^st ‘ ( ℎ ‘ 1 ) ) ) = 𝑥 ∧ ( 𝐹 ‘ ( 2^nd ‘ ( ℎ ‘ 𝑛 ) ) ) = 𝑦 ∧ ∀ 𝑖 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 𝐹 ‘ ( 2^nd ‘ ( ℎ ‘ 𝑖 ) ) ) = ( 𝐹 ‘ ( 1^st ‘ ( ℎ ‘ ( 𝑖 + 1 ) ) ) ) ) } ↦ ( ℝ^_𝑠 Σ_g ( 𝐸 ∘ 𝑔 ) ) ) , ℝ^ , < ) ) )
21		eqidd	⊢ ( 𝜑 → ( ( 𝐹 ∘ ( le ‘ 𝑅 ) ) ∘ ^◡ 𝐹 ) = ( ( 𝐹 ∘ ( le ‘ 𝑅 ) ) ∘ ^◡ 𝐹 ) )
22	1 2 7 8 9 10 11 12 13 5 14 15 16 17 18 19 20 21 3 4	imasval	⊢ ( 𝜑 → 𝑈 = ( ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +_g ‘ ndx ) , ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 { ⟨ ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ , ( 𝐹 ‘ ( 𝑝 ( +_g ‘ 𝑅 ) 𝑞 ) ) ⟩ } ⟩ , ⟨ ( ._r ‘ ndx ) , ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 { ⟨ ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ , ( 𝐹 ‘ ( 𝑝 ( ._r ‘ 𝑅 ) 𝑞 ) ) ⟩ } ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , ( Scalar ‘ 𝑅 ) ⟩ , ⟨ ( ·_𝑠 ‘ ndx ) , ∪ 𝑞 ∈ 𝑉 ( 𝑝 ∈ ( Base ‘ ( Scalar ‘ 𝑅 ) ) , 𝑥 ∈ { ( 𝐹 ‘ 𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 ( ·_𝑠 ‘ 𝑅 ) 𝑞 ) ) ) ⟩ , ⟨ ( ·_𝑖 ‘ ndx ) , ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 { ⟨ ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ , ( 𝑝 ( ·_𝑖 ‘ 𝑅 ) 𝑞 ) ⟩ } ⟩ } ) ∪ { ⟨ ( TopSet ‘ ndx ) , ( ( TopOpen ‘ 𝑅 ) qTop 𝐹 ) ⟩ , ⟨ ( le ‘ ndx ) , ( ( 𝐹 ∘ ( le ‘ 𝑅 ) ) ∘ ^◡ 𝐹 ) ⟩ , ⟨ ( dist ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ inf ( ∪ 𝑛 ∈ ℕ ran ( 𝑔 ∈ { ℎ ∈ ( ( 𝑉 × 𝑉 ) ↑_m ( 1 ... 𝑛 ) ) ∣ ( ( 𝐹 ‘ ( 1^st ‘ ( ℎ ‘ 1 ) ) ) = 𝑥 ∧ ( 𝐹 ‘ ( 2^nd ‘ ( ℎ ‘ 𝑛 ) ) ) = 𝑦 ∧ ∀ 𝑖 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 𝐹 ‘ ( 2^nd ‘ ( ℎ ‘ 𝑖 ) ) ) = ( 𝐹 ‘ ( 1^st ‘ ( ℎ ‘ ( 𝑖 + 1 ) ) ) ) ) } ↦ ( ℝ^_𝑠 Σ_g ( 𝐸 ∘ 𝑔 ) ) ) , ℝ^ , < ) ) ⟩ } ) )
23		eqid	⊢ ( ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +_g ‘ ndx ) , ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 { ⟨ ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ , ( 𝐹 ‘ ( 𝑝 ( +_g ‘ 𝑅 ) 𝑞 ) ) ⟩ } ⟩ , ⟨ ( ._r ‘ ndx ) , ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 { ⟨ ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ , ( 𝐹 ‘ ( 𝑝 ( ._r ‘ 𝑅 ) 𝑞 ) ) ⟩ } ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , ( Scalar ‘ 𝑅 ) ⟩ , ⟨ ( ·_𝑠 ‘ ndx ) , ∪ 𝑞 ∈ 𝑉 ( 𝑝 ∈ ( Base ‘ ( Scalar ‘ 𝑅 ) ) , 𝑥 ∈ { ( 𝐹 ‘ 𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 ( ·_𝑠 ‘ 𝑅 ) 𝑞 ) ) ) ⟩ , ⟨ ( ·_𝑖 ‘ ndx ) , ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 { ⟨ ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ , ( 𝑝 ( ·_𝑖 ‘ 𝑅 ) 𝑞 ) ⟩ } ⟩ } ) ∪ { ⟨ ( TopSet ‘ ndx ) , ( ( TopOpen ‘ 𝑅 ) qTop 𝐹 ) ⟩ , ⟨ ( le ‘ ndx ) , ( ( 𝐹 ∘ ( le ‘ 𝑅 ) ) ∘ ^◡ 𝐹 ) ⟩ , ⟨ ( dist ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ inf ( ∪ 𝑛 ∈ ℕ ran ( 𝑔 ∈ { ℎ ∈ ( ( 𝑉 × 𝑉 ) ↑_m ( 1 ... 𝑛 ) ) ∣ ( ( 𝐹 ‘ ( 1^st ‘ ( ℎ ‘ 1 ) ) ) = 𝑥 ∧ ( 𝐹 ‘ ( 2^nd ‘ ( ℎ ‘ 𝑛 ) ) ) = 𝑦 ∧ ∀ 𝑖 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 𝐹 ‘ ( 2^nd ‘ ( ℎ ‘ 𝑖 ) ) ) = ( 𝐹 ‘ ( 1^st ‘ ( ℎ ‘ ( 𝑖 + 1 ) ) ) ) ) } ↦ ( ℝ^_𝑠 Σ_g ( 𝐸 ∘ 𝑔 ) ) ) , ℝ^ , < ) ) ⟩ } ) = ( ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +_g ‘ ndx ) , ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 { ⟨ ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ , ( 𝐹 ‘ ( 𝑝 ( +_g ‘ 𝑅 ) 𝑞 ) ) ⟩ } ⟩ , ⟨ ( ._r ‘ ndx ) , ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 { ⟨ ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ , ( 𝐹 ‘ ( 𝑝 ( ._r ‘ 𝑅 ) 𝑞 ) ) ⟩ } ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , ( Scalar ‘ 𝑅 ) ⟩ , ⟨ ( ·_𝑠 ‘ ndx ) , ∪ 𝑞 ∈ 𝑉 ( 𝑝 ∈ ( Base ‘ ( Scalar ‘ 𝑅 ) ) , 𝑥 ∈ { ( 𝐹 ‘ 𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 ( ·_𝑠 ‘ 𝑅 ) 𝑞 ) ) ) ⟩ , ⟨ ( ·_𝑖 ‘ ndx ) , ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 { ⟨ ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ , ( 𝑝 ( ·_𝑖 ‘ 𝑅 ) 𝑞 ) ⟩ } ⟩ } ) ∪ { ⟨ ( TopSet ‘ ndx ) , ( ( TopOpen ‘ 𝑅 ) qTop 𝐹 ) ⟩ , ⟨ ( le ‘ ndx ) , ( ( 𝐹 ∘ ( le ‘ 𝑅 ) ) ∘ ^◡ 𝐹 ) ⟩ , ⟨ ( dist ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ inf ( ∪ 𝑛 ∈ ℕ ran ( 𝑔 ∈ { ℎ ∈ ( ( 𝑉 × 𝑉 ) ↑_m ( 1 ... 𝑛 ) ) ∣ ( ( 𝐹 ‘ ( 1^st ‘ ( ℎ ‘ 1 ) ) ) = 𝑥 ∧ ( 𝐹 ‘ ( 2^nd ‘ ( ℎ ‘ 𝑛 ) ) ) = 𝑦 ∧ ∀ 𝑖 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 𝐹 ‘ ( 2^nd ‘ ( ℎ ‘ 𝑖 ) ) ) = ( 𝐹 ‘ ( 1^st ‘ ( ℎ ‘ ( 𝑖 + 1 ) ) ) ) ) } ↦ ( ℝ^_𝑠 Σ_g ( 𝐸 ∘ 𝑔 ) ) ) , ℝ^ , < ) ) ⟩ } )
24	23	imasvalstr	⊢ ( ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +_g ‘ ndx ) , ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 { ⟨ ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ , ( 𝐹 ‘ ( 𝑝 ( +_g ‘ 𝑅 ) 𝑞 ) ) ⟩ } ⟩ , ⟨ ( ._r ‘ ndx ) , ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 { ⟨ ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ , ( 𝐹 ‘ ( 𝑝 ( ._r ‘ 𝑅 ) 𝑞 ) ) ⟩ } ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , ( Scalar ‘ 𝑅 ) ⟩ , ⟨ ( ·_𝑠 ‘ ndx ) , ∪ 𝑞 ∈ 𝑉 ( 𝑝 ∈ ( Base ‘ ( Scalar ‘ 𝑅 ) ) , 𝑥 ∈ { ( 𝐹 ‘ 𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 ( ·_𝑠 ‘ 𝑅 ) 𝑞 ) ) ) ⟩ , ⟨ ( ·_𝑖 ‘ ndx ) , ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 { ⟨ ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ , ( 𝑝 ( ·_𝑖 ‘ 𝑅 ) 𝑞 ) ⟩ } ⟩ } ) ∪ { ⟨ ( TopSet ‘ ndx ) , ( ( TopOpen ‘ 𝑅 ) qTop 𝐹 ) ⟩ , ⟨ ( le ‘ ndx ) , ( ( 𝐹 ∘ ( le ‘ 𝑅 ) ) ∘ ^◡ 𝐹 ) ⟩ , ⟨ ( dist ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ inf ( ∪ 𝑛 ∈ ℕ ran ( 𝑔 ∈ { ℎ ∈ ( ( 𝑉 × 𝑉 ) ↑_m ( 1 ... 𝑛 ) ) ∣ ( ( 𝐹 ‘ ( 1^st ‘ ( ℎ ‘ 1 ) ) ) = 𝑥 ∧ ( 𝐹 ‘ ( 2^nd ‘ ( ℎ ‘ 𝑛 ) ) ) = 𝑦 ∧ ∀ 𝑖 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 𝐹 ‘ ( 2^nd ‘ ( ℎ ‘ 𝑖 ) ) ) = ( 𝐹 ‘ ( 1^st ‘ ( ℎ ‘ ( 𝑖 + 1 ) ) ) ) ) } ↦ ( ℝ^_𝑠 Σ_g ( 𝐸 ∘ 𝑔 ) ) ) , ℝ^ , < ) ) ⟩ } ) Struct ⟨ 1 , ; 1 2 ⟩
25		dsid	⊢ dist = Slot ( dist ‘ ndx )
26		snsstp3	⊢ { ⟨ ( dist ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ inf ( ∪ 𝑛 ∈ ℕ ran ( 𝑔 ∈ { ℎ ∈ ( ( 𝑉 × 𝑉 ) ↑_m ( 1 ... 𝑛 ) ) ∣ ( ( 𝐹 ‘ ( 1^st ‘ ( ℎ ‘ 1 ) ) ) = 𝑥 ∧ ( 𝐹 ‘ ( 2^nd ‘ ( ℎ ‘ 𝑛 ) ) ) = 𝑦 ∧ ∀ 𝑖 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 𝐹 ‘ ( 2^nd ‘ ( ℎ ‘ 𝑖 ) ) ) = ( 𝐹 ‘ ( 1^st ‘ ( ℎ ‘ ( 𝑖 + 1 ) ) ) ) ) } ↦ ( ℝ^_𝑠 Σ_g ( 𝐸 ∘ 𝑔 ) ) ) , ℝ^ , < ) ) ⟩ } ⊆ { ⟨ ( TopSet ‘ ndx ) , ( ( TopOpen ‘ 𝑅 ) qTop 𝐹 ) ⟩ , ⟨ ( le ‘ ndx ) , ( ( 𝐹 ∘ ( le ‘ 𝑅 ) ) ∘ ^◡ 𝐹 ) ⟩ , ⟨ ( dist ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ inf ( ∪ 𝑛 ∈ ℕ ran ( 𝑔 ∈ { ℎ ∈ ( ( 𝑉 × 𝑉 ) ↑_m ( 1 ... 𝑛 ) ) ∣ ( ( 𝐹 ‘ ( 1^st ‘ ( ℎ ‘ 1 ) ) ) = 𝑥 ∧ ( 𝐹 ‘ ( 2^nd ‘ ( ℎ ‘ 𝑛 ) ) ) = 𝑦 ∧ ∀ 𝑖 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 𝐹 ‘ ( 2^nd ‘ ( ℎ ‘ 𝑖 ) ) ) = ( 𝐹 ‘ ( 1^st ‘ ( ℎ ‘ ( 𝑖 + 1 ) ) ) ) ) } ↦ ( ℝ^_𝑠 Σ_g ( 𝐸 ∘ 𝑔 ) ) ) , ℝ^ , < ) ) ⟩ }
27		ssun2	⊢ { ⟨ ( TopSet ‘ ndx ) , ( ( TopOpen ‘ 𝑅 ) qTop 𝐹 ) ⟩ , ⟨ ( le ‘ ndx ) , ( ( 𝐹 ∘ ( le ‘ 𝑅 ) ) ∘ ^◡ 𝐹 ) ⟩ , ⟨ ( dist ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ inf ( ∪ 𝑛 ∈ ℕ ran ( 𝑔 ∈ { ℎ ∈ ( ( 𝑉 × 𝑉 ) ↑_m ( 1 ... 𝑛 ) ) ∣ ( ( 𝐹 ‘ ( 1^st ‘ ( ℎ ‘ 1 ) ) ) = 𝑥 ∧ ( 𝐹 ‘ ( 2^nd ‘ ( ℎ ‘ 𝑛 ) ) ) = 𝑦 ∧ ∀ 𝑖 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 𝐹 ‘ ( 2^nd ‘ ( ℎ ‘ 𝑖 ) ) ) = ( 𝐹 ‘ ( 1^st ‘ ( ℎ ‘ ( 𝑖 + 1 ) ) ) ) ) } ↦ ( ℝ^_𝑠 Σ_g ( 𝐸 ∘ 𝑔 ) ) ) , ℝ^ , < ) ) ⟩ } ⊆ ( ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +_g ‘ ndx ) , ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 { ⟨ ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ , ( 𝐹 ‘ ( 𝑝 ( +_g ‘ 𝑅 ) 𝑞 ) ) ⟩ } ⟩ , ⟨ ( ._r ‘ ndx ) , ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 { ⟨ ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ , ( 𝐹 ‘ ( 𝑝 ( ._r ‘ 𝑅 ) 𝑞 ) ) ⟩ } ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , ( Scalar ‘ 𝑅 ) ⟩ , ⟨ ( ·_𝑠 ‘ ndx ) , ∪ 𝑞 ∈ 𝑉 ( 𝑝 ∈ ( Base ‘ ( Scalar ‘ 𝑅 ) ) , 𝑥 ∈ { ( 𝐹 ‘ 𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 ( ·_𝑠 ‘ 𝑅 ) 𝑞 ) ) ) ⟩ , ⟨ ( ·_𝑖 ‘ ndx ) , ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 { ⟨ ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ , ( 𝑝 ( ·_𝑖 ‘ 𝑅 ) 𝑞 ) ⟩ } ⟩ } ) ∪ { ⟨ ( TopSet ‘ ndx ) , ( ( TopOpen ‘ 𝑅 ) qTop 𝐹 ) ⟩ , ⟨ ( le ‘ ndx ) , ( ( 𝐹 ∘ ( le ‘ 𝑅 ) ) ∘ ^◡ 𝐹 ) ⟩ , ⟨ ( dist ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ inf ( ∪ 𝑛 ∈ ℕ ran ( 𝑔 ∈ { ℎ ∈ ( ( 𝑉 × 𝑉 ) ↑_m ( 1 ... 𝑛 ) ) ∣ ( ( 𝐹 ‘ ( 1^st ‘ ( ℎ ‘ 1 ) ) ) = 𝑥 ∧ ( 𝐹 ‘ ( 2^nd ‘ ( ℎ ‘ 𝑛 ) ) ) = 𝑦 ∧ ∀ 𝑖 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 𝐹 ‘ ( 2^nd ‘ ( ℎ ‘ 𝑖 ) ) ) = ( 𝐹 ‘ ( 1^st ‘ ( ℎ ‘ ( 𝑖 + 1 ) ) ) ) ) } ↦ ( ℝ^_𝑠 Σ_g ( 𝐸 ∘ 𝑔 ) ) ) , ℝ^ , < ) ) ⟩ } )
28	26 27	sstri	⊢ { ⟨ ( dist ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ inf ( ∪ 𝑛 ∈ ℕ ran ( 𝑔 ∈ { ℎ ∈ ( ( 𝑉 × 𝑉 ) ↑_m ( 1 ... 𝑛 ) ) ∣ ( ( 𝐹 ‘ ( 1^st ‘ ( ℎ ‘ 1 ) ) ) = 𝑥 ∧ ( 𝐹 ‘ ( 2^nd ‘ ( ℎ ‘ 𝑛 ) ) ) = 𝑦 ∧ ∀ 𝑖 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 𝐹 ‘ ( 2^nd ‘ ( ℎ ‘ 𝑖 ) ) ) = ( 𝐹 ‘ ( 1^st ‘ ( ℎ ‘ ( 𝑖 + 1 ) ) ) ) ) } ↦ ( ℝ^_𝑠 Σ_g ( 𝐸 ∘ 𝑔 ) ) ) , ℝ^ , < ) ) ⟩ } ⊆ ( ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +_g ‘ ndx ) , ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 { ⟨ ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ , ( 𝐹 ‘ ( 𝑝 ( +_g ‘ 𝑅 ) 𝑞 ) ) ⟩ } ⟩ , ⟨ ( ._r ‘ ndx ) , ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 { ⟨ ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ , ( 𝐹 ‘ ( 𝑝 ( ._r ‘ 𝑅 ) 𝑞 ) ) ⟩ } ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , ( Scalar ‘ 𝑅 ) ⟩ , ⟨ ( ·_𝑠 ‘ ndx ) , ∪ 𝑞 ∈ 𝑉 ( 𝑝 ∈ ( Base ‘ ( Scalar ‘ 𝑅 ) ) , 𝑥 ∈ { ( 𝐹 ‘ 𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 ( ·_𝑠 ‘ 𝑅 ) 𝑞 ) ) ) ⟩ , ⟨ ( ·_𝑖 ‘ ndx ) , ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 { ⟨ ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ , ( 𝑝 ( ·_𝑖 ‘ 𝑅 ) 𝑞 ) ⟩ } ⟩ } ) ∪ { ⟨ ( TopSet ‘ ndx ) , ( ( TopOpen ‘ 𝑅 ) qTop 𝐹 ) ⟩ , ⟨ ( le ‘ ndx ) , ( ( 𝐹 ∘ ( le ‘ 𝑅 ) ) ∘ ^◡ 𝐹 ) ⟩ , ⟨ ( dist ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ inf ( ∪ 𝑛 ∈ ℕ ran ( 𝑔 ∈ { ℎ ∈ ( ( 𝑉 × 𝑉 ) ↑_m ( 1 ... 𝑛 ) ) ∣ ( ( 𝐹 ‘ ( 1^st ‘ ( ℎ ‘ 1 ) ) ) = 𝑥 ∧ ( 𝐹 ‘ ( 2^nd ‘ ( ℎ ‘ 𝑛 ) ) ) = 𝑦 ∧ ∀ 𝑖 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 𝐹 ‘ ( 2^nd ‘ ( ℎ ‘ 𝑖 ) ) ) = ( 𝐹 ‘ ( 1^st ‘ ( ℎ ‘ ( 𝑖 + 1 ) ) ) ) ) } ↦ ( ℝ^_𝑠 Σ_g ( 𝐸 ∘ 𝑔 ) ) ) , ℝ^ , < ) ) ⟩ } )
29		fvex	⊢ ( Base ‘ 𝑅 ) ∈ V
30	2 29	eqeltrdi	⊢ ( 𝜑 → 𝑉 ∈ V )
31		focdmex	⊢ ( 𝑉 ∈ V → ( 𝐹 : 𝑉 –onto→ 𝐵 → 𝐵 ∈ V ) )
32	30 3 31	sylc	⊢ ( 𝜑 → 𝐵 ∈ V )
33		mpoexga	⊢ ( ( 𝐵 ∈ V ∧ 𝐵 ∈ V ) → ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ inf ( ∪ 𝑛 ∈ ℕ ran ( 𝑔 ∈ { ℎ ∈ ( ( 𝑉 × 𝑉 ) ↑_m ( 1 ... 𝑛 ) ) ∣ ( ( 𝐹 ‘ ( 1^st ‘ ( ℎ ‘ 1 ) ) ) = 𝑥 ∧ ( 𝐹 ‘ ( 2^nd ‘ ( ℎ ‘ 𝑛 ) ) ) = 𝑦 ∧ ∀ 𝑖 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 𝐹 ‘ ( 2^nd ‘ ( ℎ ‘ 𝑖 ) ) ) = ( 𝐹 ‘ ( 1^st ‘ ( ℎ ‘ ( 𝑖 + 1 ) ) ) ) ) } ↦ ( ℝ^_𝑠 Σ_g ( 𝐸 ∘ 𝑔 ) ) ) , ℝ^ , < ) ) ∈ V )
34	32 32 33	syl2anc	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ inf ( ∪ 𝑛 ∈ ℕ ran ( 𝑔 ∈ { ℎ ∈ ( ( 𝑉 × 𝑉 ) ↑_m ( 1 ... 𝑛 ) ) ∣ ( ( 𝐹 ‘ ( 1^st ‘ ( ℎ ‘ 1 ) ) ) = 𝑥 ∧ ( 𝐹 ‘ ( 2^nd ‘ ( ℎ ‘ 𝑛 ) ) ) = 𝑦 ∧ ∀ 𝑖 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 𝐹 ‘ ( 2^nd ‘ ( ℎ ‘ 𝑖 ) ) ) = ( 𝐹 ‘ ( 1^st ‘ ( ℎ ‘ ( 𝑖 + 1 ) ) ) ) ) } ↦ ( ℝ^_𝑠 Σ_g ( 𝐸 ∘ 𝑔 ) ) ) , ℝ^ , < ) ) ∈ V )
35	22 24 25 28 34 6	strfv3	⊢ ( 𝜑 → 𝐷 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ inf ( ∪ 𝑛 ∈ ℕ ran ( 𝑔 ∈ { ℎ ∈ ( ( 𝑉 × 𝑉 ) ↑_m ( 1 ... 𝑛 ) ) ∣ ( ( 𝐹 ‘ ( 1^st ‘ ( ℎ ‘ 1 ) ) ) = 𝑥 ∧ ( 𝐹 ‘ ( 2^nd ‘ ( ℎ ‘ 𝑛 ) ) ) = 𝑦 ∧ ∀ 𝑖 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 𝐹 ‘ ( 2^nd ‘ ( ℎ ‘ 𝑖 ) ) ) = ( 𝐹 ‘ ( 1^st ‘ ( ℎ ‘ ( 𝑖 + 1 ) ) ) ) ) } ↦ ( ℝ^_𝑠 Σ_g ( 𝐸 ∘ 𝑔 ) ) ) , ℝ^ , < ) ) )

Metamath Proof Explorer

Theorem imasds

Proof