df-uss

Description: Define the uniform structure extractor function. Similarly with df-topn this differs from df-unif when a structure has been restricted using df-ress ; in this case the UnifSet component will still have a uniform set over the larger set, and this function fixes this by restricting the uniform set as well. (Contributed by Thierry Arnoux, 1-Dec-2017)

		Ref	Expression
	Assertion	df-uss	⊢ UnifSt = ( 𝑓 ∈ V ↦ ( ( UnifSet ‘ 𝑓 ) ↾_t ( ( Base ‘ 𝑓 ) × ( Base ‘ 𝑓 ) ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cuss	⊢ UnifSt
1		vf	⊢ 𝑓
2		cvv	⊢ V
3		cunif	⊢ UnifSet
4	1	cv	⊢ 𝑓
5	4 3	cfv	⊢ ( UnifSet ‘ 𝑓 )
6		crest	⊢ ↾_t
7		cbs	⊢ Base
8	4 7	cfv	⊢ ( Base ‘ 𝑓 )
9	8 8	cxp	⊢ ( ( Base ‘ 𝑓 ) × ( Base ‘ 𝑓 ) )
10	5 9 6	co	⊢ ( ( UnifSet ‘ 𝑓 ) ↾_t ( ( Base ‘ 𝑓 ) × ( Base ‘ 𝑓 ) ) )
11	1 2 10	cmpt	⊢ ( 𝑓 ∈ V ↦ ( ( UnifSet ‘ 𝑓 ) ↾_t ( ( Base ‘ 𝑓 ) × ( Base ‘ 𝑓 ) ) ) )
12	0 11	wceq	⊢ UnifSt = ( 𝑓 ∈ V ↦ ( ( UnifSet ‘ 𝑓 ) ↾_t ( ( Base ‘ 𝑓 ) × ( Base ‘ 𝑓 ) ) ) )

Metamath Proof Explorer

Definition df-uss

Detailed syntax breakdown