Metamath Proof Explorer

Theorem cvmsval

Description: Elementhood in the set S of all even coverings of an open set in J . S is an even covering of U if it is a nonempty collection of disjoint open sets in C whose union is the preimage of U , such that each set u e. S is homeomorphic under F to U . (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 cvmsval 
|- ( C e. V -> ( 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 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 3anass 
 |-  ( ( 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 ) ) ) ) ) <-> ( 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 ) ) ) ) ) ) )
4 id 
 |-  ( U e. J -> U e. J )
5 pwexg 
 |-  ( C e. V -> ~P C e. _V )
6 difexg 
 |-  ( ~P C e. _V -> ( ~P C \ { (/) } ) e. _V )
7 rabexg 
 |-  ( ( ~P C \ { (/) } ) e. _V -> { 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 ) ) ) ) } e. _V )
8 5 6 7 3syl 
 |-  ( C e. V -> { 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 ) ) ) ) } e. _V )
9 imaeq2 
 |-  ( k = U -> ( `' F " k ) = ( `' F " U ) )
10 9 eqeq2d 
 |-  ( k = U -> ( U. s = ( `' F " k ) <-> U. s = ( `' F " U ) ) )
11 oveq2 
 |-  ( k = U -> ( J |`t k ) = ( J |`t U ) )
12 11 oveq2d 
 |-  ( k = U -> ( ( C |`t u ) Homeo ( J |`t k ) ) = ( ( C |`t u ) Homeo ( J |`t U ) ) )
13 12 eleq2d 
 |-  ( k = U -> ( ( F |` u ) e. ( ( C |`t u ) Homeo ( J |`t k ) ) <-> ( F |` u ) e. ( ( C |`t u ) Homeo ( J |`t U ) ) ) )
14 13 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 ) ) ) ) )
15 14 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 ) ) ) ) )
16 10 15 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 ) ) ) ) ) )
17 16 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 ) ) ) ) } )
18 17 1 fvmptg 
 |-  ( ( U e. J /\ { 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 ) ) ) ) } e. _V ) -> ( S ` U ) = { 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 ) ) ) ) } )
19 4 8 18 syl2anr 
 |-  ( ( C e. V /\ U e. J ) -> ( S ` U ) = { 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 ) ) ) ) } )
20 19 eleq2d 
 |-  ( ( C e. V /\ U e. J ) -> ( 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 ) ) ) ) } ) )
21 unieq 
 |-  ( s = T -> U. s = U. T )
22 21 eqeq1d 
 |-  ( s = T -> ( U. s = ( `' F " U ) <-> U. T = ( `' F " U ) ) )
23 difeq1 
 |-  ( s = T -> ( s \ { u } ) = ( T \ { u } ) )
24 23 raleqdv 
 |-  ( s = T -> ( A. v e. ( s \ { u } ) ( u i^i v ) = (/) <-> A. v e. ( T \ { u } ) ( u i^i v ) = (/) ) )
25 24 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 ) ) ) ) )
26 25 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 ) ) ) ) )
27 22 26 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 ) ) ) ) ) )
28 27 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 ) ) ) ) ) )
29 eldifsn 
 |-  ( T e. ( ~P C \ { (/) } ) <-> ( T e. ~P C /\ T =/= (/) ) )
30 elpw2g 
 |-  ( C e. V -> ( T e. ~P C <-> T C_ C ) )
31 30 adantr 
 |-  ( ( C e. V /\ U e. J ) -> ( T e. ~P C <-> T C_ C ) )
32 31 anbi1d 
 |-  ( ( C e. V /\ U e. J ) -> ( ( T e. ~P C /\ T =/= (/) ) <-> ( T C_ C /\ T =/= (/) ) ) )
33 29 32 syl5bb 
 |-  ( ( C e. V /\ U e. J ) -> ( T e. ( ~P C \ { (/) } ) <-> ( T C_ C /\ T =/= (/) ) ) )
34 33 anbi1d 
 |-  ( ( C e. V /\ U e. J ) -> ( ( 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 ) ) ) ) ) <-> ( ( 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 ) ) ) ) ) ) )
35 28 34 syl5bb 
 |-  ( ( C e. V /\ U e. J ) -> ( 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 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 ) ) ) ) ) ) )
36 20 35 bitrd 
 |-  ( ( C e. V /\ U e. J ) -> ( T e. ( S ` U ) <-> ( ( 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 ) ) ) ) ) ) )
37 36 biimprd 
 |-  ( ( C e. V /\ 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 ) ) ) ) ) -> T e. ( S ` U ) ) )
38 37 expimpd 
 |-  ( C e. V -> ( ( 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 ) ) ) ) ) ) -> T e. ( S ` U ) ) )
39 3 38 syl5bi 
 |-  ( C e. V -> ( ( 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 ) ) ) ) ) -> T e. ( S ` U ) ) )
40 2 39 impbid2 
 |-  ( C e. V -> ( 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 ) ) ) ) ) ) )