Metamath Proof Explorer


Theorem ustuni

Description: The set union of a uniform structure is the Cartesian product of its base. (Contributed by Thierry Arnoux, 5-Dec-2017)

Ref Expression
Assertion ustuni
|- ( U e. ( UnifOn ` X ) -> U. U = ( X X. X ) )

Proof

Step Hyp Ref Expression
1 ustbasel
 |-  ( U e. ( UnifOn ` X ) -> ( X X. X ) e. U )
2 ustssxp
 |-  ( ( U e. ( UnifOn ` X ) /\ u e. U ) -> u C_ ( X X. X ) )
3 2 ralrimiva
 |-  ( U e. ( UnifOn ` X ) -> A. u e. U u C_ ( X X. X ) )
4 pwssb
 |-  ( U C_ ~P ( X X. X ) <-> A. u e. U u C_ ( X X. X ) )
5 3 4 sylibr
 |-  ( U e. ( UnifOn ` X ) -> U C_ ~P ( X X. X ) )
6 elpwuni
 |-  ( ( X X. X ) e. U -> ( U C_ ~P ( X X. X ) <-> U. U = ( X X. X ) ) )
7 6 biimpa
 |-  ( ( ( X X. X ) e. U /\ U C_ ~P ( X X. X ) ) -> U. U = ( X X. X ) )
8 1 5 7 syl2anc
 |-  ( U e. ( UnifOn ` X ) -> U. U = ( X X. X ) )