Description: An even covering is a subset of the topology of the domain (i.e. a collection of open sets). (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 | cvmsss | |- ( T e. ( S ` U ) -> T C_ C ) |
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 | simp2d | |- ( T e. ( S ` U ) -> ( T C_ C /\ T =/= (/) ) ) |
4 | 3 | simpld | |- ( T e. ( S ` U ) -> T C_ C ) |