Metamath Proof Explorer

Theorem cvmsi

Description: One direction of cvmsval . (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 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 ) ) ) ) ) )

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 cvmsrcl 
 |-  ( T e. ( S ` U ) -> U e. J )
3 imaeq2 
 |-  ( k = U -> ( `' F " k ) = ( `' F " U ) )
4 3 eqeq2d 
 |-  ( k = U -> ( U. s = ( `' F " k ) <-> U. s = ( `' F " U ) ) )
5 oveq2 
 |-  ( k = U -> ( J |`t k ) = ( J |`t U ) )
6 5 oveq2d 
 |-  ( k = U -> ( ( C |`t u ) Homeo ( J |`t k ) ) = ( ( C |`t u ) Homeo ( J |`t U ) ) )
7 6 eleq2d 
 |-  ( k = U -> ( ( F |` u ) e. ( ( C |`t u ) Homeo ( J |`t k ) ) <-> ( F |` u ) e. ( ( C |`t u ) Homeo ( J |`t U ) ) ) )
8 7 anbi2d 
 |-  ( k = U -> ( ( A. v e. ( s \ { u } ) ( u i^i v ) = (/) /\ ( F |` u ) e. ( ( C |`t u ) Homeo ( J |`t k ) ) ) <-> ( A. v e. ( s \ { u } ) ( u i^i v ) = (/) /\ ( F |` u ) e. ( ( C |`t u ) Homeo ( J |`t U ) ) ) ) )
9 8 ralbidv 
 |-  ( k = U -> ( A. u e. s ( A. v e. ( s \ { u } ) ( u i^i v ) = (/) /\ ( F |` u ) e. ( ( C |`t u ) Homeo ( J |`t k ) ) ) <-> A. u e. s ( A. v e. ( s \ { u } ) ( u i^i v ) = (/) /\ ( F |` u ) e. ( ( C |`t u ) Homeo ( J |`t U ) ) ) ) )
10 4 9 anbi12d 
 |-  ( k = U -> ( ( 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 ) ) ) ) <-> ( U. s = ( `' F " U ) /\ A. u e. s ( A. v e. ( s \ { u } ) ( u i^i v ) = (/) /\ ( F |` u ) e. ( ( C |`t u ) Homeo ( J |`t U ) ) ) ) ) )
11 10 rabbidv 
 |-  ( k = U -> { 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 ) ) ) ) } = { s e. ( ~P C \ { (/) } ) | ( U. s = ( `' F " U ) /\ A. u e. s ( A. v e. ( s \ { u } ) ( u i^i v ) = (/) /\ ( F |` u ) e. ( ( C |`t u ) Homeo ( J |`t U ) ) ) ) } )
12 11 1 fvmptss2 
 |-  ( S ` U ) C_ { s e. ( ~P C \ { (/) } ) | ( U. s = ( `' F " U ) /\ A. u e. s ( A. v e. ( s \ { u } ) ( u i^i v ) = (/) /\ ( F |` u ) e. ( ( C |`t u ) Homeo ( J |`t U ) ) ) ) }
13 12 sseli 
 |-  ( T e. ( S ` U ) -> T e. { s e. ( ~P C \ { (/) } ) | ( U. s = ( `' F " U ) /\ A. u e. s ( A. v e. ( s \ { u } ) ( u i^i v ) = (/) /\ ( F |` u ) e. ( ( C |`t u ) Homeo ( J |`t U ) ) ) ) } )
14 unieq 
 |-  ( s = T -> U. s = U. T )
15 14 eqeq1d 
 |-  ( s = T -> ( U. s = ( `' F " U ) <-> U. T = ( `' F " U ) ) )
16 difeq1 
 |-  ( s = T -> ( s \ { u } ) = ( T \ { u } ) )
17 16 raleqdv 
 |-  ( s = T -> ( A. v e. ( s \ { u } ) ( u i^i v ) = (/) <-> A. v e. ( T \ { u } ) ( u i^i v ) = (/) ) )
18 17 anbi1d 
 |-  ( s = T -> ( ( A. v e. ( s \ { u } ) ( u i^i v ) = (/) /\ ( F |` u ) e. ( ( C |`t u ) Homeo ( J |`t U ) ) ) <-> ( A. v e. ( T \ { u } ) ( u i^i v ) = (/) /\ ( F |` u ) e. ( ( C |`t u ) Homeo ( J |`t U ) ) ) ) )
19 18 raleqbi1dv 
 |-  ( s = T -> ( A. u e. s ( A. v e. ( s \ { u } ) ( u i^i v ) = (/) /\ ( F |` u ) e. ( ( C |`t u ) Homeo ( J |`t U ) ) ) <-> A. u e. T ( A. v e. ( T \ { u } ) ( u i^i v ) = (/) /\ ( F |` u ) e. ( ( C |`t u ) Homeo ( J |`t U ) ) ) ) )
20 15 19 anbi12d 
 |-  ( s = T -> ( ( U. s = ( `' F " U ) /\ A. u e. s ( A. v e. ( s \ { u } ) ( u i^i v ) = (/) /\ ( F |` u ) e. ( ( C |`t u ) Homeo ( J |`t 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 ) ) ) ) ) )
21 20 elrab 
 |-  ( T e. { s e. ( ~P C \ { (/) } ) | ( U. s = ( `' F " U ) /\ A. u e. s ( A. v e. ( s \ { u } ) ( u i^i v ) = (/) /\ ( F |` u ) e. ( ( C |`t u ) Homeo ( J |`t U ) ) ) ) } <-> ( T e. ( ~P C \ { (/) } ) /\ ( 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 ) ) ) ) ) )
22 13 21 sylib 
 |-  ( T e. ( S ` U ) -> ( T e. ( ~P C \ { (/) } ) /\ ( 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 ) ) ) ) ) )
23 22 simpld 
 |-  ( T e. ( S ` U ) -> T e. ( ~P C \ { (/) } ) )
24 eldifsn 
 |-  ( T e. ( ~P C \ { (/) } ) <-> ( T e. ~P C /\ T =/= (/) ) )
25 23 24 sylib 
 |-  ( T e. ( S ` U ) -> ( T e. ~P C /\ T =/= (/) ) )
26 elpwi 
 |-  ( T e. ~P C -> T C_ C )
27 26 anim1i 
 |-  ( ( T e. ~P C /\ T =/= (/) ) -> ( T C_ C /\ T =/= (/) ) )
28 25 27 syl 
 |-  ( T e. ( S ` U ) -> ( T C_ C /\ T =/= (/) ) )
29 22 simprd 
 |-  ( 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 ) ) ) ) )
30 2 28 29 3jca 
 |-  ( 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 ) ) ) ) ) )