Step | Hyp | Ref
| Expression |
1 | | cvmliftmoi.g |
. . . . . . . . . 10
⊢ (𝜑 → (𝐹 ∘ 𝑀) = (𝐹 ∘ 𝑁)) |
2 | 1 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝜓) → (𝐹 ∘ 𝑀) = (𝐹 ∘ 𝑁)) |
3 | 2 | fveq1d 6776 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝜓) → ((𝐹 ∘ 𝑀)‘𝑅) = ((𝐹 ∘ 𝑁)‘𝑅)) |
4 | | cvmliftmolem.4 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝜓) → 𝐼 ⊆ (◡𝑀 “ 𝑊)) |
5 | | cvmliftmolem.8 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝜓) → 𝑅 ∈ 𝐼) |
6 | 4, 5 | sseldd 3922 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝜓) → 𝑅 ∈ (◡𝑀 “ 𝑊)) |
7 | | cvmliftmoi.m |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑀 ∈ (𝐾 Cn 𝐶)) |
8 | | cvmliftmo.y |
. . . . . . . . . . . . . . 15
⊢ 𝑌 = ∪
𝐾 |
9 | | cvmliftmo.b |
. . . . . . . . . . . . . . 15
⊢ 𝐵 = ∪
𝐶 |
10 | 8, 9 | cnf 22397 |
. . . . . . . . . . . . . 14
⊢ (𝑀 ∈ (𝐾 Cn 𝐶) → 𝑀:𝑌⟶𝐵) |
11 | 7, 10 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑀:𝑌⟶𝐵) |
12 | 11 | ffnd 6601 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑀 Fn 𝑌) |
13 | | elpreima 6935 |
. . . . . . . . . . . 12
⊢ (𝑀 Fn 𝑌 → (𝑅 ∈ (◡𝑀 “ 𝑊) ↔ (𝑅 ∈ 𝑌 ∧ (𝑀‘𝑅) ∈ 𝑊))) |
14 | 12, 13 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑅 ∈ (◡𝑀 “ 𝑊) ↔ (𝑅 ∈ 𝑌 ∧ (𝑀‘𝑅) ∈ 𝑊))) |
15 | 14 | simprbda 499 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑅 ∈ (◡𝑀 “ 𝑊)) → 𝑅 ∈ 𝑌) |
16 | 6, 15 | syldan 591 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝜓) → 𝑅 ∈ 𝑌) |
17 | | fvco3 6867 |
. . . . . . . . . 10
⊢ ((𝑀:𝑌⟶𝐵 ∧ 𝑅 ∈ 𝑌) → ((𝐹 ∘ 𝑀)‘𝑅) = (𝐹‘(𝑀‘𝑅))) |
18 | 11, 17 | sylan 580 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑅 ∈ 𝑌) → ((𝐹 ∘ 𝑀)‘𝑅) = (𝐹‘(𝑀‘𝑅))) |
19 | 16, 18 | syldan 591 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝜓) → ((𝐹 ∘ 𝑀)‘𝑅) = (𝐹‘(𝑀‘𝑅))) |
20 | | cvmliftmoi.n |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑁 ∈ (𝐾 Cn 𝐶)) |
21 | 8, 9 | cnf 22397 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ (𝐾 Cn 𝐶) → 𝑁:𝑌⟶𝐵) |
22 | 20, 21 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑁:𝑌⟶𝐵) |
23 | | fvco3 6867 |
. . . . . . . . . 10
⊢ ((𝑁:𝑌⟶𝐵 ∧ 𝑅 ∈ 𝑌) → ((𝐹 ∘ 𝑁)‘𝑅) = (𝐹‘(𝑁‘𝑅))) |
24 | 22, 23 | sylan 580 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑅 ∈ 𝑌) → ((𝐹 ∘ 𝑁)‘𝑅) = (𝐹‘(𝑁‘𝑅))) |
25 | 16, 24 | syldan 591 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝜓) → ((𝐹 ∘ 𝑁)‘𝑅) = (𝐹‘(𝑁‘𝑅))) |
26 | 3, 19, 25 | 3eqtr3d 2786 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝜓) → (𝐹‘(𝑀‘𝑅)) = (𝐹‘(𝑁‘𝑅))) |
27 | 26 | adantr 481 |
. . . . . 6
⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → (𝐹‘(𝑀‘𝑅)) = (𝐹‘(𝑁‘𝑅))) |
28 | 14 | simplbda 500 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑅 ∈ (◡𝑀 “ 𝑊)) → (𝑀‘𝑅) ∈ 𝑊) |
29 | 6, 28 | syldan 591 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝜓) → (𝑀‘𝑅) ∈ 𝑊) |
30 | 29 | adantr 481 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → (𝑀‘𝑅) ∈ 𝑊) |
31 | | fvres 6793 |
. . . . . . 7
⊢ ((𝑀‘𝑅) ∈ 𝑊 → ((𝐹 ↾ 𝑊)‘(𝑀‘𝑅)) = (𝐹‘(𝑀‘𝑅))) |
32 | 30, 31 | syl 17 |
. . . . . 6
⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → ((𝐹 ↾ 𝑊)‘(𝑀‘𝑅)) = (𝐹‘(𝑀‘𝑅))) |
33 | 5 | adantr 481 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → 𝑅 ∈ 𝐼) |
34 | | fvres 6793 |
. . . . . . . . 9
⊢ (𝑅 ∈ 𝐼 → ((𝑁 ↾ 𝐼)‘𝑅) = (𝑁‘𝑅)) |
35 | 33, 34 | syl 17 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → ((𝑁 ↾ 𝐼)‘𝑅) = (𝑁‘𝑅)) |
36 | | eqid 2738 |
. . . . . . . . . . 11
⊢ ∪ (𝐾
↾t 𝐼) =
∪ (𝐾 ↾t 𝐼) |
37 | | cvmliftmolem.5 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝜓) → (𝐾 ↾t 𝐼) ∈ Conn) |
38 | 37 | adantr 481 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → (𝐾 ↾t 𝐼) ∈ Conn) |
39 | 20 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝜓) → 𝑁 ∈ (𝐾 Cn 𝐶)) |
40 | | cnvimass 5989 |
. . . . . . . . . . . . . . . . 17
⊢ (◡𝑀 “ 𝑊) ⊆ dom 𝑀 |
41 | 40, 11 | fssdm 6620 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (◡𝑀 “ 𝑊) ⊆ 𝑌) |
42 | 41 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝜓) → (◡𝑀 “ 𝑊) ⊆ 𝑌) |
43 | 4, 42 | sstrd 3931 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝜓) → 𝐼 ⊆ 𝑌) |
44 | 8 | cnrest 22436 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ (𝐾 Cn 𝐶) ∧ 𝐼 ⊆ 𝑌) → (𝑁 ↾ 𝐼) ∈ ((𝐾 ↾t 𝐼) Cn 𝐶)) |
45 | 39, 43, 44 | syl2anc 584 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝜓) → (𝑁 ↾ 𝐼) ∈ ((𝐾 ↾t 𝐼) Cn 𝐶)) |
46 | | cvmliftmo.f |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐹 ∈ (𝐶 CovMap 𝐽)) |
47 | 46 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝜓) → 𝐹 ∈ (𝐶 CovMap 𝐽)) |
48 | | cvmtop1 33222 |
. . . . . . . . . . . . . . . 16
⊢ (𝐹 ∈ (𝐶 CovMap 𝐽) → 𝐶 ∈ Top) |
49 | 47, 48 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝜓) → 𝐶 ∈ Top) |
50 | 9 | toptopon 22066 |
. . . . . . . . . . . . . . 15
⊢ (𝐶 ∈ Top ↔ 𝐶 ∈ (TopOn‘𝐵)) |
51 | 49, 50 | sylib 217 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝜓) → 𝐶 ∈ (TopOn‘𝐵)) |
52 | | df-ima 5602 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 “ 𝐼) = ran (𝑁 ↾ 𝐼) |
53 | | cvmliftmolem.3 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝜓) → 𝑊 ∈ 𝑇) |
54 | | elssuni 4871 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑊 ∈ 𝑇 → 𝑊 ⊆ ∪ 𝑇) |
55 | 53, 54 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝜓) → 𝑊 ⊆ ∪ 𝑇) |
56 | | cvmliftmolem.2 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝜓) → 𝑇 ∈ (𝑆‘𝑈)) |
57 | | cvmliftmolem.1 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 =
(◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾t 𝑢)Homeo(𝐽 ↾t 𝑘))))}) |
58 | 57 | cvmsuni 33231 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑇 ∈ (𝑆‘𝑈) → ∪ 𝑇 = (◡𝐹 “ 𝑈)) |
59 | 56, 58 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝜓) → ∪ 𝑇 = (◡𝐹 “ 𝑈)) |
60 | 55, 59 | sseqtrd 3961 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝜓) → 𝑊 ⊆ (◡𝐹 “ 𝑈)) |
61 | | imass2 6010 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑊 ⊆ (◡𝐹 “ 𝑈) → (◡𝑀 “ 𝑊) ⊆ (◡𝑀 “ (◡𝐹 “ 𝑈))) |
62 | 60, 61 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝜓) → (◡𝑀 “ 𝑊) ⊆ (◡𝑀 “ (◡𝐹 “ 𝑈))) |
63 | 4, 62 | sstrd 3931 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝜓) → 𝐼 ⊆ (◡𝑀 “ (◡𝐹 “ 𝑈))) |
64 | 2 | cnveqd 5784 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝜓) → ◡(𝐹 ∘ 𝑀) = ◡(𝐹 ∘ 𝑁)) |
65 | | cnvco 5794 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ◡(𝐹 ∘ 𝑀) = (◡𝑀 ∘ ◡𝐹) |
66 | | cnvco 5794 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ◡(𝐹 ∘ 𝑁) = (◡𝑁 ∘ ◡𝐹) |
67 | 64, 65, 66 | 3eqtr3g 2801 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝜓) → (◡𝑀 ∘ ◡𝐹) = (◡𝑁 ∘ ◡𝐹)) |
68 | 67 | imaeq1d 5968 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝜓) → ((◡𝑀 ∘ ◡𝐹) “ 𝑈) = ((◡𝑁 ∘ ◡𝐹) “ 𝑈)) |
69 | | imaco 6155 |
. . . . . . . . . . . . . . . . . 18
⊢ ((◡𝑀 ∘ ◡𝐹) “ 𝑈) = (◡𝑀 “ (◡𝐹 “ 𝑈)) |
70 | | imaco 6155 |
. . . . . . . . . . . . . . . . . 18
⊢ ((◡𝑁 ∘ ◡𝐹) “ 𝑈) = (◡𝑁 “ (◡𝐹 “ 𝑈)) |
71 | 68, 69, 70 | 3eqtr3g 2801 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝜓) → (◡𝑀 “ (◡𝐹 “ 𝑈)) = (◡𝑁 “ (◡𝐹 “ 𝑈))) |
72 | 63, 71 | sseqtrd 3961 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝜓) → 𝐼 ⊆ (◡𝑁 “ (◡𝐹 “ 𝑈))) |
73 | 22 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝜓) → 𝑁:𝑌⟶𝐵) |
74 | 73 | ffund 6604 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝜓) → Fun 𝑁) |
75 | 73 | fdmd 6611 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝜓) → dom 𝑁 = 𝑌) |
76 | 43, 75 | sseqtrrd 3962 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝜓) → 𝐼 ⊆ dom 𝑁) |
77 | | funimass3 6931 |
. . . . . . . . . . . . . . . . 17
⊢ ((Fun
𝑁 ∧ 𝐼 ⊆ dom 𝑁) → ((𝑁 “ 𝐼) ⊆ (◡𝐹 “ 𝑈) ↔ 𝐼 ⊆ (◡𝑁 “ (◡𝐹 “ 𝑈)))) |
78 | 74, 76, 77 | syl2anc 584 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝜓) → ((𝑁 “ 𝐼) ⊆ (◡𝐹 “ 𝑈) ↔ 𝐼 ⊆ (◡𝑁 “ (◡𝐹 “ 𝑈)))) |
79 | 72, 78 | mpbird 256 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝜓) → (𝑁 “ 𝐼) ⊆ (◡𝐹 “ 𝑈)) |
80 | 52, 79 | eqsstrrid 3970 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝜓) → ran (𝑁 ↾ 𝐼) ⊆ (◡𝐹 “ 𝑈)) |
81 | | cnvimass 5989 |
. . . . . . . . . . . . . . 15
⊢ (◡𝐹 “ 𝑈) ⊆ dom 𝐹 |
82 | | cvmcn 33224 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐹 ∈ (𝐶 CovMap 𝐽) → 𝐹 ∈ (𝐶 Cn 𝐽)) |
83 | 46, 82 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐹 ∈ (𝐶 Cn 𝐽)) |
84 | | eqid 2738 |
. . . . . . . . . . . . . . . . . . 19
⊢ ∪ 𝐽 =
∪ 𝐽 |
85 | 9, 84 | cnf 22397 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐹 ∈ (𝐶 Cn 𝐽) → 𝐹:𝐵⟶∪ 𝐽) |
86 | 83, 85 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐹:𝐵⟶∪ 𝐽) |
87 | 86 | fdmd 6611 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → dom 𝐹 = 𝐵) |
88 | 87 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝜓) → dom 𝐹 = 𝐵) |
89 | 81, 88 | sseqtrid 3973 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝜓) → (◡𝐹 “ 𝑈) ⊆ 𝐵) |
90 | | cnrest2 22437 |
. . . . . . . . . . . . . 14
⊢ ((𝐶 ∈ (TopOn‘𝐵) ∧ ran (𝑁 ↾ 𝐼) ⊆ (◡𝐹 “ 𝑈) ∧ (◡𝐹 “ 𝑈) ⊆ 𝐵) → ((𝑁 ↾ 𝐼) ∈ ((𝐾 ↾t 𝐼) Cn 𝐶) ↔ (𝑁 ↾ 𝐼) ∈ ((𝐾 ↾t 𝐼) Cn (𝐶 ↾t (◡𝐹 “ 𝑈))))) |
91 | 51, 80, 89, 90 | syl3anc 1370 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝜓) → ((𝑁 ↾ 𝐼) ∈ ((𝐾 ↾t 𝐼) Cn 𝐶) ↔ (𝑁 ↾ 𝐼) ∈ ((𝐾 ↾t 𝐼) Cn (𝐶 ↾t (◡𝐹 “ 𝑈))))) |
92 | 45, 91 | mpbid 231 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝜓) → (𝑁 ↾ 𝐼) ∈ ((𝐾 ↾t 𝐼) Cn (𝐶 ↾t (◡𝐹 “ 𝑈)))) |
93 | 92 | adantr 481 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → (𝑁 ↾ 𝐼) ∈ ((𝐾 ↾t 𝐼) Cn (𝐶 ↾t (◡𝐹 “ 𝑈)))) |
94 | | df-ss 3904 |
. . . . . . . . . . . . . 14
⊢ (𝑊 ⊆ (◡𝐹 “ 𝑈) ↔ (𝑊 ∩ (◡𝐹 “ 𝑈)) = 𝑊) |
95 | 60, 94 | sylib 217 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝜓) → (𝑊 ∩ (◡𝐹 “ 𝑈)) = 𝑊) |
96 | 9 | topopn 22055 |
. . . . . . . . . . . . . . . 16
⊢ (𝐶 ∈ Top → 𝐵 ∈ 𝐶) |
97 | 49, 96 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝜓) → 𝐵 ∈ 𝐶) |
98 | 97, 89 | ssexd 5248 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝜓) → (◡𝐹 “ 𝑈) ∈ V) |
99 | 57 | cvmsss 33229 |
. . . . . . . . . . . . . . . 16
⊢ (𝑇 ∈ (𝑆‘𝑈) → 𝑇 ⊆ 𝐶) |
100 | 56, 99 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝜓) → 𝑇 ⊆ 𝐶) |
101 | 100, 53 | sseldd 3922 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝜓) → 𝑊 ∈ 𝐶) |
102 | | elrestr 17139 |
. . . . . . . . . . . . . 14
⊢ ((𝐶 ∈ Top ∧ (◡𝐹 “ 𝑈) ∈ V ∧ 𝑊 ∈ 𝐶) → (𝑊 ∩ (◡𝐹 “ 𝑈)) ∈ (𝐶 ↾t (◡𝐹 “ 𝑈))) |
103 | 49, 98, 101, 102 | syl3anc 1370 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝜓) → (𝑊 ∩ (◡𝐹 “ 𝑈)) ∈ (𝐶 ↾t (◡𝐹 “ 𝑈))) |
104 | 95, 103 | eqeltrrd 2840 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝜓) → 𝑊 ∈ (𝐶 ↾t (◡𝐹 “ 𝑈))) |
105 | 104 | adantr 481 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → 𝑊 ∈ (𝐶 ↾t (◡𝐹 “ 𝑈))) |
106 | 57 | cvmscld 33235 |
. . . . . . . . . . . . 13
⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑇 ∈ (𝑆‘𝑈) ∧ 𝑊 ∈ 𝑇) → 𝑊 ∈ (Clsd‘(𝐶 ↾t (◡𝐹 “ 𝑈)))) |
107 | 47, 56, 53, 106 | syl3anc 1370 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝜓) → 𝑊 ∈ (Clsd‘(𝐶 ↾t (◡𝐹 “ 𝑈)))) |
108 | 107 | adantr 481 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → 𝑊 ∈ (Clsd‘(𝐶 ↾t (◡𝐹 “ 𝑈)))) |
109 | | cvmliftmolem.7 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝜓) → 𝑄 ∈ 𝐼) |
110 | | cvmliftmo.k |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐾 ∈ Conn) |
111 | | conntop 22568 |
. . . . . . . . . . . . . . . 16
⊢ (𝐾 ∈ Conn → 𝐾 ∈ Top) |
112 | 110, 111 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐾 ∈ Top) |
113 | 112 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝜓) → 𝐾 ∈ Top) |
114 | 8 | restuni 22313 |
. . . . . . . . . . . . . 14
⊢ ((𝐾 ∈ Top ∧ 𝐼 ⊆ 𝑌) → 𝐼 = ∪ (𝐾 ↾t 𝐼)) |
115 | 113, 43, 114 | syl2anc 584 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝜓) → 𝐼 = ∪ (𝐾 ↾t 𝐼)) |
116 | 109, 115 | eleqtrd 2841 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝜓) → 𝑄 ∈ ∪ (𝐾 ↾t 𝐼)) |
117 | 116 | adantr 481 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → 𝑄 ∈ ∪ (𝐾 ↾t 𝐼)) |
118 | 109 | adantr 481 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → 𝑄 ∈ 𝐼) |
119 | | fvres 6793 |
. . . . . . . . . . . . 13
⊢ (𝑄 ∈ 𝐼 → ((𝑁 ↾ 𝐼)‘𝑄) = (𝑁‘𝑄)) |
120 | 118, 119 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → ((𝑁 ↾ 𝐼)‘𝑄) = (𝑁‘𝑄)) |
121 | | simpr 485 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → (𝑀‘𝑄) = (𝑁‘𝑄)) |
122 | 4, 109 | sseldd 3922 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝜓) → 𝑄 ∈ (◡𝑀 “ 𝑊)) |
123 | | elpreima 6935 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑀 Fn 𝑌 → (𝑄 ∈ (◡𝑀 “ 𝑊) ↔ (𝑄 ∈ 𝑌 ∧ (𝑀‘𝑄) ∈ 𝑊))) |
124 | 12, 123 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑄 ∈ (◡𝑀 “ 𝑊) ↔ (𝑄 ∈ 𝑌 ∧ (𝑀‘𝑄) ∈ 𝑊))) |
125 | 124 | simplbda 500 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑄 ∈ (◡𝑀 “ 𝑊)) → (𝑀‘𝑄) ∈ 𝑊) |
126 | 122, 125 | syldan 591 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝜓) → (𝑀‘𝑄) ∈ 𝑊) |
127 | 126 | adantr 481 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → (𝑀‘𝑄) ∈ 𝑊) |
128 | 121, 127 | eqeltrrd 2840 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → (𝑁‘𝑄) ∈ 𝑊) |
129 | 120, 128 | eqeltrd 2839 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → ((𝑁 ↾ 𝐼)‘𝑄) ∈ 𝑊) |
130 | 36, 38, 93, 105, 108, 117, 129 | conncn 22577 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → (𝑁 ↾ 𝐼):∪ (𝐾 ↾t 𝐼)⟶𝑊) |
131 | 115 | adantr 481 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → 𝐼 = ∪ (𝐾 ↾t 𝐼)) |
132 | 131 | feq2d 6586 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → ((𝑁 ↾ 𝐼):𝐼⟶𝑊 ↔ (𝑁 ↾ 𝐼):∪ (𝐾 ↾t 𝐼)⟶𝑊)) |
133 | 130, 132 | mpbird 256 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → (𝑁 ↾ 𝐼):𝐼⟶𝑊) |
134 | 133, 33 | ffvelrnd 6962 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → ((𝑁 ↾ 𝐼)‘𝑅) ∈ 𝑊) |
135 | 35, 134 | eqeltrrd 2840 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → (𝑁‘𝑅) ∈ 𝑊) |
136 | | fvres 6793 |
. . . . . . 7
⊢ ((𝑁‘𝑅) ∈ 𝑊 → ((𝐹 ↾ 𝑊)‘(𝑁‘𝑅)) = (𝐹‘(𝑁‘𝑅))) |
137 | 135, 136 | syl 17 |
. . . . . 6
⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → ((𝐹 ↾ 𝑊)‘(𝑁‘𝑅)) = (𝐹‘(𝑁‘𝑅))) |
138 | 27, 32, 137 | 3eqtr4d 2788 |
. . . . 5
⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → ((𝐹 ↾ 𝑊)‘(𝑀‘𝑅)) = ((𝐹 ↾ 𝑊)‘(𝑁‘𝑅))) |
139 | 57 | cvmsf1o 33234 |
. . . . . . . . 9
⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑇 ∈ (𝑆‘𝑈) ∧ 𝑊 ∈ 𝑇) → (𝐹 ↾ 𝑊):𝑊–1-1-onto→𝑈) |
140 | 47, 56, 53, 139 | syl3anc 1370 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝜓) → (𝐹 ↾ 𝑊):𝑊–1-1-onto→𝑈) |
141 | | f1of1 6715 |
. . . . . . . 8
⊢ ((𝐹 ↾ 𝑊):𝑊–1-1-onto→𝑈 → (𝐹 ↾ 𝑊):𝑊–1-1→𝑈) |
142 | 140, 141 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝜓) → (𝐹 ↾ 𝑊):𝑊–1-1→𝑈) |
143 | 142 | adantr 481 |
. . . . . 6
⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → (𝐹 ↾ 𝑊):𝑊–1-1→𝑈) |
144 | | f1fveq 7135 |
. . . . . 6
⊢ (((𝐹 ↾ 𝑊):𝑊–1-1→𝑈 ∧ ((𝑀‘𝑅) ∈ 𝑊 ∧ (𝑁‘𝑅) ∈ 𝑊)) → (((𝐹 ↾ 𝑊)‘(𝑀‘𝑅)) = ((𝐹 ↾ 𝑊)‘(𝑁‘𝑅)) ↔ (𝑀‘𝑅) = (𝑁‘𝑅))) |
145 | 143, 30, 135, 144 | syl12anc 834 |
. . . . 5
⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → (((𝐹 ↾ 𝑊)‘(𝑀‘𝑅)) = ((𝐹 ↾ 𝑊)‘(𝑁‘𝑅)) ↔ (𝑀‘𝑅) = (𝑁‘𝑅))) |
146 | 138, 145 | mpbid 231 |
. . . 4
⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → (𝑀‘𝑅) = (𝑁‘𝑅)) |
147 | 146 | ex 413 |
. . 3
⊢ ((𝜑 ∧ 𝜓) → ((𝑀‘𝑄) = (𝑁‘𝑄) → (𝑀‘𝑅) = (𝑁‘𝑅))) |
148 | 124 | simprbda 499 |
. . . . 5
⊢ ((𝜑 ∧ 𝑄 ∈ (◡𝑀 “ 𝑊)) → 𝑄 ∈ 𝑌) |
149 | 122, 148 | syldan 591 |
. . . 4
⊢ ((𝜑 ∧ 𝜓) → 𝑄 ∈ 𝑌) |
150 | | fveq2 6774 |
. . . . . 6
⊢ (𝑥 = 𝑄 → (𝑀‘𝑥) = (𝑀‘𝑄)) |
151 | | fveq2 6774 |
. . . . . 6
⊢ (𝑥 = 𝑄 → (𝑁‘𝑥) = (𝑁‘𝑄)) |
152 | 150, 151 | eqeq12d 2754 |
. . . . 5
⊢ (𝑥 = 𝑄 → ((𝑀‘𝑥) = (𝑁‘𝑥) ↔ (𝑀‘𝑄) = (𝑁‘𝑄))) |
153 | 152 | elrab3 3625 |
. . . 4
⊢ (𝑄 ∈ 𝑌 → (𝑄 ∈ {𝑥 ∈ 𝑌 ∣ (𝑀‘𝑥) = (𝑁‘𝑥)} ↔ (𝑀‘𝑄) = (𝑁‘𝑄))) |
154 | 149, 153 | syl 17 |
. . 3
⊢ ((𝜑 ∧ 𝜓) → (𝑄 ∈ {𝑥 ∈ 𝑌 ∣ (𝑀‘𝑥) = (𝑁‘𝑥)} ↔ (𝑀‘𝑄) = (𝑁‘𝑄))) |
155 | | fveq2 6774 |
. . . . . 6
⊢ (𝑥 = 𝑅 → (𝑀‘𝑥) = (𝑀‘𝑅)) |
156 | | fveq2 6774 |
. . . . . 6
⊢ (𝑥 = 𝑅 → (𝑁‘𝑥) = (𝑁‘𝑅)) |
157 | 155, 156 | eqeq12d 2754 |
. . . . 5
⊢ (𝑥 = 𝑅 → ((𝑀‘𝑥) = (𝑁‘𝑥) ↔ (𝑀‘𝑅) = (𝑁‘𝑅))) |
158 | 157 | elrab3 3625 |
. . . 4
⊢ (𝑅 ∈ 𝑌 → (𝑅 ∈ {𝑥 ∈ 𝑌 ∣ (𝑀‘𝑥) = (𝑁‘𝑥)} ↔ (𝑀‘𝑅) = (𝑁‘𝑅))) |
159 | 16, 158 | syl 17 |
. . 3
⊢ ((𝜑 ∧ 𝜓) → (𝑅 ∈ {𝑥 ∈ 𝑌 ∣ (𝑀‘𝑥) = (𝑁‘𝑥)} ↔ (𝑀‘𝑅) = (𝑁‘𝑅))) |
160 | 147, 154,
159 | 3imtr4d 294 |
. 2
⊢ ((𝜑 ∧ 𝜓) → (𝑄 ∈ {𝑥 ∈ 𝑌 ∣ (𝑀‘𝑥) = (𝑁‘𝑥)} → 𝑅 ∈ {𝑥 ∈ 𝑌 ∣ (𝑀‘𝑥) = (𝑁‘𝑥)})) |
161 | 22 | ffnd 6601 |
. . . . 5
⊢ (𝜑 → 𝑁 Fn 𝑌) |
162 | | fndmin 6922 |
. . . . 5
⊢ ((𝑀 Fn 𝑌 ∧ 𝑁 Fn 𝑌) → dom (𝑀 ∩ 𝑁) = {𝑥 ∈ 𝑌 ∣ (𝑀‘𝑥) = (𝑁‘𝑥)}) |
163 | 12, 161, 162 | syl2anc 584 |
. . . 4
⊢ (𝜑 → dom (𝑀 ∩ 𝑁) = {𝑥 ∈ 𝑌 ∣ (𝑀‘𝑥) = (𝑁‘𝑥)}) |
164 | 163 | adantr 481 |
. . 3
⊢ ((𝜑 ∧ 𝜓) → dom (𝑀 ∩ 𝑁) = {𝑥 ∈ 𝑌 ∣ (𝑀‘𝑥) = (𝑁‘𝑥)}) |
165 | 164 | eleq2d 2824 |
. 2
⊢ ((𝜑 ∧ 𝜓) → (𝑄 ∈ dom (𝑀 ∩ 𝑁) ↔ 𝑄 ∈ {𝑥 ∈ 𝑌 ∣ (𝑀‘𝑥) = (𝑁‘𝑥)})) |
166 | 164 | eleq2d 2824 |
. 2
⊢ ((𝜑 ∧ 𝜓) → (𝑅 ∈ dom (𝑀 ∩ 𝑁) ↔ 𝑅 ∈ {𝑥 ∈ 𝑌 ∣ (𝑀‘𝑥) = (𝑁‘𝑥)})) |
167 | 160, 165,
166 | 3imtr4d 294 |
1
⊢ ((𝜑 ∧ 𝜓) → (𝑄 ∈ dom (𝑀 ∩ 𝑁) → 𝑅 ∈ dom (𝑀 ∩ 𝑁))) |