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 |
|
cvmtop1 |
|- ( F e. ( C CovMap J ) -> C e. Top ) |
3 |
2
|
3ad2ant1 |
|- ( ( F e. ( C CovMap J ) /\ T e. ( S ` U ) /\ A e. T ) -> C e. Top ) |
4 |
1
|
cvmsuni |
|- ( T e. ( S ` U ) -> U. T = ( `' F " U ) ) |
5 |
4
|
3ad2ant2 |
|- ( ( F e. ( C CovMap J ) /\ T e. ( S ` U ) /\ A e. T ) -> U. T = ( `' F " U ) ) |
6 |
1
|
cvmsss |
|- ( T e. ( S ` U ) -> T C_ C ) |
7 |
6
|
3ad2ant2 |
|- ( ( F e. ( C CovMap J ) /\ T e. ( S ` U ) /\ A e. T ) -> T C_ C ) |
8 |
7
|
unissd |
|- ( ( F e. ( C CovMap J ) /\ T e. ( S ` U ) /\ A e. T ) -> U. T C_ U. C ) |
9 |
5 8
|
eqsstrrd |
|- ( ( F e. ( C CovMap J ) /\ T e. ( S ` U ) /\ A e. T ) -> ( `' F " U ) C_ U. C ) |
10 |
|
eqid |
|- U. C = U. C |
11 |
10
|
restuni |
|- ( ( C e. Top /\ ( `' F " U ) C_ U. C ) -> ( `' F " U ) = U. ( C |`t ( `' F " U ) ) ) |
12 |
3 9 11
|
syl2anc |
|- ( ( F e. ( C CovMap J ) /\ T e. ( S ` U ) /\ A e. T ) -> ( `' F " U ) = U. ( C |`t ( `' F " U ) ) ) |
13 |
12
|
difeq1d |
|- ( ( F e. ( C CovMap J ) /\ T e. ( S ` U ) /\ A e. T ) -> ( ( `' F " U ) \ U. ( T \ { A } ) ) = ( U. ( C |`t ( `' F " U ) ) \ U. ( T \ { A } ) ) ) |
14 |
|
unisng |
|- ( A e. T -> U. { A } = A ) |
15 |
14
|
3ad2ant3 |
|- ( ( F e. ( C CovMap J ) /\ T e. ( S ` U ) /\ A e. T ) -> U. { A } = A ) |
16 |
15
|
uneq2d |
|- ( ( F e. ( C CovMap J ) /\ T e. ( S ` U ) /\ A e. T ) -> ( U. ( T \ { A } ) u. U. { A } ) = ( U. ( T \ { A } ) u. A ) ) |
17 |
|
uniun |
|- U. ( ( T \ { A } ) u. { A } ) = ( U. ( T \ { A } ) u. U. { A } ) |
18 |
|
undif1 |
|- ( ( T \ { A } ) u. { A } ) = ( T u. { A } ) |
19 |
|
simp3 |
|- ( ( F e. ( C CovMap J ) /\ T e. ( S ` U ) /\ A e. T ) -> A e. T ) |
20 |
19
|
snssd |
|- ( ( F e. ( C CovMap J ) /\ T e. ( S ` U ) /\ A e. T ) -> { A } C_ T ) |
21 |
|
ssequn2 |
|- ( { A } C_ T <-> ( T u. { A } ) = T ) |
22 |
20 21
|
sylib |
|- ( ( F e. ( C CovMap J ) /\ T e. ( S ` U ) /\ A e. T ) -> ( T u. { A } ) = T ) |
23 |
18 22
|
syl5eq |
|- ( ( F e. ( C CovMap J ) /\ T e. ( S ` U ) /\ A e. T ) -> ( ( T \ { A } ) u. { A } ) = T ) |
24 |
23
|
unieqd |
|- ( ( F e. ( C CovMap J ) /\ T e. ( S ` U ) /\ A e. T ) -> U. ( ( T \ { A } ) u. { A } ) = U. T ) |
25 |
24 5
|
eqtrd |
|- ( ( F e. ( C CovMap J ) /\ T e. ( S ` U ) /\ A e. T ) -> U. ( ( T \ { A } ) u. { A } ) = ( `' F " U ) ) |
26 |
17 25
|
eqtr3id |
|- ( ( F e. ( C CovMap J ) /\ T e. ( S ` U ) /\ A e. T ) -> ( U. ( T \ { A } ) u. U. { A } ) = ( `' F " U ) ) |
27 |
16 26
|
eqtr3d |
|- ( ( F e. ( C CovMap J ) /\ T e. ( S ` U ) /\ A e. T ) -> ( U. ( T \ { A } ) u. A ) = ( `' F " U ) ) |
28 |
|
difss |
|- ( T \ { A } ) C_ T |
29 |
28
|
unissi |
|- U. ( T \ { A } ) C_ U. T |
30 |
29 5
|
sseqtrid |
|- ( ( F e. ( C CovMap J ) /\ T e. ( S ` U ) /\ A e. T ) -> U. ( T \ { A } ) C_ ( `' F " U ) ) |
31 |
|
uniiun |
|- U. ( T \ { A } ) = U_ x e. ( T \ { A } ) x |
32 |
31
|
ineq2i |
|- ( A i^i U. ( T \ { A } ) ) = ( A i^i U_ x e. ( T \ { A } ) x ) |
33 |
|
incom |
|- ( U. ( T \ { A } ) i^i A ) = ( A i^i U. ( T \ { A } ) ) |
34 |
|
iunin2 |
|- U_ x e. ( T \ { A } ) ( A i^i x ) = ( A i^i U_ x e. ( T \ { A } ) x ) |
35 |
32 33 34
|
3eqtr4i |
|- ( U. ( T \ { A } ) i^i A ) = U_ x e. ( T \ { A } ) ( A i^i x ) |
36 |
|
eldifsn |
|- ( x e. ( T \ { A } ) <-> ( x e. T /\ x =/= A ) ) |
37 |
|
nesym |
|- ( x =/= A <-> -. A = x ) |
38 |
1
|
cvmsdisj |
|- ( ( T e. ( S ` U ) /\ A e. T /\ x e. T ) -> ( A = x \/ ( A i^i x ) = (/) ) ) |
39 |
38
|
3expa |
|- ( ( ( T e. ( S ` U ) /\ A e. T ) /\ x e. T ) -> ( A = x \/ ( A i^i x ) = (/) ) ) |
40 |
39
|
ord |
|- ( ( ( T e. ( S ` U ) /\ A e. T ) /\ x e. T ) -> ( -. A = x -> ( A i^i x ) = (/) ) ) |
41 |
37 40
|
syl5bi |
|- ( ( ( T e. ( S ` U ) /\ A e. T ) /\ x e. T ) -> ( x =/= A -> ( A i^i x ) = (/) ) ) |
42 |
41
|
impr |
|- ( ( ( T e. ( S ` U ) /\ A e. T ) /\ ( x e. T /\ x =/= A ) ) -> ( A i^i x ) = (/) ) |
43 |
36 42
|
sylan2b |
|- ( ( ( T e. ( S ` U ) /\ A e. T ) /\ x e. ( T \ { A } ) ) -> ( A i^i x ) = (/) ) |
44 |
43
|
iuneq2dv |
|- ( ( T e. ( S ` U ) /\ A e. T ) -> U_ x e. ( T \ { A } ) ( A i^i x ) = U_ x e. ( T \ { A } ) (/) ) |
45 |
44
|
3adant1 |
|- ( ( F e. ( C CovMap J ) /\ T e. ( S ` U ) /\ A e. T ) -> U_ x e. ( T \ { A } ) ( A i^i x ) = U_ x e. ( T \ { A } ) (/) ) |
46 |
|
iun0 |
|- U_ x e. ( T \ { A } ) (/) = (/) |
47 |
45 46
|
eqtrdi |
|- ( ( F e. ( C CovMap J ) /\ T e. ( S ` U ) /\ A e. T ) -> U_ x e. ( T \ { A } ) ( A i^i x ) = (/) ) |
48 |
35 47
|
syl5eq |
|- ( ( F e. ( C CovMap J ) /\ T e. ( S ` U ) /\ A e. T ) -> ( U. ( T \ { A } ) i^i A ) = (/) ) |
49 |
|
uneqdifeq |
|- ( ( U. ( T \ { A } ) C_ ( `' F " U ) /\ ( U. ( T \ { A } ) i^i A ) = (/) ) -> ( ( U. ( T \ { A } ) u. A ) = ( `' F " U ) <-> ( ( `' F " U ) \ U. ( T \ { A } ) ) = A ) ) |
50 |
30 48 49
|
syl2anc |
|- ( ( F e. ( C CovMap J ) /\ T e. ( S ` U ) /\ A e. T ) -> ( ( U. ( T \ { A } ) u. A ) = ( `' F " U ) <-> ( ( `' F " U ) \ U. ( T \ { A } ) ) = A ) ) |
51 |
27 50
|
mpbid |
|- ( ( F e. ( C CovMap J ) /\ T e. ( S ` U ) /\ A e. T ) -> ( ( `' F " U ) \ U. ( T \ { A } ) ) = A ) |
52 |
13 51
|
eqtr3d |
|- ( ( F e. ( C CovMap J ) /\ T e. ( S ` U ) /\ A e. T ) -> ( U. ( C |`t ( `' F " U ) ) \ U. ( T \ { A } ) ) = A ) |
53 |
|
uniexg |
|- ( T e. ( S ` U ) -> U. T e. _V ) |
54 |
53
|
3ad2ant2 |
|- ( ( F e. ( C CovMap J ) /\ T e. ( S ` U ) /\ A e. T ) -> U. T e. _V ) |
55 |
5 54
|
eqeltrrd |
|- ( ( F e. ( C CovMap J ) /\ T e. ( S ` U ) /\ A e. T ) -> ( `' F " U ) e. _V ) |
56 |
|
resttop |
|- ( ( C e. Top /\ ( `' F " U ) e. _V ) -> ( C |`t ( `' F " U ) ) e. Top ) |
57 |
3 55 56
|
syl2anc |
|- ( ( F e. ( C CovMap J ) /\ T e. ( S ` U ) /\ A e. T ) -> ( C |`t ( `' F " U ) ) e. Top ) |
58 |
|
elssuni |
|- ( x e. T -> x C_ U. T ) |
59 |
58
|
adantl |
|- ( ( ( F e. ( C CovMap J ) /\ T e. ( S ` U ) /\ A e. T ) /\ x e. T ) -> x C_ U. T ) |
60 |
5
|
adantr |
|- ( ( ( F e. ( C CovMap J ) /\ T e. ( S ` U ) /\ A e. T ) /\ x e. T ) -> U. T = ( `' F " U ) ) |
61 |
59 60
|
sseqtrd |
|- ( ( ( F e. ( C CovMap J ) /\ T e. ( S ` U ) /\ A e. T ) /\ x e. T ) -> x C_ ( `' F " U ) ) |
62 |
|
df-ss |
|- ( x C_ ( `' F " U ) <-> ( x i^i ( `' F " U ) ) = x ) |
63 |
61 62
|
sylib |
|- ( ( ( F e. ( C CovMap J ) /\ T e. ( S ` U ) /\ A e. T ) /\ x e. T ) -> ( x i^i ( `' F " U ) ) = x ) |
64 |
3
|
adantr |
|- ( ( ( F e. ( C CovMap J ) /\ T e. ( S ` U ) /\ A e. T ) /\ x e. T ) -> C e. Top ) |
65 |
55
|
adantr |
|- ( ( ( F e. ( C CovMap J ) /\ T e. ( S ` U ) /\ A e. T ) /\ x e. T ) -> ( `' F " U ) e. _V ) |
66 |
7
|
sselda |
|- ( ( ( F e. ( C CovMap J ) /\ T e. ( S ` U ) /\ A e. T ) /\ x e. T ) -> x e. C ) |
67 |
|
elrestr |
|- ( ( C e. Top /\ ( `' F " U ) e. _V /\ x e. C ) -> ( x i^i ( `' F " U ) ) e. ( C |`t ( `' F " U ) ) ) |
68 |
64 65 66 67
|
syl3anc |
|- ( ( ( F e. ( C CovMap J ) /\ T e. ( S ` U ) /\ A e. T ) /\ x e. T ) -> ( x i^i ( `' F " U ) ) e. ( C |`t ( `' F " U ) ) ) |
69 |
63 68
|
eqeltrrd |
|- ( ( ( F e. ( C CovMap J ) /\ T e. ( S ` U ) /\ A e. T ) /\ x e. T ) -> x e. ( C |`t ( `' F " U ) ) ) |
70 |
69
|
ex |
|- ( ( F e. ( C CovMap J ) /\ T e. ( S ` U ) /\ A e. T ) -> ( x e. T -> x e. ( C |`t ( `' F " U ) ) ) ) |
71 |
70
|
ssrdv |
|- ( ( F e. ( C CovMap J ) /\ T e. ( S ` U ) /\ A e. T ) -> T C_ ( C |`t ( `' F " U ) ) ) |
72 |
71
|
ssdifssd |
|- ( ( F e. ( C CovMap J ) /\ T e. ( S ` U ) /\ A e. T ) -> ( T \ { A } ) C_ ( C |`t ( `' F " U ) ) ) |
73 |
|
uniopn |
|- ( ( ( C |`t ( `' F " U ) ) e. Top /\ ( T \ { A } ) C_ ( C |`t ( `' F " U ) ) ) -> U. ( T \ { A } ) e. ( C |`t ( `' F " U ) ) ) |
74 |
57 72 73
|
syl2anc |
|- ( ( F e. ( C CovMap J ) /\ T e. ( S ` U ) /\ A e. T ) -> U. ( T \ { A } ) e. ( C |`t ( `' F " U ) ) ) |
75 |
|
eqid |
|- U. ( C |`t ( `' F " U ) ) = U. ( C |`t ( `' F " U ) ) |
76 |
75
|
opncld |
|- ( ( ( C |`t ( `' F " U ) ) e. Top /\ U. ( T \ { A } ) e. ( C |`t ( `' F " U ) ) ) -> ( U. ( C |`t ( `' F " U ) ) \ U. ( T \ { A } ) ) e. ( Clsd ` ( C |`t ( `' F " U ) ) ) ) |
77 |
57 74 76
|
syl2anc |
|- ( ( F e. ( C CovMap J ) /\ T e. ( S ` U ) /\ A e. T ) -> ( U. ( C |`t ( `' F " U ) ) \ U. ( T \ { A } ) ) e. ( Clsd ` ( C |`t ( `' F " U ) ) ) ) |
78 |
52 77
|
eqeltrrd |
|- ( ( F e. ( C CovMap J ) /\ T e. ( S ` U ) /\ A e. T ) -> A e. ( Clsd ` ( C |`t ( `' F " U ) ) ) ) |