# Metamath Proof Explorer

## Theorem ustfn

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

Ref Expression
Assertion ustfn ${⊢}\mathrm{UnifOn}Fn\mathrm{V}$

### Proof

Step Hyp Ref Expression
1 velpw ${⊢}{u}\in 𝒫𝒫\left({x}×{x}\right)↔{u}\subseteq 𝒫\left({x}×{x}\right)$
2 1 abbii ${⊢}\left\{{u}|{u}\in 𝒫𝒫\left({x}×{x}\right)\right\}=\left\{{u}|{u}\subseteq 𝒫\left({x}×{x}\right)\right\}$
3 abid2 ${⊢}\left\{{u}|{u}\in 𝒫𝒫\left({x}×{x}\right)\right\}=𝒫𝒫\left({x}×{x}\right)$
4 vex ${⊢}{x}\in \mathrm{V}$
5 4 4 xpex ${⊢}{x}×{x}\in \mathrm{V}$
6 5 pwex ${⊢}𝒫\left({x}×{x}\right)\in \mathrm{V}$
7 6 pwex ${⊢}𝒫𝒫\left({x}×{x}\right)\in \mathrm{V}$
8 3 7 eqeltri ${⊢}\left\{{u}|{u}\in 𝒫𝒫\left({x}×{x}\right)\right\}\in \mathrm{V}$
9 2 8 eqeltrri ${⊢}\left\{{u}|{u}\subseteq 𝒫\left({x}×{x}\right)\right\}\in \mathrm{V}$
10 simp1 ${⊢}\left({u}\subseteq 𝒫\left({x}×{x}\right)\wedge {x}×{x}\in {u}\wedge \forall {v}\in {u}\phantom{\rule{.4em}{0ex}}\left(\forall {w}\in 𝒫\left({x}×{x}\right)\phantom{\rule{.4em}{0ex}}\left({v}\subseteq {w}\to {w}\in {u}\right)\wedge \forall {w}\in {u}\phantom{\rule{.4em}{0ex}}{v}\cap {w}\in {u}\wedge \left({\mathrm{I}↾}_{{x}}\subseteq {v}\wedge {{v}}^{-1}\in {u}\wedge \exists {w}\in {u}\phantom{\rule{.4em}{0ex}}{w}\circ {w}\subseteq {v}\right)\right)\right)\to {u}\subseteq 𝒫\left({x}×{x}\right)$
11 10 ss2abi ${⊢}\left\{{u}|\left({u}\subseteq 𝒫\left({x}×{x}\right)\wedge {x}×{x}\in {u}\wedge \forall {v}\in {u}\phantom{\rule{.4em}{0ex}}\left(\forall {w}\in 𝒫\left({x}×{x}\right)\phantom{\rule{.4em}{0ex}}\left({v}\subseteq {w}\to {w}\in {u}\right)\wedge \forall {w}\in {u}\phantom{\rule{.4em}{0ex}}{v}\cap {w}\in {u}\wedge \left({\mathrm{I}↾}_{{x}}\subseteq {v}\wedge {{v}}^{-1}\in {u}\wedge \exists {w}\in {u}\phantom{\rule{.4em}{0ex}}{w}\circ {w}\subseteq {v}\right)\right)\right)\right\}\subseteq \left\{{u}|{u}\subseteq 𝒫\left({x}×{x}\right)\right\}$
12 9 11 ssexi ${⊢}\left\{{u}|\left({u}\subseteq 𝒫\left({x}×{x}\right)\wedge {x}×{x}\in {u}\wedge \forall {v}\in {u}\phantom{\rule{.4em}{0ex}}\left(\forall {w}\in 𝒫\left({x}×{x}\right)\phantom{\rule{.4em}{0ex}}\left({v}\subseteq {w}\to {w}\in {u}\right)\wedge \forall {w}\in {u}\phantom{\rule{.4em}{0ex}}{v}\cap {w}\in {u}\wedge \left({\mathrm{I}↾}_{{x}}\subseteq {v}\wedge {{v}}^{-1}\in {u}\wedge \exists {w}\in {u}\phantom{\rule{.4em}{0ex}}{w}\circ {w}\subseteq {v}\right)\right)\right)\right\}\in \mathrm{V}$
13 df-ust ${⊢}\mathrm{UnifOn}=\left({x}\in \mathrm{V}⟼\left\{{u}|\left({u}\subseteq 𝒫\left({x}×{x}\right)\wedge {x}×{x}\in {u}\wedge \forall {v}\in {u}\phantom{\rule{.4em}{0ex}}\left(\forall {w}\in 𝒫\left({x}×{x}\right)\phantom{\rule{.4em}{0ex}}\left({v}\subseteq {w}\to {w}\in {u}\right)\wedge \forall {w}\in {u}\phantom{\rule{.4em}{0ex}}{v}\cap {w}\in {u}\wedge \left({\mathrm{I}↾}_{{x}}\subseteq {v}\wedge {{v}}^{-1}\in {u}\wedge \exists {w}\in {u}\phantom{\rule{.4em}{0ex}}{w}\circ {w}\subseteq {v}\right)\right)\right)\right\}\right)$
14 12 13 fnmpti ${⊢}\mathrm{UnifOn}Fn\mathrm{V}$