Step | Hyp | Ref
| Expression |
1 | | cvmliftmoi.g |
. . . . . . . . . 10
⊢ (𝜑 → (𝐹 ∘ 𝑀) = (𝐹 ∘ 𝑁)) |
2 | 1 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝜓) → (𝐹 ∘ 𝑀) = (𝐹 ∘ 𝑁)) |
3 | 2 | fveq1d 6105 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝜓) → ((𝐹 ∘ 𝑀)‘𝑅) = ((𝐹 ∘ 𝑁)‘𝑅)) |
4 | | cvmliftmolem.4 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝜓) → 𝐼 ⊆ (◡𝑀 “ 𝑊)) |
5 | | cvmliftmolem.8 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝜓) → 𝑅 ∈ 𝐼) |
6 | 4, 5 | sseldd 3569 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝜓) → 𝑅 ∈ (◡𝑀 “ 𝑊)) |
7 | | cvmliftmoi.m |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑀 ∈ (𝐾 Cn 𝐶)) |
8 | | cvmliftmo.y |
. . . . . . . . . . . . . . 15
⊢ 𝑌 = ∪
𝐾 |
9 | | cvmliftmo.b |
. . . . . . . . . . . . . . 15
⊢ 𝐵 = ∪
𝐶 |
10 | 8, 9 | cnf 20860 |
. . . . . . . . . . . . . 14
⊢ (𝑀 ∈ (𝐾 Cn 𝐶) → 𝑀:𝑌⟶𝐵) |
11 | 7, 10 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑀:𝑌⟶𝐵) |
12 | | ffn 5958 |
. . . . . . . . . . . . 13
⊢ (𝑀:𝑌⟶𝐵 → 𝑀 Fn 𝑌) |
13 | 11, 12 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑀 Fn 𝑌) |
14 | | elpreima 6245 |
. . . . . . . . . . . 12
⊢ (𝑀 Fn 𝑌 → (𝑅 ∈ (◡𝑀 “ 𝑊) ↔ (𝑅 ∈ 𝑌 ∧ (𝑀‘𝑅) ∈ 𝑊))) |
15 | 13, 14 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑅 ∈ (◡𝑀 “ 𝑊) ↔ (𝑅 ∈ 𝑌 ∧ (𝑀‘𝑅) ∈ 𝑊))) |
16 | 15 | simprbda 651 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑅 ∈ (◡𝑀 “ 𝑊)) → 𝑅 ∈ 𝑌) |
17 | 6, 16 | syldan 486 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝜓) → 𝑅 ∈ 𝑌) |
18 | | fvco3 6185 |
. . . . . . . . . 10
⊢ ((𝑀:𝑌⟶𝐵 ∧ 𝑅 ∈ 𝑌) → ((𝐹 ∘ 𝑀)‘𝑅) = (𝐹‘(𝑀‘𝑅))) |
19 | 11, 18 | sylan 487 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑅 ∈ 𝑌) → ((𝐹 ∘ 𝑀)‘𝑅) = (𝐹‘(𝑀‘𝑅))) |
20 | 17, 19 | syldan 486 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝜓) → ((𝐹 ∘ 𝑀)‘𝑅) = (𝐹‘(𝑀‘𝑅))) |
21 | | cvmliftmoi.n |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑁 ∈ (𝐾 Cn 𝐶)) |
22 | 8, 9 | cnf 20860 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ (𝐾 Cn 𝐶) → 𝑁:𝑌⟶𝐵) |
23 | 21, 22 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑁:𝑌⟶𝐵) |
24 | | fvco3 6185 |
. . . . . . . . . 10
⊢ ((𝑁:𝑌⟶𝐵 ∧ 𝑅 ∈ 𝑌) → ((𝐹 ∘ 𝑁)‘𝑅) = (𝐹‘(𝑁‘𝑅))) |
25 | 23, 24 | sylan 487 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑅 ∈ 𝑌) → ((𝐹 ∘ 𝑁)‘𝑅) = (𝐹‘(𝑁‘𝑅))) |
26 | 17, 25 | syldan 486 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝜓) → ((𝐹 ∘ 𝑁)‘𝑅) = (𝐹‘(𝑁‘𝑅))) |
27 | 3, 20, 26 | 3eqtr3d 2652 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝜓) → (𝐹‘(𝑀‘𝑅)) = (𝐹‘(𝑁‘𝑅))) |
28 | 27 | adantr 480 |
. . . . . 6
⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → (𝐹‘(𝑀‘𝑅)) = (𝐹‘(𝑁‘𝑅))) |
29 | 15 | simplbda 652 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑅 ∈ (◡𝑀 “ 𝑊)) → (𝑀‘𝑅) ∈ 𝑊) |
30 | 6, 29 | syldan 486 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝜓) → (𝑀‘𝑅) ∈ 𝑊) |
31 | 30 | adantr 480 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → (𝑀‘𝑅) ∈ 𝑊) |
32 | | fvres 6117 |
. . . . . . 7
⊢ ((𝑀‘𝑅) ∈ 𝑊 → ((𝐹 ↾ 𝑊)‘(𝑀‘𝑅)) = (𝐹‘(𝑀‘𝑅))) |
33 | 31, 32 | syl 17 |
. . . . . 6
⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → ((𝐹 ↾ 𝑊)‘(𝑀‘𝑅)) = (𝐹‘(𝑀‘𝑅))) |
34 | 5 | adantr 480 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → 𝑅 ∈ 𝐼) |
35 | | fvres 6117 |
. . . . . . . . 9
⊢ (𝑅 ∈ 𝐼 → ((𝑁 ↾ 𝐼)‘𝑅) = (𝑁‘𝑅)) |
36 | 34, 35 | syl 17 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → ((𝑁 ↾ 𝐼)‘𝑅) = (𝑁‘𝑅)) |
37 | | eqid 2610 |
. . . . . . . . . . 11
⊢ ∪ (𝐾
↾t 𝐼) =
∪ (𝐾 ↾t 𝐼) |
38 | | cvmliftmolem.5 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝜓) → (𝐾 ↾t 𝐼) ∈ Con) |
39 | 38 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → (𝐾 ↾t 𝐼) ∈ Con) |
40 | 21 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝜓) → 𝑁 ∈ (𝐾 Cn 𝐶)) |
41 | | cnvimass 5404 |
. . . . . . . . . . . . . . . . 17
⊢ (◡𝑀 “ 𝑊) ⊆ dom 𝑀 |
42 | | fdm 5964 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑀:𝑌⟶𝐵 → dom 𝑀 = 𝑌) |
43 | 11, 42 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → dom 𝑀 = 𝑌) |
44 | 41, 43 | syl5sseq 3616 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (◡𝑀 “ 𝑊) ⊆ 𝑌) |
45 | 44 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝜓) → (◡𝑀 “ 𝑊) ⊆ 𝑌) |
46 | 4, 45 | sstrd 3578 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝜓) → 𝐼 ⊆ 𝑌) |
47 | 8 | cnrest 20899 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ (𝐾 Cn 𝐶) ∧ 𝐼 ⊆ 𝑌) → (𝑁 ↾ 𝐼) ∈ ((𝐾 ↾t 𝐼) Cn 𝐶)) |
48 | 40, 46, 47 | syl2anc 691 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝜓) → (𝑁 ↾ 𝐼) ∈ ((𝐾 ↾t 𝐼) Cn 𝐶)) |
49 | | cvmliftmo.f |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐹 ∈ (𝐶 CovMap 𝐽)) |
50 | 49 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝜓) → 𝐹 ∈ (𝐶 CovMap 𝐽)) |
51 | | cvmtop1 30496 |
. . . . . . . . . . . . . . . 16
⊢ (𝐹 ∈ (𝐶 CovMap 𝐽) → 𝐶 ∈ Top) |
52 | 50, 51 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝜓) → 𝐶 ∈ Top) |
53 | 9 | toptopon 20548 |
. . . . . . . . . . . . . . 15
⊢ (𝐶 ∈ Top ↔ 𝐶 ∈ (TopOn‘𝐵)) |
54 | 52, 53 | sylib 207 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝜓) → 𝐶 ∈ (TopOn‘𝐵)) |
55 | | df-ima 5051 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 “ 𝐼) = ran (𝑁 ↾ 𝐼) |
56 | | cvmliftmolem.3 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝜓) → 𝑊 ∈ 𝑇) |
57 | | elssuni 4403 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑊 ∈ 𝑇 → 𝑊 ⊆ ∪ 𝑇) |
58 | 56, 57 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝜓) → 𝑊 ⊆ ∪ 𝑇) |
59 | | cvmliftmolem.2 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝜓) → 𝑇 ∈ (𝑆‘𝑈)) |
60 | | cvmliftmolem.1 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 =
(◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾t 𝑢)Homeo(𝐽 ↾t 𝑘))))}) |
61 | 60 | cvmsuni 30505 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑇 ∈ (𝑆‘𝑈) → ∪ 𝑇 = (◡𝐹 “ 𝑈)) |
62 | 59, 61 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝜓) → ∪ 𝑇 = (◡𝐹 “ 𝑈)) |
63 | 58, 62 | sseqtrd 3604 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝜓) → 𝑊 ⊆ (◡𝐹 “ 𝑈)) |
64 | | imass2 5420 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑊 ⊆ (◡𝐹 “ 𝑈) → (◡𝑀 “ 𝑊) ⊆ (◡𝑀 “ (◡𝐹 “ 𝑈))) |
65 | 63, 64 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝜓) → (◡𝑀 “ 𝑊) ⊆ (◡𝑀 “ (◡𝐹 “ 𝑈))) |
66 | 4, 65 | sstrd 3578 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝜓) → 𝐼 ⊆ (◡𝑀 “ (◡𝐹 “ 𝑈))) |
67 | 2 | cnveqd 5220 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝜓) → ◡(𝐹 ∘ 𝑀) = ◡(𝐹 ∘ 𝑁)) |
68 | | cnvco 5230 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ◡(𝐹 ∘ 𝑀) = (◡𝑀 ∘ ◡𝐹) |
69 | | cnvco 5230 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ◡(𝐹 ∘ 𝑁) = (◡𝑁 ∘ ◡𝐹) |
70 | 67, 68, 69 | 3eqtr3g 2667 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝜓) → (◡𝑀 ∘ ◡𝐹) = (◡𝑁 ∘ ◡𝐹)) |
71 | 70 | imaeq1d 5384 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝜓) → ((◡𝑀 ∘ ◡𝐹) “ 𝑈) = ((◡𝑁 ∘ ◡𝐹) “ 𝑈)) |
72 | | imaco 5557 |
. . . . . . . . . . . . . . . . . 18
⊢ ((◡𝑀 ∘ ◡𝐹) “ 𝑈) = (◡𝑀 “ (◡𝐹 “ 𝑈)) |
73 | | imaco 5557 |
. . . . . . . . . . . . . . . . . 18
⊢ ((◡𝑁 ∘ ◡𝐹) “ 𝑈) = (◡𝑁 “ (◡𝐹 “ 𝑈)) |
74 | 71, 72, 73 | 3eqtr3g 2667 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝜓) → (◡𝑀 “ (◡𝐹 “ 𝑈)) = (◡𝑁 “ (◡𝐹 “ 𝑈))) |
75 | 66, 74 | sseqtrd 3604 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝜓) → 𝐼 ⊆ (◡𝑁 “ (◡𝐹 “ 𝑈))) |
76 | 23 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝜓) → 𝑁:𝑌⟶𝐵) |
77 | | ffun 5961 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑁:𝑌⟶𝐵 → Fun 𝑁) |
78 | 76, 77 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝜓) → Fun 𝑁) |
79 | | fdm 5964 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑁:𝑌⟶𝐵 → dom 𝑁 = 𝑌) |
80 | 76, 79 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝜓) → dom 𝑁 = 𝑌) |
81 | 46, 80 | sseqtr4d 3605 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝜓) → 𝐼 ⊆ dom 𝑁) |
82 | | funimass3 6241 |
. . . . . . . . . . . . . . . . 17
⊢ ((Fun
𝑁 ∧ 𝐼 ⊆ dom 𝑁) → ((𝑁 “ 𝐼) ⊆ (◡𝐹 “ 𝑈) ↔ 𝐼 ⊆ (◡𝑁 “ (◡𝐹 “ 𝑈)))) |
83 | 78, 81, 82 | syl2anc 691 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝜓) → ((𝑁 “ 𝐼) ⊆ (◡𝐹 “ 𝑈) ↔ 𝐼 ⊆ (◡𝑁 “ (◡𝐹 “ 𝑈)))) |
84 | 75, 83 | mpbird 246 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝜓) → (𝑁 “ 𝐼) ⊆ (◡𝐹 “ 𝑈)) |
85 | 55, 84 | syl5eqssr 3613 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝜓) → ran (𝑁 ↾ 𝐼) ⊆ (◡𝐹 “ 𝑈)) |
86 | | cnvimass 5404 |
. . . . . . . . . . . . . . 15
⊢ (◡𝐹 “ 𝑈) ⊆ dom 𝐹 |
87 | | cvmcn 30498 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐹 ∈ (𝐶 CovMap 𝐽) → 𝐹 ∈ (𝐶 Cn 𝐽)) |
88 | 49, 87 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐹 ∈ (𝐶 Cn 𝐽)) |
89 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . 19
⊢ ∪ 𝐽 =
∪ 𝐽 |
90 | 9, 89 | cnf 20860 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐹 ∈ (𝐶 Cn 𝐽) → 𝐹:𝐵⟶∪ 𝐽) |
91 | 88, 90 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐹:𝐵⟶∪ 𝐽) |
92 | | fdm 5964 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐹:𝐵⟶∪ 𝐽 → dom 𝐹 = 𝐵) |
93 | 91, 92 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → dom 𝐹 = 𝐵) |
94 | 93 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝜓) → dom 𝐹 = 𝐵) |
95 | 86, 94 | syl5sseq 3616 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝜓) → (◡𝐹 “ 𝑈) ⊆ 𝐵) |
96 | | cnrest2 20900 |
. . . . . . . . . . . . . 14
⊢ ((𝐶 ∈ (TopOn‘𝐵) ∧ ran (𝑁 ↾ 𝐼) ⊆ (◡𝐹 “ 𝑈) ∧ (◡𝐹 “ 𝑈) ⊆ 𝐵) → ((𝑁 ↾ 𝐼) ∈ ((𝐾 ↾t 𝐼) Cn 𝐶) ↔ (𝑁 ↾ 𝐼) ∈ ((𝐾 ↾t 𝐼) Cn (𝐶 ↾t (◡𝐹 “ 𝑈))))) |
97 | 54, 85, 95, 96 | syl3anc 1318 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝜓) → ((𝑁 ↾ 𝐼) ∈ ((𝐾 ↾t 𝐼) Cn 𝐶) ↔ (𝑁 ↾ 𝐼) ∈ ((𝐾 ↾t 𝐼) Cn (𝐶 ↾t (◡𝐹 “ 𝑈))))) |
98 | 48, 97 | mpbid 221 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝜓) → (𝑁 ↾ 𝐼) ∈ ((𝐾 ↾t 𝐼) Cn (𝐶 ↾t (◡𝐹 “ 𝑈)))) |
99 | 98 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → (𝑁 ↾ 𝐼) ∈ ((𝐾 ↾t 𝐼) Cn (𝐶 ↾t (◡𝐹 “ 𝑈)))) |
100 | | df-ss 3554 |
. . . . . . . . . . . . . 14
⊢ (𝑊 ⊆ (◡𝐹 “ 𝑈) ↔ (𝑊 ∩ (◡𝐹 “ 𝑈)) = 𝑊) |
101 | 63, 100 | sylib 207 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝜓) → (𝑊 ∩ (◡𝐹 “ 𝑈)) = 𝑊) |
102 | 9 | topopn 20536 |
. . . . . . . . . . . . . . . 16
⊢ (𝐶 ∈ Top → 𝐵 ∈ 𝐶) |
103 | 52, 102 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝜓) → 𝐵 ∈ 𝐶) |
104 | 103, 95 | ssexd 4733 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝜓) → (◡𝐹 “ 𝑈) ∈ V) |
105 | 60 | cvmsss 30503 |
. . . . . . . . . . . . . . . 16
⊢ (𝑇 ∈ (𝑆‘𝑈) → 𝑇 ⊆ 𝐶) |
106 | 59, 105 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝜓) → 𝑇 ⊆ 𝐶) |
107 | 106, 56 | sseldd 3569 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝜓) → 𝑊 ∈ 𝐶) |
108 | | elrestr 15912 |
. . . . . . . . . . . . . 14
⊢ ((𝐶 ∈ Top ∧ (◡𝐹 “ 𝑈) ∈ V ∧ 𝑊 ∈ 𝐶) → (𝑊 ∩ (◡𝐹 “ 𝑈)) ∈ (𝐶 ↾t (◡𝐹 “ 𝑈))) |
109 | 52, 104, 107, 108 | syl3anc 1318 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝜓) → (𝑊 ∩ (◡𝐹 “ 𝑈)) ∈ (𝐶 ↾t (◡𝐹 “ 𝑈))) |
110 | 101, 109 | eqeltrrd 2689 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝜓) → 𝑊 ∈ (𝐶 ↾t (◡𝐹 “ 𝑈))) |
111 | 110 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → 𝑊 ∈ (𝐶 ↾t (◡𝐹 “ 𝑈))) |
112 | 60 | cvmscld 30509 |
. . . . . . . . . . . . 13
⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑇 ∈ (𝑆‘𝑈) ∧ 𝑊 ∈ 𝑇) → 𝑊 ∈ (Clsd‘(𝐶 ↾t (◡𝐹 “ 𝑈)))) |
113 | 50, 59, 56, 112 | syl3anc 1318 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝜓) → 𝑊 ∈ (Clsd‘(𝐶 ↾t (◡𝐹 “ 𝑈)))) |
114 | 113 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → 𝑊 ∈ (Clsd‘(𝐶 ↾t (◡𝐹 “ 𝑈)))) |
115 | | cvmliftmolem.7 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝜓) → 𝑄 ∈ 𝐼) |
116 | | cvmliftmo.k |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐾 ∈ Con) |
117 | | contop 21030 |
. . . . . . . . . . . . . . . 16
⊢ (𝐾 ∈ Con → 𝐾 ∈ Top) |
118 | 116, 117 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐾 ∈ Top) |
119 | 118 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝜓) → 𝐾 ∈ Top) |
120 | 8 | restuni 20776 |
. . . . . . . . . . . . . 14
⊢ ((𝐾 ∈ Top ∧ 𝐼 ⊆ 𝑌) → 𝐼 = ∪ (𝐾 ↾t 𝐼)) |
121 | 119, 46, 120 | syl2anc 691 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝜓) → 𝐼 = ∪ (𝐾 ↾t 𝐼)) |
122 | 115, 121 | eleqtrd 2690 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝜓) → 𝑄 ∈ ∪ (𝐾 ↾t 𝐼)) |
123 | 122 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → 𝑄 ∈ ∪ (𝐾 ↾t 𝐼)) |
124 | 115 | adantr 480 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → 𝑄 ∈ 𝐼) |
125 | | fvres 6117 |
. . . . . . . . . . . . 13
⊢ (𝑄 ∈ 𝐼 → ((𝑁 ↾ 𝐼)‘𝑄) = (𝑁‘𝑄)) |
126 | 124, 125 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → ((𝑁 ↾ 𝐼)‘𝑄) = (𝑁‘𝑄)) |
127 | | simpr 476 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → (𝑀‘𝑄) = (𝑁‘𝑄)) |
128 | 4, 115 | sseldd 3569 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝜓) → 𝑄 ∈ (◡𝑀 “ 𝑊)) |
129 | | elpreima 6245 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑀 Fn 𝑌 → (𝑄 ∈ (◡𝑀 “ 𝑊) ↔ (𝑄 ∈ 𝑌 ∧ (𝑀‘𝑄) ∈ 𝑊))) |
130 | 13, 129 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑄 ∈ (◡𝑀 “ 𝑊) ↔ (𝑄 ∈ 𝑌 ∧ (𝑀‘𝑄) ∈ 𝑊))) |
131 | 130 | simplbda 652 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑄 ∈ (◡𝑀 “ 𝑊)) → (𝑀‘𝑄) ∈ 𝑊) |
132 | 128, 131 | syldan 486 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝜓) → (𝑀‘𝑄) ∈ 𝑊) |
133 | 132 | adantr 480 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → (𝑀‘𝑄) ∈ 𝑊) |
134 | 127, 133 | eqeltrrd 2689 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → (𝑁‘𝑄) ∈ 𝑊) |
135 | 126, 134 | eqeltrd 2688 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → ((𝑁 ↾ 𝐼)‘𝑄) ∈ 𝑊) |
136 | 37, 39, 99, 111, 114, 123, 135 | concn 21039 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → (𝑁 ↾ 𝐼):∪ (𝐾 ↾t 𝐼)⟶𝑊) |
137 | 121 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → 𝐼 = ∪ (𝐾 ↾t 𝐼)) |
138 | 137 | feq2d 5944 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → ((𝑁 ↾ 𝐼):𝐼⟶𝑊 ↔ (𝑁 ↾ 𝐼):∪ (𝐾 ↾t 𝐼)⟶𝑊)) |
139 | 136, 138 | mpbird 246 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → (𝑁 ↾ 𝐼):𝐼⟶𝑊) |
140 | 139, 34 | ffvelrnd 6268 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → ((𝑁 ↾ 𝐼)‘𝑅) ∈ 𝑊) |
141 | 36, 140 | eqeltrrd 2689 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → (𝑁‘𝑅) ∈ 𝑊) |
142 | | fvres 6117 |
. . . . . . 7
⊢ ((𝑁‘𝑅) ∈ 𝑊 → ((𝐹 ↾ 𝑊)‘(𝑁‘𝑅)) = (𝐹‘(𝑁‘𝑅))) |
143 | 141, 142 | syl 17 |
. . . . . 6
⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → ((𝐹 ↾ 𝑊)‘(𝑁‘𝑅)) = (𝐹‘(𝑁‘𝑅))) |
144 | 28, 33, 143 | 3eqtr4d 2654 |
. . . . 5
⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → ((𝐹 ↾ 𝑊)‘(𝑀‘𝑅)) = ((𝐹 ↾ 𝑊)‘(𝑁‘𝑅))) |
145 | 60 | cvmsf1o 30508 |
. . . . . . . . 9
⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑇 ∈ (𝑆‘𝑈) ∧ 𝑊 ∈ 𝑇) → (𝐹 ↾ 𝑊):𝑊–1-1-onto→𝑈) |
146 | 50, 59, 56, 145 | syl3anc 1318 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝜓) → (𝐹 ↾ 𝑊):𝑊–1-1-onto→𝑈) |
147 | | f1of1 6049 |
. . . . . . . 8
⊢ ((𝐹 ↾ 𝑊):𝑊–1-1-onto→𝑈 → (𝐹 ↾ 𝑊):𝑊–1-1→𝑈) |
148 | 146, 147 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝜓) → (𝐹 ↾ 𝑊):𝑊–1-1→𝑈) |
149 | 148 | adantr 480 |
. . . . . 6
⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → (𝐹 ↾ 𝑊):𝑊–1-1→𝑈) |
150 | | f1fveq 6420 |
. . . . . 6
⊢ (((𝐹 ↾ 𝑊):𝑊–1-1→𝑈 ∧ ((𝑀‘𝑅) ∈ 𝑊 ∧ (𝑁‘𝑅) ∈ 𝑊)) → (((𝐹 ↾ 𝑊)‘(𝑀‘𝑅)) = ((𝐹 ↾ 𝑊)‘(𝑁‘𝑅)) ↔ (𝑀‘𝑅) = (𝑁‘𝑅))) |
151 | 149, 31, 141, 150 | syl12anc 1316 |
. . . . 5
⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → (((𝐹 ↾ 𝑊)‘(𝑀‘𝑅)) = ((𝐹 ↾ 𝑊)‘(𝑁‘𝑅)) ↔ (𝑀‘𝑅) = (𝑁‘𝑅))) |
152 | 144, 151 | mpbid 221 |
. . . 4
⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → (𝑀‘𝑅) = (𝑁‘𝑅)) |
153 | 152 | ex 449 |
. . 3
⊢ ((𝜑 ∧ 𝜓) → ((𝑀‘𝑄) = (𝑁‘𝑄) → (𝑀‘𝑅) = (𝑁‘𝑅))) |
154 | 130 | simprbda 651 |
. . . . 5
⊢ ((𝜑 ∧ 𝑄 ∈ (◡𝑀 “ 𝑊)) → 𝑄 ∈ 𝑌) |
155 | 128, 154 | syldan 486 |
. . . 4
⊢ ((𝜑 ∧ 𝜓) → 𝑄 ∈ 𝑌) |
156 | | fveq2 6103 |
. . . . . 6
⊢ (𝑥 = 𝑄 → (𝑀‘𝑥) = (𝑀‘𝑄)) |
157 | | fveq2 6103 |
. . . . . 6
⊢ (𝑥 = 𝑄 → (𝑁‘𝑥) = (𝑁‘𝑄)) |
158 | 156, 157 | eqeq12d 2625 |
. . . . 5
⊢ (𝑥 = 𝑄 → ((𝑀‘𝑥) = (𝑁‘𝑥) ↔ (𝑀‘𝑄) = (𝑁‘𝑄))) |
159 | 158 | elrab3 3332 |
. . . 4
⊢ (𝑄 ∈ 𝑌 → (𝑄 ∈ {𝑥 ∈ 𝑌 ∣ (𝑀‘𝑥) = (𝑁‘𝑥)} ↔ (𝑀‘𝑄) = (𝑁‘𝑄))) |
160 | 155, 159 | syl 17 |
. . 3
⊢ ((𝜑 ∧ 𝜓) → (𝑄 ∈ {𝑥 ∈ 𝑌 ∣ (𝑀‘𝑥) = (𝑁‘𝑥)} ↔ (𝑀‘𝑄) = (𝑁‘𝑄))) |
161 | | fveq2 6103 |
. . . . . 6
⊢ (𝑥 = 𝑅 → (𝑀‘𝑥) = (𝑀‘𝑅)) |
162 | | fveq2 6103 |
. . . . . 6
⊢ (𝑥 = 𝑅 → (𝑁‘𝑥) = (𝑁‘𝑅)) |
163 | 161, 162 | eqeq12d 2625 |
. . . . 5
⊢ (𝑥 = 𝑅 → ((𝑀‘𝑥) = (𝑁‘𝑥) ↔ (𝑀‘𝑅) = (𝑁‘𝑅))) |
164 | 163 | elrab3 3332 |
. . . 4
⊢ (𝑅 ∈ 𝑌 → (𝑅 ∈ {𝑥 ∈ 𝑌 ∣ (𝑀‘𝑥) = (𝑁‘𝑥)} ↔ (𝑀‘𝑅) = (𝑁‘𝑅))) |
165 | 17, 164 | syl 17 |
. . 3
⊢ ((𝜑 ∧ 𝜓) → (𝑅 ∈ {𝑥 ∈ 𝑌 ∣ (𝑀‘𝑥) = (𝑁‘𝑥)} ↔ (𝑀‘𝑅) = (𝑁‘𝑅))) |
166 | 153, 160,
165 | 3imtr4d 282 |
. 2
⊢ ((𝜑 ∧ 𝜓) → (𝑄 ∈ {𝑥 ∈ 𝑌 ∣ (𝑀‘𝑥) = (𝑁‘𝑥)} → 𝑅 ∈ {𝑥 ∈ 𝑌 ∣ (𝑀‘𝑥) = (𝑁‘𝑥)})) |
167 | | ffn 5958 |
. . . . . 6
⊢ (𝑁:𝑌⟶𝐵 → 𝑁 Fn 𝑌) |
168 | 23, 167 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑁 Fn 𝑌) |
169 | | fndmin 6232 |
. . . . 5
⊢ ((𝑀 Fn 𝑌 ∧ 𝑁 Fn 𝑌) → dom (𝑀 ∩ 𝑁) = {𝑥 ∈ 𝑌 ∣ (𝑀‘𝑥) = (𝑁‘𝑥)}) |
170 | 13, 168, 169 | syl2anc 691 |
. . . 4
⊢ (𝜑 → dom (𝑀 ∩ 𝑁) = {𝑥 ∈ 𝑌 ∣ (𝑀‘𝑥) = (𝑁‘𝑥)}) |
171 | 170 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ 𝜓) → dom (𝑀 ∩ 𝑁) = {𝑥 ∈ 𝑌 ∣ (𝑀‘𝑥) = (𝑁‘𝑥)}) |
172 | 171 | eleq2d 2673 |
. 2
⊢ ((𝜑 ∧ 𝜓) → (𝑄 ∈ dom (𝑀 ∩ 𝑁) ↔ 𝑄 ∈ {𝑥 ∈ 𝑌 ∣ (𝑀‘𝑥) = (𝑁‘𝑥)})) |
173 | 171 | eleq2d 2673 |
. 2
⊢ ((𝜑 ∧ 𝜓) → (𝑅 ∈ dom (𝑀 ∩ 𝑁) ↔ 𝑅 ∈ {𝑥 ∈ 𝑌 ∣ (𝑀‘𝑥) = (𝑁‘𝑥)})) |
174 | 166, 172,
173 | 3imtr4d 282 |
1
⊢ ((𝜑 ∧ 𝜓) → (𝑄 ∈ dom (𝑀 ∩ 𝑁) → 𝑅 ∈ dom (𝑀 ∩ 𝑁))) |