Metamath Proof Explorer

Theorem cvmshmeo

Description: Every element of an even covering of U is homeomorphic to U via F . (Contributed by Mario Carneiro, 13-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 cvmshmeo 
|- ( ( T e. ( S ` U ) /\ A e. T ) -> ( F |` A ) e. ( ( C |`t A ) Homeo ( J |`t 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 simprd 
 |-  ( T e. ( S ` U ) -> A. u e. T ( A. v e. ( T \ { u } ) ( u i^i v ) = (/) /\ ( F |` u ) e. ( ( C |`t u ) Homeo ( J |`t U ) ) ) )
5 simpr 
 |-  ( ( A. v e. ( T \ { u } ) ( u i^i v ) = (/) /\ ( F |` u ) e. ( ( C |`t u ) Homeo ( J |`t U ) ) ) -> ( F |` u ) e. ( ( C |`t u ) Homeo ( J |`t U ) ) )
6 5 ralimi 
 |-  ( A. u e. T ( A. v e. ( T \ { u } ) ( u i^i v ) = (/) /\ ( F |` u ) e. ( ( C |`t u ) Homeo ( J |`t U ) ) ) -> A. u e. T ( F |` u ) e. ( ( C |`t u ) Homeo ( J |`t U ) ) )
7 4 6 syl 
 |-  ( T e. ( S ` U ) -> A. u e. T ( F |` u ) e. ( ( C |`t u ) Homeo ( J |`t U ) ) )
8 reseq2 
 |-  ( u = A -> ( F |` u ) = ( F |` A ) )
9 oveq2 
 |-  ( u = A -> ( C |`t u ) = ( C |`t A ) )
10 9 oveq1d 
 |-  ( u = A -> ( ( C |`t u ) Homeo ( J |`t U ) ) = ( ( C |`t A ) Homeo ( J |`t U ) ) )
11 8 10 eleq12d 
 |-  ( u = A -> ( ( F |` u ) e. ( ( C |`t u ) Homeo ( J |`t U ) ) <-> ( F |` A ) e. ( ( C |`t A ) Homeo ( J |`t U ) ) ) )
12 11 rspccva 
 |-  ( ( A. u e. T ( F |` u ) e. ( ( C |`t u ) Homeo ( J |`t U ) ) /\ A e. T ) -> ( F |` A ) e. ( ( C |`t A ) Homeo ( J |`t U ) ) )
13 7 12 sylan 
 |-  ( ( T e. ( S ` U ) /\ A e. T ) -> ( F |` A ) e. ( ( C |`t A ) Homeo ( J |`t U ) ) )