Theorem cvmsuni

Description: An even covering of U has union equal to the preimage of U by F . (Contributed by Mario Carneiro, 11-Feb-2015)

	Ref	Expression
Hypothesis	cvmcov.1	|- S = ( k e. J |-> { s e. ( ~P C \ { (/) } ) | ( U. s = ( `' F " k ) /\ A. u e. s ( A. v e. ( s \ { u } ) ( u i^i v ) = (/) /\ ( F |` u ) e. ( ( C |`t u ) Homeo ( J |`t k ) ) ) ) } )
Assertion	cvmsuni	|- ( T e. ( S ` U ) -> U. T = ( `' F " U ) )

Proof

Step	Hyp	Ref	Expression
1		cvmcov.1	|- S = ( k e. J |-> { s e. ( ~P C \ { (/) } ) | ( U. s = ( `' F " k ) /\ A. u e. s ( A. v e. ( s \ { u } ) ( u i^i v ) = (/) /\ ( F |` u ) e. ( ( C |`t u ) Homeo ( J |`t k ) ) ) ) } )
2	1	cvmsi	|- ( T e. ( S ` U ) -> ( U e. J /\ ( T C_ C /\ T =/= (/) ) /\ ( U. T = ( `' F " U ) /\ A. u e. T ( A. v e. ( T \ { u } ) ( u i^i v ) = (/) /\ ( F |` u ) e. ( ( C |`t u ) Homeo ( J |`t U ) ) ) ) ) )
3	2	simp3d	|- ( T e. ( S ` U ) -> ( U. T = ( `' F " U ) /\ A. u e. T ( A. v e. ( T \ { u } ) ( u i^i v ) = (/) /\ ( F |` u ) e. ( ( C |`t u ) Homeo ( J |`t U ) ) ) ) )
4	3	simpld	|- ( T e. ( S ` U ) -> U. T = ( `' F " U ) )