prdsbas

Description: Base set of a structure product. (Contributed by Stefan O'Rear, 3-Jan-2015) (Revised by Mario Carneiro, 15-Aug-2015) (Revised by Thierry Arnoux, 16-Jun-2019) (Revised by Zhi Wang, 18-Aug-2024)

	Ref	Expression
Hypotheses	prdsbas.p	⊢ 𝑃 = ( 𝑆 X_s 𝑅 )
	prdsbas.s	⊢ ( 𝜑 → 𝑆 ∈ 𝑉 )
	prdsbas.r	⊢ ( 𝜑 → 𝑅 ∈ 𝑊 )
	prdsbas.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
	prdsbas.i	⊢ ( 𝜑 → dom 𝑅 = 𝐼 )
Assertion	prdsbas	⊢ ( 𝜑 → 𝐵 = X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) )

Proof

Step	Hyp	Ref	Expression
1		prdsbas.p	⊢ 𝑃 = ( 𝑆 X_s 𝑅 )
2		prdsbas.s	⊢ ( 𝜑 → 𝑆 ∈ 𝑉 )
3		prdsbas.r	⊢ ( 𝜑 → 𝑅 ∈ 𝑊 )
4		prdsbas.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
5		prdsbas.i	⊢ ( 𝜑 → dom 𝑅 = 𝐼 )
6		eqid	⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
7		eqidd	⊢ ( 𝜑 → X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) = X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) )
8		eqidd	⊢ ( 𝜑 → ( 𝑓 ∈ X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) , 𝑔 ∈ X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ↦ ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( +_g ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) = ( 𝑓 ∈ X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) , 𝑔 ∈ X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ↦ ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( +_g ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) )
9		eqidd	⊢ ( 𝜑 → ( 𝑓 ∈ X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) , 𝑔 ∈ X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ↦ ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( ._r ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) = ( 𝑓 ∈ X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) , 𝑔 ∈ X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ↦ ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( ._r ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) )
10		eqidd	⊢ ( 𝜑 → ( 𝑓 ∈ ( Base ‘ 𝑆 ) , 𝑔 ∈ X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ↦ ( 𝑥 ∈ 𝐼 ↦ ( 𝑓 ( ·_𝑠 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) = ( 𝑓 ∈ ( Base ‘ 𝑆 ) , 𝑔 ∈ X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ↦ ( 𝑥 ∈ 𝐼 ↦ ( 𝑓 ( ·_𝑠 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) )
11		eqidd	⊢ ( 𝜑 → ( 𝑓 ∈ X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) , 𝑔 ∈ X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ↦ ( 𝑆 Σ_g ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( ·_𝑖 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ) = ( 𝑓 ∈ X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) , 𝑔 ∈ X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ↦ ( 𝑆 Σ_g ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( ·_𝑖 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ) )
12		eqidd	⊢ ( 𝜑 → ( ∏_t ‘ ( TopOpen ∘ 𝑅 ) ) = ( ∏_t ‘ ( TopOpen ∘ 𝑅 ) ) )
13		eqidd	⊢ ( 𝜑 → { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( { 𝑓 , 𝑔 } ⊆ X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ∧ ∀ 𝑥 ∈ 𝐼 ( 𝑓 ‘ 𝑥 ) ( le ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) } = { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( { 𝑓 , 𝑔 } ⊆ X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ∧ ∀ 𝑥 ∈ 𝐼 ( 𝑓 ‘ 𝑥 ) ( le ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) } )
14		eqidd	⊢ ( 𝜑 → ( 𝑓 ∈ X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) , 𝑔 ∈ X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ↦ sup ( ( ran ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( dist ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ∪ { 0 } ) , ℝ^* , < ) ) = ( 𝑓 ∈ X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) , 𝑔 ∈ X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ↦ sup ( ( ran ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( dist ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ∪ { 0 } ) , ℝ^* , < ) ) )
15		eqidd	⊢ ( 𝜑 → ( 𝑓 ∈ X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) , 𝑔 ∈ X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ↦ X 𝑥 ∈ 𝐼 ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) = ( 𝑓 ∈ X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) , 𝑔 ∈ X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ↦ X 𝑥 ∈ 𝐼 ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) )
16		eqidd	⊢ ( 𝜑 → ( 𝑎 ∈ ( X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) × X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ) , 𝑐 ∈ X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ↦ ( 𝑑 ∈ ( ( 2^nd ‘ 𝑎 ) ( 𝑓 ∈ X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) , 𝑔 ∈ X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ↦ X 𝑥 ∈ 𝐼 ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) 𝑐 ) , 𝑒 ∈ ( ( 𝑓 ∈ X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) , 𝑔 ∈ X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ↦ X 𝑥 ∈ 𝐼 ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ‘ 𝑎 ) ↦ ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑑 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑎 ) ‘ 𝑥 ) , ( ( 2^nd ‘ 𝑎 ) ‘ 𝑥 ) ⟩ ( comp ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑐 ‘ 𝑥 ) ) ( 𝑒 ‘ 𝑥 ) ) ) ) ) = ( 𝑎 ∈ ( X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) × X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ) , 𝑐 ∈ X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ↦ ( 𝑑 ∈ ( ( 2^nd ‘ 𝑎 ) ( 𝑓 ∈ X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) , 𝑔 ∈ X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ↦ X 𝑥 ∈ 𝐼 ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) 𝑐 ) , 𝑒 ∈ ( ( 𝑓 ∈ X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) , 𝑔 ∈ X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ↦ X 𝑥 ∈ 𝐼 ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ‘ 𝑎 ) ↦ ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑑 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑎 ) ‘ 𝑥 ) , ( ( 2^nd ‘ 𝑎 ) ‘ 𝑥 ) ⟩ ( comp ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑐 ‘ 𝑥 ) ) ( 𝑒 ‘ 𝑥 ) ) ) ) ) )
17	1 6 5 7 8 9 10 11 12 13 14 15 16 2 3	prdsval	⊢ ( 𝜑 → 𝑃 = ( ( { ⟨ ( Base ‘ ndx ) , X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ⟩ , ⟨ ( +_g ‘ ndx ) , ( 𝑓 ∈ X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) , 𝑔 ∈ X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ↦ ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( +_g ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ⟩ , ⟨ ( ._r ‘ ndx ) , ( 𝑓 ∈ X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) , 𝑔 ∈ X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ↦ ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( ._r ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑆 ⟩ , ⟨ ( ·_𝑠 ‘ ndx ) , ( 𝑓 ∈ ( Base ‘ 𝑆 ) , 𝑔 ∈ X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ↦ ( 𝑥 ∈ 𝐼 ↦ ( 𝑓 ( ·_𝑠 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ⟩ , ⟨ ( ·_𝑖 ‘ ndx ) , ( 𝑓 ∈ X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) , 𝑔 ∈ X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ↦ ( 𝑆 Σ_g ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( ·_𝑖 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ) ⟩ } ) ∪ ( { ⟨ ( TopSet ‘ ndx ) , ( ∏_t ‘ ( TopOpen ∘ 𝑅 ) ) ⟩ , ⟨ ( le ‘ ndx ) , { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( { 𝑓 , 𝑔 } ⊆ X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ∧ ∀ 𝑥 ∈ 𝐼 ( 𝑓 ‘ 𝑥 ) ( le ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) } ⟩ , ⟨ ( dist ‘ ndx ) , ( 𝑓 ∈ X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) , 𝑔 ∈ X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ↦ sup ( ( ran ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( dist ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ∪ { 0 } ) , ℝ^* , < ) ) ⟩ } ∪ { ⟨ ( Hom ‘ ndx ) , ( 𝑓 ∈ X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) , 𝑔 ∈ X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ↦ X 𝑥 ∈ 𝐼 ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ⟩ , ⟨ ( comp ‘ ndx ) , ( 𝑎 ∈ ( X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) × X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ) , 𝑐 ∈ X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ↦ ( 𝑑 ∈ ( ( 2^nd ‘ 𝑎 ) ( 𝑓 ∈ X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) , 𝑔 ∈ X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ↦ X 𝑥 ∈ 𝐼 ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) 𝑐 ) , 𝑒 ∈ ( ( 𝑓 ∈ X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) , 𝑔 ∈ X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ↦ X 𝑥 ∈ 𝐼 ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ‘ 𝑎 ) ↦ ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑑 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑎 ) ‘ 𝑥 ) , ( ( 2^nd ‘ 𝑎 ) ‘ 𝑥 ) ⟩ ( comp ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑐 ‘ 𝑥 ) ) ( 𝑒 ‘ 𝑥 ) ) ) ) ) ⟩ } ) ) )
18		baseid	⊢ Base = Slot ( Base ‘ ndx )
19	18	strfvss	⊢ ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ⊆ ∪ ran ( 𝑅 ‘ 𝑥 )
20		fvssunirn	⊢ ( 𝑅 ‘ 𝑥 ) ⊆ ∪ ran 𝑅
21		rnss	⊢ ( ( 𝑅 ‘ 𝑥 ) ⊆ ∪ ran 𝑅 → ran ( 𝑅 ‘ 𝑥 ) ⊆ ran ∪ ran 𝑅 )
22		uniss	⊢ ( ran ( 𝑅 ‘ 𝑥 ) ⊆ ran ∪ ran 𝑅 → ∪ ran ( 𝑅 ‘ 𝑥 ) ⊆ ∪ ran ∪ ran 𝑅 )
23	20 21 22	mp2b	⊢ ∪ ran ( 𝑅 ‘ 𝑥 ) ⊆ ∪ ran ∪ ran 𝑅
24	19 23	sstri	⊢ ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ⊆ ∪ ran ∪ ran 𝑅
25	24	rgenw	⊢ ∀ 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ⊆ ∪ ran ∪ ran 𝑅
26		iunss	⊢ ( ∪ 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ⊆ ∪ ran ∪ ran 𝑅 ↔ ∀ 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ⊆ ∪ ran ∪ ran 𝑅 )
27	25 26	mpbir	⊢ ∪ 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ⊆ ∪ ran ∪ ran 𝑅
28		rnexg	⊢ ( 𝑅 ∈ 𝑊 → ran 𝑅 ∈ V )
29		uniexg	⊢ ( ran 𝑅 ∈ V → ∪ ran 𝑅 ∈ V )
30	3 28 29	3syl	⊢ ( 𝜑 → ∪ ran 𝑅 ∈ V )
31		rnexg	⊢ ( ∪ ran 𝑅 ∈ V → ran ∪ ran 𝑅 ∈ V )
32		uniexg	⊢ ( ran ∪ ran 𝑅 ∈ V → ∪ ran ∪ ran 𝑅 ∈ V )
33	30 31 32	3syl	⊢ ( 𝜑 → ∪ ran ∪ ran 𝑅 ∈ V )
34		ssexg	⊢ ( ( ∪ 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ⊆ ∪ ran ∪ ran 𝑅 ∧ ∪ ran ∪ ran 𝑅 ∈ V ) → ∪ 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ∈ V )
35	27 33 34	sylancr	⊢ ( 𝜑 → ∪ 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ∈ V )
36		ixpssmap2g	⊢ ( ∪ 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ∈ V → X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ⊆ ( ∪ 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ↑_m 𝐼 ) )
37		ovex	⊢ ( ∪ 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ↑_m 𝐼 ) ∈ V
38	37	ssex	⊢ ( X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ⊆ ( ∪ 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ↑_m 𝐼 ) → X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ∈ V )
39	35 36 38	3syl	⊢ ( 𝜑 → X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ∈ V )
40		snsstp1	⊢ { ⟨ ( Base ‘ ndx ) , X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ⟩ } ⊆ { ⟨ ( Base ‘ ndx ) , X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ⟩ , ⟨ ( +_g ‘ ndx ) , ( 𝑓 ∈ X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) , 𝑔 ∈ X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ↦ ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( +_g ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ⟩ , ⟨ ( ._r ‘ ndx ) , ( 𝑓 ∈ X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) , 𝑔 ∈ X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ↦ ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( ._r ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ⟩ }
41		ssun1	⊢ { ⟨ ( Base ‘ ndx ) , X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ⟩ , ⟨ ( +_g ‘ ndx ) , ( 𝑓 ∈ X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) , 𝑔 ∈ X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ↦ ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( +_g ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ⟩ , ⟨ ( ._r ‘ ndx ) , ( 𝑓 ∈ X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) , 𝑔 ∈ X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ↦ ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( ._r ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ⟩ } ⊆ ( { ⟨ ( Base ‘ ndx ) , X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ⟩ , ⟨ ( +_g ‘ ndx ) , ( 𝑓 ∈ X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) , 𝑔 ∈ X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ↦ ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( +_g ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ⟩ , ⟨ ( ._r ‘ ndx ) , ( 𝑓 ∈ X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) , 𝑔 ∈ X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ↦ ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( ._r ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑆 ⟩ , ⟨ ( ·_𝑠 ‘ ndx ) , ( 𝑓 ∈ ( Base ‘ 𝑆 ) , 𝑔 ∈ X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ↦ ( 𝑥 ∈ 𝐼 ↦ ( 𝑓 ( ·_𝑠 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ⟩ , ⟨ ( ·_𝑖 ‘ ndx ) , ( 𝑓 ∈ X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) , 𝑔 ∈ X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ↦ ( 𝑆 Σ_g ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( ·_𝑖 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ) ⟩ } )
42	40 41	sstri	⊢ { ⟨ ( Base ‘ ndx ) , X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ⟩ } ⊆ ( { ⟨ ( Base ‘ ndx ) , X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ⟩ , ⟨ ( +_g ‘ ndx ) , ( 𝑓 ∈ X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) , 𝑔 ∈ X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ↦ ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( +_g ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ⟩ , ⟨ ( ._r ‘ ndx ) , ( 𝑓 ∈ X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) , 𝑔 ∈ X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ↦ ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( ._r ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑆 ⟩ , ⟨ ( ·_𝑠 ‘ ndx ) , ( 𝑓 ∈ ( Base ‘ 𝑆 ) , 𝑔 ∈ X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ↦ ( 𝑥 ∈ 𝐼 ↦ ( 𝑓 ( ·_𝑠 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ⟩ , ⟨ ( ·_𝑖 ‘ ndx ) , ( 𝑓 ∈ X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) , 𝑔 ∈ X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ↦ ( 𝑆 Σ_g ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( ·_𝑖 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ) ⟩ } )
43		ssun1	⊢ ( { ⟨ ( Base ‘ ndx ) , X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ⟩ , ⟨ ( +_g ‘ ndx ) , ( 𝑓 ∈ X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) , 𝑔 ∈ X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ↦ ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( +_g ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ⟩ , ⟨ ( ._r ‘ ndx ) , ( 𝑓 ∈ X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) , 𝑔 ∈ X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ↦ ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( ._r ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑆 ⟩ , ⟨ ( ·_𝑠 ‘ ndx ) , ( 𝑓 ∈ ( Base ‘ 𝑆 ) , 𝑔 ∈ X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ↦ ( 𝑥 ∈ 𝐼 ↦ ( 𝑓 ( ·_𝑠 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ⟩ , ⟨ ( ·_𝑖 ‘ ndx ) , ( 𝑓 ∈ X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) , 𝑔 ∈ X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ↦ ( 𝑆 Σ_g ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( ·_𝑖 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ) ⟩ } ) ⊆ ( ( { ⟨ ( Base ‘ ndx ) , X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ⟩ , ⟨ ( +_g ‘ ndx ) , ( 𝑓 ∈ X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) , 𝑔 ∈ X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ↦ ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( +_g ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ⟩ , ⟨ ( ._r ‘ ndx ) , ( 𝑓 ∈ X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) , 𝑔 ∈ X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ↦ ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( ._r ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑆 ⟩ , ⟨ ( ·_𝑠 ‘ ndx ) , ( 𝑓 ∈ ( Base ‘ 𝑆 ) , 𝑔 ∈ X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ↦ ( 𝑥 ∈ 𝐼 ↦ ( 𝑓 ( ·_𝑠 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ⟩ , ⟨ ( ·_𝑖 ‘ ndx ) , ( 𝑓 ∈ X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) , 𝑔 ∈ X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ↦ ( 𝑆 Σ_g ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( ·_𝑖 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ) ⟩ } ) ∪ ( { ⟨ ( TopSet ‘ ndx ) , ( ∏_t ‘ ( TopOpen ∘ 𝑅 ) ) ⟩ , ⟨ ( le ‘ ndx ) , { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( { 𝑓 , 𝑔 } ⊆ X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ∧ ∀ 𝑥 ∈ 𝐼 ( 𝑓 ‘ 𝑥 ) ( le ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) } ⟩ , ⟨ ( dist ‘ ndx ) , ( 𝑓 ∈ X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) , 𝑔 ∈ X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ↦ sup ( ( ran ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( dist ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ∪ { 0 } ) , ℝ^* , < ) ) ⟩ } ∪ { ⟨ ( Hom ‘ ndx ) , ( 𝑓 ∈ X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) , 𝑔 ∈ X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ↦ X 𝑥 ∈ 𝐼 ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ⟩ , ⟨ ( comp ‘ ndx ) , ( 𝑎 ∈ ( X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) × X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ) , 𝑐 ∈ X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ↦ ( 𝑑 ∈ ( ( 2^nd ‘ 𝑎 ) ( 𝑓 ∈ X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) , 𝑔 ∈ X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ↦ X 𝑥 ∈ 𝐼 ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) 𝑐 ) , 𝑒 ∈ ( ( 𝑓 ∈ X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) , 𝑔 ∈ X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ↦ X 𝑥 ∈ 𝐼 ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ‘ 𝑎 ) ↦ ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑑 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑎 ) ‘ 𝑥 ) , ( ( 2^nd ‘ 𝑎 ) ‘ 𝑥 ) ⟩ ( comp ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑐 ‘ 𝑥 ) ) ( 𝑒 ‘ 𝑥 ) ) ) ) ) ⟩ } ) )
44	42 43	sstri	⊢ { ⟨ ( Base ‘ ndx ) , X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ⟩ } ⊆ ( ( { ⟨ ( Base ‘ ndx ) , X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ⟩ , ⟨ ( +_g ‘ ndx ) , ( 𝑓 ∈ X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) , 𝑔 ∈ X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ↦ ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( +_g ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ⟩ , ⟨ ( ._r ‘ ndx ) , ( 𝑓 ∈ X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) , 𝑔 ∈ X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ↦ ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( ._r ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑆 ⟩ , ⟨ ( ·_𝑠 ‘ ndx ) , ( 𝑓 ∈ ( Base ‘ 𝑆 ) , 𝑔 ∈ X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ↦ ( 𝑥 ∈ 𝐼 ↦ ( 𝑓 ( ·_𝑠 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ⟩ , ⟨ ( ·_𝑖 ‘ ndx ) , ( 𝑓 ∈ X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) , 𝑔 ∈ X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ↦ ( 𝑆 Σ_g ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( ·_𝑖 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ) ⟩ } ) ∪ ( { ⟨ ( TopSet ‘ ndx ) , ( ∏_t ‘ ( TopOpen ∘ 𝑅 ) ) ⟩ , ⟨ ( le ‘ ndx ) , { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( { 𝑓 , 𝑔 } ⊆ X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ∧ ∀ 𝑥 ∈ 𝐼 ( 𝑓 ‘ 𝑥 ) ( le ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) } ⟩ , ⟨ ( dist ‘ ndx ) , ( 𝑓 ∈ X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) , 𝑔 ∈ X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ↦ sup ( ( ran ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( dist ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ∪ { 0 } ) , ℝ^* , < ) ) ⟩ } ∪ { ⟨ ( Hom ‘ ndx ) , ( 𝑓 ∈ X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) , 𝑔 ∈ X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ↦ X 𝑥 ∈ 𝐼 ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ⟩ , ⟨ ( comp ‘ ndx ) , ( 𝑎 ∈ ( X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) × X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ) , 𝑐 ∈ X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ↦ ( 𝑑 ∈ ( ( 2^nd ‘ 𝑎 ) ( 𝑓 ∈ X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) , 𝑔 ∈ X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ↦ X 𝑥 ∈ 𝐼 ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) 𝑐 ) , 𝑒 ∈ ( ( 𝑓 ∈ X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) , 𝑔 ∈ X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ↦ X 𝑥 ∈ 𝐼 ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ‘ 𝑎 ) ↦ ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑑 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑎 ) ‘ 𝑥 ) , ( ( 2^nd ‘ 𝑎 ) ‘ 𝑥 ) ⟩ ( comp ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑐 ‘ 𝑥 ) ) ( 𝑒 ‘ 𝑥 ) ) ) ) ) ⟩ } ) )
45	17 4 18 39 44	prdsbaslem	⊢ ( 𝜑 → 𝐵 = X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) )

Metamath Proof Explorer

Theorem prdsbas

Proof