# Metamath Proof Explorer

## Theorem ustbas2

Description: Second direction for ustbas . (Contributed by Thierry Arnoux, 16-Nov-2017)

Ref Expression
Assertion ustbas2 ${⊢}{U}\in \mathrm{UnifOn}\left({X}\right)\to {X}=\mathrm{dom}\bigcup {U}$

### Proof

Step Hyp Ref Expression
1 dmxpid ${⊢}\mathrm{dom}\left({X}×{X}\right)={X}$
2 ustbasel ${⊢}{U}\in \mathrm{UnifOn}\left({X}\right)\to {X}×{X}\in {U}$
3 elssuni ${⊢}{X}×{X}\in {U}\to {X}×{X}\subseteq \bigcup {U}$
4 2 3 syl ${⊢}{U}\in \mathrm{UnifOn}\left({X}\right)\to {X}×{X}\subseteq \bigcup {U}$
5 elfvex ${⊢}{U}\in \mathrm{UnifOn}\left({X}\right)\to {X}\in \mathrm{V}$
6 isust ${⊢}{X}\in \mathrm{V}\to \left({U}\in \mathrm{UnifOn}\left({X}\right)↔\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)$
7 5 6 syl ${⊢}{U}\in \mathrm{UnifOn}\left({X}\right)\to \left({U}\in \mathrm{UnifOn}\left({X}\right)↔\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)$
8 7 ibi ${⊢}{U}\in \mathrm{UnifOn}\left({X}\right)\to \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)$
9 8 simp1d ${⊢}{U}\in \mathrm{UnifOn}\left({X}\right)\to {U}\subseteq 𝒫\left({X}×{X}\right)$
10 9 unissd ${⊢}{U}\in \mathrm{UnifOn}\left({X}\right)\to \bigcup {U}\subseteq \bigcup 𝒫\left({X}×{X}\right)$
11 unipw ${⊢}\bigcup 𝒫\left({X}×{X}\right)={X}×{X}$
12 10 11 sseqtrdi ${⊢}{U}\in \mathrm{UnifOn}\left({X}\right)\to \bigcup {U}\subseteq {X}×{X}$
13 4 12 eqssd ${⊢}{U}\in \mathrm{UnifOn}\left({X}\right)\to {X}×{X}=\bigcup {U}$
14 13 dmeqd ${⊢}{U}\in \mathrm{UnifOn}\left({X}\right)\to \mathrm{dom}\left({X}×{X}\right)=\mathrm{dom}\bigcup {U}$
15 1 14 syl5eqr ${⊢}{U}\in \mathrm{UnifOn}\left({X}\right)\to {X}=\mathrm{dom}\bigcup {U}$