This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition 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 = f ∈ V ⟼ UnifSet ⁡ f ↾ 𝑡 Base f × Base f

Detailed syntax breakdown

Step Hyp Ref Expression
0 cuss class UnifSt
1 vf setvar f
2 cvv class V
3 cunif class UnifSet
4 1 cv setvar f
5 4 3 cfv class UnifSet ⁡ f
6 crest class ↾ 𝑡
7 cbs class Base
8 4 7 cfv class Base f
9 8 8 cxp class Base f × Base f
10 5 9 6 co class UnifSet ⁡ f ↾ 𝑡 Base f × Base f
11 1 2 10 cmpt class f ∈ V ⟼ UnifSet ⁡ f ↾ 𝑡 Base f × Base f
12 0 11 wceq wff UnifSt = f ∈ V ⟼ UnifSet ⁡ f ↾ 𝑡 Base f × Base f