Metamath Proof Explorer

Theorem imasbas

Description: The base set 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 ⊢ ( 𝜑 → 𝑅 ∈ 𝑍 )
Assertion imasbas ( 𝜑 → 𝐵 = ( Base ‘ 𝑈 ) )

Proof

Step Hyp Ref Expression
1 imasbas.u ⊢ ( 𝜑 → 𝑈 = ( 𝐹 “s 𝑅 ) )
2 imasbas.v ⊢ ( 𝜑 → 𝑉 = ( Base ‘ 𝑅 ) )
3 imasbas.f ⊢ ( 𝜑 → 𝐹 : 𝑉 –onto→ 𝐵 )
4 imasbas.r ⊢ ( 𝜑 → 𝑅 ∈ 𝑍 )
5 eqid ⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
6 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
7 eqid ⊢ ( Scalar ‘ 𝑅 ) = ( Scalar ‘ 𝑅 )
8 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝑅 ) ) = ( Base ‘ ( Scalar ‘ 𝑅 ) )
9 eqid ⊢ ( ·𝑠 ‘ 𝑅 ) = ( ·𝑠 ‘ 𝑅 )
10 eqid ⊢ ( ·𝑖 ‘ 𝑅 ) = ( ·𝑖 ‘ 𝑅 )
11 eqid ⊢ ( TopOpen ‘ 𝑅 ) = ( TopOpen ‘ 𝑅 )
12 eqid ⊢ ( dist ‘ 𝑅 ) = ( dist ‘ 𝑅 )
13 eqid ⊢ ( le ‘ 𝑅 ) = ( le ‘ 𝑅 )
14 eqidd ⊢ ( 𝜑 → ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 { ⟨ ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ , ( 𝐹 ‘ ( 𝑝 ( +g ‘ 𝑅 ) 𝑞 ) ) ⟩ } = ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 { ⟨ ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ , ( 𝐹 ‘ ( 𝑝 ( +g ‘ 𝑅 ) 𝑞 ) ) ⟩ } )
15 eqidd ⊢ ( 𝜑 → ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 { ⟨ ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ , ( 𝐹 ‘ ( 𝑝 ( .r ‘ 𝑅 ) 𝑞 ) ) ⟩ } = ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 { ⟨ ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ , ( 𝐹 ‘ ( 𝑝 ( .r ‘ 𝑅 ) 𝑞 ) ) ⟩ } )
16 eqidd ⊢ ( 𝜑 → ∪ 𝑞 ∈ 𝑉 ( 𝑝 ∈ ( Base ‘ ( Scalar ‘ 𝑅 ) ) , 𝑥 ∈ { ( 𝐹 ‘ 𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 ( ·𝑠 ‘ 𝑅 ) 𝑞 ) ) ) = ∪ 𝑞 ∈ 𝑉 ( 𝑝 ∈ ( Base ‘ ( Scalar ‘ 𝑅 ) ) , 𝑥 ∈ { ( 𝐹 ‘ 𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 ( ·𝑠 ‘ 𝑅 ) 𝑞 ) ) ) )
17 eqidd ⊢ ( 𝜑 → ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 { ⟨ ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ , ( 𝑝 ( ·𝑖 ‘ 𝑅 ) 𝑞 ) ⟩ } = ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 { ⟨ ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ , ( 𝑝 ( ·𝑖 ‘ 𝑅 ) 𝑞 ) ⟩ } )
18 eqidd ⊢ ( 𝜑 → ( ( TopOpen ‘ 𝑅 ) qTop 𝐹 ) = ( ( TopOpen ‘ 𝑅 ) qTop 𝐹 ) )
19 eqidd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ inf ( ∪ 𝑛 ∈ ℕ ran ( 𝑔 ∈ { ℎ ∈ ( ( 𝑉 × 𝑉 ) ↑m ( 1 ... 𝑛 ) ) ∣ ( ( 𝐹 ‘ ( 1st ‘ ( ℎ ‘ 1 ) ) ) = 𝑥 ∧ ( 𝐹 ‘ ( 2nd ‘ ( ℎ ‘ 𝑛 ) ) ) = 𝑦 ∧ ∀ 𝑖 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 𝐹 ‘ ( 2nd ‘ ( ℎ ‘ 𝑖 ) ) ) = ( 𝐹 ‘ ( 1st ‘ ( ℎ ‘ ( 𝑖 + 1 ) ) ) ) ) } ↦ ( ℝ*𝑠 Σg ( ( dist ‘ 𝑅 ) ∘ 𝑔 ) ) ) , ℝ* , < ) ) = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ inf ( ∪ 𝑛 ∈ ℕ ran ( 𝑔 ∈ { ℎ ∈ ( ( 𝑉 × 𝑉 ) ↑m ( 1 ... 𝑛 ) ) ∣ ( ( 𝐹 ‘ ( 1st ‘ ( ℎ ‘ 1 ) ) ) = 𝑥 ∧ ( 𝐹 ‘ ( 2nd ‘ ( ℎ ‘ 𝑛 ) ) ) = 𝑦 ∧ ∀ 𝑖 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 𝐹 ‘ ( 2nd ‘ ( ℎ ‘ 𝑖 ) ) ) = ( 𝐹 ‘ ( 1st ‘ ( ℎ ‘ ( 𝑖 + 1 ) ) ) ) ) } ↦ ( ℝ*𝑠 Σg ( ( dist ‘ 𝑅 ) ∘ 𝑔 ) ) ) , ℝ* , < ) ) )
20 eqidd ⊢ ( 𝜑 → ( ( 𝐹 ∘ ( le ‘ 𝑅 ) ) ∘ ◡ 𝐹 ) = ( ( 𝐹 ∘ ( le ‘ 𝑅 ) ) ∘ ◡ 𝐹 ) )
21 1 2 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 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 ... 𝑛 ) ) ∣ ( ( 𝐹 ‘ ( 1st ‘ ( ℎ ‘ 1 ) ) ) = 𝑥 ∧ ( 𝐹 ‘ ( 2nd ‘ ( ℎ ‘ 𝑛 ) ) ) = 𝑦 ∧ ∀ 𝑖 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 𝐹 ‘ ( 2nd ‘ ( ℎ ‘ 𝑖 ) ) ) = ( 𝐹 ‘ ( 1st ‘ ( ℎ ‘ ( 𝑖 + 1 ) ) ) ) ) } ↦ ( ℝ*𝑠 Σg ( ( dist ‘ 𝑅 ) ∘ 𝑔 ) ) ) , ℝ* , < ) ) ⟩ } ) )
22 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 ... 𝑛 ) ) ∣ ( ( 𝐹 ‘ ( 1st ‘ ( ℎ ‘ 1 ) ) ) = 𝑥 ∧ ( 𝐹 ‘ ( 2nd ‘ ( ℎ ‘ 𝑛 ) ) ) = 𝑦 ∧ ∀ 𝑖 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 𝐹 ‘ ( 2nd ‘ ( ℎ ‘ 𝑖 ) ) ) = ( 𝐹 ‘ ( 1st ‘ ( ℎ ‘ ( 𝑖 + 1 ) ) ) ) ) } ↦ ( ℝ*𝑠 Σg ( ( dist ‘ 𝑅 ) ∘ 𝑔 ) ) ) , ℝ* , < ) ) ⟩ } ) = ( ( { ⟨ ( 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 ... 𝑛 ) ) ∣ ( ( 𝐹 ‘ ( 1st ‘ ( ℎ ‘ 1 ) ) ) = 𝑥 ∧ ( 𝐹 ‘ ( 2nd ‘ ( ℎ ‘ 𝑛 ) ) ) = 𝑦 ∧ ∀ 𝑖 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 𝐹 ‘ ( 2nd ‘ ( ℎ ‘ 𝑖 ) ) ) = ( 𝐹 ‘ ( 1st ‘ ( ℎ ‘ ( 𝑖 + 1 ) ) ) ) ) } ↦ ( ℝ*𝑠 Σg ( ( dist ‘ 𝑅 ) ∘ 𝑔 ) ) ) , ℝ* , < ) ) ⟩ } )
23 22 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 ... 𝑛 ) ) ∣ ( ( 𝐹 ‘ ( 1st ‘ ( ℎ ‘ 1 ) ) ) = 𝑥 ∧ ( 𝐹 ‘ ( 2nd ‘ ( ℎ ‘ 𝑛 ) ) ) = 𝑦 ∧ ∀ 𝑖 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 𝐹 ‘ ( 2nd ‘ ( ℎ ‘ 𝑖 ) ) ) = ( 𝐹 ‘ ( 1st ‘ ( ℎ ‘ ( 𝑖 + 1 ) ) ) ) ) } ↦ ( ℝ*𝑠 Σg ( ( dist ‘ 𝑅 ) ∘ 𝑔 ) ) ) , ℝ* , < ) ) ⟩ } ) Struct ⟨ 1 , 1 2 ⟩
24 baseid ⊢ Base = Slot ( Base ‘ ndx )
25 snsstp1 ⊢ { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ } ⊆ { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 { ⟨ ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ , ( 𝐹 ‘ ( 𝑝 ( +g ‘ 𝑅 ) 𝑞 ) ) ⟩ } ⟩ , ⟨ ( .r ‘ ndx ) , ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 { ⟨ ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ , ( 𝐹 ‘ ( 𝑝 ( .r ‘ 𝑅 ) 𝑞 ) ) ⟩ } ⟩ }
26 ssun1 ⊢ { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 { ⟨ ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ , ( 𝐹 ‘ ( 𝑝 ( +g ‘ 𝑅 ) 𝑞 ) ) ⟩ } ⟩ , ⟨ ( .r ‘ ndx ) , ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 { ⟨ ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ , ( 𝐹 ‘ ( 𝑝 ( .r ‘ 𝑅 ) 𝑞 ) ) ⟩ } ⟩ } ⊆ ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 { ⟨ ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ , ( 𝐹 ‘ ( 𝑝 ( +g ‘ 𝑅 ) 𝑞 ) ) ⟩ } ⟩ , ⟨ ( .r ‘ ndx ) , ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 { ⟨ ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ , ( 𝐹 ‘ ( 𝑝 ( .r ‘ 𝑅 ) 𝑞 ) ) ⟩ } ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , ( Scalar ‘ 𝑅 ) ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ∪ 𝑞 ∈ 𝑉 ( 𝑝 ∈ ( Base ‘ ( Scalar ‘ 𝑅 ) ) , 𝑥 ∈ { ( 𝐹 ‘ 𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 ( ·𝑠 ‘ 𝑅 ) 𝑞 ) ) ) ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 { ⟨ ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ , ( 𝑝 ( ·𝑖 ‘ 𝑅 ) 𝑞 ) ⟩ } ⟩ } )
27 25 26 sstri ⊢ { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ } ⊆ ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 { ⟨ ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ , ( 𝐹 ‘ ( 𝑝 ( +g ‘ 𝑅 ) 𝑞 ) ) ⟩ } ⟩ , ⟨ ( .r ‘ ndx ) , ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 { ⟨ ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ , ( 𝐹 ‘ ( 𝑝 ( .r ‘ 𝑅 ) 𝑞 ) ) ⟩ } ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , ( Scalar ‘ 𝑅 ) ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ∪ 𝑞 ∈ 𝑉 ( 𝑝 ∈ ( Base ‘ ( Scalar ‘ 𝑅 ) ) , 𝑥 ∈ { ( 𝐹 ‘ 𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 ( ·𝑠 ‘ 𝑅 ) 𝑞 ) ) ) ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 { ⟨ ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ , ( 𝑝 ( ·𝑖 ‘ 𝑅 ) 𝑞 ) ⟩ } ⟩ } )
28 ssun1 ⊢ ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 { ⟨ ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ , ( 𝐹 ‘ ( 𝑝 ( +g ‘ 𝑅 ) 𝑞 ) ) ⟩ } ⟩ , ⟨ ( .r ‘ ndx ) , ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 { ⟨ ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ , ( 𝐹 ‘ ( 𝑝 ( .r ‘ 𝑅 ) 𝑞 ) ) ⟩ } ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , ( Scalar ‘ 𝑅 ) ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ∪ 𝑞 ∈ 𝑉 ( 𝑝 ∈ ( Base ‘ ( Scalar ‘ 𝑅 ) ) , 𝑥 ∈ { ( 𝐹 ‘ 𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 ( ·𝑠 ‘ 𝑅 ) 𝑞 ) ) ) ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 { ⟨ ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ , ( 𝑝 ( ·𝑖 ‘ 𝑅 ) 𝑞 ) ⟩ } ⟩ } ) ⊆ ( ( { ⟨ ( 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 ... 𝑛 ) ) ∣ ( ( 𝐹 ‘ ( 1st ‘ ( ℎ ‘ 1 ) ) ) = 𝑥 ∧ ( 𝐹 ‘ ( 2nd ‘ ( ℎ ‘ 𝑛 ) ) ) = 𝑦 ∧ ∀ 𝑖 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 𝐹 ‘ ( 2nd ‘ ( ℎ ‘ 𝑖 ) ) ) = ( 𝐹 ‘ ( 1st ‘ ( ℎ ‘ ( 𝑖 + 1 ) ) ) ) ) } ↦ ( ℝ*𝑠 Σg ( ( dist ‘ 𝑅 ) ∘ 𝑔 ) ) ) , ℝ* , < ) ) ⟩ } )
29 27 28 sstri ⊢ { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ } ⊆ ( ( { ⟨ ( 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 ... 𝑛 ) ) ∣ ( ( 𝐹 ‘ ( 1st ‘ ( ℎ ‘ 1 ) ) ) = 𝑥 ∧ ( 𝐹 ‘ ( 2nd ‘ ( ℎ ‘ 𝑛 ) ) ) = 𝑦 ∧ ∀ 𝑖 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 𝐹 ‘ ( 2nd ‘ ( ℎ ‘ 𝑖 ) ) ) = ( 𝐹 ‘ ( 1st ‘ ( ℎ ‘ ( 𝑖 + 1 ) ) ) ) ) } ↦ ( ℝ*𝑠 Σg ( ( dist ‘ 𝑅 ) ∘ 𝑔 ) ) ) , ℝ* , < ) ) ⟩ } )
30 fvex ⊢ ( Base ‘ 𝑅 ) ∈ V
31 2 30 eqeltrdi ⊢ ( 𝜑 → 𝑉 ∈ V )
32 fornex ⊢ ( 𝑉 ∈ V → ( 𝐹 : 𝑉 –onto→ 𝐵 → 𝐵 ∈ V ) )
33 31 3 32 sylc ⊢ ( 𝜑 → 𝐵 ∈ V )
34 eqid ⊢ ( Base ‘ 𝑈 ) = ( Base ‘ 𝑈 )
35 21 23 24 29 33 34 strfv3 ⊢ ( 𝜑 → ( Base ‘ 𝑈 ) = 𝐵 )
36 35 eqcomd ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝑈 ) )