Metamath Proof Explorer

Theorem cvmsss2

Description: An open subset of an evenly covered set is evenly covered. (Contributed by Mario Carneiro, 7-Jul-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 cvmsss2 
|- ( ( F e. ( C CovMap J ) /\ V e. J /\ V C_ U ) -> ( ( S ` U ) =/= (/) -> ( S ` V ) =/= (/) ) )

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 n0 
 |-  ( ( S ` U ) =/= (/) <-> E. x x e. ( S ` U ) )
3 simpl2 
 |-  ( ( ( F e. ( C CovMap J ) /\ V e. J /\ V C_ U ) /\ x e. ( S ` U ) ) -> V e. J )
4 simpl1 
 |-  ( ( ( F e. ( C CovMap J ) /\ V e. J /\ V C_ U ) /\ x e. ( S ` U ) ) -> F e. ( C CovMap J ) )
5 cvmtop1 
 |-  ( F e. ( C CovMap J ) -> C e. Top )
6 4 5 syl 
 |-  ( ( ( F e. ( C CovMap J ) /\ V e. J /\ V C_ U ) /\ x e. ( S ` U ) ) -> C e. Top )
7 6 adantr 
 |-  ( ( ( ( F e. ( C CovMap J ) /\ V e. J /\ V C_ U ) /\ x e. ( S ` U ) ) /\ y e. x ) -> C e. Top )
8 1 cvmsss 
 |-  ( x e. ( S ` U ) -> x C_ C )
9 8 adantl 
 |-  ( ( ( F e. ( C CovMap J ) /\ V e. J /\ V C_ U ) /\ x e. ( S ` U ) ) -> x C_ C )
10 9 sselda 
 |-  ( ( ( ( F e. ( C CovMap J ) /\ V e. J /\ V C_ U ) /\ x e. ( S ` U ) ) /\ y e. x ) -> y e. C )
11 cvmcn 
 |-  ( F e. ( C CovMap J ) -> F e. ( C Cn J ) )
12 4 11 syl 
 |-  ( ( ( F e. ( C CovMap J ) /\ V e. J /\ V C_ U ) /\ x e. ( S ` U ) ) -> F e. ( C Cn J ) )
13 cnima 
 |-  ( ( F e. ( C Cn J ) /\ V e. J ) -> ( `' F " V ) e. C )
14 12 3 13 syl2anc 
 |-  ( ( ( F e. ( C CovMap J ) /\ V e. J /\ V C_ U ) /\ x e. ( S ` U ) ) -> ( `' F " V ) e. C )
15 14 adantr 
 |-  ( ( ( ( F e. ( C CovMap J ) /\ V e. J /\ V C_ U ) /\ x e. ( S ` U ) ) /\ y e. x ) -> ( `' F " V ) e. C )
16 inopn 
 |-  ( ( C e. Top /\ y e. C /\ ( `' F " V ) e. C ) -> ( y i^i ( `' F " V ) ) e. C )
17 7 10 15 16 syl3anc 
 |-  ( ( ( ( F e. ( C CovMap J ) /\ V e. J /\ V C_ U ) /\ x e. ( S ` U ) ) /\ y e. x ) -> ( y i^i ( `' F " V ) ) e. C )
18 17 fmpttd 
 |-  ( ( ( F e. ( C CovMap J ) /\ V e. J /\ V C_ U ) /\ x e. ( S ` U ) ) -> ( y e. x |-> ( y i^i ( `' F " V ) ) ) : x --> C )
19 18 frnd 
 |-  ( ( ( F e. ( C CovMap J ) /\ V e. J /\ V C_ U ) /\ x e. ( S ` U ) ) -> ran ( y e. x |-> ( y i^i ( `' F " V ) ) ) C_ C )
20 1 cvmsn0 
 |-  ( x e. ( S ` U ) -> x =/= (/) )
21 20 adantl 
 |-  ( ( ( F e. ( C CovMap J ) /\ V e. J /\ V C_ U ) /\ x e. ( S ` U ) ) -> x =/= (/) )
22 dmmptg 
 |-  ( A. y e. x ( y i^i ( `' F " V ) ) e. _V -> dom ( y e. x |-> ( y i^i ( `' F " V ) ) ) = x )
23 inex1g 
 |-  ( y e. x -> ( y i^i ( `' F " V ) ) e. _V )
24 22 23 mprg 
 |-  dom ( y e. x |-> ( y i^i ( `' F " V ) ) ) = x
25 24 eqeq1i 
 |-  ( dom ( y e. x |-> ( y i^i ( `' F " V ) ) ) = (/) <-> x = (/) )
26 dm0rn0 
 |-  ( dom ( y e. x |-> ( y i^i ( `' F " V ) ) ) = (/) <-> ran ( y e. x |-> ( y i^i ( `' F " V ) ) ) = (/) )
27 25 26 bitr3i 
 |-  ( x = (/) <-> ran ( y e. x |-> ( y i^i ( `' F " V ) ) ) = (/) )
28 27 necon3bii 
 |-  ( x =/= (/) <-> ran ( y e. x |-> ( y i^i ( `' F " V ) ) ) =/= (/) )
29 21 28 sylib 
 |-  ( ( ( F e. ( C CovMap J ) /\ V e. J /\ V C_ U ) /\ x e. ( S ` U ) ) -> ran ( y e. x |-> ( y i^i ( `' F " V ) ) ) =/= (/) )
30 19 29 jca 
 |-  ( ( ( F e. ( C CovMap J ) /\ V e. J /\ V C_ U ) /\ x e. ( S ` U ) ) -> ( ran ( y e. x |-> ( y i^i ( `' F " V ) ) ) C_ C /\ ran ( y e. x |-> ( y i^i ( `' F " V ) ) ) =/= (/) ) )
31 inss2 
 |-  ( y i^i ( `' F " V ) ) C_ ( `' F " V )
32 elpw2g 
 |-  ( ( `' F " V ) e. C -> ( ( y i^i ( `' F " V ) ) e. ~P ( `' F " V ) <-> ( y i^i ( `' F " V ) ) C_ ( `' F " V ) ) )
33 15 32 syl 
 |-  ( ( ( ( F e. ( C CovMap J ) /\ V e. J /\ V C_ U ) /\ x e. ( S ` U ) ) /\ y e. x ) -> ( ( y i^i ( `' F " V ) ) e. ~P ( `' F " V ) <-> ( y i^i ( `' F " V ) ) C_ ( `' F " V ) ) )
34 31 33 mpbiri 
 |-  ( ( ( ( F e. ( C CovMap J ) /\ V e. J /\ V C_ U ) /\ x e. ( S ` U ) ) /\ y e. x ) -> ( y i^i ( `' F " V ) ) e. ~P ( `' F " V ) )
35 34 fmpttd 
 |-  ( ( ( F e. ( C CovMap J ) /\ V e. J /\ V C_ U ) /\ x e. ( S ` U ) ) -> ( y e. x |-> ( y i^i ( `' F " V ) ) ) : x --> ~P ( `' F " V ) )
36 35 frnd 
 |-  ( ( ( F e. ( C CovMap J ) /\ V e. J /\ V C_ U ) /\ x e. ( S ` U ) ) -> ran ( y e. x |-> ( y i^i ( `' F " V ) ) ) C_ ~P ( `' F " V ) )
37 sspwuni 
 |-  ( ran ( y e. x |-> ( y i^i ( `' F " V ) ) ) C_ ~P ( `' F " V ) <-> U. ran ( y e. x |-> ( y i^i ( `' F " V ) ) ) C_ ( `' F " V ) )
38 36 37 sylib 
 |-  ( ( ( F e. ( C CovMap J ) /\ V e. J /\ V C_ U ) /\ x e. ( S ` U ) ) -> U. ran ( y e. x |-> ( y i^i ( `' F " V ) ) ) C_ ( `' F " V ) )
39 simpl3 
 |-  ( ( ( F e. ( C CovMap J ) /\ V e. J /\ V C_ U ) /\ x e. ( S ` U ) ) -> V C_ U )
40 imass2 
 |-  ( V C_ U -> ( `' F " V ) C_ ( `' F " U ) )
41 39 40 syl 
 |-  ( ( ( F e. ( C CovMap J ) /\ V e. J /\ V C_ U ) /\ x e. ( S ` U ) ) -> ( `' F " V ) C_ ( `' F " U ) )
42 1 cvmsuni 
 |-  ( x e. ( S ` U ) -> U. x = ( `' F " U ) )
43 42 adantl 
 |-  ( ( ( F e. ( C CovMap J ) /\ V e. J /\ V C_ U ) /\ x e. ( S ` U ) ) -> U. x = ( `' F " U ) )
44 41 43 sseqtrrd 
 |-  ( ( ( F e. ( C CovMap J ) /\ V e. J /\ V C_ U ) /\ x e. ( S ` U ) ) -> ( `' F " V ) C_ U. x )
45 44 sselda 
 |-  ( ( ( ( F e. ( C CovMap J ) /\ V e. J /\ V C_ U ) /\ x e. ( S ` U ) ) /\ z e. ( `' F " V ) ) -> z e. U. x )
46 eqid 
 |-  ( t i^i ( `' F " V ) ) = ( t i^i ( `' F " V ) )
47 ineq1 
 |-  ( y = t -> ( y i^i ( `' F " V ) ) = ( t i^i ( `' F " V ) ) )
48 47 rspceeqv 
 |-  ( ( t e. x /\ ( t i^i ( `' F " V ) ) = ( t i^i ( `' F " V ) ) ) -> E. y e. x ( t i^i ( `' F " V ) ) = ( y i^i ( `' F " V ) ) )
49 46 48 mpan2 
 |-  ( t e. x -> E. y e. x ( t i^i ( `' F " V ) ) = ( y i^i ( `' F " V ) ) )
50 49 ad2antrl 
 |-  ( ( ( ( ( F e. ( C CovMap J ) /\ V e. J /\ V C_ U ) /\ x e. ( S ` U ) ) /\ z e. ( `' F " V ) ) /\ ( t e. x /\ z e. t ) ) -> E. y e. x ( t i^i ( `' F " V ) ) = ( y i^i ( `' F " V ) ) )
51 vex 
 |-  t e. _V
52 51 inex1 
 |-  ( t i^i ( `' F " V ) ) e. _V
53 eqid 
 |-  ( y e. x |-> ( y i^i ( `' F " V ) ) ) = ( y e. x |-> ( y i^i ( `' F " V ) ) )
54 53 elrnmpt 
 |-  ( ( t i^i ( `' F " V ) ) e. _V -> ( ( t i^i ( `' F " V ) ) e. ran ( y e. x |-> ( y i^i ( `' F " V ) ) ) <-> E. y e. x ( t i^i ( `' F " V ) ) = ( y i^i ( `' F " V ) ) ) )
55 52 54 ax-mp 
 |-  ( ( t i^i ( `' F " V ) ) e. ran ( y e. x |-> ( y i^i ( `' F " V ) ) ) <-> E. y e. x ( t i^i ( `' F " V ) ) = ( y i^i ( `' F " V ) ) )
56 50 55 sylibr 
 |-  ( ( ( ( ( F e. ( C CovMap J ) /\ V e. J /\ V C_ U ) /\ x e. ( S ` U ) ) /\ z e. ( `' F " V ) ) /\ ( t e. x /\ z e. t ) ) -> ( t i^i ( `' F " V ) ) e. ran ( y e. x |-> ( y i^i ( `' F " V ) ) ) )
57 simprr 
 |-  ( ( ( ( ( F e. ( C CovMap J ) /\ V e. J /\ V C_ U ) /\ x e. ( S ` U ) ) /\ z e. ( `' F " V ) ) /\ ( t e. x /\ z e. t ) ) -> z e. t )
58 simplr 
 |-  ( ( ( ( ( F e. ( C CovMap J ) /\ V e. J /\ V C_ U ) /\ x e. ( S ` U ) ) /\ z e. ( `' F " V ) ) /\ ( t e. x /\ z e. t ) ) -> z e. ( `' F " V ) )
59 57 58 elind 
 |-  ( ( ( ( ( F e. ( C CovMap J ) /\ V e. J /\ V C_ U ) /\ x e. ( S ` U ) ) /\ z e. ( `' F " V ) ) /\ ( t e. x /\ z e. t ) ) -> z e. ( t i^i ( `' F " V ) ) )
60 eleq2 
 |-  ( w = ( t i^i ( `' F " V ) ) -> ( z e. w <-> z e. ( t i^i ( `' F " V ) ) ) )
61 60 rspcev 
 |-  ( ( ( t i^i ( `' F " V ) ) e. ran ( y e. x |-> ( y i^i ( `' F " V ) ) ) /\ z e. ( t i^i ( `' F " V ) ) ) -> E. w e. ran ( y e. x |-> ( y i^i ( `' F " V ) ) ) z e. w )
62 56 59 61 syl2anc 
 |-  ( ( ( ( ( F e. ( C CovMap J ) /\ V e. J /\ V C_ U ) /\ x e. ( S ` U ) ) /\ z e. ( `' F " V ) ) /\ ( t e. x /\ z e. t ) ) -> E. w e. ran ( y e. x |-> ( y i^i ( `' F " V ) ) ) z e. w )
63 62 rexlimdvaa 
 |-  ( ( ( ( F e. ( C CovMap J ) /\ V e. J /\ V C_ U ) /\ x e. ( S ` U ) ) /\ z e. ( `' F " V ) ) -> ( E. t e. x z e. t -> E. w e. ran ( y e. x |-> ( y i^i ( `' F " V ) ) ) z e. w ) )
64 eluni2 
 |-  ( z e. U. x <-> E. t e. x z e. t )
65 eluni2 
 |-  ( z e. U. ran ( y e. x |-> ( y i^i ( `' F " V ) ) ) <-> E. w e. ran ( y e. x |-> ( y i^i ( `' F " V ) ) ) z e. w )
66 63 64 65 3imtr4g 
 |-  ( ( ( ( F e. ( C CovMap J ) /\ V e. J /\ V C_ U ) /\ x e. ( S ` U ) ) /\ z e. ( `' F " V ) ) -> ( z e. U. x -> z e. U. ran ( y e. x |-> ( y i^i ( `' F " V ) ) ) ) )
67 45 66 mpd 
 |-  ( ( ( ( F e. ( C CovMap J ) /\ V e. J /\ V C_ U ) /\ x e. ( S ` U ) ) /\ z e. ( `' F " V ) ) -> z e. U. ran ( y e. x |-> ( y i^i ( `' F " V ) ) ) )
68 38 67 eqelssd 
 |-  ( ( ( F e. ( C CovMap J ) /\ V e. J /\ V C_ U ) /\ x e. ( S ` U ) ) -> U. ran ( y e. x |-> ( y i^i ( `' F " V ) ) ) = ( `' F " V ) )
69 eldifsn 
 |-  ( z e. ( ran ( y e. x |-> ( y i^i ( `' F " V ) ) ) \ { ( t i^i ( `' F " V ) ) } ) <-> ( z e. ran ( y e. x |-> ( y i^i ( `' F " V ) ) ) /\ z =/= ( t i^i ( `' F " V ) ) ) )
70 vex 
 |-  z e. _V
71 53 elrnmpt 
 |-  ( z e. _V -> ( z e. ran ( y e. x |-> ( y i^i ( `' F " V ) ) ) <-> E. y e. x z = ( y i^i ( `' F " V ) ) ) )
72 70 71 ax-mp 
 |-  ( z e. ran ( y e. x |-> ( y i^i ( `' F " V ) ) ) <-> E. y e. x z = ( y i^i ( `' F " V ) ) )
73 47 equcoms 
 |-  ( t = y -> ( y i^i ( `' F " V ) ) = ( t i^i ( `' F " V ) ) )
74 73 necon3ai 
 |-  ( ( y i^i ( `' F " V ) ) =/= ( t i^i ( `' F " V ) ) -> -. t = y )
75 simpllr 
 |-  ( ( ( ( ( F e. ( C CovMap J ) /\ V e. J /\ V C_ U ) /\ x e. ( S ` U ) ) /\ t e. x ) /\ y e. x ) -> x e. ( S ` U ) )
76 simplr 
 |-  ( ( ( ( ( F e. ( C CovMap J ) /\ V e. J /\ V C_ U ) /\ x e. ( S ` U ) ) /\ t e. x ) /\ y e. x ) -> t e. x )
77 simpr 
 |-  ( ( ( ( ( F e. ( C CovMap J ) /\ V e. J /\ V C_ U ) /\ x e. ( S ` U ) ) /\ t e. x ) /\ y e. x ) -> y e. x )
78 1 cvmsdisj 
 |-  ( ( x e. ( S ` U ) /\ t e. x /\ y e. x ) -> ( t = y \/ ( t i^i y ) = (/) ) )
79 75 76 77 78 syl3anc 
 |-  ( ( ( ( ( F e. ( C CovMap J ) /\ V e. J /\ V C_ U ) /\ x e. ( S ` U ) ) /\ t e. x ) /\ y e. x ) -> ( t = y \/ ( t i^i y ) = (/) ) )
80 79 ord 
 |-  ( ( ( ( ( F e. ( C CovMap J ) /\ V e. J /\ V C_ U ) /\ x e. ( S ` U ) ) /\ t e. x ) /\ y e. x ) -> ( -. t = y -> ( t i^i y ) = (/) ) )
81 inss1 
 |-  ( ( t i^i y ) i^i ( `' F " V ) ) C_ ( t i^i y )
82 sseq0 
 |-  ( ( ( ( t i^i y ) i^i ( `' F " V ) ) C_ ( t i^i y ) /\ ( t i^i y ) = (/) ) -> ( ( t i^i y ) i^i ( `' F " V ) ) = (/) )
83 81 82 mpan 
 |-  ( ( t i^i y ) = (/) -> ( ( t i^i y ) i^i ( `' F " V ) ) = (/) )
84 74 80 83 syl56 
 |-  ( ( ( ( ( F e. ( C CovMap J ) /\ V e. J /\ V C_ U ) /\ x e. ( S ` U ) ) /\ t e. x ) /\ y e. x ) -> ( ( y i^i ( `' F " V ) ) =/= ( t i^i ( `' F " V ) ) -> ( ( t i^i y ) i^i ( `' F " V ) ) = (/) ) )
85 neeq1 
 |-  ( z = ( y i^i ( `' F " V ) ) -> ( z =/= ( t i^i ( `' F " V ) ) <-> ( y i^i ( `' F " V ) ) =/= ( t i^i ( `' F " V ) ) ) )
86 ineq2 
 |-  ( z = ( y i^i ( `' F " V ) ) -> ( ( t i^i ( `' F " V ) ) i^i z ) = ( ( t i^i ( `' F " V ) ) i^i ( y i^i ( `' F " V ) ) ) )
87 inindir 
 |-  ( ( t i^i y ) i^i ( `' F " V ) ) = ( ( t i^i ( `' F " V ) ) i^i ( y i^i ( `' F " V ) ) )
88 86 87 eqtr4di 
 |-  ( z = ( y i^i ( `' F " V ) ) -> ( ( t i^i ( `' F " V ) ) i^i z ) = ( ( t i^i y ) i^i ( `' F " V ) ) )
89 88 eqeq1d 
 |-  ( z = ( y i^i ( `' F " V ) ) -> ( ( ( t i^i ( `' F " V ) ) i^i z ) = (/) <-> ( ( t i^i y ) i^i ( `' F " V ) ) = (/) ) )
90 85 89 imbi12d 
 |-  ( z = ( y i^i ( `' F " V ) ) -> ( ( z =/= ( t i^i ( `' F " V ) ) -> ( ( t i^i ( `' F " V ) ) i^i z ) = (/) ) <-> ( ( y i^i ( `' F " V ) ) =/= ( t i^i ( `' F " V ) ) -> ( ( t i^i y ) i^i ( `' F " V ) ) = (/) ) ) )
91 84 90 syl5ibrcom 
 |-  ( ( ( ( ( F e. ( C CovMap J ) /\ V e. J /\ V C_ U ) /\ x e. ( S ` U ) ) /\ t e. x ) /\ y e. x ) -> ( z = ( y i^i ( `' F " V ) ) -> ( z =/= ( t i^i ( `' F " V ) ) -> ( ( t i^i ( `' F " V ) ) i^i z ) = (/) ) ) )
92 91 rexlimdva 
 |-  ( ( ( ( F e. ( C CovMap J ) /\ V e. J /\ V C_ U ) /\ x e. ( S ` U ) ) /\ t e. x ) -> ( E. y e. x z = ( y i^i ( `' F " V ) ) -> ( z =/= ( t i^i ( `' F " V ) ) -> ( ( t i^i ( `' F " V ) ) i^i z ) = (/) ) ) )
93 72 92 syl5bi 
 |-  ( ( ( ( F e. ( C CovMap J ) /\ V e. J /\ V C_ U ) /\ x e. ( S ` U ) ) /\ t e. x ) -> ( z e. ran ( y e. x |-> ( y i^i ( `' F " V ) ) ) -> ( z =/= ( t i^i ( `' F " V ) ) -> ( ( t i^i ( `' F " V ) ) i^i z ) = (/) ) ) )
94 93 impd 
 |-  ( ( ( ( F e. ( C CovMap J ) /\ V e. J /\ V C_ U ) /\ x e. ( S ` U ) ) /\ t e. x ) -> ( ( z e. ran ( y e. x |-> ( y i^i ( `' F " V ) ) ) /\ z =/= ( t i^i ( `' F " V ) ) ) -> ( ( t i^i ( `' F " V ) ) i^i z ) = (/) ) )
95 69 94 syl5bi 
 |-  ( ( ( ( F e. ( C CovMap J ) /\ V e. J /\ V C_ U ) /\ x e. ( S ` U ) ) /\ t e. x ) -> ( z e. ( ran ( y e. x |-> ( y i^i ( `' F " V ) ) ) \ { ( t i^i ( `' F " V ) ) } ) -> ( ( t i^i ( `' F " V ) ) i^i z ) = (/) ) )
96 95 ralrimiv 
 |-  ( ( ( ( F e. ( C CovMap J ) /\ V e. J /\ V C_ U ) /\ x e. ( S ` U ) ) /\ t e. x ) -> A. z e. ( ran ( y e. x |-> ( y i^i ( `' F " V ) ) ) \ { ( t i^i ( `' F " V ) ) } ) ( ( t i^i ( `' F " V ) ) i^i z ) = (/) )
97 inss1 
 |-  ( t i^i ( `' F " V ) ) C_ t
98 resabs1 
 |-  ( ( t i^i ( `' F " V ) ) C_ t -> ( ( F |` t ) |` ( t i^i ( `' F " V ) ) ) = ( F |` ( t i^i ( `' F " V ) ) ) )
99 97 98 ax-mp 
 |-  ( ( F |` t ) |` ( t i^i ( `' F " V ) ) ) = ( F |` ( t i^i ( `' F " V ) ) )
100 1 cvmshmeo 
 |-  ( ( x e. ( S ` U ) /\ t e. x ) -> ( F |` t ) e. ( ( C |`t t ) Homeo ( J |`t U ) ) )
101 100 adantll 
 |-  ( ( ( ( F e. ( C CovMap J ) /\ V e. J /\ V C_ U ) /\ x e. ( S ` U ) ) /\ t e. x ) -> ( F |` t ) e. ( ( C |`t t ) Homeo ( J |`t U ) ) )
102 6 adantr 
 |-  ( ( ( ( F e. ( C CovMap J ) /\ V e. J /\ V C_ U ) /\ x e. ( S ` U ) ) /\ t e. x ) -> C e. Top )
103 9 sselda 
 |-  ( ( ( ( F e. ( C CovMap J ) /\ V e. J /\ V C_ U ) /\ x e. ( S ` U ) ) /\ t e. x ) -> t e. C )
104 elssuni 
 |-  ( t e. C -> t C_ U. C )
105 103 104 syl 
 |-  ( ( ( ( F e. ( C CovMap J ) /\ V e. J /\ V C_ U ) /\ x e. ( S ` U ) ) /\ t e. x ) -> t C_ U. C )
106 eqid 
 |-  U. C = U. C
107 106 restuni 
 |-  ( ( C e. Top /\ t C_ U. C ) -> t = U. ( C |`t t ) )
108 102 105 107 syl2anc 
 |-  ( ( ( ( F e. ( C CovMap J ) /\ V e. J /\ V C_ U ) /\ x e. ( S ` U ) ) /\ t e. x ) -> t = U. ( C |`t t ) )
109 97 108 sseqtrid 
 |-  ( ( ( ( F e. ( C CovMap J ) /\ V e. J /\ V C_ U ) /\ x e. ( S ` U ) ) /\ t e. x ) -> ( t i^i ( `' F " V ) ) C_ U. ( C |`t t ) )
110 eqid 
 |-  U. ( C |`t t ) = U. ( C |`t t )
111 110 hmeores 
 |-  ( ( ( F |` t ) e. ( ( C |`t t ) Homeo ( J |`t U ) ) /\ ( t i^i ( `' F " V ) ) C_ U. ( C |`t t ) ) -> ( ( F |` t ) |` ( t i^i ( `' F " V ) ) ) e. ( ( ( C |`t t ) |`t ( t i^i ( `' F " V ) ) ) Homeo ( ( J |`t U ) |`t ( ( F |` t ) " ( t i^i ( `' F " V ) ) ) ) ) )
112 101 109 111 syl2anc 
 |-  ( ( ( ( F e. ( C CovMap J ) /\ V e. J /\ V C_ U ) /\ x e. ( S ` U ) ) /\ t e. x ) -> ( ( F |` t ) |` ( t i^i ( `' F " V ) ) ) e. ( ( ( C |`t t ) |`t ( t i^i ( `' F " V ) ) ) Homeo ( ( J |`t U ) |`t ( ( F |` t ) " ( t i^i ( `' F " V ) ) ) ) ) )
113 99 112 eqeltrrid 
 |-  ( ( ( ( F e. ( C CovMap J ) /\ V e. J /\ V C_ U ) /\ x e. ( S ` U ) ) /\ t e. x ) -> ( F |` ( t i^i ( `' F " V ) ) ) e. ( ( ( C |`t t ) |`t ( t i^i ( `' F " V ) ) ) Homeo ( ( J |`t U ) |`t ( ( F |` t ) " ( t i^i ( `' F " V ) ) ) ) ) )
114 97 a1i 
 |-  ( ( ( ( F e. ( C CovMap J ) /\ V e. J /\ V C_ U ) /\ x e. ( S ` U ) ) /\ t e. x ) -> ( t i^i ( `' F " V ) ) C_ t )
115 simpr 
 |-  ( ( ( ( F e. ( C CovMap J ) /\ V e. J /\ V C_ U ) /\ x e. ( S ` U ) ) /\ t e. x ) -> t e. x )
116 restabs 
 |-  ( ( C e. Top /\ ( t i^i ( `' F " V ) ) C_ t /\ t e. x ) -> ( ( C |`t t ) |`t ( t i^i ( `' F " V ) ) ) = ( C |`t ( t i^i ( `' F " V ) ) ) )
117 102 114 115 116 syl3anc 
 |-  ( ( ( ( F e. ( C CovMap J ) /\ V e. J /\ V C_ U ) /\ x e. ( S ` U ) ) /\ t e. x ) -> ( ( C |`t t ) |`t ( t i^i ( `' F " V ) ) ) = ( C |`t ( t i^i ( `' F " V ) ) ) )
118 incom 
 |-  ( t i^i ( `' F " V ) ) = ( ( `' F " V ) i^i t )
119 cnvresima 
 |-  ( `' ( F |` t ) " V ) = ( ( `' F " V ) i^i t )
120 118 119 eqtr4i 
 |-  ( t i^i ( `' F " V ) ) = ( `' ( F |` t ) " V )
121 120 imaeq2i 
 |-  ( ( F |` t ) " ( t i^i ( `' F " V ) ) ) = ( ( F |` t ) " ( `' ( F |` t ) " V ) )
122 4 adantr 
 |-  ( ( ( ( F e. ( C CovMap J ) /\ V e. J /\ V C_ U ) /\ x e. ( S ` U ) ) /\ t e. x ) -> F e. ( C CovMap J ) )
123 simplr 
 |-  ( ( ( ( F e. ( C CovMap J ) /\ V e. J /\ V C_ U ) /\ x e. ( S ` U ) ) /\ t e. x ) -> x e. ( S ` U ) )
124 1 cvmsf1o 
 |-  ( ( F e. ( C CovMap J ) /\ x e. ( S ` U ) /\ t e. x ) -> ( F |` t ) : t -1-1-onto-> U )
125 122 123 115 124 syl3anc 
 |-  ( ( ( ( F e. ( C CovMap J ) /\ V e. J /\ V C_ U ) /\ x e. ( S ` U ) ) /\ t e. x ) -> ( F |` t ) : t -1-1-onto-> U )
126 f1ofo 
 |-  ( ( F |` t ) : t -1-1-onto-> U -> ( F |` t ) : t -onto-> U )
127 125 126 syl 
 |-  ( ( ( ( F e. ( C CovMap J ) /\ V e. J /\ V C_ U ) /\ x e. ( S ` U ) ) /\ t e. x ) -> ( F |` t ) : t -onto-> U )
128 39 adantr 
 |-  ( ( ( ( F e. ( C CovMap J ) /\ V e. J /\ V C_ U ) /\ x e. ( S ` U ) ) /\ t e. x ) -> V C_ U )
129 foimacnv 
 |-  ( ( ( F |` t ) : t -onto-> U /\ V C_ U ) -> ( ( F |` t ) " ( `' ( F |` t ) " V ) ) = V )
130 127 128 129 syl2anc 
 |-  ( ( ( ( F e. ( C CovMap J ) /\ V e. J /\ V C_ U ) /\ x e. ( S ` U ) ) /\ t e. x ) -> ( ( F |` t ) " ( `' ( F |` t ) " V ) ) = V )
131 121 130 syl5eq 
 |-  ( ( ( ( F e. ( C CovMap J ) /\ V e. J /\ V C_ U ) /\ x e. ( S ` U ) ) /\ t e. x ) -> ( ( F |` t ) " ( t i^i ( `' F " V ) ) ) = V )
132 131 oveq2d 
 |-  ( ( ( ( F e. ( C CovMap J ) /\ V e. J /\ V C_ U ) /\ x e. ( S ` U ) ) /\ t e. x ) -> ( ( J |`t U ) |`t ( ( F |` t ) " ( t i^i ( `' F " V ) ) ) ) = ( ( J |`t U ) |`t V ) )
133 cvmtop2 
 |-  ( F e. ( C CovMap J ) -> J e. Top )
134 4 133 syl 
 |-  ( ( ( F e. ( C CovMap J ) /\ V e. J /\ V C_ U ) /\ x e. ( S ` U ) ) -> J e. Top )
135 1 cvmsrcl 
 |-  ( x e. ( S ` U ) -> U e. J )
136 135 adantl 
 |-  ( ( ( F e. ( C CovMap J ) /\ V e. J /\ V C_ U ) /\ x e. ( S ` U ) ) -> U e. J )
137 restabs 
 |-  ( ( J e. Top /\ V C_ U /\ U e. J ) -> ( ( J |`t U ) |`t V ) = ( J |`t V ) )
138 134 39 136 137 syl3anc 
 |-  ( ( ( F e. ( C CovMap J ) /\ V e. J /\ V C_ U ) /\ x e. ( S ` U ) ) -> ( ( J |`t U ) |`t V ) = ( J |`t V ) )
139 138 adantr 
 |-  ( ( ( ( F e. ( C CovMap J ) /\ V e. J /\ V C_ U ) /\ x e. ( S ` U ) ) /\ t e. x ) -> ( ( J |`t U ) |`t V ) = ( J |`t V ) )
140 132 139 eqtrd 
 |-  ( ( ( ( F e. ( C CovMap J ) /\ V e. J /\ V C_ U ) /\ x e. ( S ` U ) ) /\ t e. x ) -> ( ( J |`t U ) |`t ( ( F |` t ) " ( t i^i ( `' F " V ) ) ) ) = ( J |`t V ) )
141 117 140 oveq12d 
 |-  ( ( ( ( F e. ( C CovMap J ) /\ V e. J /\ V C_ U ) /\ x e. ( S ` U ) ) /\ t e. x ) -> ( ( ( C |`t t ) |`t ( t i^i ( `' F " V ) ) ) Homeo ( ( J |`t U ) |`t ( ( F |` t ) " ( t i^i ( `' F " V ) ) ) ) ) = ( ( C |`t ( t i^i ( `' F " V ) ) ) Homeo ( J |`t V ) ) )
142 113 141 eleqtrd 
 |-  ( ( ( ( F e. ( C CovMap J ) /\ V e. J /\ V C_ U ) /\ x e. ( S ` U ) ) /\ t e. x ) -> ( F |` ( t i^i ( `' F " V ) ) ) e. ( ( C |`t ( t i^i ( `' F " V ) ) ) Homeo ( J |`t V ) ) )
143 96 142 jca 
 |-  ( ( ( ( F e. ( C CovMap J ) /\ V e. J /\ V C_ U ) /\ x e. ( S ` U ) ) /\ t e. x ) -> ( A. z e. ( ran ( y e. x |-> ( y i^i ( `' F " V ) ) ) \ { ( t i^i ( `' F " V ) ) } ) ( ( t i^i ( `' F " V ) ) i^i z ) = (/) /\ ( F |` ( t i^i ( `' F " V ) ) ) e. ( ( C |`t ( t i^i ( `' F " V ) ) ) Homeo ( J |`t V ) ) ) )
144 143 ralrimiva 
 |-  ( ( ( F e. ( C CovMap J ) /\ V e. J /\ V C_ U ) /\ x e. ( S ` U ) ) -> A. t e. x ( A. z e. ( ran ( y e. x |-> ( y i^i ( `' F " V ) ) ) \ { ( t i^i ( `' F " V ) ) } ) ( ( t i^i ( `' F " V ) ) i^i z ) = (/) /\ ( F |` ( t i^i ( `' F " V ) ) ) e. ( ( C |`t ( t i^i ( `' F " V ) ) ) Homeo ( J |`t V ) ) ) )
145 52 rgenw 
 |-  A. t e. x ( t i^i ( `' F " V ) ) e. _V
146 47 cbvmptv 
 |-  ( y e. x |-> ( y i^i ( `' F " V ) ) ) = ( t e. x |-> ( t i^i ( `' F " V ) ) )
147 sneq 
 |-  ( w = ( t i^i ( `' F " V ) ) -> { w } = { ( t i^i ( `' F " V ) ) } )
148 147 difeq2d 
 |-  ( w = ( t i^i ( `' F " V ) ) -> ( ran ( y e. x |-> ( y i^i ( `' F " V ) ) ) \ { w } ) = ( ran ( y e. x |-> ( y i^i ( `' F " V ) ) ) \ { ( t i^i ( `' F " V ) ) } ) )
149 ineq1 
 |-  ( w = ( t i^i ( `' F " V ) ) -> ( w i^i z ) = ( ( t i^i ( `' F " V ) ) i^i z ) )
150 149 eqeq1d 
 |-  ( w = ( t i^i ( `' F " V ) ) -> ( ( w i^i z ) = (/) <-> ( ( t i^i ( `' F " V ) ) i^i z ) = (/) ) )
151 148 150 raleqbidv 
 |-  ( w = ( t i^i ( `' F " V ) ) -> ( A. z e. ( ran ( y e. x |-> ( y i^i ( `' F " V ) ) ) \ { w } ) ( w i^i z ) = (/) <-> A. z e. ( ran ( y e. x |-> ( y i^i ( `' F " V ) ) ) \ { ( t i^i ( `' F " V ) ) } ) ( ( t i^i ( `' F " V ) ) i^i z ) = (/) ) )
152 reseq2 
 |-  ( w = ( t i^i ( `' F " V ) ) -> ( F |` w ) = ( F |` ( t i^i ( `' F " V ) ) ) )
153 oveq2 
 |-  ( w = ( t i^i ( `' F " V ) ) -> ( C |`t w ) = ( C |`t ( t i^i ( `' F " V ) ) ) )
154 153 oveq1d 
 |-  ( w = ( t i^i ( `' F " V ) ) -> ( ( C |`t w ) Homeo ( J |`t V ) ) = ( ( C |`t ( t i^i ( `' F " V ) ) ) Homeo ( J |`t V ) ) )
155 152 154 eleq12d 
 |-  ( w = ( t i^i ( `' F " V ) ) -> ( ( F |` w ) e. ( ( C |`t w ) Homeo ( J |`t V ) ) <-> ( F |` ( t i^i ( `' F " V ) ) ) e. ( ( C |`t ( t i^i ( `' F " V ) ) ) Homeo ( J |`t V ) ) ) )
156 151 155 anbi12d 
 |-  ( w = ( t i^i ( `' F " V ) ) -> ( ( A. z e. ( ran ( y e. x |-> ( y i^i ( `' F " V ) ) ) \ { w } ) ( w i^i z ) = (/) /\ ( F |` w ) e. ( ( C |`t w ) Homeo ( J |`t V ) ) ) <-> ( A. z e. ( ran ( y e. x |-> ( y i^i ( `' F " V ) ) ) \ { ( t i^i ( `' F " V ) ) } ) ( ( t i^i ( `' F " V ) ) i^i z ) = (/) /\ ( F |` ( t i^i ( `' F " V ) ) ) e. ( ( C |`t ( t i^i ( `' F " V ) ) ) Homeo ( J |`t V ) ) ) ) )
157 146 156 ralrnmptw 
 |-  ( A. t e. x ( t i^i ( `' F " V ) ) e. _V -> ( A. w e. ran ( y e. x |-> ( y i^i ( `' F " V ) ) ) ( A. z e. ( ran ( y e. x |-> ( y i^i ( `' F " V ) ) ) \ { w } ) ( w i^i z ) = (/) /\ ( F |` w ) e. ( ( C |`t w ) Homeo ( J |`t V ) ) ) <-> A. t e. x ( A. z e. ( ran ( y e. x |-> ( y i^i ( `' F " V ) ) ) \ { ( t i^i ( `' F " V ) ) } ) ( ( t i^i ( `' F " V ) ) i^i z ) = (/) /\ ( F |` ( t i^i ( `' F " V ) ) ) e. ( ( C |`t ( t i^i ( `' F " V ) ) ) Homeo ( J |`t V ) ) ) ) )
158 145 157 ax-mp 
 |-  ( A. w e. ran ( y e. x |-> ( y i^i ( `' F " V ) ) ) ( A. z e. ( ran ( y e. x |-> ( y i^i ( `' F " V ) ) ) \ { w } ) ( w i^i z ) = (/) /\ ( F |` w ) e. ( ( C |`t w ) Homeo ( J |`t V ) ) ) <-> A. t e. x ( A. z e. ( ran ( y e. x |-> ( y i^i ( `' F " V ) ) ) \ { ( t i^i ( `' F " V ) ) } ) ( ( t i^i ( `' F " V ) ) i^i z ) = (/) /\ ( F |` ( t i^i ( `' F " V ) ) ) e. ( ( C |`t ( t i^i ( `' F " V ) ) ) Homeo ( J |`t V ) ) ) )
159 144 158 sylibr 
 |-  ( ( ( F e. ( C CovMap J ) /\ V e. J /\ V C_ U ) /\ x e. ( S ` U ) ) -> A. w e. ran ( y e. x |-> ( y i^i ( `' F " V ) ) ) ( A. z e. ( ran ( y e. x |-> ( y i^i ( `' F " V ) ) ) \ { w } ) ( w i^i z ) = (/) /\ ( F |` w ) e. ( ( C |`t w ) Homeo ( J |`t V ) ) ) )
160 68 159 jca 
 |-  ( ( ( F e. ( C CovMap J ) /\ V e. J /\ V C_ U ) /\ x e. ( S ` U ) ) -> ( U. ran ( y e. x |-> ( y i^i ( `' F " V ) ) ) = ( `' F " V ) /\ A. w e. ran ( y e. x |-> ( y i^i ( `' F " V ) ) ) ( A. z e. ( ran ( y e. x |-> ( y i^i ( `' F " V ) ) ) \ { w } ) ( w i^i z ) = (/) /\ ( F |` w ) e. ( ( C |`t w ) Homeo ( J |`t V ) ) ) ) )
161 1 cvmscbv 
 |-  S = ( a e. J |-> { b e. ( ~P C \ { (/) } ) | ( U. b = ( `' F " a ) /\ A. w e. b ( A. z e. ( b \ { w } ) ( w i^i z ) = (/) /\ ( F |` w ) e. ( ( C |`t w ) Homeo ( J |`t a ) ) ) ) } )
162 161 cvmsval 
 |-  ( C e. Top -> ( ran ( y e. x |-> ( y i^i ( `' F " V ) ) ) e. ( S ` V ) <-> ( V e. J /\ ( ran ( y e. x |-> ( y i^i ( `' F " V ) ) ) C_ C /\ ran ( y e. x |-> ( y i^i ( `' F " V ) ) ) =/= (/) ) /\ ( U. ran ( y e. x |-> ( y i^i ( `' F " V ) ) ) = ( `' F " V ) /\ A. w e. ran ( y e. x |-> ( y i^i ( `' F " V ) ) ) ( A. z e. ( ran ( y e. x |-> ( y i^i ( `' F " V ) ) ) \ { w } ) ( w i^i z ) = (/) /\ ( F |` w ) e. ( ( C |`t w ) Homeo ( J |`t V ) ) ) ) ) ) )
163 6 162 syl 
 |-  ( ( ( F e. ( C CovMap J ) /\ V e. J /\ V C_ U ) /\ x e. ( S ` U ) ) -> ( ran ( y e. x |-> ( y i^i ( `' F " V ) ) ) e. ( S ` V ) <-> ( V e. J /\ ( ran ( y e. x |-> ( y i^i ( `' F " V ) ) ) C_ C /\ ran ( y e. x |-> ( y i^i ( `' F " V ) ) ) =/= (/) ) /\ ( U. ran ( y e. x |-> ( y i^i ( `' F " V ) ) ) = ( `' F " V ) /\ A. w e. ran ( y e. x |-> ( y i^i ( `' F " V ) ) ) ( A. z e. ( ran ( y e. x |-> ( y i^i ( `' F " V ) ) ) \ { w } ) ( w i^i z ) = (/) /\ ( F |` w ) e. ( ( C |`t w ) Homeo ( J |`t V ) ) ) ) ) ) )
164 3 30 160 163 mpbir3and 
 |-  ( ( ( F e. ( C CovMap J ) /\ V e. J /\ V C_ U ) /\ x e. ( S ` U ) ) -> ran ( y e. x |-> ( y i^i ( `' F " V ) ) ) e. ( S ` V ) )
165 164 ne0d 
 |-  ( ( ( F e. ( C CovMap J ) /\ V e. J /\ V C_ U ) /\ x e. ( S ` U ) ) -> ( S ` V ) =/= (/) )
166 165 ex 
 |-  ( ( F e. ( C CovMap J ) /\ V e. J /\ V C_ U ) -> ( x e. ( S ` U ) -> ( S ` V ) =/= (/) ) )
167 166 exlimdv 
 |-  ( ( F e. ( C CovMap J ) /\ V e. J /\ V C_ U ) -> ( E. x x e. ( S ` U ) -> ( S ` V ) =/= (/) ) )
168 2 167 syl5bi 
 |-  ( ( F e. ( C CovMap J ) /\ V e. J /\ V C_ U ) -> ( ( S ` U ) =/= (/) -> ( S ` V ) =/= (/) ) )