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 |
|
cvmseu.1 |
|- B = U. C |
3 |
|
simpr2 |
|- ( ( F e. ( C CovMap J ) /\ ( T e. ( S ` U ) /\ A e. B /\ ( F ` A ) e. U ) ) -> A e. B ) |
4 |
|
simpr3 |
|- ( ( F e. ( C CovMap J ) /\ ( T e. ( S ` U ) /\ A e. B /\ ( F ` A ) e. U ) ) -> ( F ` A ) e. U ) |
5 |
|
cvmcn |
|- ( F e. ( C CovMap J ) -> F e. ( C Cn J ) ) |
6 |
5
|
adantr |
|- ( ( F e. ( C CovMap J ) /\ ( T e. ( S ` U ) /\ A e. B /\ ( F ` A ) e. U ) ) -> F e. ( C Cn J ) ) |
7 |
|
eqid |
|- U. J = U. J |
8 |
2 7
|
cnf |
|- ( F e. ( C Cn J ) -> F : B --> U. J ) |
9 |
|
ffn |
|- ( F : B --> U. J -> F Fn B ) |
10 |
|
elpreima |
|- ( F Fn B -> ( A e. ( `' F " U ) <-> ( A e. B /\ ( F ` A ) e. U ) ) ) |
11 |
6 8 9 10
|
4syl |
|- ( ( F e. ( C CovMap J ) /\ ( T e. ( S ` U ) /\ A e. B /\ ( F ` A ) e. U ) ) -> ( A e. ( `' F " U ) <-> ( A e. B /\ ( F ` A ) e. U ) ) ) |
12 |
3 4 11
|
mpbir2and |
|- ( ( F e. ( C CovMap J ) /\ ( T e. ( S ` U ) /\ A e. B /\ ( F ` A ) e. U ) ) -> A e. ( `' F " U ) ) |
13 |
|
simpr1 |
|- ( ( F e. ( C CovMap J ) /\ ( T e. ( S ` U ) /\ A e. B /\ ( F ` A ) e. U ) ) -> T e. ( S ` U ) ) |
14 |
1
|
cvmsuni |
|- ( T e. ( S ` U ) -> U. T = ( `' F " U ) ) |
15 |
13 14
|
syl |
|- ( ( F e. ( C CovMap J ) /\ ( T e. ( S ` U ) /\ A e. B /\ ( F ` A ) e. U ) ) -> U. T = ( `' F " U ) ) |
16 |
12 15
|
eleqtrrd |
|- ( ( F e. ( C CovMap J ) /\ ( T e. ( S ` U ) /\ A e. B /\ ( F ` A ) e. U ) ) -> A e. U. T ) |
17 |
|
eluni2 |
|- ( A e. U. T <-> E. x e. T A e. x ) |
18 |
16 17
|
sylib |
|- ( ( F e. ( C CovMap J ) /\ ( T e. ( S ` U ) /\ A e. B /\ ( F ` A ) e. U ) ) -> E. x e. T A e. x ) |
19 |
|
inelcm |
|- ( ( A e. x /\ A e. z ) -> ( x i^i z ) =/= (/) ) |
20 |
1
|
cvmsdisj |
|- ( ( T e. ( S ` U ) /\ x e. T /\ z e. T ) -> ( x = z \/ ( x i^i z ) = (/) ) ) |
21 |
20
|
3expb |
|- ( ( T e. ( S ` U ) /\ ( x e. T /\ z e. T ) ) -> ( x = z \/ ( x i^i z ) = (/) ) ) |
22 |
13 21
|
sylan |
|- ( ( ( F e. ( C CovMap J ) /\ ( T e. ( S ` U ) /\ A e. B /\ ( F ` A ) e. U ) ) /\ ( x e. T /\ z e. T ) ) -> ( x = z \/ ( x i^i z ) = (/) ) ) |
23 |
22
|
ord |
|- ( ( ( F e. ( C CovMap J ) /\ ( T e. ( S ` U ) /\ A e. B /\ ( F ` A ) e. U ) ) /\ ( x e. T /\ z e. T ) ) -> ( -. x = z -> ( x i^i z ) = (/) ) ) |
24 |
23
|
necon1ad |
|- ( ( ( F e. ( C CovMap J ) /\ ( T e. ( S ` U ) /\ A e. B /\ ( F ` A ) e. U ) ) /\ ( x e. T /\ z e. T ) ) -> ( ( x i^i z ) =/= (/) -> x = z ) ) |
25 |
19 24
|
syl5 |
|- ( ( ( F e. ( C CovMap J ) /\ ( T e. ( S ` U ) /\ A e. B /\ ( F ` A ) e. U ) ) /\ ( x e. T /\ z e. T ) ) -> ( ( A e. x /\ A e. z ) -> x = z ) ) |
26 |
25
|
ralrimivva |
|- ( ( F e. ( C CovMap J ) /\ ( T e. ( S ` U ) /\ A e. B /\ ( F ` A ) e. U ) ) -> A. x e. T A. z e. T ( ( A e. x /\ A e. z ) -> x = z ) ) |
27 |
|
eleq2w |
|- ( x = z -> ( A e. x <-> A e. z ) ) |
28 |
27
|
reu4 |
|- ( E! x e. T A e. x <-> ( E. x e. T A e. x /\ A. x e. T A. z e. T ( ( A e. x /\ A e. z ) -> x = z ) ) ) |
29 |
18 26 28
|
sylanbrc |
|- ( ( F e. ( C CovMap J ) /\ ( T e. ( S ` U ) /\ A e. B /\ ( F ` A ) e. U ) ) -> E! x e. T A e. x ) |