Step |
Hyp |
Ref |
Expression |
1 |
|
cvmliftmo.b |
⊢ 𝐵 = ∪ 𝐶 |
2 |
|
cvmliftmo.y |
⊢ 𝑌 = ∪ 𝐾 |
3 |
|
cvmliftmo.f |
⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ) |
4 |
|
cvmliftmo.k |
⊢ ( 𝜑 → 𝐾 ∈ Conn ) |
5 |
|
cvmliftmo.l |
⊢ ( 𝜑 → 𝐾 ∈ 𝑛-Locally Conn ) |
6 |
|
cvmliftmo.o |
⊢ ( 𝜑 → 𝑂 ∈ 𝑌 ) |
7 |
|
cvmliftmoi.m |
⊢ ( 𝜑 → 𝑀 ∈ ( 𝐾 Cn 𝐶 ) ) |
8 |
|
cvmliftmoi.n |
⊢ ( 𝜑 → 𝑁 ∈ ( 𝐾 Cn 𝐶 ) ) |
9 |
|
cvmliftmoi.g |
⊢ ( 𝜑 → ( 𝐹 ∘ 𝑀 ) = ( 𝐹 ∘ 𝑁 ) ) |
10 |
|
cvmliftmoi.p |
⊢ ( 𝜑 → ( 𝑀 ‘ 𝑂 ) = ( 𝑁 ‘ 𝑂 ) ) |
11 |
|
cvmliftmolem.1 |
⊢ 𝑆 = ( 𝑘 ∈ 𝐽 ↦ { 𝑠 ∈ ( 𝒫 𝐶 ∖ { ∅ } ) ∣ ( ∪ 𝑠 = ( ◡ 𝐹 “ 𝑘 ) ∧ ∀ 𝑢 ∈ 𝑠 ( ∀ 𝑣 ∈ ( 𝑠 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝐹 ↾ 𝑢 ) ∈ ( ( 𝐶 ↾t 𝑢 ) Homeo ( 𝐽 ↾t 𝑘 ) ) ) ) } ) |
12 |
|
cvmliftmolem.2 |
⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑇 ∈ ( 𝑆 ‘ 𝑈 ) ) |
13 |
|
cvmliftmolem.3 |
⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑊 ∈ 𝑇 ) |
14 |
|
cvmliftmolem.4 |
⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝐼 ⊆ ( ◡ 𝑀 “ 𝑊 ) ) |
15 |
|
cvmliftmolem.5 |
⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝐾 ↾t 𝐼 ) ∈ Conn ) |
16 |
|
cvmliftmolem.6 |
⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑋 ∈ 𝐼 ) |
17 |
|
cvmliftmolem.7 |
⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑄 ∈ 𝐼 ) |
18 |
|
cvmliftmolem.8 |
⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑅 ∈ 𝐼 ) |
19 |
|
cvmliftmolem.9 |
⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝐹 ‘ ( 𝑀 ‘ 𝑋 ) ) ∈ 𝑈 ) |
20 |
9
|
adantr |
⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝐹 ∘ 𝑀 ) = ( 𝐹 ∘ 𝑁 ) ) |
21 |
20
|
fveq1d |
⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( 𝐹 ∘ 𝑀 ) ‘ 𝑅 ) = ( ( 𝐹 ∘ 𝑁 ) ‘ 𝑅 ) ) |
22 |
14 18
|
sseldd |
⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑅 ∈ ( ◡ 𝑀 “ 𝑊 ) ) |
23 |
2 1
|
cnf |
⊢ ( 𝑀 ∈ ( 𝐾 Cn 𝐶 ) → 𝑀 : 𝑌 ⟶ 𝐵 ) |
24 |
7 23
|
syl |
⊢ ( 𝜑 → 𝑀 : 𝑌 ⟶ 𝐵 ) |
25 |
24
|
ffnd |
⊢ ( 𝜑 → 𝑀 Fn 𝑌 ) |
26 |
|
elpreima |
⊢ ( 𝑀 Fn 𝑌 → ( 𝑅 ∈ ( ◡ 𝑀 “ 𝑊 ) ↔ ( 𝑅 ∈ 𝑌 ∧ ( 𝑀 ‘ 𝑅 ) ∈ 𝑊 ) ) ) |
27 |
25 26
|
syl |
⊢ ( 𝜑 → ( 𝑅 ∈ ( ◡ 𝑀 “ 𝑊 ) ↔ ( 𝑅 ∈ 𝑌 ∧ ( 𝑀 ‘ 𝑅 ) ∈ 𝑊 ) ) ) |
28 |
27
|
simprbda |
⊢ ( ( 𝜑 ∧ 𝑅 ∈ ( ◡ 𝑀 “ 𝑊 ) ) → 𝑅 ∈ 𝑌 ) |
29 |
22 28
|
syldan |
⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑅 ∈ 𝑌 ) |
30 |
|
fvco3 |
⊢ ( ( 𝑀 : 𝑌 ⟶ 𝐵 ∧ 𝑅 ∈ 𝑌 ) → ( ( 𝐹 ∘ 𝑀 ) ‘ 𝑅 ) = ( 𝐹 ‘ ( 𝑀 ‘ 𝑅 ) ) ) |
31 |
24 30
|
sylan |
⊢ ( ( 𝜑 ∧ 𝑅 ∈ 𝑌 ) → ( ( 𝐹 ∘ 𝑀 ) ‘ 𝑅 ) = ( 𝐹 ‘ ( 𝑀 ‘ 𝑅 ) ) ) |
32 |
29 31
|
syldan |
⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( 𝐹 ∘ 𝑀 ) ‘ 𝑅 ) = ( 𝐹 ‘ ( 𝑀 ‘ 𝑅 ) ) ) |
33 |
2 1
|
cnf |
⊢ ( 𝑁 ∈ ( 𝐾 Cn 𝐶 ) → 𝑁 : 𝑌 ⟶ 𝐵 ) |
34 |
8 33
|
syl |
⊢ ( 𝜑 → 𝑁 : 𝑌 ⟶ 𝐵 ) |
35 |
|
fvco3 |
⊢ ( ( 𝑁 : 𝑌 ⟶ 𝐵 ∧ 𝑅 ∈ 𝑌 ) → ( ( 𝐹 ∘ 𝑁 ) ‘ 𝑅 ) = ( 𝐹 ‘ ( 𝑁 ‘ 𝑅 ) ) ) |
36 |
34 35
|
sylan |
⊢ ( ( 𝜑 ∧ 𝑅 ∈ 𝑌 ) → ( ( 𝐹 ∘ 𝑁 ) ‘ 𝑅 ) = ( 𝐹 ‘ ( 𝑁 ‘ 𝑅 ) ) ) |
37 |
29 36
|
syldan |
⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( 𝐹 ∘ 𝑁 ) ‘ 𝑅 ) = ( 𝐹 ‘ ( 𝑁 ‘ 𝑅 ) ) ) |
38 |
21 32 37
|
3eqtr3d |
⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝐹 ‘ ( 𝑀 ‘ 𝑅 ) ) = ( 𝐹 ‘ ( 𝑁 ‘ 𝑅 ) ) ) |
39 |
38
|
adantr |
⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ ( 𝑀 ‘ 𝑄 ) = ( 𝑁 ‘ 𝑄 ) ) → ( 𝐹 ‘ ( 𝑀 ‘ 𝑅 ) ) = ( 𝐹 ‘ ( 𝑁 ‘ 𝑅 ) ) ) |
40 |
27
|
simplbda |
⊢ ( ( 𝜑 ∧ 𝑅 ∈ ( ◡ 𝑀 “ 𝑊 ) ) → ( 𝑀 ‘ 𝑅 ) ∈ 𝑊 ) |
41 |
22 40
|
syldan |
⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝑀 ‘ 𝑅 ) ∈ 𝑊 ) |
42 |
41
|
adantr |
⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ ( 𝑀 ‘ 𝑄 ) = ( 𝑁 ‘ 𝑄 ) ) → ( 𝑀 ‘ 𝑅 ) ∈ 𝑊 ) |
43 |
|
fvres |
⊢ ( ( 𝑀 ‘ 𝑅 ) ∈ 𝑊 → ( ( 𝐹 ↾ 𝑊 ) ‘ ( 𝑀 ‘ 𝑅 ) ) = ( 𝐹 ‘ ( 𝑀 ‘ 𝑅 ) ) ) |
44 |
42 43
|
syl |
⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ ( 𝑀 ‘ 𝑄 ) = ( 𝑁 ‘ 𝑄 ) ) → ( ( 𝐹 ↾ 𝑊 ) ‘ ( 𝑀 ‘ 𝑅 ) ) = ( 𝐹 ‘ ( 𝑀 ‘ 𝑅 ) ) ) |
45 |
18
|
adantr |
⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ ( 𝑀 ‘ 𝑄 ) = ( 𝑁 ‘ 𝑄 ) ) → 𝑅 ∈ 𝐼 ) |
46 |
|
fvres |
⊢ ( 𝑅 ∈ 𝐼 → ( ( 𝑁 ↾ 𝐼 ) ‘ 𝑅 ) = ( 𝑁 ‘ 𝑅 ) ) |
47 |
45 46
|
syl |
⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ ( 𝑀 ‘ 𝑄 ) = ( 𝑁 ‘ 𝑄 ) ) → ( ( 𝑁 ↾ 𝐼 ) ‘ 𝑅 ) = ( 𝑁 ‘ 𝑅 ) ) |
48 |
|
eqid |
⊢ ∪ ( 𝐾 ↾t 𝐼 ) = ∪ ( 𝐾 ↾t 𝐼 ) |
49 |
15
|
adantr |
⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ ( 𝑀 ‘ 𝑄 ) = ( 𝑁 ‘ 𝑄 ) ) → ( 𝐾 ↾t 𝐼 ) ∈ Conn ) |
50 |
8
|
adantr |
⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑁 ∈ ( 𝐾 Cn 𝐶 ) ) |
51 |
|
cnvimass |
⊢ ( ◡ 𝑀 “ 𝑊 ) ⊆ dom 𝑀 |
52 |
51 24
|
fssdm |
⊢ ( 𝜑 → ( ◡ 𝑀 “ 𝑊 ) ⊆ 𝑌 ) |
53 |
52
|
adantr |
⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ◡ 𝑀 “ 𝑊 ) ⊆ 𝑌 ) |
54 |
14 53
|
sstrd |
⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝐼 ⊆ 𝑌 ) |
55 |
2
|
cnrest |
⊢ ( ( 𝑁 ∈ ( 𝐾 Cn 𝐶 ) ∧ 𝐼 ⊆ 𝑌 ) → ( 𝑁 ↾ 𝐼 ) ∈ ( ( 𝐾 ↾t 𝐼 ) Cn 𝐶 ) ) |
56 |
50 54 55
|
syl2anc |
⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝑁 ↾ 𝐼 ) ∈ ( ( 𝐾 ↾t 𝐼 ) Cn 𝐶 ) ) |
57 |
3
|
adantr |
⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ) |
58 |
|
cvmtop1 |
⊢ ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) → 𝐶 ∈ Top ) |
59 |
57 58
|
syl |
⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝐶 ∈ Top ) |
60 |
1
|
toptopon |
⊢ ( 𝐶 ∈ Top ↔ 𝐶 ∈ ( TopOn ‘ 𝐵 ) ) |
61 |
59 60
|
sylib |
⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝐶 ∈ ( TopOn ‘ 𝐵 ) ) |
62 |
|
df-ima |
⊢ ( 𝑁 “ 𝐼 ) = ran ( 𝑁 ↾ 𝐼 ) |
63 |
|
elssuni |
⊢ ( 𝑊 ∈ 𝑇 → 𝑊 ⊆ ∪ 𝑇 ) |
64 |
13 63
|
syl |
⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑊 ⊆ ∪ 𝑇 ) |
65 |
11
|
cvmsuni |
⊢ ( 𝑇 ∈ ( 𝑆 ‘ 𝑈 ) → ∪ 𝑇 = ( ◡ 𝐹 “ 𝑈 ) ) |
66 |
12 65
|
syl |
⊢ ( ( 𝜑 ∧ 𝜓 ) → ∪ 𝑇 = ( ◡ 𝐹 “ 𝑈 ) ) |
67 |
64 66
|
sseqtrd |
⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑊 ⊆ ( ◡ 𝐹 “ 𝑈 ) ) |
68 |
|
imass2 |
⊢ ( 𝑊 ⊆ ( ◡ 𝐹 “ 𝑈 ) → ( ◡ 𝑀 “ 𝑊 ) ⊆ ( ◡ 𝑀 “ ( ◡ 𝐹 “ 𝑈 ) ) ) |
69 |
67 68
|
syl |
⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ◡ 𝑀 “ 𝑊 ) ⊆ ( ◡ 𝑀 “ ( ◡ 𝐹 “ 𝑈 ) ) ) |
70 |
14 69
|
sstrd |
⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝐼 ⊆ ( ◡ 𝑀 “ ( ◡ 𝐹 “ 𝑈 ) ) ) |
71 |
20
|
cnveqd |
⊢ ( ( 𝜑 ∧ 𝜓 ) → ◡ ( 𝐹 ∘ 𝑀 ) = ◡ ( 𝐹 ∘ 𝑁 ) ) |
72 |
|
cnvco |
⊢ ◡ ( 𝐹 ∘ 𝑀 ) = ( ◡ 𝑀 ∘ ◡ 𝐹 ) |
73 |
|
cnvco |
⊢ ◡ ( 𝐹 ∘ 𝑁 ) = ( ◡ 𝑁 ∘ ◡ 𝐹 ) |
74 |
71 72 73
|
3eqtr3g |
⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ◡ 𝑀 ∘ ◡ 𝐹 ) = ( ◡ 𝑁 ∘ ◡ 𝐹 ) ) |
75 |
74
|
imaeq1d |
⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( ◡ 𝑀 ∘ ◡ 𝐹 ) “ 𝑈 ) = ( ( ◡ 𝑁 ∘ ◡ 𝐹 ) “ 𝑈 ) ) |
76 |
|
imaco |
⊢ ( ( ◡ 𝑀 ∘ ◡ 𝐹 ) “ 𝑈 ) = ( ◡ 𝑀 “ ( ◡ 𝐹 “ 𝑈 ) ) |
77 |
|
imaco |
⊢ ( ( ◡ 𝑁 ∘ ◡ 𝐹 ) “ 𝑈 ) = ( ◡ 𝑁 “ ( ◡ 𝐹 “ 𝑈 ) ) |
78 |
75 76 77
|
3eqtr3g |
⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ◡ 𝑀 “ ( ◡ 𝐹 “ 𝑈 ) ) = ( ◡ 𝑁 “ ( ◡ 𝐹 “ 𝑈 ) ) ) |
79 |
70 78
|
sseqtrd |
⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝐼 ⊆ ( ◡ 𝑁 “ ( ◡ 𝐹 “ 𝑈 ) ) ) |
80 |
34
|
adantr |
⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑁 : 𝑌 ⟶ 𝐵 ) |
81 |
80
|
ffund |
⊢ ( ( 𝜑 ∧ 𝜓 ) → Fun 𝑁 ) |
82 |
80
|
fdmd |
⊢ ( ( 𝜑 ∧ 𝜓 ) → dom 𝑁 = 𝑌 ) |
83 |
54 82
|
sseqtrrd |
⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝐼 ⊆ dom 𝑁 ) |
84 |
|
funimass3 |
⊢ ( ( Fun 𝑁 ∧ 𝐼 ⊆ dom 𝑁 ) → ( ( 𝑁 “ 𝐼 ) ⊆ ( ◡ 𝐹 “ 𝑈 ) ↔ 𝐼 ⊆ ( ◡ 𝑁 “ ( ◡ 𝐹 “ 𝑈 ) ) ) ) |
85 |
81 83 84
|
syl2anc |
⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( 𝑁 “ 𝐼 ) ⊆ ( ◡ 𝐹 “ 𝑈 ) ↔ 𝐼 ⊆ ( ◡ 𝑁 “ ( ◡ 𝐹 “ 𝑈 ) ) ) ) |
86 |
79 85
|
mpbird |
⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝑁 “ 𝐼 ) ⊆ ( ◡ 𝐹 “ 𝑈 ) ) |
87 |
62 86
|
eqsstrrid |
⊢ ( ( 𝜑 ∧ 𝜓 ) → ran ( 𝑁 ↾ 𝐼 ) ⊆ ( ◡ 𝐹 “ 𝑈 ) ) |
88 |
|
cnvimass |
⊢ ( ◡ 𝐹 “ 𝑈 ) ⊆ dom 𝐹 |
89 |
|
cvmcn |
⊢ ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) → 𝐹 ∈ ( 𝐶 Cn 𝐽 ) ) |
90 |
3 89
|
syl |
⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Cn 𝐽 ) ) |
91 |
|
eqid |
⊢ ∪ 𝐽 = ∪ 𝐽 |
92 |
1 91
|
cnf |
⊢ ( 𝐹 ∈ ( 𝐶 Cn 𝐽 ) → 𝐹 : 𝐵 ⟶ ∪ 𝐽 ) |
93 |
90 92
|
syl |
⊢ ( 𝜑 → 𝐹 : 𝐵 ⟶ ∪ 𝐽 ) |
94 |
93
|
fdmd |
⊢ ( 𝜑 → dom 𝐹 = 𝐵 ) |
95 |
94
|
adantr |
⊢ ( ( 𝜑 ∧ 𝜓 ) → dom 𝐹 = 𝐵 ) |
96 |
88 95
|
sseqtrid |
⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ◡ 𝐹 “ 𝑈 ) ⊆ 𝐵 ) |
97 |
|
cnrest2 |
⊢ ( ( 𝐶 ∈ ( TopOn ‘ 𝐵 ) ∧ ran ( 𝑁 ↾ 𝐼 ) ⊆ ( ◡ 𝐹 “ 𝑈 ) ∧ ( ◡ 𝐹 “ 𝑈 ) ⊆ 𝐵 ) → ( ( 𝑁 ↾ 𝐼 ) ∈ ( ( 𝐾 ↾t 𝐼 ) Cn 𝐶 ) ↔ ( 𝑁 ↾ 𝐼 ) ∈ ( ( 𝐾 ↾t 𝐼 ) Cn ( 𝐶 ↾t ( ◡ 𝐹 “ 𝑈 ) ) ) ) ) |
98 |
61 87 96 97
|
syl3anc |
⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( 𝑁 ↾ 𝐼 ) ∈ ( ( 𝐾 ↾t 𝐼 ) Cn 𝐶 ) ↔ ( 𝑁 ↾ 𝐼 ) ∈ ( ( 𝐾 ↾t 𝐼 ) Cn ( 𝐶 ↾t ( ◡ 𝐹 “ 𝑈 ) ) ) ) ) |
99 |
56 98
|
mpbid |
⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝑁 ↾ 𝐼 ) ∈ ( ( 𝐾 ↾t 𝐼 ) Cn ( 𝐶 ↾t ( ◡ 𝐹 “ 𝑈 ) ) ) ) |
100 |
99
|
adantr |
⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ ( 𝑀 ‘ 𝑄 ) = ( 𝑁 ‘ 𝑄 ) ) → ( 𝑁 ↾ 𝐼 ) ∈ ( ( 𝐾 ↾t 𝐼 ) Cn ( 𝐶 ↾t ( ◡ 𝐹 “ 𝑈 ) ) ) ) |
101 |
|
df-ss |
⊢ ( 𝑊 ⊆ ( ◡ 𝐹 “ 𝑈 ) ↔ ( 𝑊 ∩ ( ◡ 𝐹 “ 𝑈 ) ) = 𝑊 ) |
102 |
67 101
|
sylib |
⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝑊 ∩ ( ◡ 𝐹 “ 𝑈 ) ) = 𝑊 ) |
103 |
1
|
topopn |
⊢ ( 𝐶 ∈ Top → 𝐵 ∈ 𝐶 ) |
104 |
59 103
|
syl |
⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝐵 ∈ 𝐶 ) |
105 |
104 96
|
ssexd |
⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ◡ 𝐹 “ 𝑈 ) ∈ V ) |
106 |
11
|
cvmsss |
⊢ ( 𝑇 ∈ ( 𝑆 ‘ 𝑈 ) → 𝑇 ⊆ 𝐶 ) |
107 |
12 106
|
syl |
⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑇 ⊆ 𝐶 ) |
108 |
107 13
|
sseldd |
⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑊 ∈ 𝐶 ) |
109 |
|
elrestr |
⊢ ( ( 𝐶 ∈ Top ∧ ( ◡ 𝐹 “ 𝑈 ) ∈ V ∧ 𝑊 ∈ 𝐶 ) → ( 𝑊 ∩ ( ◡ 𝐹 “ 𝑈 ) ) ∈ ( 𝐶 ↾t ( ◡ 𝐹 “ 𝑈 ) ) ) |
110 |
59 105 108 109
|
syl3anc |
⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝑊 ∩ ( ◡ 𝐹 “ 𝑈 ) ) ∈ ( 𝐶 ↾t ( ◡ 𝐹 “ 𝑈 ) ) ) |
111 |
102 110
|
eqeltrrd |
⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑊 ∈ ( 𝐶 ↾t ( ◡ 𝐹 “ 𝑈 ) ) ) |
112 |
111
|
adantr |
⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ ( 𝑀 ‘ 𝑄 ) = ( 𝑁 ‘ 𝑄 ) ) → 𝑊 ∈ ( 𝐶 ↾t ( ◡ 𝐹 “ 𝑈 ) ) ) |
113 |
11
|
cvmscld |
⊢ ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑇 ∈ ( 𝑆 ‘ 𝑈 ) ∧ 𝑊 ∈ 𝑇 ) → 𝑊 ∈ ( Clsd ‘ ( 𝐶 ↾t ( ◡ 𝐹 “ 𝑈 ) ) ) ) |
114 |
57 12 13 113
|
syl3anc |
⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑊 ∈ ( Clsd ‘ ( 𝐶 ↾t ( ◡ 𝐹 “ 𝑈 ) ) ) ) |
115 |
114
|
adantr |
⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ ( 𝑀 ‘ 𝑄 ) = ( 𝑁 ‘ 𝑄 ) ) → 𝑊 ∈ ( Clsd ‘ ( 𝐶 ↾t ( ◡ 𝐹 “ 𝑈 ) ) ) ) |
116 |
|
conntop |
⊢ ( 𝐾 ∈ Conn → 𝐾 ∈ Top ) |
117 |
4 116
|
syl |
⊢ ( 𝜑 → 𝐾 ∈ Top ) |
118 |
117
|
adantr |
⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝐾 ∈ Top ) |
119 |
2
|
restuni |
⊢ ( ( 𝐾 ∈ Top ∧ 𝐼 ⊆ 𝑌 ) → 𝐼 = ∪ ( 𝐾 ↾t 𝐼 ) ) |
120 |
118 54 119
|
syl2anc |
⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝐼 = ∪ ( 𝐾 ↾t 𝐼 ) ) |
121 |
17 120
|
eleqtrd |
⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑄 ∈ ∪ ( 𝐾 ↾t 𝐼 ) ) |
122 |
121
|
adantr |
⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ ( 𝑀 ‘ 𝑄 ) = ( 𝑁 ‘ 𝑄 ) ) → 𝑄 ∈ ∪ ( 𝐾 ↾t 𝐼 ) ) |
123 |
17
|
adantr |
⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ ( 𝑀 ‘ 𝑄 ) = ( 𝑁 ‘ 𝑄 ) ) → 𝑄 ∈ 𝐼 ) |
124 |
|
fvres |
⊢ ( 𝑄 ∈ 𝐼 → ( ( 𝑁 ↾ 𝐼 ) ‘ 𝑄 ) = ( 𝑁 ‘ 𝑄 ) ) |
125 |
123 124
|
syl |
⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ ( 𝑀 ‘ 𝑄 ) = ( 𝑁 ‘ 𝑄 ) ) → ( ( 𝑁 ↾ 𝐼 ) ‘ 𝑄 ) = ( 𝑁 ‘ 𝑄 ) ) |
126 |
|
simpr |
⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ ( 𝑀 ‘ 𝑄 ) = ( 𝑁 ‘ 𝑄 ) ) → ( 𝑀 ‘ 𝑄 ) = ( 𝑁 ‘ 𝑄 ) ) |
127 |
14 17
|
sseldd |
⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑄 ∈ ( ◡ 𝑀 “ 𝑊 ) ) |
128 |
|
elpreima |
⊢ ( 𝑀 Fn 𝑌 → ( 𝑄 ∈ ( ◡ 𝑀 “ 𝑊 ) ↔ ( 𝑄 ∈ 𝑌 ∧ ( 𝑀 ‘ 𝑄 ) ∈ 𝑊 ) ) ) |
129 |
25 128
|
syl |
⊢ ( 𝜑 → ( 𝑄 ∈ ( ◡ 𝑀 “ 𝑊 ) ↔ ( 𝑄 ∈ 𝑌 ∧ ( 𝑀 ‘ 𝑄 ) ∈ 𝑊 ) ) ) |
130 |
129
|
simplbda |
⊢ ( ( 𝜑 ∧ 𝑄 ∈ ( ◡ 𝑀 “ 𝑊 ) ) → ( 𝑀 ‘ 𝑄 ) ∈ 𝑊 ) |
131 |
127 130
|
syldan |
⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝑀 ‘ 𝑄 ) ∈ 𝑊 ) |
132 |
131
|
adantr |
⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ ( 𝑀 ‘ 𝑄 ) = ( 𝑁 ‘ 𝑄 ) ) → ( 𝑀 ‘ 𝑄 ) ∈ 𝑊 ) |
133 |
126 132
|
eqeltrrd |
⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ ( 𝑀 ‘ 𝑄 ) = ( 𝑁 ‘ 𝑄 ) ) → ( 𝑁 ‘ 𝑄 ) ∈ 𝑊 ) |
134 |
125 133
|
eqeltrd |
⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ ( 𝑀 ‘ 𝑄 ) = ( 𝑁 ‘ 𝑄 ) ) → ( ( 𝑁 ↾ 𝐼 ) ‘ 𝑄 ) ∈ 𝑊 ) |
135 |
48 49 100 112 115 122 134
|
conncn |
⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ ( 𝑀 ‘ 𝑄 ) = ( 𝑁 ‘ 𝑄 ) ) → ( 𝑁 ↾ 𝐼 ) : ∪ ( 𝐾 ↾t 𝐼 ) ⟶ 𝑊 ) |
136 |
120
|
adantr |
⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ ( 𝑀 ‘ 𝑄 ) = ( 𝑁 ‘ 𝑄 ) ) → 𝐼 = ∪ ( 𝐾 ↾t 𝐼 ) ) |
137 |
136
|
feq2d |
⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ ( 𝑀 ‘ 𝑄 ) = ( 𝑁 ‘ 𝑄 ) ) → ( ( 𝑁 ↾ 𝐼 ) : 𝐼 ⟶ 𝑊 ↔ ( 𝑁 ↾ 𝐼 ) : ∪ ( 𝐾 ↾t 𝐼 ) ⟶ 𝑊 ) ) |
138 |
135 137
|
mpbird |
⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ ( 𝑀 ‘ 𝑄 ) = ( 𝑁 ‘ 𝑄 ) ) → ( 𝑁 ↾ 𝐼 ) : 𝐼 ⟶ 𝑊 ) |
139 |
138 45
|
ffvelrnd |
⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ ( 𝑀 ‘ 𝑄 ) = ( 𝑁 ‘ 𝑄 ) ) → ( ( 𝑁 ↾ 𝐼 ) ‘ 𝑅 ) ∈ 𝑊 ) |
140 |
47 139
|
eqeltrrd |
⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ ( 𝑀 ‘ 𝑄 ) = ( 𝑁 ‘ 𝑄 ) ) → ( 𝑁 ‘ 𝑅 ) ∈ 𝑊 ) |
141 |
|
fvres |
⊢ ( ( 𝑁 ‘ 𝑅 ) ∈ 𝑊 → ( ( 𝐹 ↾ 𝑊 ) ‘ ( 𝑁 ‘ 𝑅 ) ) = ( 𝐹 ‘ ( 𝑁 ‘ 𝑅 ) ) ) |
142 |
140 141
|
syl |
⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ ( 𝑀 ‘ 𝑄 ) = ( 𝑁 ‘ 𝑄 ) ) → ( ( 𝐹 ↾ 𝑊 ) ‘ ( 𝑁 ‘ 𝑅 ) ) = ( 𝐹 ‘ ( 𝑁 ‘ 𝑅 ) ) ) |
143 |
39 44 142
|
3eqtr4d |
⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ ( 𝑀 ‘ 𝑄 ) = ( 𝑁 ‘ 𝑄 ) ) → ( ( 𝐹 ↾ 𝑊 ) ‘ ( 𝑀 ‘ 𝑅 ) ) = ( ( 𝐹 ↾ 𝑊 ) ‘ ( 𝑁 ‘ 𝑅 ) ) ) |
144 |
11
|
cvmsf1o |
⊢ ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑇 ∈ ( 𝑆 ‘ 𝑈 ) ∧ 𝑊 ∈ 𝑇 ) → ( 𝐹 ↾ 𝑊 ) : 𝑊 –1-1-onto→ 𝑈 ) |
145 |
57 12 13 144
|
syl3anc |
⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝐹 ↾ 𝑊 ) : 𝑊 –1-1-onto→ 𝑈 ) |
146 |
|
f1of1 |
⊢ ( ( 𝐹 ↾ 𝑊 ) : 𝑊 –1-1-onto→ 𝑈 → ( 𝐹 ↾ 𝑊 ) : 𝑊 –1-1→ 𝑈 ) |
147 |
145 146
|
syl |
⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝐹 ↾ 𝑊 ) : 𝑊 –1-1→ 𝑈 ) |
148 |
147
|
adantr |
⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ ( 𝑀 ‘ 𝑄 ) = ( 𝑁 ‘ 𝑄 ) ) → ( 𝐹 ↾ 𝑊 ) : 𝑊 –1-1→ 𝑈 ) |
149 |
|
f1fveq |
⊢ ( ( ( 𝐹 ↾ 𝑊 ) : 𝑊 –1-1→ 𝑈 ∧ ( ( 𝑀 ‘ 𝑅 ) ∈ 𝑊 ∧ ( 𝑁 ‘ 𝑅 ) ∈ 𝑊 ) ) → ( ( ( 𝐹 ↾ 𝑊 ) ‘ ( 𝑀 ‘ 𝑅 ) ) = ( ( 𝐹 ↾ 𝑊 ) ‘ ( 𝑁 ‘ 𝑅 ) ) ↔ ( 𝑀 ‘ 𝑅 ) = ( 𝑁 ‘ 𝑅 ) ) ) |
150 |
148 42 140 149
|
syl12anc |
⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ ( 𝑀 ‘ 𝑄 ) = ( 𝑁 ‘ 𝑄 ) ) → ( ( ( 𝐹 ↾ 𝑊 ) ‘ ( 𝑀 ‘ 𝑅 ) ) = ( ( 𝐹 ↾ 𝑊 ) ‘ ( 𝑁 ‘ 𝑅 ) ) ↔ ( 𝑀 ‘ 𝑅 ) = ( 𝑁 ‘ 𝑅 ) ) ) |
151 |
143 150
|
mpbid |
⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ ( 𝑀 ‘ 𝑄 ) = ( 𝑁 ‘ 𝑄 ) ) → ( 𝑀 ‘ 𝑅 ) = ( 𝑁 ‘ 𝑅 ) ) |
152 |
151
|
ex |
⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( 𝑀 ‘ 𝑄 ) = ( 𝑁 ‘ 𝑄 ) → ( 𝑀 ‘ 𝑅 ) = ( 𝑁 ‘ 𝑅 ) ) ) |
153 |
129
|
simprbda |
⊢ ( ( 𝜑 ∧ 𝑄 ∈ ( ◡ 𝑀 “ 𝑊 ) ) → 𝑄 ∈ 𝑌 ) |
154 |
127 153
|
syldan |
⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑄 ∈ 𝑌 ) |
155 |
|
fveq2 |
⊢ ( 𝑥 = 𝑄 → ( 𝑀 ‘ 𝑥 ) = ( 𝑀 ‘ 𝑄 ) ) |
156 |
|
fveq2 |
⊢ ( 𝑥 = 𝑄 → ( 𝑁 ‘ 𝑥 ) = ( 𝑁 ‘ 𝑄 ) ) |
157 |
155 156
|
eqeq12d |
⊢ ( 𝑥 = 𝑄 → ( ( 𝑀 ‘ 𝑥 ) = ( 𝑁 ‘ 𝑥 ) ↔ ( 𝑀 ‘ 𝑄 ) = ( 𝑁 ‘ 𝑄 ) ) ) |
158 |
157
|
elrab3 |
⊢ ( 𝑄 ∈ 𝑌 → ( 𝑄 ∈ { 𝑥 ∈ 𝑌 ∣ ( 𝑀 ‘ 𝑥 ) = ( 𝑁 ‘ 𝑥 ) } ↔ ( 𝑀 ‘ 𝑄 ) = ( 𝑁 ‘ 𝑄 ) ) ) |
159 |
154 158
|
syl |
⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝑄 ∈ { 𝑥 ∈ 𝑌 ∣ ( 𝑀 ‘ 𝑥 ) = ( 𝑁 ‘ 𝑥 ) } ↔ ( 𝑀 ‘ 𝑄 ) = ( 𝑁 ‘ 𝑄 ) ) ) |
160 |
|
fveq2 |
⊢ ( 𝑥 = 𝑅 → ( 𝑀 ‘ 𝑥 ) = ( 𝑀 ‘ 𝑅 ) ) |
161 |
|
fveq2 |
⊢ ( 𝑥 = 𝑅 → ( 𝑁 ‘ 𝑥 ) = ( 𝑁 ‘ 𝑅 ) ) |
162 |
160 161
|
eqeq12d |
⊢ ( 𝑥 = 𝑅 → ( ( 𝑀 ‘ 𝑥 ) = ( 𝑁 ‘ 𝑥 ) ↔ ( 𝑀 ‘ 𝑅 ) = ( 𝑁 ‘ 𝑅 ) ) ) |
163 |
162
|
elrab3 |
⊢ ( 𝑅 ∈ 𝑌 → ( 𝑅 ∈ { 𝑥 ∈ 𝑌 ∣ ( 𝑀 ‘ 𝑥 ) = ( 𝑁 ‘ 𝑥 ) } ↔ ( 𝑀 ‘ 𝑅 ) = ( 𝑁 ‘ 𝑅 ) ) ) |
164 |
29 163
|
syl |
⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝑅 ∈ { 𝑥 ∈ 𝑌 ∣ ( 𝑀 ‘ 𝑥 ) = ( 𝑁 ‘ 𝑥 ) } ↔ ( 𝑀 ‘ 𝑅 ) = ( 𝑁 ‘ 𝑅 ) ) ) |
165 |
152 159 164
|
3imtr4d |
⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝑄 ∈ { 𝑥 ∈ 𝑌 ∣ ( 𝑀 ‘ 𝑥 ) = ( 𝑁 ‘ 𝑥 ) } → 𝑅 ∈ { 𝑥 ∈ 𝑌 ∣ ( 𝑀 ‘ 𝑥 ) = ( 𝑁 ‘ 𝑥 ) } ) ) |
166 |
34
|
ffnd |
⊢ ( 𝜑 → 𝑁 Fn 𝑌 ) |
167 |
|
fndmin |
⊢ ( ( 𝑀 Fn 𝑌 ∧ 𝑁 Fn 𝑌 ) → dom ( 𝑀 ∩ 𝑁 ) = { 𝑥 ∈ 𝑌 ∣ ( 𝑀 ‘ 𝑥 ) = ( 𝑁 ‘ 𝑥 ) } ) |
168 |
25 166 167
|
syl2anc |
⊢ ( 𝜑 → dom ( 𝑀 ∩ 𝑁 ) = { 𝑥 ∈ 𝑌 ∣ ( 𝑀 ‘ 𝑥 ) = ( 𝑁 ‘ 𝑥 ) } ) |
169 |
168
|
adantr |
⊢ ( ( 𝜑 ∧ 𝜓 ) → dom ( 𝑀 ∩ 𝑁 ) = { 𝑥 ∈ 𝑌 ∣ ( 𝑀 ‘ 𝑥 ) = ( 𝑁 ‘ 𝑥 ) } ) |
170 |
169
|
eleq2d |
⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝑄 ∈ dom ( 𝑀 ∩ 𝑁 ) ↔ 𝑄 ∈ { 𝑥 ∈ 𝑌 ∣ ( 𝑀 ‘ 𝑥 ) = ( 𝑁 ‘ 𝑥 ) } ) ) |
171 |
169
|
eleq2d |
⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝑅 ∈ dom ( 𝑀 ∩ 𝑁 ) ↔ 𝑅 ∈ { 𝑥 ∈ 𝑌 ∣ ( 𝑀 ‘ 𝑥 ) = ( 𝑁 ‘ 𝑥 ) } ) ) |
172 |
165 170 171
|
3imtr4d |
⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝑄 ∈ dom ( 𝑀 ∩ 𝑁 ) → 𝑅 ∈ dom ( 𝑀 ∩ 𝑁 ) ) ) |