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 ) )