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	\|- P = ( S Xs_ R )
	prdsbas.s	\|- ( ph -> S e. V )
	prdsbas.r	\|- ( ph -> R e. W )
	prdsbas.b	\|- B = ( Base ` P )
	prdsbas.i	\|- ( ph -> dom R = I )
Assertion	prdsbas	\|- ( ph -> B = X_ x e. I ( Base ` ( R ` x ) ) )

Proof

Step	Hyp	Ref	Expression
1		prdsbas.p	\|- P = ( S Xs_ R )
2		prdsbas.s	\|- ( ph -> S e. V )
3		prdsbas.r	\|- ( ph -> R e. W )
4		prdsbas.b	\|- B = ( Base ` P )
5		prdsbas.i	\|- ( ph -> dom R = I )
6		eqid	\|- ( Base ` S ) = ( Base ` S )
7		eqidd	\|- ( ph -> X_ x e. I ( Base ` ( R ` x ) ) = X_ x e. I ( Base ` ( R ` x ) ) )
8		eqidd	\|- ( ph -> ( f e. X_ x e. I ( Base ` ( R ` x ) ) , g e. X_ x e. I ( Base ` ( R ` x ) ) \|-> ( x e. I \|-> ( ( f ` x ) ( +g ` ( R ` x ) ) ( g ` x ) ) ) ) = ( f e. X_ x e. I ( Base ` ( R ` x ) ) , g e. X_ x e. I ( Base ` ( R ` x ) ) \|-> ( x e. I \|-> ( ( f ` x ) ( +g ` ( R ` x ) ) ( g ` x ) ) ) ) )
9		eqidd	\|- ( ph -> ( f e. X_ x e. I ( Base ` ( R ` x ) ) , g e. X_ x e. I ( Base ` ( R ` x ) ) \|-> ( x e. I \|-> ( ( f ` x ) ( .r ` ( R ` x ) ) ( g ` x ) ) ) ) = ( f e. X_ x e. I ( Base ` ( R ` x ) ) , g e. X_ x e. I ( Base ` ( R ` x ) ) \|-> ( x e. I \|-> ( ( f ` x ) ( .r ` ( R ` x ) ) ( g ` x ) ) ) ) )
10		eqidd	\|- ( ph -> ( f e. ( Base ` S ) , g e. X_ x e. I ( Base ` ( R ` x ) ) \|-> ( x e. I \|-> ( f ( .s ` ( R ` x ) ) ( g ` x ) ) ) ) = ( f e. ( Base ` S ) , g e. X_ x e. I ( Base ` ( R ` x ) ) \|-> ( x e. I \|-> ( f ( .s ` ( R ` x ) ) ( g ` x ) ) ) ) )
11		eqidd	\|- ( ph -> ( f e. X_ x e. I ( Base ` ( R ` x ) ) , g e. X_ x e. I ( Base ` ( R ` x ) ) \|-> ( S gsum ( x e. I \|-> ( ( f ` x ) ( .i ` ( R ` x ) ) ( g ` x ) ) ) ) ) = ( f e. X_ x e. I ( Base ` ( R ` x ) ) , g e. X_ x e. I ( Base ` ( R ` x ) ) \|-> ( S gsum ( x e. I \|-> ( ( f ` x ) ( .i ` ( R ` x ) ) ( g ` x ) ) ) ) ) )
12		eqidd	\|- ( ph -> ( Xt_ ` ( TopOpen o. R ) ) = ( Xt_ ` ( TopOpen o. R ) ) )
13		eqidd	\|- ( ph -> { <. f , g >. \| ( { f , g } C_ X_ x e. I ( Base ` ( R ` x ) ) /\ A. x e. I ( f ` x ) ( le ` ( R ` x ) ) ( g ` x ) ) } = { <. f , g >. \| ( { f , g } C_ X_ x e. I ( Base ` ( R ` x ) ) /\ A. x e. I ( f ` x ) ( le ` ( R ` x ) ) ( g ` x ) ) } )
14		eqidd	\|- ( ph -> ( f e. X_ x e. I ( Base ` ( R ` x ) ) , g e. X_ x e. I ( Base ` ( R ` x ) ) \|-> sup ( ( ran ( x e. I \|-> ( ( f ` x ) ( dist ` ( R ` x ) ) ( g ` x ) ) ) u. { 0 } ) , RR* , < ) ) = ( f e. X_ x e. I ( Base ` ( R ` x ) ) , g e. X_ x e. I ( Base ` ( R ` x ) ) \|-> sup ( ( ran ( x e. I \|-> ( ( f ` x ) ( dist ` ( R ` x ) ) ( g ` x ) ) ) u. { 0 } ) , RR* , < ) ) )
15		eqidd	\|- ( ph -> ( f e. X_ x e. I ( Base ` ( R ` x ) ) , g e. X_ x e. I ( Base ` ( R ` x ) ) \|-> X_ x e. I ( ( f ` x ) ( Hom ` ( R ` x ) ) ( g ` x ) ) ) = ( f e. X_ x e. I ( Base ` ( R ` x ) ) , g e. X_ x e. I ( Base ` ( R ` x ) ) \|-> X_ x e. I ( ( f ` x ) ( Hom ` ( R ` x ) ) ( g ` x ) ) ) )
16		eqidd	\|- ( ph -> ( a e. ( X_ x e. I ( Base ` ( R ` x ) ) X. X_ x e. I ( Base ` ( R ` x ) ) ) , c e. X_ x e. I ( Base ` ( R ` x ) ) \|-> ( d e. ( ( 2nd ` a ) ( f e. X_ x e. I ( Base ` ( R ` x ) ) , g e. X_ x e. I ( Base ` ( R ` x ) ) \|-> X_ x e. I ( ( f ` x ) ( Hom ` ( R ` x ) ) ( g ` x ) ) ) c ) , e e. ( ( f e. X_ x e. I ( Base ` ( R ` x ) ) , g e. X_ x e. I ( Base ` ( R ` x ) ) \|-> X_ x e. I ( ( f ` x ) ( Hom ` ( R ` x ) ) ( g ` x ) ) ) ` a ) \|-> ( x e. I \|-> ( ( d ` x ) ( <. ( ( 1st ` a ) ` x ) , ( ( 2nd ` a ) ` x ) >. ( comp ` ( R ` x ) ) ( c ` x ) ) ( e ` x ) ) ) ) ) = ( a e. ( X_ x e. I ( Base ` ( R ` x ) ) X. X_ x e. I ( Base ` ( R ` x ) ) ) , c e. X_ x e. I ( Base ` ( R ` x ) ) \|-> ( d e. ( ( 2nd ` a ) ( f e. X_ x e. I ( Base ` ( R ` x ) ) , g e. X_ x e. I ( Base ` ( R ` x ) ) \|-> X_ x e. I ( ( f ` x ) ( Hom ` ( R ` x ) ) ( g ` x ) ) ) c ) , e e. ( ( f e. X_ x e. I ( Base ` ( R ` x ) ) , g e. X_ x e. I ( Base ` ( R ` x ) ) \|-> X_ x e. I ( ( f ` x ) ( Hom ` ( R ` x ) ) ( g ` x ) ) ) ` a ) \|-> ( x e. I \|-> ( ( d ` x ) ( <. ( ( 1st ` a ) ` x ) , ( ( 2nd ` a ) ` x ) >. ( comp ` ( R ` x ) ) ( c ` x ) ) ( e ` x ) ) ) ) ) )
17	1 6 5 7 8 9 10 11 12 13 14 15 16 2 3	prdsval	\|- ( ph -> P = ( ( { <. ( Base ` ndx ) , X_ x e. I ( Base ` ( R ` x ) ) >. , <. ( +g ` ndx ) , ( f e. X_ x e. I ( Base ` ( R ` x ) ) , g e. X_ x e. I ( Base ` ( R ` x ) ) \|-> ( x e. I \|-> ( ( f ` x ) ( +g ` ( R ` x ) ) ( g ` x ) ) ) ) >. , <. ( .r ` ndx ) , ( f e. X_ x e. I ( Base ` ( R ` x ) ) , g e. X_ x e. I ( Base ` ( R ` x ) ) \|-> ( x e. I \|-> ( ( f ` x ) ( .r ` ( R ` x ) ) ( g ` x ) ) ) ) >. } u. { <. ( Scalar ` ndx ) , S >. , <. ( .s ` ndx ) , ( f e. ( Base ` S ) , g e. X_ x e. I ( Base ` ( R ` x ) ) \|-> ( x e. I \|-> ( f ( .s ` ( R ` x ) ) ( g ` x ) ) ) ) >. , <. ( .i ` ndx ) , ( f e. X_ x e. I ( Base ` ( R ` x ) ) , g e. X_ x e. I ( Base ` ( R ` x ) ) \|-> ( S gsum ( x e. I \|-> ( ( f ` x ) ( .i ` ( R ` x ) ) ( g ` x ) ) ) ) ) >. } ) u. ( { <. ( TopSet ` ndx ) , ( Xt_ ` ( TopOpen o. R ) ) >. , <. ( le ` ndx ) , { <. f , g >. \| ( { f , g } C_ X_ x e. I ( Base ` ( R ` x ) ) /\ A. x e. I ( f ` x ) ( le ` ( R ` x ) ) ( g ` x ) ) } >. , <. ( dist ` ndx ) , ( f e. X_ x e. I ( Base ` ( R ` x ) ) , g e. X_ x e. I ( Base ` ( R ` x ) ) \|-> sup ( ( ran ( x e. I \|-> ( ( f ` x ) ( dist ` ( R ` x ) ) ( g ` x ) ) ) u. { 0 } ) , RR* , < ) ) >. } u. { <. ( Hom ` ndx ) , ( f e. X_ x e. I ( Base ` ( R ` x ) ) , g e. X_ x e. I ( Base ` ( R ` x ) ) \|-> X_ x e. I ( ( f ` x ) ( Hom ` ( R ` x ) ) ( g ` x ) ) ) >. , <. ( comp ` ndx ) , ( a e. ( X_ x e. I ( Base ` ( R ` x ) ) X. X_ x e. I ( Base ` ( R ` x ) ) ) , c e. X_ x e. I ( Base ` ( R ` x ) ) \|-> ( d e. ( ( 2nd ` a ) ( f e. X_ x e. I ( Base ` ( R ` x ) ) , g e. X_ x e. I ( Base ` ( R ` x ) ) \|-> X_ x e. I ( ( f ` x ) ( Hom ` ( R ` x ) ) ( g ` x ) ) ) c ) , e e. ( ( f e. X_ x e. I ( Base ` ( R ` x ) ) , g e. X_ x e. I ( Base ` ( R ` x ) ) \|-> X_ x e. I ( ( f ` x ) ( Hom ` ( R ` x ) ) ( g ` x ) ) ) ` a ) \|-> ( x e. I \|-> ( ( d ` x ) ( <. ( ( 1st ` a ) ` x ) , ( ( 2nd ` a ) ` x ) >. ( comp ` ( R ` x ) ) ( c ` x ) ) ( e ` x ) ) ) ) ) >. } ) ) )
18		baseid	\|- Base = Slot ( Base ` ndx )
19	18	strfvss	\|- ( Base ` ( R ` x ) ) C_ U. ran ( R ` x )
20		fvssunirn	\|- ( R ` x ) C_ U. ran R
21		rnss	\|- ( ( R ` x ) C_ U. ran R -> ran ( R ` x ) C_ ran U. ran R )
22		uniss	\|- ( ran ( R ` x ) C_ ran U. ran R -> U. ran ( R ` x ) C_ U. ran U. ran R )
23	20 21 22	mp2b	\|- U. ran ( R ` x ) C_ U. ran U. ran R
24	19 23	sstri	\|- ( Base ` ( R ` x ) ) C_ U. ran U. ran R
25	24	rgenw	\|- A. x e. I ( Base ` ( R ` x ) ) C_ U. ran U. ran R
26		iunss	\|- ( U_ x e. I ( Base ` ( R ` x ) ) C_ U. ran U. ran R <-> A. x e. I ( Base ` ( R ` x ) ) C_ U. ran U. ran R )
27	25 26	mpbir	\|- U_ x e. I ( Base ` ( R ` x ) ) C_ U. ran U. ran R
28		rnexg	\|- ( R e. W -> ran R e. _V )
29		uniexg	\|- ( ran R e. _V -> U. ran R e. _V )
30	3 28 29	3syl	\|- ( ph -> U. ran R e. _V )
31		rnexg	\|- ( U. ran R e. _V -> ran U. ran R e. _V )
32		uniexg	\|- ( ran U. ran R e. _V -> U. ran U. ran R e. _V )
33	30 31 32	3syl	\|- ( ph -> U. ran U. ran R e. _V )
34		ssexg	\|- ( ( U_ x e. I ( Base ` ( R ` x ) ) C_ U. ran U. ran R /\ U. ran U. ran R e. _V ) -> U_ x e. I ( Base ` ( R ` x ) ) e. _V )
35	27 33 34	sylancr	\|- ( ph -> U_ x e. I ( Base ` ( R ` x ) ) e. _V )
36		ixpssmap2g	\|- ( U_ x e. I ( Base ` ( R ` x ) ) e. _V -> X_ x e. I ( Base ` ( R ` x ) ) C_ ( U_ x e. I ( Base ` ( R ` x ) ) ^m I ) )
37		ovex	\|- ( U_ x e. I ( Base ` ( R ` x ) ) ^m I ) e. _V
38	37	ssex	\|- ( X_ x e. I ( Base ` ( R ` x ) ) C_ ( U_ x e. I ( Base ` ( R ` x ) ) ^m I ) -> X_ x e. I ( Base ` ( R ` x ) ) e. _V )
39	35 36 38	3syl	\|- ( ph -> X_ x e. I ( Base ` ( R ` x ) ) e. _V )
40		snsstp1	\|- { <. ( Base ` ndx ) , X_ x e. I ( Base ` ( R ` x ) ) >. } C_ { <. ( Base ` ndx ) , X_ x e. I ( Base ` ( R ` x ) ) >. , <. ( +g ` ndx ) , ( f e. X_ x e. I ( Base ` ( R ` x ) ) , g e. X_ x e. I ( Base ` ( R ` x ) ) \|-> ( x e. I \|-> ( ( f ` x ) ( +g ` ( R ` x ) ) ( g ` x ) ) ) ) >. , <. ( .r ` ndx ) , ( f e. X_ x e. I ( Base ` ( R ` x ) ) , g e. X_ x e. I ( Base ` ( R ` x ) ) \|-> ( x e. I \|-> ( ( f ` x ) ( .r ` ( R ` x ) ) ( g ` x ) ) ) ) >. }
41		ssun1	\|- { <. ( Base ` ndx ) , X_ x e. I ( Base ` ( R ` x ) ) >. , <. ( +g ` ndx ) , ( f e. X_ x e. I ( Base ` ( R ` x ) ) , g e. X_ x e. I ( Base ` ( R ` x ) ) \|-> ( x e. I \|-> ( ( f ` x ) ( +g ` ( R ` x ) ) ( g ` x ) ) ) ) >. , <. ( .r ` ndx ) , ( f e. X_ x e. I ( Base ` ( R ` x ) ) , g e. X_ x e. I ( Base ` ( R ` x ) ) \|-> ( x e. I \|-> ( ( f ` x ) ( .r ` ( R ` x ) ) ( g ` x ) ) ) ) >. } C_ ( { <. ( Base ` ndx ) , X_ x e. I ( Base ` ( R ` x ) ) >. , <. ( +g ` ndx ) , ( f e. X_ x e. I ( Base ` ( R ` x ) ) , g e. X_ x e. I ( Base ` ( R ` x ) ) \|-> ( x e. I \|-> ( ( f ` x ) ( +g ` ( R ` x ) ) ( g ` x ) ) ) ) >. , <. ( .r ` ndx ) , ( f e. X_ x e. I ( Base ` ( R ` x ) ) , g e. X_ x e. I ( Base ` ( R ` x ) ) \|-> ( x e. I \|-> ( ( f ` x ) ( .r ` ( R ` x ) ) ( g ` x ) ) ) ) >. } u. { <. ( Scalar ` ndx ) , S >. , <. ( .s ` ndx ) , ( f e. ( Base ` S ) , g e. X_ x e. I ( Base ` ( R ` x ) ) \|-> ( x e. I \|-> ( f ( .s ` ( R ` x ) ) ( g ` x ) ) ) ) >. , <. ( .i ` ndx ) , ( f e. X_ x e. I ( Base ` ( R ` x ) ) , g e. X_ x e. I ( Base ` ( R ` x ) ) \|-> ( S gsum ( x e. I \|-> ( ( f ` x ) ( .i ` ( R ` x ) ) ( g ` x ) ) ) ) ) >. } )
42	40 41	sstri	\|- { <. ( Base ` ndx ) , X_ x e. I ( Base ` ( R ` x ) ) >. } C_ ( { <. ( Base ` ndx ) , X_ x e. I ( Base ` ( R ` x ) ) >. , <. ( +g ` ndx ) , ( f e. X_ x e. I ( Base ` ( R ` x ) ) , g e. X_ x e. I ( Base ` ( R ` x ) ) \|-> ( x e. I \|-> ( ( f ` x ) ( +g ` ( R ` x ) ) ( g ` x ) ) ) ) >. , <. ( .r ` ndx ) , ( f e. X_ x e. I ( Base ` ( R ` x ) ) , g e. X_ x e. I ( Base ` ( R ` x ) ) \|-> ( x e. I \|-> ( ( f ` x ) ( .r ` ( R ` x ) ) ( g ` x ) ) ) ) >. } u. { <. ( Scalar ` ndx ) , S >. , <. ( .s ` ndx ) , ( f e. ( Base ` S ) , g e. X_ x e. I ( Base ` ( R ` x ) ) \|-> ( x e. I \|-> ( f ( .s ` ( R ` x ) ) ( g ` x ) ) ) ) >. , <. ( .i ` ndx ) , ( f e. X_ x e. I ( Base ` ( R ` x ) ) , g e. X_ x e. I ( Base ` ( R ` x ) ) \|-> ( S gsum ( x e. I \|-> ( ( f ` x ) ( .i ` ( R ` x ) ) ( g ` x ) ) ) ) ) >. } )
43		ssun1	\|- ( { <. ( Base ` ndx ) , X_ x e. I ( Base ` ( R ` x ) ) >. , <. ( +g ` ndx ) , ( f e. X_ x e. I ( Base ` ( R ` x ) ) , g e. X_ x e. I ( Base ` ( R ` x ) ) \|-> ( x e. I \|-> ( ( f ` x ) ( +g ` ( R ` x ) ) ( g ` x ) ) ) ) >. , <. ( .r ` ndx ) , ( f e. X_ x e. I ( Base ` ( R ` x ) ) , g e. X_ x e. I ( Base ` ( R ` x ) ) \|-> ( x e. I \|-> ( ( f ` x ) ( .r ` ( R ` x ) ) ( g ` x ) ) ) ) >. } u. { <. ( Scalar ` ndx ) , S >. , <. ( .s ` ndx ) , ( f e. ( Base ` S ) , g e. X_ x e. I ( Base ` ( R ` x ) ) \|-> ( x e. I \|-> ( f ( .s ` ( R ` x ) ) ( g ` x ) ) ) ) >. , <. ( .i ` ndx ) , ( f e. X_ x e. I ( Base ` ( R ` x ) ) , g e. X_ x e. I ( Base ` ( R ` x ) ) \|-> ( S gsum ( x e. I \|-> ( ( f ` x ) ( .i ` ( R ` x ) ) ( g ` x ) ) ) ) ) >. } ) C_ ( ( { <. ( Base ` ndx ) , X_ x e. I ( Base ` ( R ` x ) ) >. , <. ( +g ` ndx ) , ( f e. X_ x e. I ( Base ` ( R ` x ) ) , g e. X_ x e. I ( Base ` ( R ` x ) ) \|-> ( x e. I \|-> ( ( f ` x ) ( +g ` ( R ` x ) ) ( g ` x ) ) ) ) >. , <. ( .r ` ndx ) , ( f e. X_ x e. I ( Base ` ( R ` x ) ) , g e. X_ x e. I ( Base ` ( R ` x ) ) \|-> ( x e. I \|-> ( ( f ` x ) ( .r ` ( R ` x ) ) ( g ` x ) ) ) ) >. } u. { <. ( Scalar ` ndx ) , S >. , <. ( .s ` ndx ) , ( f e. ( Base ` S ) , g e. X_ x e. I ( Base ` ( R ` x ) ) \|-> ( x e. I \|-> ( f ( .s ` ( R ` x ) ) ( g ` x ) ) ) ) >. , <. ( .i ` ndx ) , ( f e. X_ x e. I ( Base ` ( R ` x ) ) , g e. X_ x e. I ( Base ` ( R ` x ) ) \|-> ( S gsum ( x e. I \|-> ( ( f ` x ) ( .i ` ( R ` x ) ) ( g ` x ) ) ) ) ) >. } ) u. ( { <. ( TopSet ` ndx ) , ( Xt_ ` ( TopOpen o. R ) ) >. , <. ( le ` ndx ) , { <. f , g >. \| ( { f , g } C_ X_ x e. I ( Base ` ( R ` x ) ) /\ A. x e. I ( f ` x ) ( le ` ( R ` x ) ) ( g ` x ) ) } >. , <. ( dist ` ndx ) , ( f e. X_ x e. I ( Base ` ( R ` x ) ) , g e. X_ x e. I ( Base ` ( R ` x ) ) \|-> sup ( ( ran ( x e. I \|-> ( ( f ` x ) ( dist ` ( R ` x ) ) ( g ` x ) ) ) u. { 0 } ) , RR* , < ) ) >. } u. { <. ( Hom ` ndx ) , ( f e. X_ x e. I ( Base ` ( R ` x ) ) , g e. X_ x e. I ( Base ` ( R ` x ) ) \|-> X_ x e. I ( ( f ` x ) ( Hom ` ( R ` x ) ) ( g ` x ) ) ) >. , <. ( comp ` ndx ) , ( a e. ( X_ x e. I ( Base ` ( R ` x ) ) X. X_ x e. I ( Base ` ( R ` x ) ) ) , c e. X_ x e. I ( Base ` ( R ` x ) ) \|-> ( d e. ( ( 2nd ` a ) ( f e. X_ x e. I ( Base ` ( R ` x ) ) , g e. X_ x e. I ( Base ` ( R ` x ) ) \|-> X_ x e. I ( ( f ` x ) ( Hom ` ( R ` x ) ) ( g ` x ) ) ) c ) , e e. ( ( f e. X_ x e. I ( Base ` ( R ` x ) ) , g e. X_ x e. I ( Base ` ( R ` x ) ) \|-> X_ x e. I ( ( f ` x ) ( Hom ` ( R ` x ) ) ( g ` x ) ) ) ` a ) \|-> ( x e. I \|-> ( ( d ` x ) ( <. ( ( 1st ` a ) ` x ) , ( ( 2nd ` a ) ` x ) >. ( comp ` ( R ` x ) ) ( c ` x ) ) ( e ` x ) ) ) ) ) >. } ) )
44	42 43	sstri	\|- { <. ( Base ` ndx ) , X_ x e. I ( Base ` ( R ` x ) ) >. } C_ ( ( { <. ( Base ` ndx ) , X_ x e. I ( Base ` ( R ` x ) ) >. , <. ( +g ` ndx ) , ( f e. X_ x e. I ( Base ` ( R ` x ) ) , g e. X_ x e. I ( Base ` ( R ` x ) ) \|-> ( x e. I \|-> ( ( f ` x ) ( +g ` ( R ` x ) ) ( g ` x ) ) ) ) >. , <. ( .r ` ndx ) , ( f e. X_ x e. I ( Base ` ( R ` x ) ) , g e. X_ x e. I ( Base ` ( R ` x ) ) \|-> ( x e. I \|-> ( ( f ` x ) ( .r ` ( R ` x ) ) ( g ` x ) ) ) ) >. } u. { <. ( Scalar ` ndx ) , S >. , <. ( .s ` ndx ) , ( f e. ( Base ` S ) , g e. X_ x e. I ( Base ` ( R ` x ) ) \|-> ( x e. I \|-> ( f ( .s ` ( R ` x ) ) ( g ` x ) ) ) ) >. , <. ( .i ` ndx ) , ( f e. X_ x e. I ( Base ` ( R ` x ) ) , g e. X_ x e. I ( Base ` ( R ` x ) ) \|-> ( S gsum ( x e. I \|-> ( ( f ` x ) ( .i ` ( R ` x ) ) ( g ` x ) ) ) ) ) >. } ) u. ( { <. ( TopSet ` ndx ) , ( Xt_ ` ( TopOpen o. R ) ) >. , <. ( le ` ndx ) , { <. f , g >. \| ( { f , g } C_ X_ x e. I ( Base ` ( R ` x ) ) /\ A. x e. I ( f ` x ) ( le ` ( R ` x ) ) ( g ` x ) ) } >. , <. ( dist ` ndx ) , ( f e. X_ x e. I ( Base ` ( R ` x ) ) , g e. X_ x e. I ( Base ` ( R ` x ) ) \|-> sup ( ( ran ( x e. I \|-> ( ( f ` x ) ( dist ` ( R ` x ) ) ( g ` x ) ) ) u. { 0 } ) , RR* , < ) ) >. } u. { <. ( Hom ` ndx ) , ( f e. X_ x e. I ( Base ` ( R ` x ) ) , g e. X_ x e. I ( Base ` ( R ` x ) ) \|-> X_ x e. I ( ( f ` x ) ( Hom ` ( R ` x ) ) ( g ` x ) ) ) >. , <. ( comp ` ndx ) , ( a e. ( X_ x e. I ( Base ` ( R ` x ) ) X. X_ x e. I ( Base ` ( R ` x ) ) ) , c e. X_ x e. I ( Base ` ( R ` x ) ) \|-> ( d e. ( ( 2nd ` a ) ( f e. X_ x e. I ( Base ` ( R ` x ) ) , g e. X_ x e. I ( Base ` ( R ` x ) ) \|-> X_ x e. I ( ( f ` x ) ( Hom ` ( R ` x ) ) ( g ` x ) ) ) c ) , e e. ( ( f e. X_ x e. I ( Base ` ( R ` x ) ) , g e. X_ x e. I ( Base ` ( R ` x ) ) \|-> X_ x e. I ( ( f ` x ) ( Hom ` ( R ` x ) ) ( g ` x ) ) ) ` a ) \|-> ( x e. I \|-> ( ( d ` x ) ( <. ( ( 1st ` a ) ` x ) , ( ( 2nd ` a ) ` x ) >. ( comp ` ( R ` x ) ) ( c ` x ) ) ( e ` x ) ) ) ) ) >. } ) )
45	17 4 18 39 44	prdsbaslem	\|- ( ph -> B = X_ x e. I ( Base ` ( R ` x ) ) )

Metamath Proof Explorer

Theorem prdsbas

Proof