Metamath Proof Explorer


Theorem ustbas2

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

Ref Expression
Assertion ustbas2 U UnifOn X X = dom U

Proof

Step Hyp Ref Expression
1 dmxpid dom X × X = X
2 ustbasel U UnifOn X X × X U
3 elssuni X × X U X × X U
4 2 3 syl U UnifOn X X × X U
5 elfvex U UnifOn X X V
6 isust X V U UnifOn X U 𝒫 X × X X × X U v U w 𝒫 X × X v w w U w U v w U I X v v -1 U w U w w v
7 5 6 syl U UnifOn X U UnifOn X U 𝒫 X × X X × X U v U w 𝒫 X × X v w w U w U v w U I X v v -1 U w U w w v
8 7 ibi U UnifOn X U 𝒫 X × X X × X U v U w 𝒫 X × X v w w U w U v w U I X v v -1 U w U w w v
9 8 simp1d U UnifOn X U 𝒫 X × X
10 9 unissd U UnifOn X U 𝒫 X × X
11 unipw 𝒫 X × X = X × X
12 10 11 sseqtrdi U UnifOn X U X × X
13 4 12 eqssd U UnifOn X X × X = U
14 13 dmeqd U UnifOn X dom X × X = dom U
15 1 14 eqtr3id U UnifOn X X = dom U