Theorem prdsex 13302

Description: Existence of the structure product. (Contributed by Jim Kingdon, 18-Mar-2025.)

Assertion

Ref	Expression
prdsex	⊢ ((𝑆 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊) → (𝑆Xs𝑅) ∈ V)

Proof of Theorem prdsex

Dummy variables 𝑎 𝑐 𝑑 𝑒 𝑓 𝑔 ℎ 𝑟 𝑠 𝑣 𝑥 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		elex 2811	. . . 4 ⊢ (𝑆 ∈ 𝑉 → 𝑆 ∈ V)
2	1	adantr 276	. . 3 ⊢ ((𝑆 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊) → 𝑆 ∈ V)
3		elex 2811	. . . 4 ⊢ (𝑅 ∈ 𝑊 → 𝑅 ∈ V)
4	3	adantl 277	. . 3 ⊢ ((𝑆 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊) → 𝑅 ∈ V)
5		dmexg 4988	. . . . 5 ⊢ (𝑅 ∈ 𝑊 → dom 𝑅 ∈ V)
6		basfn 13091	. . . . . . 7 ⊢ Base Fn V
7		simpr 110	. . . . . . . 8 ⊢ ((𝑆 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊) → 𝑅 ∈ 𝑊)
8		vex 2802	. . . . . . . 8 ⊢ 𝑥 ∈ V
9		fvexg 5646	. . . . . . . 8 ⊢ ((𝑅 ∈ 𝑊 ∧ 𝑥 ∈ V) → (𝑅‘𝑥) ∈ V)
10	7, 8, 9	sylancl 413	. . . . . . 7 ⊢ ((𝑆 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊) → (𝑅‘𝑥) ∈ V)
11		funfvex 5644	. . . . . . . 8 ⊢ ((Fun Base ∧ (𝑅‘𝑥) ∈ dom Base) → (Base‘(𝑅‘𝑥)) ∈ V)
12	11	funfni 5423	. . . . . . 7 ⊢ ((Base Fn V ∧ (𝑅‘𝑥) ∈ V) → (Base‘(𝑅‘𝑥)) ∈ V)
13	6, 10, 12	sylancr 414	. . . . . 6 ⊢ ((𝑆 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊) → (Base‘(𝑅‘𝑥)) ∈ V)
14	13	ralrimivw 2604	. . . . 5 ⊢ ((𝑆 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊) → ∀𝑥 ∈ dom 𝑅(Base‘(𝑅‘𝑥)) ∈ V)
15		ixpexgg 6869	. . . . 5 ⊢ ((dom 𝑅 ∈ V ∧ ∀𝑥 ∈ dom 𝑅(Base‘(𝑅‘𝑥)) ∈ V) → X𝑥 ∈ dom 𝑅(Base‘(𝑅‘𝑥)) ∈ V)
16	5, 14, 15	syl2an2 596	. . . 4 ⊢ ((𝑆 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊) → X𝑥 ∈ dom 𝑅(Base‘(𝑅‘𝑥)) ∈ V)
17		vex 2802	. . . . . . 7 ⊢ 𝑣 ∈ V
18	17, 17	mpoex 6360	. . . . . 6 ⊢ (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ X𝑥 ∈ dom 𝑅((𝑓‘𝑥)(Hom ‘(𝑅‘𝑥))(𝑔‘𝑥))) ∈ V
19		basendxnn 13088	. . . . . . . . . . 11 ⊢ (Base‘ndx) ∈ ℕ
20	17	a1i 9	. . . . . . . . . . 11 ⊢ ((𝑆 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊) → 𝑣 ∈ V)
21		opexg 4314	. . . . . . . . . . 11 ⊢ (((Base‘ndx) ∈ ℕ ∧ 𝑣 ∈ V) → ⟨(Base‘ndx), 𝑣⟩ ∈ V)
22	19, 20, 21	sylancr 414	. . . . . . . . . 10 ⊢ ((𝑆 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊) → ⟨(Base‘ndx), 𝑣⟩ ∈ V)
23		plusgndxnn 13144	. . . . . . . . . . . . 13 ⊢ (+g‘ndx) ∈ ℕ
24	23	elexi 2812	. . . . . . . . . . . 12 ⊢ (+g‘ndx) ∈ V
25	17, 17	mpoex 6360	. . . . . . . . . . . 12 ⊢ (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑅 ↦ ((𝑓‘𝑥)(+g‘(𝑅‘𝑥))(𝑔‘𝑥)))) ∈ V
26	24, 25	opex 4315	. . . . . . . . . . 11 ⊢ ⟨(+g‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑅 ↦ ((𝑓‘𝑥)(+g‘(𝑅‘𝑥))(𝑔‘𝑥))))⟩ ∈ V
27	26	a1i 9	. . . . . . . . . 10 ⊢ ((𝑆 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊) → ⟨(+g‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑅 ↦ ((𝑓‘𝑥)(+g‘(𝑅‘𝑥))(𝑔‘𝑥))))⟩ ∈ V)
28		mulrslid 13165	. . . . . . . . . . . . . 14 ⊢ (.r = Slot (.r‘ndx) ∧ (.r‘ndx) ∈ ℕ)
29	28	simpri 113	. . . . . . . . . . . . 13 ⊢ (.r‘ndx) ∈ ℕ
30	29	elexi 2812	. . . . . . . . . . . 12 ⊢ (.r‘ndx) ∈ V
31	17, 17	mpoex 6360	. . . . . . . . . . . 12 ⊢ (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑅 ↦ ((𝑓‘𝑥)(.r‘(𝑅‘𝑥))(𝑔‘𝑥)))) ∈ V
32	30, 31	opex 4315	. . . . . . . . . . 11 ⊢ ⟨(.r‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑅 ↦ ((𝑓‘𝑥)(.r‘(𝑅‘𝑥))(𝑔‘𝑥))))⟩ ∈ V
33	32	a1i 9	. . . . . . . . . 10 ⊢ ((𝑆 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊) → ⟨(.r‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑅 ↦ ((𝑓‘𝑥)(.r‘(𝑅‘𝑥))(𝑔‘𝑥))))⟩ ∈ V)
34		tpexg 4535	. . . . . . . . . 10 ⊢ ((⟨(Base‘ndx), 𝑣⟩ ∈ V ∧ ⟨(+g‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑅 ↦ ((𝑓‘𝑥)(+g‘(𝑅‘𝑥))(𝑔‘𝑥))))⟩ ∈ V ∧ ⟨(.r‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑅 ↦ ((𝑓‘𝑥)(.r‘(𝑅‘𝑥))(𝑔‘𝑥))))⟩ ∈ V) → {⟨(Base‘ndx), 𝑣⟩, ⟨(+g‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑅 ↦ ((𝑓‘𝑥)(+g‘(𝑅‘𝑥))(𝑔‘𝑥))))⟩, ⟨(.r‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑅 ↦ ((𝑓‘𝑥)(.r‘(𝑅‘𝑥))(𝑔‘𝑥))))⟩} ∈ V)
35	22, 27, 33, 34	syl3anc 1271	. . . . . . . . 9 ⊢ ((𝑆 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊) → {⟨(Base‘ndx), 𝑣⟩, ⟨(+g‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑅 ↦ ((𝑓‘𝑥)(+g‘(𝑅‘𝑥))(𝑔‘𝑥))))⟩, ⟨(.r‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑅 ↦ ((𝑓‘𝑥)(.r‘(𝑅‘𝑥))(𝑔‘𝑥))))⟩} ∈ V)
36		scaslid 13186	. . . . . . . . . . . 12 ⊢ (Scalar = Slot (Scalar‘ndx) ∧ (Scalar‘ndx) ∈ ℕ)
37	36	simpri 113	. . . . . . . . . . 11 ⊢ (Scalar‘ndx) ∈ ℕ
38		simpl 109	. . . . . . . . . . 11 ⊢ ((𝑆 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊) → 𝑆 ∈ 𝑉)
39		opexg 4314	. . . . . . . . . . 11 ⊢ (((Scalar‘ndx) ∈ ℕ ∧ 𝑆 ∈ 𝑉) → ⟨(Scalar‘ndx), 𝑆⟩ ∈ V)
40	37, 38, 39	sylancr 414	. . . . . . . . . 10 ⊢ ((𝑆 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊) → ⟨(Scalar‘ndx), 𝑆⟩ ∈ V)
41		vscaslid 13196	. . . . . . . . . . . 12 ⊢ ( ·𝑠 = Slot ( ·𝑠 ‘ndx) ∧ ( ·𝑠 ‘ndx) ∈ ℕ)
42	41	simpri 113	. . . . . . . . . . 11 ⊢ ( ·𝑠 ‘ndx) ∈ ℕ
43	38	elexd 2813	. . . . . . . . . . . . 13 ⊢ ((𝑆 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊) → 𝑆 ∈ V)
44		funfvex 5644	. . . . . . . . . . . . . 14 ⊢ ((Fun Base ∧ 𝑆 ∈ dom Base) → (Base‘𝑆) ∈ V)
45	44	funfni 5423	. . . . . . . . . . . . 13 ⊢ ((Base Fn V ∧ 𝑆 ∈ V) → (Base‘𝑆) ∈ V)
46	6, 43, 45	sylancr 414	. . . . . . . . . . . 12 ⊢ ((𝑆 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊) → (Base‘𝑆) ∈ V)
47		mpoexga 6358	. . . . . . . . . . . 12 ⊢ (((Base‘𝑆) ∈ V ∧ 𝑣 ∈ V) → (𝑓 ∈ (Base‘𝑆), 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑅 ↦ (𝑓( ·𝑠 ‘(𝑅‘𝑥))(𝑔‘𝑥)))) ∈ V)
48	46, 17, 47	sylancl 413	. . . . . . . . . . 11 ⊢ ((𝑆 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊) → (𝑓 ∈ (Base‘𝑆), 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑅 ↦ (𝑓( ·𝑠 ‘(𝑅‘𝑥))(𝑔‘𝑥)))) ∈ V)
49		opexg 4314	. . . . . . . . . . 11 ⊢ ((( ·𝑠 ‘ndx) ∈ ℕ ∧ (𝑓 ∈ (Base‘𝑆), 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑅 ↦ (𝑓( ·𝑠 ‘(𝑅‘𝑥))(𝑔‘𝑥)))) ∈ V) → ⟨( ·𝑠 ‘ndx), (𝑓 ∈ (Base‘𝑆), 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑅 ↦ (𝑓( ·𝑠 ‘(𝑅‘𝑥))(𝑔‘𝑥))))⟩ ∈ V)
50	42, 48, 49	sylancr 414	. . . . . . . . . 10 ⊢ ((𝑆 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊) → ⟨( ·𝑠 ‘ndx), (𝑓 ∈ (Base‘𝑆), 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑅 ↦ (𝑓( ·𝑠 ‘(𝑅‘𝑥))(𝑔‘𝑥))))⟩ ∈ V)
51		ipslid 13204	. . . . . . . . . . . . . 14 ⊢ (·𝑖 = Slot (·𝑖‘ndx) ∧ (·𝑖‘ndx) ∈ ℕ)
52	51	simpri 113	. . . . . . . . . . . . 13 ⊢ (·𝑖‘ndx) ∈ ℕ
53	52	elexi 2812	. . . . . . . . . . . 12 ⊢ (·𝑖‘ndx) ∈ V
54	17, 17	mpoex 6360	. . . . . . . . . . . 12 ⊢ (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑆 Σg (𝑥 ∈ dom 𝑅 ↦ ((𝑓‘𝑥)(·𝑖‘(𝑅‘𝑥))(𝑔‘𝑥))))) ∈ V
55	53, 54	opex 4315	. . . . . . . . . . 11 ⊢ ⟨(·𝑖‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑆 Σg (𝑥 ∈ dom 𝑅 ↦ ((𝑓‘𝑥)(·𝑖‘(𝑅‘𝑥))(𝑔‘𝑥)))))⟩ ∈ V
56	55	a1i 9	. . . . . . . . . 10 ⊢ ((𝑆 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊) → ⟨(·𝑖‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑆 Σg (𝑥 ∈ dom 𝑅 ↦ ((𝑓‘𝑥)(·𝑖‘(𝑅‘𝑥))(𝑔‘𝑥)))))⟩ ∈ V)
57		tpexg 4535	. . . . . . . . . 10 ⊢ ((⟨(Scalar‘ndx), 𝑆⟩ ∈ V ∧ ⟨( ·𝑠 ‘ndx), (𝑓 ∈ (Base‘𝑆), 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑅 ↦ (𝑓( ·𝑠 ‘(𝑅‘𝑥))(𝑔‘𝑥))))⟩ ∈ V ∧ ⟨(·𝑖‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑆 Σg (𝑥 ∈ dom 𝑅 ↦ ((𝑓‘𝑥)(·𝑖‘(𝑅‘𝑥))(𝑔‘𝑥)))))⟩ ∈ V) → {⟨(Scalar‘ndx), 𝑆⟩, ⟨( ·𝑠 ‘ndx), (𝑓 ∈ (Base‘𝑆), 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑅 ↦ (𝑓( ·𝑠 ‘(𝑅‘𝑥))(𝑔‘𝑥))))⟩, ⟨(·𝑖‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑆 Σg (𝑥 ∈ dom 𝑅 ↦ ((𝑓‘𝑥)(·𝑖‘(𝑅‘𝑥))(𝑔‘𝑥)))))⟩} ∈ V)
58	40, 50, 56, 57	syl3anc 1271	. . . . . . . . 9 ⊢ ((𝑆 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊) → {⟨(Scalar‘ndx), 𝑆⟩, ⟨( ·𝑠 ‘ndx), (𝑓 ∈ (Base‘𝑆), 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑅 ↦ (𝑓( ·𝑠 ‘(𝑅‘𝑥))(𝑔‘𝑥))))⟩, ⟨(·𝑖‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑆 Σg (𝑥 ∈ dom 𝑅 ↦ ((𝑓‘𝑥)(·𝑖‘(𝑅‘𝑥))(𝑔‘𝑥)))))⟩} ∈ V)
59		unexg 4534	. . . . . . . . 9 ⊢ (({⟨(Base‘ndx), 𝑣⟩, ⟨(+g‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑅 ↦ ((𝑓‘𝑥)(+g‘(𝑅‘𝑥))(𝑔‘𝑥))))⟩, ⟨(.r‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑅 ↦ ((𝑓‘𝑥)(.r‘(𝑅‘𝑥))(𝑔‘𝑥))))⟩} ∈ V ∧ {⟨(Scalar‘ndx), 𝑆⟩, ⟨( ·𝑠 ‘ndx), (𝑓 ∈ (Base‘𝑆), 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑅 ↦ (𝑓( ·𝑠 ‘(𝑅‘𝑥))(𝑔‘𝑥))))⟩, ⟨(·𝑖‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑆 Σg (𝑥 ∈ dom 𝑅 ↦ ((𝑓‘𝑥)(·𝑖‘(𝑅‘𝑥))(𝑔‘𝑥)))))⟩} ∈ V) → ({⟨(Base‘ndx), 𝑣⟩, ⟨(+g‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑅 ↦ ((𝑓‘𝑥)(+g‘(𝑅‘𝑥))(𝑔‘𝑥))))⟩, ⟨(.r‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑅 ↦ ((𝑓‘𝑥)(.r‘(𝑅‘𝑥))(𝑔‘𝑥))))⟩} ∪ {⟨(Scalar‘ndx), 𝑆⟩, ⟨( ·𝑠 ‘ndx), (𝑓 ∈ (Base‘𝑆), 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑅 ↦ (𝑓( ·𝑠 ‘(𝑅‘𝑥))(𝑔‘𝑥))))⟩, ⟨(·𝑖‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑆 Σg (𝑥 ∈ dom 𝑅 ↦ ((𝑓‘𝑥)(·𝑖‘(𝑅‘𝑥))(𝑔‘𝑥)))))⟩}) ∈ V)
60	35, 58, 59	syl2anc 411	. . . . . . . 8 ⊢ ((𝑆 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊) → ({⟨(Base‘ndx), 𝑣⟩, ⟨(+g‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑅 ↦ ((𝑓‘𝑥)(+g‘(𝑅‘𝑥))(𝑔‘𝑥))))⟩, ⟨(.r‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑅 ↦ ((𝑓‘𝑥)(.r‘(𝑅‘𝑥))(𝑔‘𝑥))))⟩} ∪ {⟨(Scalar‘ndx), 𝑆⟩, ⟨( ·𝑠 ‘ndx), (𝑓 ∈ (Base‘𝑆), 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑅 ↦ (𝑓( ·𝑠 ‘(𝑅‘𝑥))(𝑔‘𝑥))))⟩, ⟨(·𝑖‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑆 Σg (𝑥 ∈ dom 𝑅 ↦ ((𝑓‘𝑥)(·𝑖‘(𝑅‘𝑥))(𝑔‘𝑥)))))⟩}) ∈ V)
61		tsetndxnn 13222	. . . . . . . . . . 11 ⊢ (TopSet‘ndx) ∈ ℕ
62		topnfn 13277	. . . . . . . . . . . . . 14 ⊢ TopOpen Fn V
63		fnfun 5418	. . . . . . . . . . . . . 14 ⊢ (TopOpen Fn V → Fun TopOpen)
64	62, 63	ax-mp 5	. . . . . . . . . . . . 13 ⊢ Fun TopOpen
65		cofunexg 6254	. . . . . . . . . . . . 13 ⊢ ((Fun TopOpen ∧ 𝑅 ∈ 𝑊) → (TopOpen ∘ 𝑅) ∈ V)
66	64, 7, 65	sylancr 414	. . . . . . . . . . . 12 ⊢ ((𝑆 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊) → (TopOpen ∘ 𝑅) ∈ V)
67		ptex 13297	. . . . . . . . . . . 12 ⊢ ((TopOpen ∘ 𝑅) ∈ V → (∏t‘(TopOpen ∘ 𝑅)) ∈ V)
68	66, 67	syl 14	. . . . . . . . . . 11 ⊢ ((𝑆 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊) → (∏t‘(TopOpen ∘ 𝑅)) ∈ V)
69		opexg 4314	. . . . . . . . . . 11 ⊢ (((TopSet‘ndx) ∈ ℕ ∧ (∏t‘(TopOpen ∘ 𝑅)) ∈ V) → ⟨(TopSet‘ndx), (∏t‘(TopOpen ∘ 𝑅))⟩ ∈ V)
70	61, 68, 69	sylancr 414	. . . . . . . . . 10 ⊢ ((𝑆 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊) → ⟨(TopSet‘ndx), (∏t‘(TopOpen ∘ 𝑅))⟩ ∈ V)
71		plendxnn 13236	. . . . . . . . . . 11 ⊢ (le‘ndx) ∈ ℕ
72		vex 2802	. . . . . . . . . . . . . . . 16 ⊢ 𝑓 ∈ V
73		vex 2802	. . . . . . . . . . . . . . . 16 ⊢ 𝑔 ∈ V
74	72, 73	prss 3824	. . . . . . . . . . . . . . 15 ⊢ ((𝑓 ∈ 𝑣 ∧ 𝑔 ∈ 𝑣) ↔ {𝑓, 𝑔} ⊆ 𝑣)
75	74	anbi1i 458	. . . . . . . . . . . . . 14 ⊢ (((𝑓 ∈ 𝑣 ∧ 𝑔 ∈ 𝑣) ∧ ∀𝑥 ∈ dom 𝑅(𝑓‘𝑥)(le‘(𝑅‘𝑥))(𝑔‘𝑥)) ↔ ({𝑓, 𝑔} ⊆ 𝑣 ∧ ∀𝑥 ∈ dom 𝑅(𝑓‘𝑥)(le‘(𝑅‘𝑥))(𝑔‘𝑥)))
76	75	opabbii 4151	. . . . . . . . . . . . 13 ⊢ {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ 𝑣 ∧ 𝑔 ∈ 𝑣) ∧ ∀𝑥 ∈ dom 𝑅(𝑓‘𝑥)(le‘(𝑅‘𝑥))(𝑔‘𝑥))} = {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝑣 ∧ ∀𝑥 ∈ dom 𝑅(𝑓‘𝑥)(le‘(𝑅‘𝑥))(𝑔‘𝑥))}
77	17, 17	xpex 4834	. . . . . . . . . . . . . 14 ⊢ (𝑣 × 𝑣) ∈ V
78		opabssxp 4793	. . . . . . . . . . . . . 14 ⊢ {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ 𝑣 ∧ 𝑔 ∈ 𝑣) ∧ ∀𝑥 ∈ dom 𝑅(𝑓‘𝑥)(le‘(𝑅‘𝑥))(𝑔‘𝑥))} ⊆ (𝑣 × 𝑣)
79	77, 78	ssexi 4222	. . . . . . . . . . . . 13 ⊢ {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ 𝑣 ∧ 𝑔 ∈ 𝑣) ∧ ∀𝑥 ∈ dom 𝑅(𝑓‘𝑥)(le‘(𝑅‘𝑥))(𝑔‘𝑥))} ∈ V
80	76, 79	eqeltrri 2303	. . . . . . . . . . . 12 ⊢ {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝑣 ∧ ∀𝑥 ∈ dom 𝑅(𝑓‘𝑥)(le‘(𝑅‘𝑥))(𝑔‘𝑥))} ∈ V
81	80	a1i 9	. . . . . . . . . . 11 ⊢ ((𝑆 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊) → {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝑣 ∧ ∀𝑥 ∈ dom 𝑅(𝑓‘𝑥)(le‘(𝑅‘𝑥))(𝑔‘𝑥))} ∈ V)
82		opexg 4314	. . . . . . . . . . 11 ⊢ (((le‘ndx) ∈ ℕ ∧ {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝑣 ∧ ∀𝑥 ∈ dom 𝑅(𝑓‘𝑥)(le‘(𝑅‘𝑥))(𝑔‘𝑥))} ∈ V) → ⟨(le‘ndx), {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝑣 ∧ ∀𝑥 ∈ dom 𝑅(𝑓‘𝑥)(le‘(𝑅‘𝑥))(𝑔‘𝑥))}⟩ ∈ V)
83	71, 81, 82	sylancr 414	. . . . . . . . . 10 ⊢ ((𝑆 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊) → ⟨(le‘ndx), {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝑣 ∧ ∀𝑥 ∈ dom 𝑅(𝑓‘𝑥)(le‘(𝑅‘𝑥))(𝑔‘𝑥))}⟩ ∈ V)
84		dsndxnn 13251	. . . . . . . . . . . 12 ⊢ (dist‘ndx) ∈ ℕ
85	17, 17	mpoex 6360	. . . . . . . . . . . 12 ⊢ (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ sup((ran (𝑥 ∈ dom 𝑅 ↦ ((𝑓‘𝑥)(dist‘(𝑅‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ*, < )) ∈ V
86		opexg 4314	. . . . . . . . . . . 12 ⊢ (((dist‘ndx) ∈ ℕ ∧ (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ sup((ran (𝑥 ∈ dom 𝑅 ↦ ((𝑓‘𝑥)(dist‘(𝑅‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ*, < )) ∈ V) → ⟨(dist‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ sup((ran (𝑥 ∈ dom 𝑅 ↦ ((𝑓‘𝑥)(dist‘(𝑅‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ*, < ))⟩ ∈ V)
87	84, 85, 86	mp2an 426	. . . . . . . . . . 11 ⊢ ⟨(dist‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ sup((ran (𝑥 ∈ dom 𝑅 ↦ ((𝑓‘𝑥)(dist‘(𝑅‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ*, < ))⟩ ∈ V
88	87	a1i 9	. . . . . . . . . 10 ⊢ ((𝑆 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊) → ⟨(dist‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ sup((ran (𝑥 ∈ dom 𝑅 ↦ ((𝑓‘𝑥)(dist‘(𝑅‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ*, < ))⟩ ∈ V)
89		tpexg 4535	. . . . . . . . . 10 ⊢ ((⟨(TopSet‘ndx), (∏t‘(TopOpen ∘ 𝑅))⟩ ∈ V ∧ ⟨(le‘ndx), {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝑣 ∧ ∀𝑥 ∈ dom 𝑅(𝑓‘𝑥)(le‘(𝑅‘𝑥))(𝑔‘𝑥))}⟩ ∈ V ∧ ⟨(dist‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ sup((ran (𝑥 ∈ dom 𝑅 ↦ ((𝑓‘𝑥)(dist‘(𝑅‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ*, < ))⟩ ∈ V) → {⟨(TopSet‘ndx), (∏t‘(TopOpen ∘ 𝑅))⟩, ⟨(le‘ndx), {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝑣 ∧ ∀𝑥 ∈ dom 𝑅(𝑓‘𝑥)(le‘(𝑅‘𝑥))(𝑔‘𝑥))}⟩, ⟨(dist‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ sup((ran (𝑥 ∈ dom 𝑅 ↦ ((𝑓‘𝑥)(dist‘(𝑅‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ*, < ))⟩} ∈ V)
90	70, 83, 88, 89	syl3anc 1271	. . . . . . . . 9 ⊢ ((𝑆 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊) → {⟨(TopSet‘ndx), (∏t‘(TopOpen ∘ 𝑅))⟩, ⟨(le‘ndx), {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝑣 ∧ ∀𝑥 ∈ dom 𝑅(𝑓‘𝑥)(le‘(𝑅‘𝑥))(𝑔‘𝑥))}⟩, ⟨(dist‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ sup((ran (𝑥 ∈ dom 𝑅 ↦ ((𝑓‘𝑥)(dist‘(𝑅‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ*, < ))⟩} ∈ V)
91		homslid 13268	. . . . . . . . . . . 12 ⊢ (Hom = Slot (Hom ‘ndx) ∧ (Hom ‘ndx) ∈ ℕ)
92	91	simpri 113	. . . . . . . . . . 11 ⊢ (Hom ‘ndx) ∈ ℕ
93		vex 2802	. . . . . . . . . . 11 ⊢ ℎ ∈ V
94		opexg 4314	. . . . . . . . . . 11 ⊢ (((Hom ‘ndx) ∈ ℕ ∧ ℎ ∈ V) → ⟨(Hom ‘ndx), ℎ⟩ ∈ V)
95	92, 93, 94	mp2an 426	. . . . . . . . . 10 ⊢ ⟨(Hom ‘ndx), ℎ⟩ ∈ V
96		ccoslid 13271	. . . . . . . . . . . . 13 ⊢ (comp = Slot (comp‘ndx) ∧ (comp‘ndx) ∈ ℕ)
97	96	simpri 113	. . . . . . . . . . . 12 ⊢ (comp‘ndx) ∈ ℕ
98	77, 17	mpoex 6360	. . . . . . . . . . . 12 ⊢ (𝑎 ∈ (𝑣 × 𝑣), 𝑐 ∈ 𝑣 ↦ (𝑑 ∈ ((2nd ‘𝑎)ℎ𝑐), 𝑒 ∈ (ℎ‘𝑎) ↦ (𝑥 ∈ dom 𝑅 ↦ ((𝑑‘𝑥)(⟨((1st ‘𝑎)‘𝑥), ((2nd ‘𝑎)‘𝑥)⟩(comp‘(𝑅‘𝑥))(𝑐‘𝑥))(𝑒‘𝑥))))) ∈ V
99		opexg 4314	. . . . . . . . . . . 12 ⊢ (((comp‘ndx) ∈ ℕ ∧ (𝑎 ∈ (𝑣 × 𝑣), 𝑐 ∈ 𝑣 ↦ (𝑑 ∈ ((2nd ‘𝑎)ℎ𝑐), 𝑒 ∈ (ℎ‘𝑎) ↦ (𝑥 ∈ dom 𝑅 ↦ ((𝑑‘𝑥)(⟨((1st ‘𝑎)‘𝑥), ((2nd ‘𝑎)‘𝑥)⟩(comp‘(𝑅‘𝑥))(𝑐‘𝑥))(𝑒‘𝑥))))) ∈ V) → ⟨(comp‘ndx), (𝑎 ∈ (𝑣 × 𝑣), 𝑐 ∈ 𝑣 ↦ (𝑑 ∈ ((2nd ‘𝑎)ℎ𝑐), 𝑒 ∈ (ℎ‘𝑎) ↦ (𝑥 ∈ dom 𝑅 ↦ ((𝑑‘𝑥)(⟨((1st ‘𝑎)‘𝑥), ((2nd ‘𝑎)‘𝑥)⟩(comp‘(𝑅‘𝑥))(𝑐‘𝑥))(𝑒‘𝑥)))))⟩ ∈ V)
100	97, 98, 99	mp2an 426	. . . . . . . . . . 11 ⊢ ⟨(comp‘ndx), (𝑎 ∈ (𝑣 × 𝑣), 𝑐 ∈ 𝑣 ↦ (𝑑 ∈ ((2nd ‘𝑎)ℎ𝑐), 𝑒 ∈ (ℎ‘𝑎) ↦ (𝑥 ∈ dom 𝑅 ↦ ((𝑑‘𝑥)(⟨((1st ‘𝑎)‘𝑥), ((2nd ‘𝑎)‘𝑥)⟩(comp‘(𝑅‘𝑥))(𝑐‘𝑥))(𝑒‘𝑥)))))⟩ ∈ V
101	100	a1i 9	. . . . . . . . . 10 ⊢ ((𝑆 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊) → ⟨(comp‘ndx), (𝑎 ∈ (𝑣 × 𝑣), 𝑐 ∈ 𝑣 ↦ (𝑑 ∈ ((2nd ‘𝑎)ℎ𝑐), 𝑒 ∈ (ℎ‘𝑎) ↦ (𝑥 ∈ dom 𝑅 ↦ ((𝑑‘𝑥)(⟨((1st ‘𝑎)‘𝑥), ((2nd ‘𝑎)‘𝑥)⟩(comp‘(𝑅‘𝑥))(𝑐‘𝑥))(𝑒‘𝑥)))))⟩ ∈ V)
102		prexg 4295	. . . . . . . . . 10 ⊢ ((⟨(Hom ‘ndx), ℎ⟩ ∈ V ∧ ⟨(comp‘ndx), (𝑎 ∈ (𝑣 × 𝑣), 𝑐 ∈ 𝑣 ↦ (𝑑 ∈ ((2nd ‘𝑎)ℎ𝑐), 𝑒 ∈ (ℎ‘𝑎) ↦ (𝑥 ∈ dom 𝑅 ↦ ((𝑑‘𝑥)(⟨((1st ‘𝑎)‘𝑥), ((2nd ‘𝑎)‘𝑥)⟩(comp‘(𝑅‘𝑥))(𝑐‘𝑥))(𝑒‘𝑥)))))⟩ ∈ V) → {⟨(Hom ‘ndx), ℎ⟩, ⟨(comp‘ndx), (𝑎 ∈ (𝑣 × 𝑣), 𝑐 ∈ 𝑣 ↦ (𝑑 ∈ ((2nd ‘𝑎)ℎ𝑐), 𝑒 ∈ (ℎ‘𝑎) ↦ (𝑥 ∈ dom 𝑅 ↦ ((𝑑‘𝑥)(⟨((1st ‘𝑎)‘𝑥), ((2nd ‘𝑎)‘𝑥)⟩(comp‘(𝑅‘𝑥))(𝑐‘𝑥))(𝑒‘𝑥)))))⟩} ∈ V)
103	95, 101, 102	sylancr 414	. . . . . . . . 9 ⊢ ((𝑆 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊) → {⟨(Hom ‘ndx), ℎ⟩, ⟨(comp‘ndx), (𝑎 ∈ (𝑣 × 𝑣), 𝑐 ∈ 𝑣 ↦ (𝑑 ∈ ((2nd ‘𝑎)ℎ𝑐), 𝑒 ∈ (ℎ‘𝑎) ↦ (𝑥 ∈ dom 𝑅 ↦ ((𝑑‘𝑥)(⟨((1st ‘𝑎)‘𝑥), ((2nd ‘𝑎)‘𝑥)⟩(comp‘(𝑅‘𝑥))(𝑐‘𝑥))(𝑒‘𝑥)))))⟩} ∈ V)
104		unexg 4534	. . . . . . . . 9 ⊢ (({⟨(TopSet‘ndx), (∏t‘(TopOpen ∘ 𝑅))⟩, ⟨(le‘ndx), {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝑣 ∧ ∀𝑥 ∈ dom 𝑅(𝑓‘𝑥)(le‘(𝑅‘𝑥))(𝑔‘𝑥))}⟩, ⟨(dist‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ sup((ran (𝑥 ∈ dom 𝑅 ↦ ((𝑓‘𝑥)(dist‘(𝑅‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ*, < ))⟩} ∈ V ∧ {⟨(Hom ‘ndx), ℎ⟩, ⟨(comp‘ndx), (𝑎 ∈ (𝑣 × 𝑣), 𝑐 ∈ 𝑣 ↦ (𝑑 ∈ ((2nd ‘𝑎)ℎ𝑐), 𝑒 ∈ (ℎ‘𝑎) ↦ (𝑥 ∈ dom 𝑅 ↦ ((𝑑‘𝑥)(⟨((1st ‘𝑎)‘𝑥), ((2nd ‘𝑎)‘𝑥)⟩(comp‘(𝑅‘𝑥))(𝑐‘𝑥))(𝑒‘𝑥)))))⟩} ∈ V) → ({⟨(TopSet‘ndx), (∏t‘(TopOpen ∘ 𝑅))⟩, ⟨(le‘ndx), {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝑣 ∧ ∀𝑥 ∈ dom 𝑅(𝑓‘𝑥)(le‘(𝑅‘𝑥))(𝑔‘𝑥))}⟩, ⟨(dist‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ sup((ran (𝑥 ∈ dom 𝑅 ↦ ((𝑓‘𝑥)(dist‘(𝑅‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ*, < ))⟩} ∪ {⟨(Hom ‘ndx), ℎ⟩, ⟨(comp‘ndx), (𝑎 ∈ (𝑣 × 𝑣), 𝑐 ∈ 𝑣 ↦ (𝑑 ∈ ((2nd ‘𝑎)ℎ𝑐), 𝑒 ∈ (ℎ‘𝑎) ↦ (𝑥 ∈ dom 𝑅 ↦ ((𝑑‘𝑥)(⟨((1st ‘𝑎)‘𝑥), ((2nd ‘𝑎)‘𝑥)⟩(comp‘(𝑅‘𝑥))(𝑐‘𝑥))(𝑒‘𝑥)))))⟩}) ∈ V)
105	90, 103, 104	syl2anc 411	. . . . . . . 8 ⊢ ((𝑆 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊) → ({⟨(TopSet‘ndx), (∏t‘(TopOpen ∘ 𝑅))⟩, ⟨(le‘ndx), {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝑣 ∧ ∀𝑥 ∈ dom 𝑅(𝑓‘𝑥)(le‘(𝑅‘𝑥))(𝑔‘𝑥))}⟩, ⟨(dist‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ sup((ran (𝑥 ∈ dom 𝑅 ↦ ((𝑓‘𝑥)(dist‘(𝑅‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ*, < ))⟩} ∪ {⟨(Hom ‘ndx), ℎ⟩, ⟨(comp‘ndx), (𝑎 ∈ (𝑣 × 𝑣), 𝑐 ∈ 𝑣 ↦ (𝑑 ∈ ((2nd ‘𝑎)ℎ𝑐), 𝑒 ∈ (ℎ‘𝑎) ↦ (𝑥 ∈ dom 𝑅 ↦ ((𝑑‘𝑥)(⟨((1st ‘𝑎)‘𝑥), ((2nd ‘𝑎)‘𝑥)⟩(comp‘(𝑅‘𝑥))(𝑐‘𝑥))(𝑒‘𝑥)))))⟩}) ∈ V)
106		unexg 4534	. . . . . . . 8 ⊢ ((({⟨(Base‘ndx), 𝑣⟩, ⟨(+g‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑅 ↦ ((𝑓‘𝑥)(+g‘(𝑅‘𝑥))(𝑔‘𝑥))))⟩, ⟨(.r‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑅 ↦ ((𝑓‘𝑥)(.r‘(𝑅‘𝑥))(𝑔‘𝑥))))⟩} ∪ {⟨(Scalar‘ndx), 𝑆⟩, ⟨( ·𝑠 ‘ndx), (𝑓 ∈ (Base‘𝑆), 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑅 ↦ (𝑓( ·𝑠 ‘(𝑅‘𝑥))(𝑔‘𝑥))))⟩, ⟨(·𝑖‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑆 Σg (𝑥 ∈ dom 𝑅 ↦ ((𝑓‘𝑥)(·𝑖‘(𝑅‘𝑥))(𝑔‘𝑥)))))⟩}) ∈ V ∧ ({⟨(TopSet‘ndx), (∏t‘(TopOpen ∘ 𝑅))⟩, ⟨(le‘ndx), {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝑣 ∧ ∀𝑥 ∈ dom 𝑅(𝑓‘𝑥)(le‘(𝑅‘𝑥))(𝑔‘𝑥))}⟩, ⟨(dist‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ sup((ran (𝑥 ∈ dom 𝑅 ↦ ((𝑓‘𝑥)(dist‘(𝑅‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ*, < ))⟩} ∪ {⟨(Hom ‘ndx), ℎ⟩, ⟨(comp‘ndx), (𝑎 ∈ (𝑣 × 𝑣), 𝑐 ∈ 𝑣 ↦ (𝑑 ∈ ((2nd ‘𝑎)ℎ𝑐), 𝑒 ∈ (ℎ‘𝑎) ↦ (𝑥 ∈ dom 𝑅 ↦ ((𝑑‘𝑥)(⟨((1st ‘𝑎)‘𝑥), ((2nd ‘𝑎)‘𝑥)⟩(comp‘(𝑅‘𝑥))(𝑐‘𝑥))(𝑒‘𝑥)))))⟩}) ∈ V) → (({⟨(Base‘ndx), 𝑣⟩, ⟨(+g‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑅 ↦ ((𝑓‘𝑥)(+g‘(𝑅‘𝑥))(𝑔‘𝑥))))⟩, ⟨(.r‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑅 ↦ ((𝑓‘𝑥)(.r‘(𝑅‘𝑥))(𝑔‘𝑥))))⟩} ∪ {⟨(Scalar‘ndx), 𝑆⟩, ⟨( ·𝑠 ‘ndx), (𝑓 ∈ (Base‘𝑆), 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑅 ↦ (𝑓( ·𝑠 ‘(𝑅‘𝑥))(𝑔‘𝑥))))⟩, ⟨(·𝑖‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑆 Σg (𝑥 ∈ dom 𝑅 ↦ ((𝑓‘𝑥)(·𝑖‘(𝑅‘𝑥))(𝑔‘𝑥)))))⟩}) ∪ ({⟨(TopSet‘ndx), (∏t‘(TopOpen ∘ 𝑅))⟩, ⟨(le‘ndx), {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝑣 ∧ ∀𝑥 ∈ dom 𝑅(𝑓‘𝑥)(le‘(𝑅‘𝑥))(𝑔‘𝑥))}⟩, ⟨(dist‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ sup((ran (𝑥 ∈ dom 𝑅 ↦ ((𝑓‘𝑥)(dist‘(𝑅‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ*, < ))⟩} ∪ {⟨(Hom ‘ndx), ℎ⟩, ⟨(comp‘ndx), (𝑎 ∈ (𝑣 × 𝑣), 𝑐 ∈ 𝑣 ↦ (𝑑 ∈ ((2nd ‘𝑎)ℎ𝑐), 𝑒 ∈ (ℎ‘𝑎) ↦ (𝑥 ∈ dom 𝑅 ↦ ((𝑑‘𝑥)(⟨((1st ‘𝑎)‘𝑥), ((2nd ‘𝑎)‘𝑥)⟩(comp‘(𝑅‘𝑥))(𝑐‘𝑥))(𝑒‘𝑥)))))⟩})) ∈ V)
107	60, 105, 106	syl2anc 411	. . . . . . 7 ⊢ ((𝑆 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊) → (({⟨(Base‘ndx), 𝑣⟩, ⟨(+g‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑅 ↦ ((𝑓‘𝑥)(+g‘(𝑅‘𝑥))(𝑔‘𝑥))))⟩, ⟨(.r‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑅 ↦ ((𝑓‘𝑥)(.r‘(𝑅‘𝑥))(𝑔‘𝑥))))⟩} ∪ {⟨(Scalar‘ndx), 𝑆⟩, ⟨( ·𝑠 ‘ndx), (𝑓 ∈ (Base‘𝑆), 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑅 ↦ (𝑓( ·𝑠 ‘(𝑅‘𝑥))(𝑔‘𝑥))))⟩, ⟨(·𝑖‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑆 Σg (𝑥 ∈ dom 𝑅 ↦ ((𝑓‘𝑥)(·𝑖‘(𝑅‘𝑥))(𝑔‘𝑥)))))⟩}) ∪ ({⟨(TopSet‘ndx), (∏t‘(TopOpen ∘ 𝑅))⟩, ⟨(le‘ndx), {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝑣 ∧ ∀𝑥 ∈ dom 𝑅(𝑓‘𝑥)(le‘(𝑅‘𝑥))(𝑔‘𝑥))}⟩, ⟨(dist‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ sup((ran (𝑥 ∈ dom 𝑅 ↦ ((𝑓‘𝑥)(dist‘(𝑅‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ*, < ))⟩} ∪ {⟨(Hom ‘ndx), ℎ⟩, ⟨(comp‘ndx), (𝑎 ∈ (𝑣 × 𝑣), 𝑐 ∈ 𝑣 ↦ (𝑑 ∈ ((2nd ‘𝑎)ℎ𝑐), 𝑒 ∈ (ℎ‘𝑎) ↦ (𝑥 ∈ dom 𝑅 ↦ ((𝑑‘𝑥)(⟨((1st ‘𝑎)‘𝑥), ((2nd ‘𝑎)‘𝑥)⟩(comp‘(𝑅‘𝑥))(𝑐‘𝑥))(𝑒‘𝑥)))))⟩})) ∈ V)
108	107	alrimiv 1920	. . . . . 6 ⊢ ((𝑆 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊) → ∀ℎ(({⟨(Base‘ndx), 𝑣⟩, ⟨(+g‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑅 ↦ ((𝑓‘𝑥)(+g‘(𝑅‘𝑥))(𝑔‘𝑥))))⟩, ⟨(.r‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑅 ↦ ((𝑓‘𝑥)(.r‘(𝑅‘𝑥))(𝑔‘𝑥))))⟩} ∪ {⟨(Scalar‘ndx), 𝑆⟩, ⟨( ·𝑠 ‘ndx), (𝑓 ∈ (Base‘𝑆), 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑅 ↦ (𝑓( ·𝑠 ‘(𝑅‘𝑥))(𝑔‘𝑥))))⟩, ⟨(·𝑖‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑆 Σg (𝑥 ∈ dom 𝑅 ↦ ((𝑓‘𝑥)(·𝑖‘(𝑅‘𝑥))(𝑔‘𝑥)))))⟩}) ∪ ({⟨(TopSet‘ndx), (∏t‘(TopOpen ∘ 𝑅))⟩, ⟨(le‘ndx), {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝑣 ∧ ∀𝑥 ∈ dom 𝑅(𝑓‘𝑥)(le‘(𝑅‘𝑥))(𝑔‘𝑥))}⟩, ⟨(dist‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ sup((ran (𝑥 ∈ dom 𝑅 ↦ ((𝑓‘𝑥)(dist‘(𝑅‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ*, < ))⟩} ∪ {⟨(Hom ‘ndx), ℎ⟩, ⟨(comp‘ndx), (𝑎 ∈ (𝑣 × 𝑣), 𝑐 ∈ 𝑣 ↦ (𝑑 ∈ ((2nd ‘𝑎)ℎ𝑐), 𝑒 ∈ (ℎ‘𝑎) ↦ (𝑥 ∈ dom 𝑅 ↦ ((𝑑‘𝑥)(⟨((1st ‘𝑎)‘𝑥), ((2nd ‘𝑎)‘𝑥)⟩(comp‘(𝑅‘𝑥))(𝑐‘𝑥))(𝑒‘𝑥)))))⟩})) ∈ V)
109		csbexga 4212	. . . . . 6 ⊢ (((𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ X𝑥 ∈ dom 𝑅((𝑓‘𝑥)(Hom ‘(𝑅‘𝑥))(𝑔‘𝑥))) ∈ V ∧ ∀ℎ(({⟨(Base‘ndx), 𝑣⟩, ⟨(+g‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑅 ↦ ((𝑓‘𝑥)(+g‘(𝑅‘𝑥))(𝑔‘𝑥))))⟩, ⟨(.r‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑅 ↦ ((𝑓‘𝑥)(.r‘(𝑅‘𝑥))(𝑔‘𝑥))))⟩} ∪ {⟨(Scalar‘ndx), 𝑆⟩, ⟨( ·𝑠 ‘ndx), (𝑓 ∈ (Base‘𝑆), 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑅 ↦ (𝑓( ·𝑠 ‘(𝑅‘𝑥))(𝑔‘𝑥))))⟩, ⟨(·𝑖‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑆 Σg (𝑥 ∈ dom 𝑅 ↦ ((𝑓‘𝑥)(·𝑖‘(𝑅‘𝑥))(𝑔‘𝑥)))))⟩}) ∪ ({⟨(TopSet‘ndx), (∏t‘(TopOpen ∘ 𝑅))⟩, ⟨(le‘ndx), {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝑣 ∧ ∀𝑥 ∈ dom 𝑅(𝑓‘𝑥)(le‘(𝑅‘𝑥))(𝑔‘𝑥))}⟩, ⟨(dist‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ sup((ran (𝑥 ∈ dom 𝑅 ↦ ((𝑓‘𝑥)(dist‘(𝑅‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ*, < ))⟩} ∪ {⟨(Hom ‘ndx), ℎ⟩, ⟨(comp‘ndx), (𝑎 ∈ (𝑣 × 𝑣), 𝑐 ∈ 𝑣 ↦ (𝑑 ∈ ((2nd ‘𝑎)ℎ𝑐), 𝑒 ∈ (ℎ‘𝑎) ↦ (𝑥 ∈ dom 𝑅 ↦ ((𝑑‘𝑥)(⟨((1st ‘𝑎)‘𝑥), ((2nd ‘𝑎)‘𝑥)⟩(comp‘(𝑅‘𝑥))(𝑐‘𝑥))(𝑒‘𝑥)))))⟩})) ∈ V) → ⦋(𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ X𝑥 ∈ dom 𝑅((𝑓‘𝑥)(Hom ‘(𝑅‘𝑥))(𝑔‘𝑥))) / ℎ⦌(({⟨(Base‘ndx), 𝑣⟩, ⟨(+g‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑅 ↦ ((𝑓‘𝑥)(+g‘(𝑅‘𝑥))(𝑔‘𝑥))))⟩, ⟨(.r‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑅 ↦ ((𝑓‘𝑥)(.r‘(𝑅‘𝑥))(𝑔‘𝑥))))⟩} ∪ {⟨(Scalar‘ndx), 𝑆⟩, ⟨( ·𝑠 ‘ndx), (𝑓 ∈ (Base‘𝑆), 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑅 ↦ (𝑓( ·𝑠 ‘(𝑅‘𝑥))(𝑔‘𝑥))))⟩, ⟨(·𝑖‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑆 Σg (𝑥 ∈ dom 𝑅 ↦ ((𝑓‘𝑥)(·𝑖‘(𝑅‘𝑥))(𝑔‘𝑥)))))⟩}) ∪ ({⟨(TopSet‘ndx), (∏t‘(TopOpen ∘ 𝑅))⟩, ⟨(le‘ndx), {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝑣 ∧ ∀𝑥 ∈ dom 𝑅(𝑓‘𝑥)(le‘(𝑅‘𝑥))(𝑔‘𝑥))}⟩, ⟨(dist‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ sup((ran (𝑥 ∈ dom 𝑅 ↦ ((𝑓‘𝑥)(dist‘(𝑅‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ*, < ))⟩} ∪ {⟨(Hom ‘ndx), ℎ⟩, ⟨(comp‘ndx), (𝑎 ∈ (𝑣 × 𝑣), 𝑐 ∈ 𝑣 ↦ (𝑑 ∈ ((2nd ‘𝑎)ℎ𝑐), 𝑒 ∈ (ℎ‘𝑎) ↦ (𝑥 ∈ dom 𝑅 ↦ ((𝑑‘𝑥)(⟨((1st ‘𝑎)‘𝑥), ((2nd ‘𝑎)‘𝑥)⟩(comp‘(𝑅‘𝑥))(𝑐‘𝑥))(𝑒‘𝑥)))))⟩})) ∈ V)
110	18, 108, 109	sylancr 414	. . . . 5 ⊢ ((𝑆 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊) → ⦋(𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ X𝑥 ∈ dom 𝑅((𝑓‘𝑥)(Hom ‘(𝑅‘𝑥))(𝑔‘𝑥))) / ℎ⦌(({⟨(Base‘ndx), 𝑣⟩, ⟨(+g‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑅 ↦ ((𝑓‘𝑥)(+g‘(𝑅‘𝑥))(𝑔‘𝑥))))⟩, ⟨(.r‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑅 ↦ ((𝑓‘𝑥)(.r‘(𝑅‘𝑥))(𝑔‘𝑥))))⟩} ∪ {⟨(Scalar‘ndx), 𝑆⟩, ⟨( ·𝑠 ‘ndx), (𝑓 ∈ (Base‘𝑆), 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑅 ↦ (𝑓( ·𝑠 ‘(𝑅‘𝑥))(𝑔‘𝑥))))⟩, ⟨(·𝑖‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑆 Σg (𝑥 ∈ dom 𝑅 ↦ ((𝑓‘𝑥)(·𝑖‘(𝑅‘𝑥))(𝑔‘𝑥)))))⟩}) ∪ ({⟨(TopSet‘ndx), (∏t‘(TopOpen ∘ 𝑅))⟩, ⟨(le‘ndx), {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝑣 ∧ ∀𝑥 ∈ dom 𝑅(𝑓‘𝑥)(le‘(𝑅‘𝑥))(𝑔‘𝑥))}⟩, ⟨(dist‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ sup((ran (𝑥 ∈ dom 𝑅 ↦ ((𝑓‘𝑥)(dist‘(𝑅‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ*, < ))⟩} ∪ {⟨(Hom ‘ndx), ℎ⟩, ⟨(comp‘ndx), (𝑎 ∈ (𝑣 × 𝑣), 𝑐 ∈ 𝑣 ↦ (𝑑 ∈ ((2nd ‘𝑎)ℎ𝑐), 𝑒 ∈ (ℎ‘𝑎) ↦ (𝑥 ∈ dom 𝑅 ↦ ((𝑑‘𝑥)(⟨((1st ‘𝑎)‘𝑥), ((2nd ‘𝑎)‘𝑥)⟩(comp‘(𝑅‘𝑥))(𝑐‘𝑥))(𝑒‘𝑥)))))⟩})) ∈ V)
111	110	alrimiv 1920	. . . 4 ⊢ ((𝑆 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊) → ∀𝑣⦋(𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ X𝑥 ∈ dom 𝑅((𝑓‘𝑥)(Hom ‘(𝑅‘𝑥))(𝑔‘𝑥))) / ℎ⦌(({⟨(Base‘ndx), 𝑣⟩, ⟨(+g‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑅 ↦ ((𝑓‘𝑥)(+g‘(𝑅‘𝑥))(𝑔‘𝑥))))⟩, ⟨(.r‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑅 ↦ ((𝑓‘𝑥)(.r‘(𝑅‘𝑥))(𝑔‘𝑥))))⟩} ∪ {⟨(Scalar‘ndx), 𝑆⟩, ⟨( ·𝑠 ‘ndx), (𝑓 ∈ (Base‘𝑆), 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑅 ↦ (𝑓( ·𝑠 ‘(𝑅‘𝑥))(𝑔‘𝑥))))⟩, ⟨(·𝑖‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑆 Σg (𝑥 ∈ dom 𝑅 ↦ ((𝑓‘𝑥)(·𝑖‘(𝑅‘𝑥))(𝑔‘𝑥)))))⟩}) ∪ ({⟨(TopSet‘ndx), (∏t‘(TopOpen ∘ 𝑅))⟩, ⟨(le‘ndx), {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝑣 ∧ ∀𝑥 ∈ dom 𝑅(𝑓‘𝑥)(le‘(𝑅‘𝑥))(𝑔‘𝑥))}⟩, ⟨(dist‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ sup((ran (𝑥 ∈ dom 𝑅 ↦ ((𝑓‘𝑥)(dist‘(𝑅‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ*, < ))⟩} ∪ {⟨(Hom ‘ndx), ℎ⟩, ⟨(comp‘ndx), (𝑎 ∈ (𝑣 × 𝑣), 𝑐 ∈ 𝑣 ↦ (𝑑 ∈ ((2nd ‘𝑎)ℎ𝑐), 𝑒 ∈ (ℎ‘𝑎) ↦ (𝑥 ∈ dom 𝑅 ↦ ((𝑑‘𝑥)(⟨((1st ‘𝑎)‘𝑥), ((2nd ‘𝑎)‘𝑥)⟩(comp‘(𝑅‘𝑥))(𝑐‘𝑥))(𝑒‘𝑥)))))⟩})) ∈ V)
112		csbexga 4212	. . . 4 ⊢ ((X𝑥 ∈ dom 𝑅(Base‘(𝑅‘𝑥)) ∈ V ∧ ∀𝑣⦋(𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ X𝑥 ∈ dom 𝑅((𝑓‘𝑥)(Hom ‘(𝑅‘𝑥))(𝑔‘𝑥))) / ℎ⦌(({⟨(Base‘ndx), 𝑣⟩, ⟨(+g‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑅 ↦ ((𝑓‘𝑥)(+g‘(𝑅‘𝑥))(𝑔‘𝑥))))⟩, ⟨(.r‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑅 ↦ ((𝑓‘𝑥)(.r‘(𝑅‘𝑥))(𝑔‘𝑥))))⟩} ∪ {⟨(Scalar‘ndx), 𝑆⟩, ⟨( ·𝑠 ‘ndx), (𝑓 ∈ (Base‘𝑆), 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑅 ↦ (𝑓( ·𝑠 ‘(𝑅‘𝑥))(𝑔‘𝑥))))⟩, ⟨(·𝑖‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑆 Σg (𝑥 ∈ dom 𝑅 ↦ ((𝑓‘𝑥)(·𝑖‘(𝑅‘𝑥))(𝑔‘𝑥)))))⟩}) ∪ ({⟨(TopSet‘ndx), (∏t‘(TopOpen ∘ 𝑅))⟩, ⟨(le‘ndx), {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝑣 ∧ ∀𝑥 ∈ dom 𝑅(𝑓‘𝑥)(le‘(𝑅‘𝑥))(𝑔‘𝑥))}⟩, ⟨(dist‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ sup((ran (𝑥 ∈ dom 𝑅 ↦ ((𝑓‘𝑥)(dist‘(𝑅‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ*, < ))⟩} ∪ {⟨(Hom ‘ndx), ℎ⟩, ⟨(comp‘ndx), (𝑎 ∈ (𝑣 × 𝑣), 𝑐 ∈ 𝑣 ↦ (𝑑 ∈ ((2nd ‘𝑎)ℎ𝑐), 𝑒 ∈ (ℎ‘𝑎) ↦ (𝑥 ∈ dom 𝑅 ↦ ((𝑑‘𝑥)(⟨((1st ‘𝑎)‘𝑥), ((2nd ‘𝑎)‘𝑥)⟩(comp‘(𝑅‘𝑥))(𝑐‘𝑥))(𝑒‘𝑥)))))⟩})) ∈ V) → ⦋X𝑥 ∈ dom 𝑅(Base‘(𝑅‘𝑥)) / 𝑣⦌⦋(𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ X𝑥 ∈ dom 𝑅((𝑓‘𝑥)(Hom ‘(𝑅‘𝑥))(𝑔‘𝑥))) / ℎ⦌(({⟨(Base‘ndx), 𝑣⟩, ⟨(+g‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑅 ↦ ((𝑓‘𝑥)(+g‘(𝑅‘𝑥))(𝑔‘𝑥))))⟩, ⟨(.r‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑅 ↦ ((𝑓‘𝑥)(.r‘(𝑅‘𝑥))(𝑔‘𝑥))))⟩} ∪ {⟨(Scalar‘ndx), 𝑆⟩, ⟨( ·𝑠 ‘ndx), (𝑓 ∈ (Base‘𝑆), 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑅 ↦ (𝑓( ·𝑠 ‘(𝑅‘𝑥))(𝑔‘𝑥))))⟩, ⟨(·𝑖‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑆 Σg (𝑥 ∈ dom 𝑅 ↦ ((𝑓‘𝑥)(·𝑖‘(𝑅‘𝑥))(𝑔‘𝑥)))))⟩}) ∪ ({⟨(TopSet‘ndx), (∏t‘(TopOpen ∘ 𝑅))⟩, ⟨(le‘ndx), {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝑣 ∧ ∀𝑥 ∈ dom 𝑅(𝑓‘𝑥)(le‘(𝑅‘𝑥))(𝑔‘𝑥))}⟩, ⟨(dist‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ sup((ran (𝑥 ∈ dom 𝑅 ↦ ((𝑓‘𝑥)(dist‘(𝑅‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ*, < ))⟩} ∪ {⟨(Hom ‘ndx), ℎ⟩, ⟨(comp‘ndx), (𝑎 ∈ (𝑣 × 𝑣), 𝑐 ∈ 𝑣 ↦ (𝑑 ∈ ((2nd ‘𝑎)ℎ𝑐), 𝑒 ∈ (ℎ‘𝑎) ↦ (𝑥 ∈ dom 𝑅 ↦ ((𝑑‘𝑥)(⟨((1st ‘𝑎)‘𝑥), ((2nd ‘𝑎)‘𝑥)⟩(comp‘(𝑅‘𝑥))(𝑐‘𝑥))(𝑒‘𝑥)))))⟩})) ∈ V)
113	16, 111, 112	syl2anc 411	. . 3 ⊢ ((𝑆 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊) → ⦋X𝑥 ∈ dom 𝑅(Base‘(𝑅‘𝑥)) / 𝑣⦌⦋(𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ X𝑥 ∈ dom 𝑅((𝑓‘𝑥)(Hom ‘(𝑅‘𝑥))(𝑔‘𝑥))) / ℎ⦌(({⟨(Base‘ndx), 𝑣⟩, ⟨(+g‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑅 ↦ ((𝑓‘𝑥)(+g‘(𝑅‘𝑥))(𝑔‘𝑥))))⟩, ⟨(.r‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑅 ↦ ((𝑓‘𝑥)(.r‘(𝑅‘𝑥))(𝑔‘𝑥))))⟩} ∪ {⟨(Scalar‘ndx), 𝑆⟩, ⟨( ·𝑠 ‘ndx), (𝑓 ∈ (Base‘𝑆), 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑅 ↦ (𝑓( ·𝑠 ‘(𝑅‘𝑥))(𝑔‘𝑥))))⟩, ⟨(·𝑖‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑆 Σg (𝑥 ∈ dom 𝑅 ↦ ((𝑓‘𝑥)(·𝑖‘(𝑅‘𝑥))(𝑔‘𝑥)))))⟩}) ∪ ({⟨(TopSet‘ndx), (∏t‘(TopOpen ∘ 𝑅))⟩, ⟨(le‘ndx), {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝑣 ∧ ∀𝑥 ∈ dom 𝑅(𝑓‘𝑥)(le‘(𝑅‘𝑥))(𝑔‘𝑥))}⟩, ⟨(dist‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ sup((ran (𝑥 ∈ dom 𝑅 ↦ ((𝑓‘𝑥)(dist‘(𝑅‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ*, < ))⟩} ∪ {⟨(Hom ‘ndx), ℎ⟩, ⟨(comp‘ndx), (𝑎 ∈ (𝑣 × 𝑣), 𝑐 ∈ 𝑣 ↦ (𝑑 ∈ ((2nd ‘𝑎)ℎ𝑐), 𝑒 ∈ (ℎ‘𝑎) ↦ (𝑥 ∈ dom 𝑅 ↦ ((𝑑‘𝑥)(⟨((1st ‘𝑎)‘𝑥), ((2nd ‘𝑎)‘𝑥)⟩(comp‘(𝑅‘𝑥))(𝑐‘𝑥))(𝑒‘𝑥)))))⟩})) ∈ V)
114		dmeq 4923	. . . . . . . . 9 ⊢ (𝑟 = 𝑅 → dom 𝑟 = dom 𝑅)
115	114	ixpeq1d 6857	. . . . . . . 8 ⊢ (𝑟 = 𝑅 → X𝑥 ∈ dom 𝑟(Base‘(𝑟‘𝑥)) = X𝑥 ∈ dom 𝑅(Base‘(𝑟‘𝑥)))
116		fveq1 5626	. . . . . . . . . 10 ⊢ (𝑟 = 𝑅 → (𝑟‘𝑥) = (𝑅‘𝑥))
117	116	fveq2d 5631	. . . . . . . . 9 ⊢ (𝑟 = 𝑅 → (Base‘(𝑟‘𝑥)) = (Base‘(𝑅‘𝑥)))
118	117	ixpeq2dv 6861	. . . . . . . 8 ⊢ (𝑟 = 𝑅 → X𝑥 ∈ dom 𝑅(Base‘(𝑟‘𝑥)) = X𝑥 ∈ dom 𝑅(Base‘(𝑅‘𝑥)))
119	115, 118	eqtrd 2262	. . . . . . 7 ⊢ (𝑟 = 𝑅 → X𝑥 ∈ dom 𝑟(Base‘(𝑟‘𝑥)) = X𝑥 ∈ dom 𝑅(Base‘(𝑅‘𝑥)))
120	119	adantl 277	. . . . . 6 ⊢ ((𝑠 = 𝑆 ∧ 𝑟 = 𝑅) → X𝑥 ∈ dom 𝑟(Base‘(𝑟‘𝑥)) = X𝑥 ∈ dom 𝑅(Base‘(𝑅‘𝑥)))
121	120	csbeq1d 3131	. . . . 5 ⊢ ((𝑠 = 𝑆 ∧ 𝑟 = 𝑅) → ⦋X𝑥 ∈ dom 𝑟(Base‘(𝑟‘𝑥)) / 𝑣⦌⦋(𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ X𝑥 ∈ dom 𝑟((𝑓‘𝑥)(Hom ‘(𝑟‘𝑥))(𝑔‘𝑥))) / ℎ⦌(({⟨(Base‘ndx), 𝑣⟩, ⟨(+g‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(+g‘(𝑟‘𝑥))(𝑔‘𝑥))))⟩, ⟨(.r‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(.r‘(𝑟‘𝑥))(𝑔‘𝑥))))⟩} ∪ {⟨(Scalar‘ndx), 𝑠⟩, ⟨( ·𝑠 ‘ndx), (𝑓 ∈ (Base‘𝑠), 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ (𝑓( ·𝑠 ‘(𝑟‘𝑥))(𝑔‘𝑥))))⟩, ⟨(·𝑖‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑠 Σg (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(·𝑖‘(𝑟‘𝑥))(𝑔‘𝑥)))))⟩}) ∪ ({⟨(TopSet‘ndx), (∏t‘(TopOpen ∘ 𝑟))⟩, ⟨(le‘ndx), {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝑣 ∧ ∀𝑥 ∈ dom 𝑟(𝑓‘𝑥)(le‘(𝑟‘𝑥))(𝑔‘𝑥))}⟩, ⟨(dist‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ sup((ran (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(dist‘(𝑟‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ*, < ))⟩} ∪ {⟨(Hom ‘ndx), ℎ⟩, ⟨(comp‘ndx), (𝑎 ∈ (𝑣 × 𝑣), 𝑐 ∈ 𝑣 ↦ (𝑑 ∈ ((2nd ‘𝑎)ℎ𝑐), 𝑒 ∈ (ℎ‘𝑎) ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑑‘𝑥)(⟨((1st ‘𝑎)‘𝑥), ((2nd ‘𝑎)‘𝑥)⟩(comp‘(𝑟‘𝑥))(𝑐‘𝑥))(𝑒‘𝑥)))))⟩})) = ⦋X𝑥 ∈ dom 𝑅(Base‘(𝑅‘𝑥)) / 𝑣⦌⦋(𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ X𝑥 ∈ dom 𝑟((𝑓‘𝑥)(Hom ‘(𝑟‘𝑥))(𝑔‘𝑥))) / ℎ⦌(({⟨(Base‘ndx), 𝑣⟩, ⟨(+g‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(+g‘(𝑟‘𝑥))(𝑔‘𝑥))))⟩, ⟨(.r‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(.r‘(𝑟‘𝑥))(𝑔‘𝑥))))⟩} ∪ {⟨(Scalar‘ndx), 𝑠⟩, ⟨( ·𝑠 ‘ndx), (𝑓 ∈ (Base‘𝑠), 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ (𝑓( ·𝑠 ‘(𝑟‘𝑥))(𝑔‘𝑥))))⟩, ⟨(·𝑖‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑠 Σg (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(·𝑖‘(𝑟‘𝑥))(𝑔‘𝑥)))))⟩}) ∪ ({⟨(TopSet‘ndx), (∏t‘(TopOpen ∘ 𝑟))⟩, ⟨(le‘ndx), {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝑣 ∧ ∀𝑥 ∈ dom 𝑟(𝑓‘𝑥)(le‘(𝑟‘𝑥))(𝑔‘𝑥))}⟩, ⟨(dist‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ sup((ran (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(dist‘(𝑟‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ*, < ))⟩} ∪ {⟨(Hom ‘ndx), ℎ⟩, ⟨(comp‘ndx), (𝑎 ∈ (𝑣 × 𝑣), 𝑐 ∈ 𝑣 ↦ (𝑑 ∈ ((2nd ‘𝑎)ℎ𝑐), 𝑒 ∈ (ℎ‘𝑎) ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑑‘𝑥)(⟨((1st ‘𝑎)‘𝑥), ((2nd ‘𝑎)‘𝑥)⟩(comp‘(𝑟‘𝑥))(𝑐‘𝑥))(𝑒‘𝑥)))))⟩})))
122	114	adantl 277	. . . . . . . . . . 11 ⊢ ((𝑠 = 𝑆 ∧ 𝑟 = 𝑅) → dom 𝑟 = dom 𝑅)
123	122	ixpeq1d 6857	. . . . . . . . . 10 ⊢ ((𝑠 = 𝑆 ∧ 𝑟 = 𝑅) → X𝑥 ∈ dom 𝑟((𝑓‘𝑥)(Hom ‘(𝑟‘𝑥))(𝑔‘𝑥)) = X𝑥 ∈ dom 𝑅((𝑓‘𝑥)(Hom ‘(𝑟‘𝑥))(𝑔‘𝑥)))
124		simpr 110	. . . . . . . . . . . . . 14 ⊢ ((𝑠 = 𝑆 ∧ 𝑟 = 𝑅) → 𝑟 = 𝑅)
125	124	fveq1d 5629	. . . . . . . . . . . . 13 ⊢ ((𝑠 = 𝑆 ∧ 𝑟 = 𝑅) → (𝑟‘𝑥) = (𝑅‘𝑥))
126	125	fveq2d 5631	. . . . . . . . . . . 12 ⊢ ((𝑠 = 𝑆 ∧ 𝑟 = 𝑅) → (Hom ‘(𝑟‘𝑥)) = (Hom ‘(𝑅‘𝑥)))
127	126	oveqd 6018	. . . . . . . . . . 11 ⊢ ((𝑠 = 𝑆 ∧ 𝑟 = 𝑅) → ((𝑓‘𝑥)(Hom ‘(𝑟‘𝑥))(𝑔‘𝑥)) = ((𝑓‘𝑥)(Hom ‘(𝑅‘𝑥))(𝑔‘𝑥)))
128	127	ixpeq2dv 6861	. . . . . . . . . 10 ⊢ ((𝑠 = 𝑆 ∧ 𝑟 = 𝑅) → X𝑥 ∈ dom 𝑅((𝑓‘𝑥)(Hom ‘(𝑟‘𝑥))(𝑔‘𝑥)) = X𝑥 ∈ dom 𝑅((𝑓‘𝑥)(Hom ‘(𝑅‘𝑥))(𝑔‘𝑥)))
129	123, 128	eqtrd 2262	. . . . . . . . 9 ⊢ ((𝑠 = 𝑆 ∧ 𝑟 = 𝑅) → X𝑥 ∈ dom 𝑟((𝑓‘𝑥)(Hom ‘(𝑟‘𝑥))(𝑔‘𝑥)) = X𝑥 ∈ dom 𝑅((𝑓‘𝑥)(Hom ‘(𝑅‘𝑥))(𝑔‘𝑥)))
130	129	mpoeq3dv 6070	. . . . . . . 8 ⊢ ((𝑠 = 𝑆 ∧ 𝑟 = 𝑅) → (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ X𝑥 ∈ dom 𝑟((𝑓‘𝑥)(Hom ‘(𝑟‘𝑥))(𝑔‘𝑥))) = (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ X𝑥 ∈ dom 𝑅((𝑓‘𝑥)(Hom ‘(𝑅‘𝑥))(𝑔‘𝑥))))
131	130	csbeq1d 3131	. . . . . . 7 ⊢ ((𝑠 = 𝑆 ∧ 𝑟 = 𝑅) → ⦋(𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ X𝑥 ∈ dom 𝑟((𝑓‘𝑥)(Hom ‘(𝑟‘𝑥))(𝑔‘𝑥))) / ℎ⦌(({⟨(Base‘ndx), 𝑣⟩, ⟨(+g‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(+g‘(𝑟‘𝑥))(𝑔‘𝑥))))⟩, ⟨(.r‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(.r‘(𝑟‘𝑥))(𝑔‘𝑥))))⟩} ∪ {⟨(Scalar‘ndx), 𝑠⟩, ⟨( ·𝑠 ‘ndx), (𝑓 ∈ (Base‘𝑠), 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ (𝑓( ·𝑠 ‘(𝑟‘𝑥))(𝑔‘𝑥))))⟩, ⟨(·𝑖‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑠 Σg (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(·𝑖‘(𝑟‘𝑥))(𝑔‘𝑥)))))⟩}) ∪ ({⟨(TopSet‘ndx), (∏t‘(TopOpen ∘ 𝑟))⟩, ⟨(le‘ndx), {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝑣 ∧ ∀𝑥 ∈ dom 𝑟(𝑓‘𝑥)(le‘(𝑟‘𝑥))(𝑔‘𝑥))}⟩, ⟨(dist‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ sup((ran (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(dist‘(𝑟‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ*, < ))⟩} ∪ {⟨(Hom ‘ndx), ℎ⟩, ⟨(comp‘ndx), (𝑎 ∈ (𝑣 × 𝑣), 𝑐 ∈ 𝑣 ↦ (𝑑 ∈ ((2nd ‘𝑎)ℎ𝑐), 𝑒 ∈ (ℎ‘𝑎) ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑑‘𝑥)(⟨((1st ‘𝑎)‘𝑥), ((2nd ‘𝑎)‘𝑥)⟩(comp‘(𝑟‘𝑥))(𝑐‘𝑥))(𝑒‘𝑥)))))⟩})) = ⦋(𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ X𝑥 ∈ dom 𝑅((𝑓‘𝑥)(Hom ‘(𝑅‘𝑥))(𝑔‘𝑥))) / ℎ⦌(({⟨(Base‘ndx), 𝑣⟩, ⟨(+g‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(+g‘(𝑟‘𝑥))(𝑔‘𝑥))))⟩, ⟨(.r‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(.r‘(𝑟‘𝑥))(𝑔‘𝑥))))⟩} ∪ {⟨(Scalar‘ndx), 𝑠⟩, ⟨( ·𝑠 ‘ndx), (𝑓 ∈ (Base‘𝑠), 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ (𝑓( ·𝑠 ‘(𝑟‘𝑥))(𝑔‘𝑥))))⟩, ⟨(·𝑖‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑠 Σg (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(·𝑖‘(𝑟‘𝑥))(𝑔‘𝑥)))))⟩}) ∪ ({⟨(TopSet‘ndx), (∏t‘(TopOpen ∘ 𝑟))⟩, ⟨(le‘ndx), {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝑣 ∧ ∀𝑥 ∈ dom 𝑟(𝑓‘𝑥)(le‘(𝑟‘𝑥))(𝑔‘𝑥))}⟩, ⟨(dist‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ sup((ran (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(dist‘(𝑟‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ*, < ))⟩} ∪ {⟨(Hom ‘ndx), ℎ⟩, ⟨(comp‘ndx), (𝑎 ∈ (𝑣 × 𝑣), 𝑐 ∈ 𝑣 ↦ (𝑑 ∈ ((2nd ‘𝑎)ℎ𝑐), 𝑒 ∈ (ℎ‘𝑎) ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑑‘𝑥)(⟨((1st ‘𝑎)‘𝑥), ((2nd ‘𝑎)‘𝑥)⟩(comp‘(𝑟‘𝑥))(𝑐‘𝑥))(𝑒‘𝑥)))))⟩})))
132		eqidd 2230	. . . . . . . . . . 11 ⊢ ((𝑠 = 𝑆 ∧ 𝑟 = 𝑅) → ⟨(Base‘ndx), 𝑣⟩ = ⟨(Base‘ndx), 𝑣⟩)
133	125	fveq2d 5631	. . . . . . . . . . . . . . 15 ⊢ ((𝑠 = 𝑆 ∧ 𝑟 = 𝑅) → (+g‘(𝑟‘𝑥)) = (+g‘(𝑅‘𝑥)))
134	133	oveqd 6018	. . . . . . . . . . . . . 14 ⊢ ((𝑠 = 𝑆 ∧ 𝑟 = 𝑅) → ((𝑓‘𝑥)(+g‘(𝑟‘𝑥))(𝑔‘𝑥)) = ((𝑓‘𝑥)(+g‘(𝑅‘𝑥))(𝑔‘𝑥)))
135	122, 134	mpteq12dv 4166	. . . . . . . . . . . . 13 ⊢ ((𝑠 = 𝑆 ∧ 𝑟 = 𝑅) → (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(+g‘(𝑟‘𝑥))(𝑔‘𝑥))) = (𝑥 ∈ dom 𝑅 ↦ ((𝑓‘𝑥)(+g‘(𝑅‘𝑥))(𝑔‘𝑥))))
136	135	mpoeq3dv 6070	. . . . . . . . . . . 12 ⊢ ((𝑠 = 𝑆 ∧ 𝑟 = 𝑅) → (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(+g‘(𝑟‘𝑥))(𝑔‘𝑥)))) = (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑅 ↦ ((𝑓‘𝑥)(+g‘(𝑅‘𝑥))(𝑔‘𝑥)))))
137	136	opeq2d 3864	. . . . . . . . . . 11 ⊢ ((𝑠 = 𝑆 ∧ 𝑟 = 𝑅) → ⟨(+g‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(+g‘(𝑟‘𝑥))(𝑔‘𝑥))))⟩ = ⟨(+g‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑅 ↦ ((𝑓‘𝑥)(+g‘(𝑅‘𝑥))(𝑔‘𝑥))))⟩)
138	125	fveq2d 5631	. . . . . . . . . . . . . . 15 ⊢ ((𝑠 = 𝑆 ∧ 𝑟 = 𝑅) → (.r‘(𝑟‘𝑥)) = (.r‘(𝑅‘𝑥)))
139	138	oveqd 6018	. . . . . . . . . . . . . 14 ⊢ ((𝑠 = 𝑆 ∧ 𝑟 = 𝑅) → ((𝑓‘𝑥)(.r‘(𝑟‘𝑥))(𝑔‘𝑥)) = ((𝑓‘𝑥)(.r‘(𝑅‘𝑥))(𝑔‘𝑥)))
140	122, 139	mpteq12dv 4166	. . . . . . . . . . . . 13 ⊢ ((𝑠 = 𝑆 ∧ 𝑟 = 𝑅) → (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(.r‘(𝑟‘𝑥))(𝑔‘𝑥))) = (𝑥 ∈ dom 𝑅 ↦ ((𝑓‘𝑥)(.r‘(𝑅‘𝑥))(𝑔‘𝑥))))
141	140	mpoeq3dv 6070	. . . . . . . . . . . 12 ⊢ ((𝑠 = 𝑆 ∧ 𝑟 = 𝑅) → (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(.r‘(𝑟‘𝑥))(𝑔‘𝑥)))) = (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑅 ↦ ((𝑓‘𝑥)(.r‘(𝑅‘𝑥))(𝑔‘𝑥)))))
142	141	opeq2d 3864	. . . . . . . . . . 11 ⊢ ((𝑠 = 𝑆 ∧ 𝑟 = 𝑅) → ⟨(.r‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(.r‘(𝑟‘𝑥))(𝑔‘𝑥))))⟩ = ⟨(.r‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑅 ↦ ((𝑓‘𝑥)(.r‘(𝑅‘𝑥))(𝑔‘𝑥))))⟩)
143	132, 137, 142	tpeq123d 3758	. . . . . . . . . 10 ⊢ ((𝑠 = 𝑆 ∧ 𝑟 = 𝑅) → {⟨(Base‘ndx), 𝑣⟩, ⟨(+g‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(+g‘(𝑟‘𝑥))(𝑔‘𝑥))))⟩, ⟨(.r‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(.r‘(𝑟‘𝑥))(𝑔‘𝑥))))⟩} = {⟨(Base‘ndx), 𝑣⟩, ⟨(+g‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑅 ↦ ((𝑓‘𝑥)(+g‘(𝑅‘𝑥))(𝑔‘𝑥))))⟩, ⟨(.r‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑅 ↦ ((𝑓‘𝑥)(.r‘(𝑅‘𝑥))(𝑔‘𝑥))))⟩})
144		simpl 109	. . . . . . . . . . . 12 ⊢ ((𝑠 = 𝑆 ∧ 𝑟 = 𝑅) → 𝑠 = 𝑆)
145	144	opeq2d 3864	. . . . . . . . . . 11 ⊢ ((𝑠 = 𝑆 ∧ 𝑟 = 𝑅) → ⟨(Scalar‘ndx), 𝑠⟩ = ⟨(Scalar‘ndx), 𝑆⟩)
146	144	fveq2d 5631	. . . . . . . . . . . . 13 ⊢ ((𝑠 = 𝑆 ∧ 𝑟 = 𝑅) → (Base‘𝑠) = (Base‘𝑆))
147		eqidd 2230	. . . . . . . . . . . . 13 ⊢ ((𝑠 = 𝑆 ∧ 𝑟 = 𝑅) → 𝑣 = 𝑣)
148	125	fveq2d 5631	. . . . . . . . . . . . . . 15 ⊢ ((𝑠 = 𝑆 ∧ 𝑟 = 𝑅) → ( ·𝑠 ‘(𝑟‘𝑥)) = ( ·𝑠 ‘(𝑅‘𝑥)))
149	148	oveqd 6018	. . . . . . . . . . . . . 14 ⊢ ((𝑠 = 𝑆 ∧ 𝑟 = 𝑅) → (𝑓( ·𝑠 ‘(𝑟‘𝑥))(𝑔‘𝑥)) = (𝑓( ·𝑠 ‘(𝑅‘𝑥))(𝑔‘𝑥)))
150	122, 149	mpteq12dv 4166	. . . . . . . . . . . . 13 ⊢ ((𝑠 = 𝑆 ∧ 𝑟 = 𝑅) → (𝑥 ∈ dom 𝑟 ↦ (𝑓( ·𝑠 ‘(𝑟‘𝑥))(𝑔‘𝑥))) = (𝑥 ∈ dom 𝑅 ↦ (𝑓( ·𝑠 ‘(𝑅‘𝑥))(𝑔‘𝑥))))
151	146, 147, 150	mpoeq123dv 6066	. . . . . . . . . . . 12 ⊢ ((𝑠 = 𝑆 ∧ 𝑟 = 𝑅) → (𝑓 ∈ (Base‘𝑠), 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ (𝑓( ·𝑠 ‘(𝑟‘𝑥))(𝑔‘𝑥)))) = (𝑓 ∈ (Base‘𝑆), 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑅 ↦ (𝑓( ·𝑠 ‘(𝑅‘𝑥))(𝑔‘𝑥)))))
152	151	opeq2d 3864	. . . . . . . . . . 11 ⊢ ((𝑠 = 𝑆 ∧ 𝑟 = 𝑅) → ⟨( ·𝑠 ‘ndx), (𝑓 ∈ (Base‘𝑠), 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ (𝑓( ·𝑠 ‘(𝑟‘𝑥))(𝑔‘𝑥))))⟩ = ⟨( ·𝑠 ‘ndx), (𝑓 ∈ (Base‘𝑆), 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑅 ↦ (𝑓( ·𝑠 ‘(𝑅‘𝑥))(𝑔‘𝑥))))⟩)
153	125	fveq2d 5631	. . . . . . . . . . . . . . . 16 ⊢ ((𝑠 = 𝑆 ∧ 𝑟 = 𝑅) → (·𝑖‘(𝑟‘𝑥)) = (·𝑖‘(𝑅‘𝑥)))
154	153	oveqd 6018	. . . . . . . . . . . . . . 15 ⊢ ((𝑠 = 𝑆 ∧ 𝑟 = 𝑅) → ((𝑓‘𝑥)(·𝑖‘(𝑟‘𝑥))(𝑔‘𝑥)) = ((𝑓‘𝑥)(·𝑖‘(𝑅‘𝑥))(𝑔‘𝑥)))
155	122, 154	mpteq12dv 4166	. . . . . . . . . . . . . 14 ⊢ ((𝑠 = 𝑆 ∧ 𝑟 = 𝑅) → (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(·𝑖‘(𝑟‘𝑥))(𝑔‘𝑥))) = (𝑥 ∈ dom 𝑅 ↦ ((𝑓‘𝑥)(·𝑖‘(𝑅‘𝑥))(𝑔‘𝑥))))
156	144, 155	oveq12d 6019	. . . . . . . . . . . . 13 ⊢ ((𝑠 = 𝑆 ∧ 𝑟 = 𝑅) → (𝑠 Σg (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(·𝑖‘(𝑟‘𝑥))(𝑔‘𝑥)))) = (𝑆 Σg (𝑥 ∈ dom 𝑅 ↦ ((𝑓‘𝑥)(·𝑖‘(𝑅‘𝑥))(𝑔‘𝑥)))))
157	156	mpoeq3dv 6070	. . . . . . . . . . . 12 ⊢ ((𝑠 = 𝑆 ∧ 𝑟 = 𝑅) → (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑠 Σg (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(·𝑖‘(𝑟‘𝑥))(𝑔‘𝑥))))) = (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑆 Σg (𝑥 ∈ dom 𝑅 ↦ ((𝑓‘𝑥)(·𝑖‘(𝑅‘𝑥))(𝑔‘𝑥))))))
158	157	opeq2d 3864	. . . . . . . . . . 11 ⊢ ((𝑠 = 𝑆 ∧ 𝑟 = 𝑅) → ⟨(·𝑖‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑠 Σg (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(·𝑖‘(𝑟‘𝑥))(𝑔‘𝑥)))))⟩ = ⟨(·𝑖‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑆 Σg (𝑥 ∈ dom 𝑅 ↦ ((𝑓‘𝑥)(·𝑖‘(𝑅‘𝑥))(𝑔‘𝑥)))))⟩)
159	145, 152, 158	tpeq123d 3758	. . . . . . . . . 10 ⊢ ((𝑠 = 𝑆 ∧ 𝑟 = 𝑅) → {⟨(Scalar‘ndx), 𝑠⟩, ⟨( ·𝑠 ‘ndx), (𝑓 ∈ (Base‘𝑠), 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ (𝑓( ·𝑠 ‘(𝑟‘𝑥))(𝑔‘𝑥))))⟩, ⟨(·𝑖‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑠 Σg (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(·𝑖‘(𝑟‘𝑥))(𝑔‘𝑥)))))⟩} = {⟨(Scalar‘ndx), 𝑆⟩, ⟨( ·𝑠 ‘ndx), (𝑓 ∈ (Base‘𝑆), 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑅 ↦ (𝑓( ·𝑠 ‘(𝑅‘𝑥))(𝑔‘𝑥))))⟩, ⟨(·𝑖‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑆 Σg (𝑥 ∈ dom 𝑅 ↦ ((𝑓‘𝑥)(·𝑖‘(𝑅‘𝑥))(𝑔‘𝑥)))))⟩})
160	143, 159	uneq12d 3359	. . . . . . . . 9 ⊢ ((𝑠 = 𝑆 ∧ 𝑟 = 𝑅) → ({⟨(Base‘ndx), 𝑣⟩, ⟨(+g‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(+g‘(𝑟‘𝑥))(𝑔‘𝑥))))⟩, ⟨(.r‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(.r‘(𝑟‘𝑥))(𝑔‘𝑥))))⟩} ∪ {⟨(Scalar‘ndx), 𝑠⟩, ⟨( ·𝑠 ‘ndx), (𝑓 ∈ (Base‘𝑠), 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ (𝑓( ·𝑠 ‘(𝑟‘𝑥))(𝑔‘𝑥))))⟩, ⟨(·𝑖‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑠 Σg (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(·𝑖‘(𝑟‘𝑥))(𝑔‘𝑥)))))⟩}) = ({⟨(Base‘ndx), 𝑣⟩, ⟨(+g‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑅 ↦ ((𝑓‘𝑥)(+g‘(𝑅‘𝑥))(𝑔‘𝑥))))⟩, ⟨(.r‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑅 ↦ ((𝑓‘𝑥)(.r‘(𝑅‘𝑥))(𝑔‘𝑥))))⟩} ∪ {⟨(Scalar‘ndx), 𝑆⟩, ⟨( ·𝑠 ‘ndx), (𝑓 ∈ (Base‘𝑆), 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑅 ↦ (𝑓( ·𝑠 ‘(𝑅‘𝑥))(𝑔‘𝑥))))⟩, ⟨(·𝑖‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑆 Σg (𝑥 ∈ dom 𝑅 ↦ ((𝑓‘𝑥)(·𝑖‘(𝑅‘𝑥))(𝑔‘𝑥)))))⟩}))
161	124	coeq2d 4884	. . . . . . . . . . . . 13 ⊢ ((𝑠 = 𝑆 ∧ 𝑟 = 𝑅) → (TopOpen ∘ 𝑟) = (TopOpen ∘ 𝑅))
162	161	fveq2d 5631	. . . . . . . . . . . 12 ⊢ ((𝑠 = 𝑆 ∧ 𝑟 = 𝑅) → (∏t‘(TopOpen ∘ 𝑟)) = (∏t‘(TopOpen ∘ 𝑅)))
163	162	opeq2d 3864	. . . . . . . . . . 11 ⊢ ((𝑠 = 𝑆 ∧ 𝑟 = 𝑅) → ⟨(TopSet‘ndx), (∏t‘(TopOpen ∘ 𝑟))⟩ = ⟨(TopSet‘ndx), (∏t‘(TopOpen ∘ 𝑅))⟩)
164	125	fveq2d 5631	. . . . . . . . . . . . . . . 16 ⊢ ((𝑠 = 𝑆 ∧ 𝑟 = 𝑅) → (le‘(𝑟‘𝑥)) = (le‘(𝑅‘𝑥)))
165	164	breqd 4094	. . . . . . . . . . . . . . 15 ⊢ ((𝑠 = 𝑆 ∧ 𝑟 = 𝑅) → ((𝑓‘𝑥)(le‘(𝑟‘𝑥))(𝑔‘𝑥) ↔ (𝑓‘𝑥)(le‘(𝑅‘𝑥))(𝑔‘𝑥)))
166	122, 165	raleqbidv 2744	. . . . . . . . . . . . . 14 ⊢ ((𝑠 = 𝑆 ∧ 𝑟 = 𝑅) → (∀𝑥 ∈ dom 𝑟(𝑓‘𝑥)(le‘(𝑟‘𝑥))(𝑔‘𝑥) ↔ ∀𝑥 ∈ dom 𝑅(𝑓‘𝑥)(le‘(𝑅‘𝑥))(𝑔‘𝑥)))
167	166	anbi2d 464	. . . . . . . . . . . . 13 ⊢ ((𝑠 = 𝑆 ∧ 𝑟 = 𝑅) → (({𝑓, 𝑔} ⊆ 𝑣 ∧ ∀𝑥 ∈ dom 𝑟(𝑓‘𝑥)(le‘(𝑟‘𝑥))(𝑔‘𝑥)) ↔ ({𝑓, 𝑔} ⊆ 𝑣 ∧ ∀𝑥 ∈ dom 𝑅(𝑓‘𝑥)(le‘(𝑅‘𝑥))(𝑔‘𝑥))))
168	167	opabbidv 4150	. . . . . . . . . . . 12 ⊢ ((𝑠 = 𝑆 ∧ 𝑟 = 𝑅) → {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝑣 ∧ ∀𝑥 ∈ dom 𝑟(𝑓‘𝑥)(le‘(𝑟‘𝑥))(𝑔‘𝑥))} = {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝑣 ∧ ∀𝑥 ∈ dom 𝑅(𝑓‘𝑥)(le‘(𝑅‘𝑥))(𝑔‘𝑥))})
169	168	opeq2d 3864	. . . . . . . . . . 11 ⊢ ((𝑠 = 𝑆 ∧ 𝑟 = 𝑅) → ⟨(le‘ndx), {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝑣 ∧ ∀𝑥 ∈ dom 𝑟(𝑓‘𝑥)(le‘(𝑟‘𝑥))(𝑔‘𝑥))}⟩ = ⟨(le‘ndx), {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝑣 ∧ ∀𝑥 ∈ dom 𝑅(𝑓‘𝑥)(le‘(𝑅‘𝑥))(𝑔‘𝑥))}⟩)
170	125	fveq2d 5631	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑠 = 𝑆 ∧ 𝑟 = 𝑅) → (dist‘(𝑟‘𝑥)) = (dist‘(𝑅‘𝑥)))
171	170	oveqd 6018	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑠 = 𝑆 ∧ 𝑟 = 𝑅) → ((𝑓‘𝑥)(dist‘(𝑟‘𝑥))(𝑔‘𝑥)) = ((𝑓‘𝑥)(dist‘(𝑅‘𝑥))(𝑔‘𝑥)))
172	122, 171	mpteq12dv 4166	. . . . . . . . . . . . . . . 16 ⊢ ((𝑠 = 𝑆 ∧ 𝑟 = 𝑅) → (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(dist‘(𝑟‘𝑥))(𝑔‘𝑥))) = (𝑥 ∈ dom 𝑅 ↦ ((𝑓‘𝑥)(dist‘(𝑅‘𝑥))(𝑔‘𝑥))))
173	172	rneqd 4953	. . . . . . . . . . . . . . 15 ⊢ ((𝑠 = 𝑆 ∧ 𝑟 = 𝑅) → ran (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(dist‘(𝑟‘𝑥))(𝑔‘𝑥))) = ran (𝑥 ∈ dom 𝑅 ↦ ((𝑓‘𝑥)(dist‘(𝑅‘𝑥))(𝑔‘𝑥))))
174	173	uneq1d 3357	. . . . . . . . . . . . . 14 ⊢ ((𝑠 = 𝑆 ∧ 𝑟 = 𝑅) → (ran (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(dist‘(𝑟‘𝑥))(𝑔‘𝑥))) ∪ {0}) = (ran (𝑥 ∈ dom 𝑅 ↦ ((𝑓‘𝑥)(dist‘(𝑅‘𝑥))(𝑔‘𝑥))) ∪ {0}))
175	174	supeq1d 7154	. . . . . . . . . . . . 13 ⊢ ((𝑠 = 𝑆 ∧ 𝑟 = 𝑅) → sup((ran (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(dist‘(𝑟‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ*, < ) = sup((ran (𝑥 ∈ dom 𝑅 ↦ ((𝑓‘𝑥)(dist‘(𝑅‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ*, < ))
176	175	mpoeq3dv 6070	. . . . . . . . . . . 12 ⊢ ((𝑠 = 𝑆 ∧ 𝑟 = 𝑅) → (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ sup((ran (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(dist‘(𝑟‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ*, < )) = (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ sup((ran (𝑥 ∈ dom 𝑅 ↦ ((𝑓‘𝑥)(dist‘(𝑅‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ*, < )))
177	176	opeq2d 3864	. . . . . . . . . . 11 ⊢ ((𝑠 = 𝑆 ∧ 𝑟 = 𝑅) → ⟨(dist‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ sup((ran (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(dist‘(𝑟‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ*, < ))⟩ = ⟨(dist‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ sup((ran (𝑥 ∈ dom 𝑅 ↦ ((𝑓‘𝑥)(dist‘(𝑅‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ*, < ))⟩)
178	163, 169, 177	tpeq123d 3758	. . . . . . . . . 10 ⊢ ((𝑠 = 𝑆 ∧ 𝑟 = 𝑅) → {⟨(TopSet‘ndx), (∏t‘(TopOpen ∘ 𝑟))⟩, ⟨(le‘ndx), {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝑣 ∧ ∀𝑥 ∈ dom 𝑟(𝑓‘𝑥)(le‘(𝑟‘𝑥))(𝑔‘𝑥))}⟩, ⟨(dist‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ sup((ran (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(dist‘(𝑟‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ*, < ))⟩} = {⟨(TopSet‘ndx), (∏t‘(TopOpen ∘ 𝑅))⟩, ⟨(le‘ndx), {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝑣 ∧ ∀𝑥 ∈ dom 𝑅(𝑓‘𝑥)(le‘(𝑅‘𝑥))(𝑔‘𝑥))}⟩, ⟨(dist‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ sup((ran (𝑥 ∈ dom 𝑅 ↦ ((𝑓‘𝑥)(dist‘(𝑅‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ*, < ))⟩})
179	125	fveq2d 5631	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑠 = 𝑆 ∧ 𝑟 = 𝑅) → (comp‘(𝑟‘𝑥)) = (comp‘(𝑅‘𝑥)))
180	179	oveqd 6018	. . . . . . . . . . . . . . . 16 ⊢ ((𝑠 = 𝑆 ∧ 𝑟 = 𝑅) → (⟨((1st ‘𝑎)‘𝑥), ((2nd ‘𝑎)‘𝑥)⟩(comp‘(𝑟‘𝑥))(𝑐‘𝑥)) = (⟨((1st ‘𝑎)‘𝑥), ((2nd ‘𝑎)‘𝑥)⟩(comp‘(𝑅‘𝑥))(𝑐‘𝑥)))
181	180	oveqd 6018	. . . . . . . . . . . . . . 15 ⊢ ((𝑠 = 𝑆 ∧ 𝑟 = 𝑅) → ((𝑑‘𝑥)(⟨((1st ‘𝑎)‘𝑥), ((2nd ‘𝑎)‘𝑥)⟩(comp‘(𝑟‘𝑥))(𝑐‘𝑥))(𝑒‘𝑥)) = ((𝑑‘𝑥)(⟨((1st ‘𝑎)‘𝑥), ((2nd ‘𝑎)‘𝑥)⟩(comp‘(𝑅‘𝑥))(𝑐‘𝑥))(𝑒‘𝑥)))
182	122, 181	mpteq12dv 4166	. . . . . . . . . . . . . 14 ⊢ ((𝑠 = 𝑆 ∧ 𝑟 = 𝑅) → (𝑥 ∈ dom 𝑟 ↦ ((𝑑‘𝑥)(⟨((1st ‘𝑎)‘𝑥), ((2nd ‘𝑎)‘𝑥)⟩(comp‘(𝑟‘𝑥))(𝑐‘𝑥))(𝑒‘𝑥))) = (𝑥 ∈ dom 𝑅 ↦ ((𝑑‘𝑥)(⟨((1st ‘𝑎)‘𝑥), ((2nd ‘𝑎)‘𝑥)⟩(comp‘(𝑅‘𝑥))(𝑐‘𝑥))(𝑒‘𝑥))))
183	182	mpoeq3dv 6070	. . . . . . . . . . . . 13 ⊢ ((𝑠 = 𝑆 ∧ 𝑟 = 𝑅) → (𝑑 ∈ ((2nd ‘𝑎)ℎ𝑐), 𝑒 ∈ (ℎ‘𝑎) ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑑‘𝑥)(⟨((1st ‘𝑎)‘𝑥), ((2nd ‘𝑎)‘𝑥)⟩(comp‘(𝑟‘𝑥))(𝑐‘𝑥))(𝑒‘𝑥)))) = (𝑑 ∈ ((2nd ‘𝑎)ℎ𝑐), 𝑒 ∈ (ℎ‘𝑎) ↦ (𝑥 ∈ dom 𝑅 ↦ ((𝑑‘𝑥)(⟨((1st ‘𝑎)‘𝑥), ((2nd ‘𝑎)‘𝑥)⟩(comp‘(𝑅‘𝑥))(𝑐‘𝑥))(𝑒‘𝑥)))))
184	183	mpoeq3dv 6070	. . . . . . . . . . . 12 ⊢ ((𝑠 = 𝑆 ∧ 𝑟 = 𝑅) → (𝑎 ∈ (𝑣 × 𝑣), 𝑐 ∈ 𝑣 ↦ (𝑑 ∈ ((2nd ‘𝑎)ℎ𝑐), 𝑒 ∈ (ℎ‘𝑎) ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑑‘𝑥)(⟨((1st ‘𝑎)‘𝑥), ((2nd ‘𝑎)‘𝑥)⟩(comp‘(𝑟‘𝑥))(𝑐‘𝑥))(𝑒‘𝑥))))) = (𝑎 ∈ (𝑣 × 𝑣), 𝑐 ∈ 𝑣 ↦ (𝑑 ∈ ((2nd ‘𝑎)ℎ𝑐), 𝑒 ∈ (ℎ‘𝑎) ↦ (𝑥 ∈ dom 𝑅 ↦ ((𝑑‘𝑥)(⟨((1st ‘𝑎)‘𝑥), ((2nd ‘𝑎)‘𝑥)⟩(comp‘(𝑅‘𝑥))(𝑐‘𝑥))(𝑒‘𝑥))))))
185	184	opeq2d 3864	. . . . . . . . . . 11 ⊢ ((𝑠 = 𝑆 ∧ 𝑟 = 𝑅) → ⟨(comp‘ndx), (𝑎 ∈ (𝑣 × 𝑣), 𝑐 ∈ 𝑣 ↦ (𝑑 ∈ ((2nd ‘𝑎)ℎ𝑐), 𝑒 ∈ (ℎ‘𝑎) ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑑‘𝑥)(⟨((1st ‘𝑎)‘𝑥), ((2nd ‘𝑎)‘𝑥)⟩(comp‘(𝑟‘𝑥))(𝑐‘𝑥))(𝑒‘𝑥)))))⟩ = ⟨(comp‘ndx), (𝑎 ∈ (𝑣 × 𝑣), 𝑐 ∈ 𝑣 ↦ (𝑑 ∈ ((2nd ‘𝑎)ℎ𝑐), 𝑒 ∈ (ℎ‘𝑎) ↦ (𝑥 ∈ dom 𝑅 ↦ ((𝑑‘𝑥)(⟨((1st ‘𝑎)‘𝑥), ((2nd ‘𝑎)‘𝑥)⟩(comp‘(𝑅‘𝑥))(𝑐‘𝑥))(𝑒‘𝑥)))))⟩)
186	185	preq2d 3750	. . . . . . . . . 10 ⊢ ((𝑠 = 𝑆 ∧ 𝑟 = 𝑅) → {⟨(Hom ‘ndx), ℎ⟩, ⟨(comp‘ndx), (𝑎 ∈ (𝑣 × 𝑣), 𝑐 ∈ 𝑣 ↦ (𝑑 ∈ ((2nd ‘𝑎)ℎ𝑐), 𝑒 ∈ (ℎ‘𝑎) ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑑‘𝑥)(⟨((1st ‘𝑎)‘𝑥), ((2nd ‘𝑎)‘𝑥)⟩(comp‘(𝑟‘𝑥))(𝑐‘𝑥))(𝑒‘𝑥)))))⟩} = {⟨(Hom ‘ndx), ℎ⟩, ⟨(comp‘ndx), (𝑎 ∈ (𝑣 × 𝑣), 𝑐 ∈ 𝑣 ↦ (𝑑 ∈ ((2nd ‘𝑎)ℎ𝑐), 𝑒 ∈ (ℎ‘𝑎) ↦ (𝑥 ∈ dom 𝑅 ↦ ((𝑑‘𝑥)(⟨((1st ‘𝑎)‘𝑥), ((2nd ‘𝑎)‘𝑥)⟩(comp‘(𝑅‘𝑥))(𝑐‘𝑥))(𝑒‘𝑥)))))⟩})
187	178, 186	uneq12d 3359	. . . . . . . . 9 ⊢ ((𝑠 = 𝑆 ∧ 𝑟 = 𝑅) → ({⟨(TopSet‘ndx), (∏t‘(TopOpen ∘ 𝑟))⟩, ⟨(le‘ndx), {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝑣 ∧ ∀𝑥 ∈ dom 𝑟(𝑓‘𝑥)(le‘(𝑟‘𝑥))(𝑔‘𝑥))}⟩, ⟨(dist‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ sup((ran (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(dist‘(𝑟‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ*, < ))⟩} ∪ {⟨(Hom ‘ndx), ℎ⟩, ⟨(comp‘ndx), (𝑎 ∈ (𝑣 × 𝑣), 𝑐 ∈ 𝑣 ↦ (𝑑 ∈ ((2nd ‘𝑎)ℎ𝑐), 𝑒 ∈ (ℎ‘𝑎) ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑑‘𝑥)(⟨((1st ‘𝑎)‘𝑥), ((2nd ‘𝑎)‘𝑥)⟩(comp‘(𝑟‘𝑥))(𝑐‘𝑥))(𝑒‘𝑥)))))⟩}) = ({⟨(TopSet‘ndx), (∏t‘(TopOpen ∘ 𝑅))⟩, ⟨(le‘ndx), {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝑣 ∧ ∀𝑥 ∈ dom 𝑅(𝑓‘𝑥)(le‘(𝑅‘𝑥))(𝑔‘𝑥))}⟩, ⟨(dist‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ sup((ran (𝑥 ∈ dom 𝑅 ↦ ((𝑓‘𝑥)(dist‘(𝑅‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ*, < ))⟩} ∪ {⟨(Hom ‘ndx), ℎ⟩, ⟨(comp‘ndx), (𝑎 ∈ (𝑣 × 𝑣), 𝑐 ∈ 𝑣 ↦ (𝑑 ∈ ((2nd ‘𝑎)ℎ𝑐), 𝑒 ∈ (ℎ‘𝑎) ↦ (𝑥 ∈ dom 𝑅 ↦ ((𝑑‘𝑥)(⟨((1st ‘𝑎)‘𝑥), ((2nd ‘𝑎)‘𝑥)⟩(comp‘(𝑅‘𝑥))(𝑐‘𝑥))(𝑒‘𝑥)))))⟩}))
188	160, 187	uneq12d 3359	. . . . . . . 8 ⊢ ((𝑠 = 𝑆 ∧ 𝑟 = 𝑅) → (({⟨(Base‘ndx), 𝑣⟩, ⟨(+g‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(+g‘(𝑟‘𝑥))(𝑔‘𝑥))))⟩, ⟨(.r‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(.r‘(𝑟‘𝑥))(𝑔‘𝑥))))⟩} ∪ {⟨(Scalar‘ndx), 𝑠⟩, ⟨( ·𝑠 ‘ndx), (𝑓 ∈ (Base‘𝑠), 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ (𝑓( ·𝑠 ‘(𝑟‘𝑥))(𝑔‘𝑥))))⟩, ⟨(·𝑖‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑠 Σg (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(·𝑖‘(𝑟‘𝑥))(𝑔‘𝑥)))))⟩}) ∪ ({⟨(TopSet‘ndx), (∏t‘(TopOpen ∘ 𝑟))⟩, ⟨(le‘ndx), {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝑣 ∧ ∀𝑥 ∈ dom 𝑟(𝑓‘𝑥)(le‘(𝑟‘𝑥))(𝑔‘𝑥))}⟩, ⟨(dist‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ sup((ran (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(dist‘(𝑟‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ*, < ))⟩} ∪ {⟨(Hom ‘ndx), ℎ⟩, ⟨(comp‘ndx), (𝑎 ∈ (𝑣 × 𝑣), 𝑐 ∈ 𝑣 ↦ (𝑑 ∈ ((2nd ‘𝑎)ℎ𝑐), 𝑒 ∈ (ℎ‘𝑎) ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑑‘𝑥)(⟨((1st ‘𝑎)‘𝑥), ((2nd ‘𝑎)‘𝑥)⟩(comp‘(𝑟‘𝑥))(𝑐‘𝑥))(𝑒‘𝑥)))))⟩})) = (({⟨(Base‘ndx), 𝑣⟩, ⟨(+g‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑅 ↦ ((𝑓‘𝑥)(+g‘(𝑅‘𝑥))(𝑔‘𝑥))))⟩, ⟨(.r‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑅 ↦ ((𝑓‘𝑥)(.r‘(𝑅‘𝑥))(𝑔‘𝑥))))⟩} ∪ {⟨(Scalar‘ndx), 𝑆⟩, ⟨( ·𝑠 ‘ndx), (𝑓 ∈ (Base‘𝑆), 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑅 ↦ (𝑓( ·𝑠 ‘(𝑅‘𝑥))(𝑔‘𝑥))))⟩, ⟨(·𝑖‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑆 Σg (𝑥 ∈ dom 𝑅 ↦ ((𝑓‘𝑥)(·𝑖‘(𝑅‘𝑥))(𝑔‘𝑥)))))⟩}) ∪ ({⟨(TopSet‘ndx), (∏t‘(TopOpen ∘ 𝑅))⟩, ⟨(le‘ndx), {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝑣 ∧ ∀𝑥 ∈ dom 𝑅(𝑓‘𝑥)(le‘(𝑅‘𝑥))(𝑔‘𝑥))}⟩, ⟨(dist‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ sup((ran (𝑥 ∈ dom 𝑅 ↦ ((𝑓‘𝑥)(dist‘(𝑅‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ*, < ))⟩} ∪ {⟨(Hom ‘ndx), ℎ⟩, ⟨(comp‘ndx), (𝑎 ∈ (𝑣 × 𝑣), 𝑐 ∈ 𝑣 ↦ (𝑑 ∈ ((2nd ‘𝑎)ℎ𝑐), 𝑒 ∈ (ℎ‘𝑎) ↦ (𝑥 ∈ dom 𝑅 ↦ ((𝑑‘𝑥)(⟨((1st ‘𝑎)‘𝑥), ((2nd ‘𝑎)‘𝑥)⟩(comp‘(𝑅‘𝑥))(𝑐‘𝑥))(𝑒‘𝑥)))))⟩})))
189	188	csbeq2dv 3150	. . . . . . 7 ⊢ ((𝑠 = 𝑆 ∧ 𝑟 = 𝑅) → ⦋(𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ X𝑥 ∈ dom 𝑅((𝑓‘𝑥)(Hom ‘(𝑅‘𝑥))(𝑔‘𝑥))) / ℎ⦌(({⟨(Base‘ndx), 𝑣⟩, ⟨(+g‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(+g‘(𝑟‘𝑥))(𝑔‘𝑥))))⟩, ⟨(.r‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(.r‘(𝑟‘𝑥))(𝑔‘𝑥))))⟩} ∪ {⟨(Scalar‘ndx), 𝑠⟩, ⟨( ·𝑠 ‘ndx), (𝑓 ∈ (Base‘𝑠), 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ (𝑓( ·𝑠 ‘(𝑟‘𝑥))(𝑔‘𝑥))))⟩, ⟨(·𝑖‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑠 Σg (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(·𝑖‘(𝑟‘𝑥))(𝑔‘𝑥)))))⟩}) ∪ ({⟨(TopSet‘ndx), (∏t‘(TopOpen ∘ 𝑟))⟩, ⟨(le‘ndx), {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝑣 ∧ ∀𝑥 ∈ dom 𝑟(𝑓‘𝑥)(le‘(𝑟‘𝑥))(𝑔‘𝑥))}⟩, ⟨(dist‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ sup((ran (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(dist‘(𝑟‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ*, < ))⟩} ∪ {⟨(Hom ‘ndx), ℎ⟩, ⟨(comp‘ndx), (𝑎 ∈ (𝑣 × 𝑣), 𝑐 ∈ 𝑣 ↦ (𝑑 ∈ ((2nd ‘𝑎)ℎ𝑐), 𝑒 ∈ (ℎ‘𝑎) ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑑‘𝑥)(⟨((1st ‘𝑎)‘𝑥), ((2nd ‘𝑎)‘𝑥)⟩(comp‘(𝑟‘𝑥))(𝑐‘𝑥))(𝑒‘𝑥)))))⟩})) = ⦋(𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ X𝑥 ∈ dom 𝑅((𝑓‘𝑥)(Hom ‘(𝑅‘𝑥))(𝑔‘𝑥))) / ℎ⦌(({⟨(Base‘ndx), 𝑣⟩, ⟨(+g‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑅 ↦ ((𝑓‘𝑥)(+g‘(𝑅‘𝑥))(𝑔‘𝑥))))⟩, ⟨(.r‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑅 ↦ ((𝑓‘𝑥)(.r‘(𝑅‘𝑥))(𝑔‘𝑥))))⟩} ∪ {⟨(Scalar‘ndx), 𝑆⟩, ⟨( ·𝑠 ‘ndx), (𝑓 ∈ (Base‘𝑆), 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑅 ↦ (𝑓( ·𝑠 ‘(𝑅‘𝑥))(𝑔‘𝑥))))⟩, ⟨(·𝑖‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑆 Σg (𝑥 ∈ dom 𝑅 ↦ ((𝑓‘𝑥)(·𝑖‘(𝑅‘𝑥))(𝑔‘𝑥)))))⟩}) ∪ ({⟨(TopSet‘ndx), (∏t‘(TopOpen ∘ 𝑅))⟩, ⟨(le‘ndx), {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝑣 ∧ ∀𝑥 ∈ dom 𝑅(𝑓‘𝑥)(le‘(𝑅‘𝑥))(𝑔‘𝑥))}⟩, ⟨(dist‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ sup((ran (𝑥 ∈ dom 𝑅 ↦ ((𝑓‘𝑥)(dist‘(𝑅‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ*, < ))⟩} ∪ {⟨(Hom ‘ndx), ℎ⟩, ⟨(comp‘ndx), (𝑎 ∈ (𝑣 × 𝑣), 𝑐 ∈ 𝑣 ↦ (𝑑 ∈ ((2nd ‘𝑎)ℎ𝑐), 𝑒 ∈ (ℎ‘𝑎) ↦ (𝑥 ∈ dom 𝑅 ↦ ((𝑑‘𝑥)(⟨((1st ‘𝑎)‘𝑥), ((2nd ‘𝑎)‘𝑥)⟩(comp‘(𝑅‘𝑥))(𝑐‘𝑥))(𝑒‘𝑥)))))⟩})))
190	131, 189	eqtrd 2262	. . . . . 6 ⊢ ((𝑠 = 𝑆 ∧ 𝑟 = 𝑅) → ⦋(𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ X𝑥 ∈ dom 𝑟((𝑓‘𝑥)(Hom ‘(𝑟‘𝑥))(𝑔‘𝑥))) / ℎ⦌(({⟨(Base‘ndx), 𝑣⟩, ⟨(+g‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(+g‘(𝑟‘𝑥))(𝑔‘𝑥))))⟩, ⟨(.r‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(.r‘(𝑟‘𝑥))(𝑔‘𝑥))))⟩} ∪ {⟨(Scalar‘ndx), 𝑠⟩, ⟨( ·𝑠 ‘ndx), (𝑓 ∈ (Base‘𝑠), 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ (𝑓( ·𝑠 ‘(𝑟‘𝑥))(𝑔‘𝑥))))⟩, ⟨(·𝑖‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑠 Σg (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(·𝑖‘(𝑟‘𝑥))(𝑔‘𝑥)))))⟩}) ∪ ({⟨(TopSet‘ndx), (∏t‘(TopOpen ∘ 𝑟))⟩, ⟨(le‘ndx), {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝑣 ∧ ∀𝑥 ∈ dom 𝑟(𝑓‘𝑥)(le‘(𝑟‘𝑥))(𝑔‘𝑥))}⟩, ⟨(dist‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ sup((ran (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(dist‘(𝑟‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ*, < ))⟩} ∪ {⟨(Hom ‘ndx), ℎ⟩, ⟨(comp‘ndx), (𝑎 ∈ (𝑣 × 𝑣), 𝑐 ∈ 𝑣 ↦ (𝑑 ∈ ((2nd ‘𝑎)ℎ𝑐), 𝑒 ∈ (ℎ‘𝑎) ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑑‘𝑥)(⟨((1st ‘𝑎)‘𝑥), ((2nd ‘𝑎)‘𝑥)⟩(comp‘(𝑟‘𝑥))(𝑐‘𝑥))(𝑒‘𝑥)))))⟩})) = ⦋(𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ X𝑥 ∈ dom 𝑅((𝑓‘𝑥)(Hom ‘(𝑅‘𝑥))(𝑔‘𝑥))) / ℎ⦌(({⟨(Base‘ndx), 𝑣⟩, ⟨(+g‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑅 ↦ ((𝑓‘𝑥)(+g‘(𝑅‘𝑥))(𝑔‘𝑥))))⟩, ⟨(.r‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑅 ↦ ((𝑓‘𝑥)(.r‘(𝑅‘𝑥))(𝑔‘𝑥))))⟩} ∪ {⟨(Scalar‘ndx), 𝑆⟩, ⟨( ·𝑠 ‘ndx), (𝑓 ∈ (Base‘𝑆), 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑅 ↦ (𝑓( ·𝑠 ‘(𝑅‘𝑥))(𝑔‘𝑥))))⟩, ⟨(·𝑖‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑆 Σg (𝑥 ∈ dom 𝑅 ↦ ((𝑓‘𝑥)(·𝑖‘(𝑅‘𝑥))(𝑔‘𝑥)))))⟩}) ∪ ({⟨(TopSet‘ndx), (∏t‘(TopOpen ∘ 𝑅))⟩, ⟨(le‘ndx), {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝑣 ∧ ∀𝑥 ∈ dom 𝑅(𝑓‘𝑥)(le‘(𝑅‘𝑥))(𝑔‘𝑥))}⟩, ⟨(dist‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ sup((ran (𝑥 ∈ dom 𝑅 ↦ ((𝑓‘𝑥)(dist‘(𝑅‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ*, < ))⟩} ∪ {⟨(Hom ‘ndx), ℎ⟩, ⟨(comp‘ndx), (𝑎 ∈ (𝑣 × 𝑣), 𝑐 ∈ 𝑣 ↦ (𝑑 ∈ ((2nd ‘𝑎)ℎ𝑐), 𝑒 ∈ (ℎ‘𝑎) ↦ (𝑥 ∈ dom 𝑅 ↦ ((𝑑‘𝑥)(⟨((1st ‘𝑎)‘𝑥), ((2nd ‘𝑎)‘𝑥)⟩(comp‘(𝑅‘𝑥))(𝑐‘𝑥))(𝑒‘𝑥)))))⟩})))
191	190	csbeq2dv 3150	. . . . 5 ⊢ ((𝑠 = 𝑆 ∧ 𝑟 = 𝑅) → ⦋X𝑥 ∈ dom 𝑅(Base‘(𝑅‘𝑥)) / 𝑣⦌⦋(𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ X𝑥 ∈ dom 𝑟((𝑓‘𝑥)(Hom ‘(𝑟‘𝑥))(𝑔‘𝑥))) / ℎ⦌(({⟨(Base‘ndx), 𝑣⟩, ⟨(+g‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(+g‘(𝑟‘𝑥))(𝑔‘𝑥))))⟩, ⟨(.r‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(.r‘(𝑟‘𝑥))(𝑔‘𝑥))))⟩} ∪ {⟨(Scalar‘ndx), 𝑠⟩, ⟨( ·𝑠 ‘ndx), (𝑓 ∈ (Base‘𝑠), 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ (𝑓( ·𝑠 ‘(𝑟‘𝑥))(𝑔‘𝑥))))⟩, ⟨(·𝑖‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑠 Σg (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(·𝑖‘(𝑟‘𝑥))(𝑔‘𝑥)))))⟩}) ∪ ({⟨(TopSet‘ndx), (∏t‘(TopOpen ∘ 𝑟))⟩, ⟨(le‘ndx), {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝑣 ∧ ∀𝑥 ∈ dom 𝑟(𝑓‘𝑥)(le‘(𝑟‘𝑥))(𝑔‘𝑥))}⟩, ⟨(dist‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ sup((ran (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(dist‘(𝑟‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ*, < ))⟩} ∪ {⟨(Hom ‘ndx), ℎ⟩, ⟨(comp‘ndx), (𝑎 ∈ (𝑣 × 𝑣), 𝑐 ∈ 𝑣 ↦ (𝑑 ∈ ((2nd ‘𝑎)ℎ𝑐), 𝑒 ∈ (ℎ‘𝑎) ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑑‘𝑥)(⟨((1st ‘𝑎)‘𝑥), ((2nd ‘𝑎)‘𝑥)⟩(comp‘(𝑟‘𝑥))(𝑐‘𝑥))(𝑒‘𝑥)))))⟩})) = ⦋X𝑥 ∈ dom 𝑅(Base‘(𝑅‘𝑥)) / 𝑣⦌⦋(𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ X𝑥 ∈ dom 𝑅((𝑓‘𝑥)(Hom ‘(𝑅‘𝑥))(𝑔‘𝑥))) / ℎ⦌(({⟨(Base‘ndx), 𝑣⟩, ⟨(+g‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑅 ↦ ((𝑓‘𝑥)(+g‘(𝑅‘𝑥))(𝑔‘𝑥))))⟩, ⟨(.r‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑅 ↦ ((𝑓‘𝑥)(.r‘(𝑅‘𝑥))(𝑔‘𝑥))))⟩} ∪ {⟨(Scalar‘ndx), 𝑆⟩, ⟨( ·𝑠 ‘ndx), (𝑓 ∈ (Base‘𝑆), 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑅 ↦ (𝑓( ·𝑠 ‘(𝑅‘𝑥))(𝑔‘𝑥))))⟩, ⟨(·𝑖‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑆 Σg (𝑥 ∈ dom 𝑅 ↦ ((𝑓‘𝑥)(·𝑖‘(𝑅‘𝑥))(𝑔‘𝑥)))))⟩}) ∪ ({⟨(TopSet‘ndx), (∏t‘(TopOpen ∘ 𝑅))⟩, ⟨(le‘ndx), {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝑣 ∧ ∀𝑥 ∈ dom 𝑅(𝑓‘𝑥)(le‘(𝑅‘𝑥))(𝑔‘𝑥))}⟩, ⟨(dist‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ sup((ran (𝑥 ∈ dom 𝑅 ↦ ((𝑓‘𝑥)(dist‘(𝑅‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ*, < ))⟩} ∪ {⟨(Hom ‘ndx), ℎ⟩, ⟨(comp‘ndx), (𝑎 ∈ (𝑣 × 𝑣), 𝑐 ∈ 𝑣 ↦ (𝑑 ∈ ((2nd ‘𝑎)ℎ𝑐), 𝑒 ∈ (ℎ‘𝑎) ↦ (𝑥 ∈ dom 𝑅 ↦ ((𝑑‘𝑥)(⟨((1st ‘𝑎)‘𝑥), ((2nd ‘𝑎)‘𝑥)⟩(comp‘(𝑅‘𝑥))(𝑐‘𝑥))(𝑒‘𝑥)))))⟩})))
192	121, 191	eqtrd 2262	. . . 4 ⊢ ((𝑠 = 𝑆 ∧ 𝑟 = 𝑅) → ⦋X𝑥 ∈ dom 𝑟(Base‘(𝑟‘𝑥)) / 𝑣⦌⦋(𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ X𝑥 ∈ dom 𝑟((𝑓‘𝑥)(Hom ‘(𝑟‘𝑥))(𝑔‘𝑥))) / ℎ⦌(({⟨(Base‘ndx), 𝑣⟩, ⟨(+g‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(+g‘(𝑟‘𝑥))(𝑔‘𝑥))))⟩, ⟨(.r‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(.r‘(𝑟‘𝑥))(𝑔‘𝑥))))⟩} ∪ {⟨(Scalar‘ndx), 𝑠⟩, ⟨( ·𝑠 ‘ndx), (𝑓 ∈ (Base‘𝑠), 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ (𝑓( ·𝑠 ‘(𝑟‘𝑥))(𝑔‘𝑥))))⟩, ⟨(·𝑖‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑠 Σg (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(·𝑖‘(𝑟‘𝑥))(𝑔‘𝑥)))))⟩}) ∪ ({⟨(TopSet‘ndx), (∏t‘(TopOpen ∘ 𝑟))⟩, ⟨(le‘ndx), {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝑣 ∧ ∀𝑥 ∈ dom 𝑟(𝑓‘𝑥)(le‘(𝑟‘𝑥))(𝑔‘𝑥))}⟩, ⟨(dist‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ sup((ran (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(dist‘(𝑟‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ*, < ))⟩} ∪ {⟨(Hom ‘ndx), ℎ⟩, ⟨(comp‘ndx), (𝑎 ∈ (𝑣 × 𝑣), 𝑐 ∈ 𝑣 ↦ (𝑑 ∈ ((2nd ‘𝑎)ℎ𝑐), 𝑒 ∈ (ℎ‘𝑎) ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑑‘𝑥)(⟨((1st ‘𝑎)‘𝑥), ((2nd ‘𝑎)‘𝑥)⟩(comp‘(𝑟‘𝑥))(𝑐‘𝑥))(𝑒‘𝑥)))))⟩})) = ⦋X𝑥 ∈ dom 𝑅(Base‘(𝑅‘𝑥)) / 𝑣⦌⦋(𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ X𝑥 ∈ dom 𝑅((𝑓‘𝑥)(Hom ‘(𝑅‘𝑥))(𝑔‘𝑥))) / ℎ⦌(({⟨(Base‘ndx), 𝑣⟩, ⟨(+g‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑅 ↦ ((𝑓‘𝑥)(+g‘(𝑅‘𝑥))(𝑔‘𝑥))))⟩, ⟨(.r‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑅 ↦ ((𝑓‘𝑥)(.r‘(𝑅‘𝑥))(𝑔‘𝑥))))⟩} ∪ {⟨(Scalar‘ndx), 𝑆⟩, ⟨( ·𝑠 ‘ndx), (𝑓 ∈ (Base‘𝑆), 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑅 ↦ (𝑓( ·𝑠 ‘(𝑅‘𝑥))(𝑔‘𝑥))))⟩, ⟨(·𝑖‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑆 Σg (𝑥 ∈ dom 𝑅 ↦ ((𝑓‘𝑥)(·𝑖‘(𝑅‘𝑥))(𝑔‘𝑥)))))⟩}) ∪ ({⟨(TopSet‘ndx), (∏t‘(TopOpen ∘ 𝑅))⟩, ⟨(le‘ndx), {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝑣 ∧ ∀𝑥 ∈ dom 𝑅(𝑓‘𝑥)(le‘(𝑅‘𝑥))(𝑔‘𝑥))}⟩, ⟨(dist‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ sup((ran (𝑥 ∈ dom 𝑅 ↦ ((𝑓‘𝑥)(dist‘(𝑅‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ*, < ))⟩} ∪ {⟨(Hom ‘ndx), ℎ⟩, ⟨(comp‘ndx), (𝑎 ∈ (𝑣 × 𝑣), 𝑐 ∈ 𝑣 ↦ (𝑑 ∈ ((2nd ‘𝑎)ℎ𝑐), 𝑒 ∈ (ℎ‘𝑎) ↦ (𝑥 ∈ dom 𝑅 ↦ ((𝑑‘𝑥)(⟨((1st ‘𝑎)‘𝑥), ((2nd ‘𝑎)‘𝑥)⟩(comp‘(𝑅‘𝑥))(𝑐‘𝑥))(𝑒‘𝑥)))))⟩})))
193		df-prds 13300	. . . 4 ⊢ Xs = (𝑠 ∈ V, 𝑟 ∈ V ↦ ⦋X𝑥 ∈ dom 𝑟(Base‘(𝑟‘𝑥)) / 𝑣⦌⦋(𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ X𝑥 ∈ dom 𝑟((𝑓‘𝑥)(Hom ‘(𝑟‘𝑥))(𝑔‘𝑥))) / ℎ⦌(({⟨(Base‘ndx), 𝑣⟩, ⟨(+g‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(+g‘(𝑟‘𝑥))(𝑔‘𝑥))))⟩, ⟨(.r‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(.r‘(𝑟‘𝑥))(𝑔‘𝑥))))⟩} ∪ {⟨(Scalar‘ndx), 𝑠⟩, ⟨( ·𝑠 ‘ndx), (𝑓 ∈ (Base‘𝑠), 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ (𝑓( ·𝑠 ‘(𝑟‘𝑥))(𝑔‘𝑥))))⟩, ⟨(·𝑖‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑠 Σg (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(·𝑖‘(𝑟‘𝑥))(𝑔‘𝑥)))))⟩}) ∪ ({⟨(TopSet‘ndx), (∏t‘(TopOpen ∘ 𝑟))⟩, ⟨(le‘ndx), {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝑣 ∧ ∀𝑥 ∈ dom 𝑟(𝑓‘𝑥)(le‘(𝑟‘𝑥))(𝑔‘𝑥))}⟩, ⟨(dist‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ sup((ran (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(dist‘(𝑟‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ*, < ))⟩} ∪ {⟨(Hom ‘ndx), ℎ⟩, ⟨(comp‘ndx), (𝑎 ∈ (𝑣 × 𝑣), 𝑐 ∈ 𝑣 ↦ (𝑑 ∈ ((2nd ‘𝑎)ℎ𝑐), 𝑒 ∈ (ℎ‘𝑎) ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑑‘𝑥)(⟨((1st ‘𝑎)‘𝑥), ((2nd ‘𝑎)‘𝑥)⟩(comp‘(𝑟‘𝑥))(𝑐‘𝑥))(𝑒‘𝑥)))))⟩})))
194	192, 193	ovmpoga 6134	. . 3 ⊢ ((𝑆 ∈ V ∧ 𝑅 ∈ V ∧ ⦋X𝑥 ∈ dom 𝑅(Base‘(𝑅‘𝑥)) / 𝑣⦌⦋(𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ X𝑥 ∈ dom 𝑅((𝑓‘𝑥)(Hom ‘(𝑅‘𝑥))(𝑔‘𝑥))) / ℎ⦌(({⟨(Base‘ndx), 𝑣⟩, ⟨(+g‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑅 ↦ ((𝑓‘𝑥)(+g‘(𝑅‘𝑥))(𝑔‘𝑥))))⟩, ⟨(.r‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑅 ↦ ((𝑓‘𝑥)(.r‘(𝑅‘𝑥))(𝑔‘𝑥))))⟩} ∪ {⟨(Scalar‘ndx), 𝑆⟩, ⟨( ·𝑠 ‘ndx), (𝑓 ∈ (Base‘𝑆), 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑅 ↦ (𝑓( ·𝑠 ‘(𝑅‘𝑥))(𝑔‘𝑥))))⟩, ⟨(·𝑖‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑆 Σg (𝑥 ∈ dom 𝑅 ↦ ((𝑓‘𝑥)(·𝑖‘(𝑅‘𝑥))(𝑔‘𝑥)))))⟩}) ∪ ({⟨(TopSet‘ndx), (∏t‘(TopOpen ∘ 𝑅))⟩, ⟨(le‘ndx), {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝑣 ∧ ∀𝑥 ∈ dom 𝑅(𝑓‘𝑥)(le‘(𝑅‘𝑥))(𝑔‘𝑥))}⟩, ⟨(dist‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ sup((ran (𝑥 ∈ dom 𝑅 ↦ ((𝑓‘𝑥)(dist‘(𝑅‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ*, < ))⟩} ∪ {⟨(Hom ‘ndx), ℎ⟩, ⟨(comp‘ndx), (𝑎 ∈ (𝑣 × 𝑣), 𝑐 ∈ 𝑣 ↦ (𝑑 ∈ ((2nd ‘𝑎)ℎ𝑐), 𝑒 ∈ (ℎ‘𝑎) ↦ (𝑥 ∈ dom 𝑅 ↦ ((𝑑‘𝑥)(⟨((1st ‘𝑎)‘𝑥), ((2nd ‘𝑎)‘𝑥)⟩(comp‘(𝑅‘𝑥))(𝑐‘𝑥))(𝑒‘𝑥)))))⟩})) ∈ V) → (𝑆Xs𝑅) = ⦋X𝑥 ∈ dom 𝑅(Base‘(𝑅‘𝑥)) / 𝑣⦌⦋(𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ X𝑥 ∈ dom 𝑅((𝑓‘𝑥)(Hom ‘(𝑅‘𝑥))(𝑔‘𝑥))) / ℎ⦌(({⟨(Base‘ndx), 𝑣⟩, ⟨(+g‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑅 ↦ ((𝑓‘𝑥)(+g‘(𝑅‘𝑥))(𝑔‘𝑥))))⟩, ⟨(.r‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑅 ↦ ((𝑓‘𝑥)(.r‘(𝑅‘𝑥))(𝑔‘𝑥))))⟩} ∪ {⟨(Scalar‘ndx), 𝑆⟩, ⟨( ·𝑠 ‘ndx), (𝑓 ∈ (Base‘𝑆), 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑅 ↦ (𝑓( ·𝑠 ‘(𝑅‘𝑥))(𝑔‘𝑥))))⟩, ⟨(·𝑖‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑆 Σg (𝑥 ∈ dom 𝑅 ↦ ((𝑓‘𝑥)(·𝑖‘(𝑅‘𝑥))(𝑔‘𝑥)))))⟩}) ∪ ({⟨(TopSet‘ndx), (∏t‘(TopOpen ∘ 𝑅))⟩, ⟨(le‘ndx), {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝑣 ∧ ∀𝑥 ∈ dom 𝑅(𝑓‘𝑥)(le‘(𝑅‘𝑥))(𝑔‘𝑥))}⟩, ⟨(dist‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ sup((ran (𝑥 ∈ dom 𝑅 ↦ ((𝑓‘𝑥)(dist‘(𝑅‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ*, < ))⟩} ∪ {⟨(Hom ‘ndx), ℎ⟩, ⟨(comp‘ndx), (𝑎 ∈ (𝑣 × 𝑣), 𝑐 ∈ 𝑣 ↦ (𝑑 ∈ ((2nd ‘𝑎)ℎ𝑐), 𝑒 ∈ (ℎ‘𝑎) ↦ (𝑥 ∈ dom 𝑅 ↦ ((𝑑‘𝑥)(⟨((1st ‘𝑎)‘𝑥), ((2nd ‘𝑎)‘𝑥)⟩(comp‘(𝑅‘𝑥))(𝑐‘𝑥))(𝑒‘𝑥)))))⟩})))
195	2, 4, 113, 194	syl3anc 1271	. 2 ⊢ ((𝑆 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊) → (𝑆Xs𝑅) = ⦋X𝑥 ∈ dom 𝑅(Base‘(𝑅‘𝑥)) / 𝑣⦌⦋(𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ X𝑥 ∈ dom 𝑅((𝑓‘𝑥)(Hom ‘(𝑅‘𝑥))(𝑔‘𝑥))) / ℎ⦌(({⟨(Base‘ndx), 𝑣⟩, ⟨(+g‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑅 ↦ ((𝑓‘𝑥)(+g‘(𝑅‘𝑥))(𝑔‘𝑥))))⟩, ⟨(.r‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑅 ↦ ((𝑓‘𝑥)(.r‘(𝑅‘𝑥))(𝑔‘𝑥))))⟩} ∪ {⟨(Scalar‘ndx), 𝑆⟩, ⟨( ·𝑠 ‘ndx), (𝑓 ∈ (Base‘𝑆), 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑅 ↦ (𝑓( ·𝑠 ‘(𝑅‘𝑥))(𝑔‘𝑥))))⟩, ⟨(·𝑖‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑆 Σg (𝑥 ∈ dom 𝑅 ↦ ((𝑓‘𝑥)(·𝑖‘(𝑅‘𝑥))(𝑔‘𝑥)))))⟩}) ∪ ({⟨(TopSet‘ndx), (∏t‘(TopOpen ∘ 𝑅))⟩, ⟨(le‘ndx), {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝑣 ∧ ∀𝑥 ∈ dom 𝑅(𝑓‘𝑥)(le‘(𝑅‘𝑥))(𝑔‘𝑥))}⟩, ⟨(dist‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ sup((ran (𝑥 ∈ dom 𝑅 ↦ ((𝑓‘𝑥)(dist‘(𝑅‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ*, < ))⟩} ∪ {⟨(Hom ‘ndx), ℎ⟩, ⟨(comp‘ndx), (𝑎 ∈ (𝑣 × 𝑣), 𝑐 ∈ 𝑣 ↦ (𝑑 ∈ ((2nd ‘𝑎)ℎ𝑐), 𝑒 ∈ (ℎ‘𝑎) ↦ (𝑥 ∈ dom 𝑅 ↦ ((𝑑‘𝑥)(⟨((1st ‘𝑎)‘𝑥), ((2nd ‘𝑎)‘𝑥)⟩(comp‘(𝑅‘𝑥))(𝑐‘𝑥))(𝑒‘𝑥)))))⟩})))
196	195, 113	eqeltrd 2306	1 ⊢ ((𝑆 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊) → (𝑆Xs𝑅) ∈ V)

Syntax hints:   → wi 4   ∧ wa 104  ∀wal 1393   = wceq 1395   ∈ wcel 2200  ∀wral 2508  Vcvv 2799  ⦋csb 3124   ∪ cun 3195   ⊆ wss 3197  {csn 3666  {cpr 3667  {ctp 3668  ⟨cop 3669   class class class wbr 4083  {copab 4144   ↦ cmpt 4145   × cxp 4717  dom cdm 4719  ran crn 4720   ∘ ccom 4723  Fun wfun 5312   Fn wfn 5313  ‘cfv 5318  (class class class)co 6001   ∈ cmpo 6003  1^st c1st 6284  2^nd c2nd 6285  Xcixp 6845  supcsup 7149  0cc0 7999  ℝ^*cxr 8180   < clt 8181  ℕcn 9110  ndxcnx 13029  Slot cslot 13031  Basecbs 13032  +_gcplusg 13110  ._rcmulr 13111  Scalarcsca 13113   ·_𝑠 cvsca 13114  ·_𝑖cip 13115  TopSetcts 13116  lecple 13117  distcds 13119  Hom chom 13121  compcco 13122  TopOpenctopn 13273  ∏_tcpt 13288   Σ_g cgsu 13290  X_scprds 13298

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 617  ax-in2 618  ax-io 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-13 2202  ax-14 2203  ax-ext 2211  ax-coll 4199  ax-sep 4202  ax-pow 4258  ax-pr 4293  ax-un 4524  ax-setind 4629  ax-cnex 8090  ax-resscn 8091  ax-1cn 8092  ax-1re 8093  ax-icn 8094  ax-addcl 8095  ax-addrcl 8096  ax-mulcl 8097  ax-addcom 8099  ax-mulcom 8100  ax-addass 8101  ax-mulass 8102  ax-distr 8103  ax-i2m1 8104  ax-1rid 8106  ax-0id 8107  ax-rnegex 8108  ax-cnre 8110

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-tru 1398  df-fal 1401  df-nf 1507  df-sb 1809  df-eu 2080  df-mo 2081  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ne 2401  df-ral 2513  df-rex 2514  df-reu 2515  df-rab 2517  df-v 2801  df-sbc 3029  df-csb 3125  df-dif 3199  df-un 3201  df-in 3203  df-ss 3210  df-pw 3651  df-sn 3672  df-pr 3673  df-tp 3674  df-op 3675  df-uni 3889  df-int 3924  df-iun 3967  df-br 4084  df-opab 4146  df-mpt 4147  df-id 4384  df-xp 4725  df-rel 4726  df-cnv 4727  df-co 4728  df-dm 4729  df-rn 4730  df-res 4731  df-ima 4732  df-iota 5278  df-fun 5320  df-fn 5321  df-f 5322  df-f1 5323  df-fo 5324  df-f1o 5325  df-fv 5326  df-riota 5954  df-ov 6004  df-oprab 6005  df-mpo 6006  df-1st 6286  df-2nd 6287  df-map 6797  df-ixp 6846  df-sup 7151  df-sub 8319  df-inn 9111  df-2 9169  df-3 9170  df-4 9171  df-5 9172  df-6 9173  df-7 9174  df-8 9175  df-9 9176  df-n0 9370  df-dec 9579  df-ndx 13035  df-slot 13036  df-base 13038  df-plusg 13123  df-mulr 13124  df-sca 13126  df-vsca 13127  df-ip 13128  df-tset 13129  df-ple 13130  df-ds 13132  df-hom 13134  df-cco 13135  df-rest 13274  df-topn 13275  df-topgen 13293  df-pt 13294  df-prds 13300

This theorem is referenced by:  prdsplusg  13310  prdsmulr  13311  pwsval  13324  xpsval  13385  prdssgrpd  13448