Metamath Proof Explorer

Theorem ustfn

Description: The defined uniform structure as a function. (Contributed by Thierry Arnoux, 15-Nov-2017)

Ref Expression
Assertion ustfn ⊢UnifOnFnV

Proof

Step Hyp Ref Expression
1 velpw ⊢u∈𝒫𝒫x×x↔u⊆𝒫x×x
2 1 abbii ⊢u|u∈𝒫𝒫x×x=u|u⊆𝒫x×x
3 abid2 ⊢u|u∈𝒫𝒫x×x=𝒫𝒫x×x
4 vex ⊢x∈V
5 4 4 xpex ⊢x×x∈V
6 5 pwex ⊢𝒫x×x∈V
7 6 pwex ⊢𝒫𝒫x×x∈V
8 3 7 eqeltri ⊢u|u∈𝒫𝒫x×x∈V
9 2 8 eqeltrri ⊢u|u⊆𝒫x×x∈V
10 simp1 ⊢u⊆𝒫x×x∧x×x∈u∧∀v∈u∀w∈𝒫x×xv⊆w→w∈u∧∀w∈uv∩w∈u∧I↾x⊆v∧v-1∈u∧∃w∈uw∘w⊆v→u⊆𝒫x×x
11 10 ss2abi ⊢u|u⊆𝒫x×x∧x×x∈u∧∀v∈u∀w∈𝒫x×xv⊆w→w∈u∧∀w∈uv∩w∈u∧I↾x⊆v∧v-1∈u∧∃w∈uw∘w⊆v⊆u|u⊆𝒫x×x
12 9 11 ssexi ⊢u|u⊆𝒫x×x∧x×x∈u∧∀v∈u∀w∈𝒫x×xv⊆w→w∈u∧∀w∈uv∩w∈u∧I↾x⊆v∧v-1∈u∧∃w∈uw∘w⊆v∈V
13 df-ust ⊢UnifOn=x∈V⟼u|u⊆𝒫x×x∧x×x∈u∧∀v∈u∀w∈𝒫x×xv⊆w→w∈u∧∀w∈uv∩w∈u∧I↾x⊆v∧v-1∈u∧∃w∈uw∘w⊆v
14 12 13 fnmpti ⊢UnifOnFnV