Users' Mathboxes Mathbox for Mario Carneiro < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  cvmliftmolem2 Structured version   Visualization version   GIF version

Theorem cvmliftmolem2 33916
Description: Lemma for cvmliftmo 33918. (Contributed by Mario Carneiro, 10-Mar-2015.)
Hypotheses
Ref Expression
cvmliftmo.b 𝐵 = 𝐶
cvmliftmo.y 𝑌 = 𝐾
cvmliftmo.f (𝜑𝐹 ∈ (𝐶 CovMap 𝐽))
cvmliftmo.k (𝜑𝐾 ∈ Conn)
cvmliftmo.l (𝜑𝐾 ∈ 𝑛-Locally Conn)
cvmliftmo.o (𝜑𝑂𝑌)
cvmliftmoi.m (𝜑𝑀 ∈ (𝐾 Cn 𝐶))
cvmliftmoi.n (𝜑𝑁 ∈ (𝐾 Cn 𝐶))
cvmliftmoi.g (𝜑 → (𝐹𝑀) = (𝐹𝑁))
cvmliftmoi.p (𝜑 → (𝑀𝑂) = (𝑁𝑂))
cvmliftmolem.1 𝑆 = (𝑘𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ ( 𝑠 = (𝐹𝑘) ∧ ∀𝑢𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢𝑣) = ∅ ∧ (𝐹𝑢) ∈ ((𝐶t 𝑢)Homeo(𝐽t 𝑘))))})
Assertion
Ref Expression
cvmliftmolem2 (𝜑𝑀 = 𝑁)
Distinct variable groups:   𝑘,𝑠,𝑢,𝑣,𝐶   𝑘,𝐽,𝑠,𝑢,𝑣   𝑣,𝐵   𝐾,𝑠   𝑘,𝑀,𝑠,𝑢,𝑣   𝑁,𝑠   𝜑,𝑠   𝑘,𝐹,𝑠,𝑢,𝑣   𝑆,𝑠   𝑌,𝑠
Allowed substitution hints:   𝜑(𝑣,𝑢,𝑘)   𝐵(𝑢,𝑘,𝑠)   𝑆(𝑣,𝑢,𝑘)   𝐾(𝑣,𝑢,𝑘)   𝑁(𝑣,𝑢,𝑘)   𝑂(𝑣,𝑢,𝑘,𝑠)   𝑌(𝑣,𝑢,𝑘)

Proof of Theorem cvmliftmolem2
Dummy variables 𝑎 𝑏 𝑡 𝑦 𝑧 𝑥 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 cvmliftmoi.m . . 3 (𝜑𝑀 ∈ (𝐾 Cn 𝐶))
2 cvmliftmo.y . . . 4 𝑌 = 𝐾
3 cvmliftmo.b . . . 4 𝐵 = 𝐶
42, 3cnf 22613 . . 3 (𝑀 ∈ (𝐾 Cn 𝐶) → 𝑀:𝑌𝐵)
5 ffn 6673 . . 3 (𝑀:𝑌𝐵𝑀 Fn 𝑌)
61, 4, 53syl 18 . 2 (𝜑𝑀 Fn 𝑌)
7 cvmliftmoi.n . . 3 (𝜑𝑁 ∈ (𝐾 Cn 𝐶))
82, 3cnf 22613 . . 3 (𝑁 ∈ (𝐾 Cn 𝐶) → 𝑁:𝑌𝐵)
9 ffn 6673 . . 3 (𝑁:𝑌𝐵𝑁 Fn 𝑌)
107, 8, 93syl 18 . 2 (𝜑𝑁 Fn 𝑌)
11 cvmliftmo.k . . . . . 6 (𝜑𝐾 ∈ Conn)
12 inss1 4193 . . . . . . 7 (𝐾 ∩ (Clsd‘𝐾)) ⊆ 𝐾
13 cvmliftmo.f . . . . . . . . . . . 12 (𝜑𝐹 ∈ (𝐶 CovMap 𝐽))
1413adantr 482 . . . . . . . . . . 11 ((𝜑𝑥𝑌) → 𝐹 ∈ (𝐶 CovMap 𝐽))
151, 4syl 17 . . . . . . . . . . . . 13 (𝜑𝑀:𝑌𝐵)
1615ffvelcdmda 7040 . . . . . . . . . . . 12 ((𝜑𝑥𝑌) → (𝑀𝑥) ∈ 𝐵)
17 cvmcn 33896 . . . . . . . . . . . . . 14 (𝐹 ∈ (𝐶 CovMap 𝐽) → 𝐹 ∈ (𝐶 Cn 𝐽))
18 eqid 2737 . . . . . . . . . . . . . . 15 𝐽 = 𝐽
193, 18cnf 22613 . . . . . . . . . . . . . 14 (𝐹 ∈ (𝐶 Cn 𝐽) → 𝐹:𝐵 𝐽)
2013, 17, 193syl 18 . . . . . . . . . . . . 13 (𝜑𝐹:𝐵 𝐽)
2120ffvelcdmda 7040 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑀𝑥) ∈ 𝐵) → (𝐹‘(𝑀𝑥)) ∈ 𝐽)
2216, 21syldan 592 . . . . . . . . . . 11 ((𝜑𝑥𝑌) → (𝐹‘(𝑀𝑥)) ∈ 𝐽)
23 cvmliftmolem.1 . . . . . . . . . . . 12 𝑆 = (𝑘𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ ( 𝑠 = (𝐹𝑘) ∧ ∀𝑢𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢𝑣) = ∅ ∧ (𝐹𝑢) ∈ ((𝐶t 𝑢)Homeo(𝐽t 𝑘))))})
2423, 18cvmcov 33897 . . . . . . . . . . 11 ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ (𝐹‘(𝑀𝑥)) ∈ 𝐽) → ∃𝑎𝐽 ((𝐹‘(𝑀𝑥)) ∈ 𝑎 ∧ (𝑆𝑎) ≠ ∅))
2514, 22, 24syl2anc 585 . . . . . . . . . 10 ((𝜑𝑥𝑌) → ∃𝑎𝐽 ((𝐹‘(𝑀𝑥)) ∈ 𝑎 ∧ (𝑆𝑎) ≠ ∅))
26 n0 4311 . . . . . . . . . . . . . 14 ((𝑆𝑎) ≠ ∅ ↔ ∃𝑡 𝑡 ∈ (𝑆𝑎))
27 cvmliftmo.l . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐾 ∈ 𝑛-Locally Conn)
2827adantr 482 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ ((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎)))) → 𝐾 ∈ 𝑛-Locally Conn)
291adantr 482 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ ((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎)))) → 𝑀 ∈ (𝐾 Cn 𝐶))
30 simprrr 781 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ ((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎)))) → 𝑡 ∈ (𝑆𝑎))
3123cvmsss 33901 . . . . . . . . . . . . . . . . . . . . . 22 (𝑡 ∈ (𝑆𝑎) → 𝑡𝐶)
3230, 31syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ ((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎)))) → 𝑡𝐶)
3313adantr 482 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ ((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎)))) → 𝐹 ∈ (𝐶 CovMap 𝐽))
3415adantr 482 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ ((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎)))) → 𝑀:𝑌𝐵)
35 simprll 778 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ ((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎)))) → 𝑥𝑌)
3634, 35ffvelcdmd 7041 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ ((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎)))) → (𝑀𝑥) ∈ 𝐵)
37 simprrl 780 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ ((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎)))) → (𝐹‘(𝑀𝑥)) ∈ 𝑎)
38 eqid 2737 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑏𝑡 (𝑀𝑥) ∈ 𝑏) = (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)
3923, 3, 38cvmsiota 33911 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ (𝑡 ∈ (𝑆𝑎) ∧ (𝑀𝑥) ∈ 𝐵 ∧ (𝐹‘(𝑀𝑥)) ∈ 𝑎)) → ((𝑏𝑡 (𝑀𝑥) ∈ 𝑏) ∈ 𝑡 ∧ (𝑀𝑥) ∈ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)))
4033, 30, 36, 37, 39syl13anc 1373 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ ((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎)))) → ((𝑏𝑡 (𝑀𝑥) ∈ 𝑏) ∈ 𝑡 ∧ (𝑀𝑥) ∈ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)))
4140simpld 496 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ ((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎)))) → (𝑏𝑡 (𝑀𝑥) ∈ 𝑏) ∈ 𝑡)
4232, 41sseldd 3950 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ ((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎)))) → (𝑏𝑡 (𝑀𝑥) ∈ 𝑏) ∈ 𝐶)
43 cnima 22632 . . . . . . . . . . . . . . . . . . . 20 ((𝑀 ∈ (𝐾 Cn 𝐶) ∧ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏) ∈ 𝐶) → (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)) ∈ 𝐾)
4429, 42, 43syl2anc 585 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ ((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎)))) → (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)) ∈ 𝐾)
4540simprd 497 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ ((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎)))) → (𝑀𝑥) ∈ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏))
46 elpreima 7013 . . . . . . . . . . . . . . . . . . . . 21 (𝑀 Fn 𝑌 → (𝑥 ∈ (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)) ↔ (𝑥𝑌 ∧ (𝑀𝑥) ∈ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏))))
4734, 5, 463syl 18 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ ((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎)))) → (𝑥 ∈ (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)) ↔ (𝑥𝑌 ∧ (𝑀𝑥) ∈ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏))))
4835, 45, 47mpbir2and 712 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ ((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎)))) → 𝑥 ∈ (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)))
49 nlly2i 22843 . . . . . . . . . . . . . . . . . . 19 ((𝐾 ∈ 𝑛-Locally Conn ∧ (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)) ∈ 𝐾𝑥 ∈ (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏))) → ∃𝑠 ∈ 𝒫 (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏))∃𝑦𝐾 (𝑥𝑦𝑦𝑠 ∧ (𝐾t 𝑠) ∈ Conn))
5028, 44, 48, 49syl3anc 1372 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ ((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎)))) → ∃𝑠 ∈ 𝒫 (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏))∃𝑦𝐾 (𝑥𝑦𝑦𝑠 ∧ (𝐾t 𝑠) ∈ Conn))
51 simprr1 1222 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ ((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎)))) ∧ ((𝑠 ∈ 𝒫 (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)) ∧ 𝑦𝐾) ∧ (𝑥𝑦𝑦𝑠 ∧ (𝐾t 𝑠) ∈ Conn))) → 𝑥𝑦)
52 cvmliftmo.o . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑𝑂𝑌)
53 cvmliftmoi.g . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → (𝐹𝑀) = (𝐹𝑁))
54 cvmliftmoi.p . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → (𝑀𝑂) = (𝑁𝑂))
55 simplrr 777 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎))) ∧ (((𝑠 ∈ 𝒫 (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)) ∧ 𝑦𝐾) ∧ (𝑥𝑦𝑦𝑠 ∧ (𝐾t 𝑠) ∈ Conn)) ∧ 𝑧𝑦)) → 𝑡 ∈ (𝑆𝑎))
5655adantl 483 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑 ∧ (((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎))) ∧ (((𝑠 ∈ 𝒫 (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)) ∧ 𝑦𝐾) ∧ (𝑥𝑦𝑦𝑠 ∧ (𝐾t 𝑠) ∈ Conn)) ∧ 𝑧𝑦))) → 𝑡 ∈ (𝑆𝑎))
5741adantrr 716 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑 ∧ (((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎))) ∧ (((𝑠 ∈ 𝒫 (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)) ∧ 𝑦𝐾) ∧ (𝑥𝑦𝑦𝑠 ∧ (𝐾t 𝑠) ∈ Conn)) ∧ 𝑧𝑦))) → (𝑏𝑡 (𝑀𝑥) ∈ 𝑏) ∈ 𝑡)
58 simplll 774 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝑠 ∈ 𝒫 (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)) ∧ 𝑦𝐾) ∧ (𝑥𝑦𝑦𝑠 ∧ (𝐾t 𝑠) ∈ Conn)) ∧ 𝑧𝑦) → 𝑠 ∈ 𝒫 (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)))
5958ad2antll 728 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑 ∧ (((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎))) ∧ (((𝑠 ∈ 𝒫 (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)) ∧ 𝑦𝐾) ∧ (𝑥𝑦𝑦𝑠 ∧ (𝐾t 𝑠) ∈ Conn)) ∧ 𝑧𝑦))) → 𝑠 ∈ 𝒫 (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)))
6059elpwid 4574 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑 ∧ (((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎))) ∧ (((𝑠 ∈ 𝒫 (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)) ∧ 𝑦𝐾) ∧ (𝑥𝑦𝑦𝑠 ∧ (𝐾t 𝑠) ∈ Conn)) ∧ 𝑧𝑦))) → 𝑠 ⊆ (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)))
61 simplr3 1218 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝑠 ∈ 𝒫 (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)) ∧ 𝑦𝐾) ∧ (𝑥𝑦𝑦𝑠 ∧ (𝐾t 𝑠) ∈ Conn)) ∧ 𝑧𝑦) → (𝐾t 𝑠) ∈ Conn)
6261ad2antll 728 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑 ∧ (((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎))) ∧ (((𝑠 ∈ 𝒫 (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)) ∧ 𝑦𝐾) ∧ (𝑥𝑦𝑦𝑠 ∧ (𝐾t 𝑠) ∈ Conn)) ∧ 𝑧𝑦))) → (𝐾t 𝑠) ∈ Conn)
63 simplr2 1217 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝑠 ∈ 𝒫 (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)) ∧ 𝑦𝐾) ∧ (𝑥𝑦𝑦𝑠 ∧ (𝐾t 𝑠) ∈ Conn)) ∧ 𝑧𝑦) → 𝑦𝑠)
6463ad2antll 728 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑 ∧ (((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎))) ∧ (((𝑠 ∈ 𝒫 (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)) ∧ 𝑦𝐾) ∧ (𝑥𝑦𝑦𝑠 ∧ (𝐾t 𝑠) ∈ Conn)) ∧ 𝑧𝑦))) → 𝑦𝑠)
65 simprr1 1222 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎))) ∧ ((𝑠 ∈ 𝒫 (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)) ∧ 𝑦𝐾) ∧ (𝑥𝑦𝑦𝑠 ∧ (𝐾t 𝑠) ∈ Conn))) → 𝑥𝑦)
6665adantl 483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑 ∧ (((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎))) ∧ ((𝑠 ∈ 𝒫 (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)) ∧ 𝑦𝐾) ∧ (𝑥𝑦𝑦𝑠 ∧ (𝐾t 𝑠) ∈ Conn)))) → 𝑥𝑦)
6766adantrrr 724 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑 ∧ (((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎))) ∧ (((𝑠 ∈ 𝒫 (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)) ∧ 𝑦𝐾) ∧ (𝑥𝑦𝑦𝑠 ∧ (𝐾t 𝑠) ∈ Conn)) ∧ 𝑧𝑦))) → 𝑥𝑦)
6864, 67sseldd 3950 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑 ∧ (((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎))) ∧ (((𝑠 ∈ 𝒫 (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)) ∧ 𝑦𝐾) ∧ (𝑥𝑦𝑦𝑠 ∧ (𝐾t 𝑠) ∈ Conn)) ∧ 𝑧𝑦))) → 𝑥𝑠)
69 simprrr 781 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑 ∧ (((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎))) ∧ (((𝑠 ∈ 𝒫 (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)) ∧ 𝑦𝐾) ∧ (𝑥𝑦𝑦𝑠 ∧ (𝐾t 𝑠) ∈ Conn)) ∧ 𝑧𝑦))) → 𝑧𝑦)
7064, 69sseldd 3950 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑 ∧ (((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎))) ∧ (((𝑠 ∈ 𝒫 (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)) ∧ 𝑦𝐾) ∧ (𝑥𝑦𝑦𝑠 ∧ (𝐾t 𝑠) ∈ Conn)) ∧ 𝑧𝑦))) → 𝑧𝑠)
7137adantrr 716 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑 ∧ (((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎))) ∧ (((𝑠 ∈ 𝒫 (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)) ∧ 𝑦𝐾) ∧ (𝑥𝑦𝑦𝑠 ∧ (𝐾t 𝑠) ∈ Conn)) ∧ 𝑧𝑦))) → (𝐹‘(𝑀𝑥)) ∈ 𝑎)
723, 2, 13, 11, 27, 52, 1, 7, 53, 54, 23, 56, 57, 60, 62, 68, 68, 70, 71cvmliftmolem1 33915 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑 ∧ (((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎))) ∧ (((𝑠 ∈ 𝒫 (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)) ∧ 𝑦𝐾) ∧ (𝑥𝑦𝑦𝑠 ∧ (𝐾t 𝑠) ∈ Conn)) ∧ 𝑧𝑦))) → (𝑥 ∈ dom (𝑀𝑁) → 𝑧 ∈ dom (𝑀𝑁)))
733, 2, 13, 11, 27, 52, 1, 7, 53, 54, 23, 56, 57, 60, 62, 68, 70, 68, 71cvmliftmolem1 33915 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑 ∧ (((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎))) ∧ (((𝑠 ∈ 𝒫 (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)) ∧ 𝑦𝐾) ∧ (𝑥𝑦𝑦𝑠 ∧ (𝐾t 𝑠) ∈ Conn)) ∧ 𝑧𝑦))) → (𝑧 ∈ dom (𝑀𝑁) → 𝑥 ∈ dom (𝑀𝑁)))
7472, 73impbid 211 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∧ (((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎))) ∧ (((𝑠 ∈ 𝒫 (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)) ∧ 𝑦𝐾) ∧ (𝑥𝑦𝑦𝑠 ∧ (𝐾t 𝑠) ∈ Conn)) ∧ 𝑧𝑦))) → (𝑥 ∈ dom (𝑀𝑁) ↔ 𝑧 ∈ dom (𝑀𝑁)))
7574anassrs 469 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ ((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎)))) ∧ (((𝑠 ∈ 𝒫 (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)) ∧ 𝑦𝐾) ∧ (𝑥𝑦𝑦𝑠 ∧ (𝐾t 𝑠) ∈ Conn)) ∧ 𝑧𝑦)) → (𝑥 ∈ dom (𝑀𝑁) ↔ 𝑧 ∈ dom (𝑀𝑁)))
7675anassrs 469 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ ((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎)))) ∧ ((𝑠 ∈ 𝒫 (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)) ∧ 𝑦𝐾) ∧ (𝑥𝑦𝑦𝑠 ∧ (𝐾t 𝑠) ∈ Conn))) ∧ 𝑧𝑦) → (𝑥 ∈ dom (𝑀𝑁) ↔ 𝑧 ∈ dom (𝑀𝑁)))
7776ralrimiva 3144 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ ((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎)))) ∧ ((𝑠 ∈ 𝒫 (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)) ∧ 𝑦𝐾) ∧ (𝑥𝑦𝑦𝑠 ∧ (𝐾t 𝑠) ∈ Conn))) → ∀𝑧𝑦 (𝑥 ∈ dom (𝑀𝑁) ↔ 𝑧 ∈ dom (𝑀𝑁)))
7851, 77jca 513 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ ((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎)))) ∧ ((𝑠 ∈ 𝒫 (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)) ∧ 𝑦𝐾) ∧ (𝑥𝑦𝑦𝑠 ∧ (𝐾t 𝑠) ∈ Conn))) → (𝑥𝑦 ∧ ∀𝑧𝑦 (𝑥 ∈ dom (𝑀𝑁) ↔ 𝑧 ∈ dom (𝑀𝑁))))
7978expr 458 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ ((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎)))) ∧ (𝑠 ∈ 𝒫 (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)) ∧ 𝑦𝐾)) → ((𝑥𝑦𝑦𝑠 ∧ (𝐾t 𝑠) ∈ Conn) → (𝑥𝑦 ∧ ∀𝑧𝑦 (𝑥 ∈ dom (𝑀𝑁) ↔ 𝑧 ∈ dom (𝑀𝑁)))))
8079anassrs 469 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ ((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎)))) ∧ 𝑠 ∈ 𝒫 (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏))) ∧ 𝑦𝐾) → ((𝑥𝑦𝑦𝑠 ∧ (𝐾t 𝑠) ∈ Conn) → (𝑥𝑦 ∧ ∀𝑧𝑦 (𝑥 ∈ dom (𝑀𝑁) ↔ 𝑧 ∈ dom (𝑀𝑁)))))
8180reximdva 3166 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ ((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎)))) ∧ 𝑠 ∈ 𝒫 (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏))) → (∃𝑦𝐾 (𝑥𝑦𝑦𝑠 ∧ (𝐾t 𝑠) ∈ Conn) → ∃𝑦𝐾 (𝑥𝑦 ∧ ∀𝑧𝑦 (𝑥 ∈ dom (𝑀𝑁) ↔ 𝑧 ∈ dom (𝑀𝑁)))))
8281rexlimdva 3153 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ ((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎)))) → (∃𝑠 ∈ 𝒫 (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏))∃𝑦𝐾 (𝑥𝑦𝑦𝑠 ∧ (𝐾t 𝑠) ∈ Conn) → ∃𝑦𝐾 (𝑥𝑦 ∧ ∀𝑧𝑦 (𝑥 ∈ dom (𝑀𝑁) ↔ 𝑧 ∈ dom (𝑀𝑁)))))
8350, 82mpd 15 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎)))) → ∃𝑦𝐾 (𝑥𝑦 ∧ ∀𝑧𝑦 (𝑥 ∈ dom (𝑀𝑁) ↔ 𝑧 ∈ dom (𝑀𝑁))))
8483anassrs 469 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥𝑌𝑎𝐽)) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎))) → ∃𝑦𝐾 (𝑥𝑦 ∧ ∀𝑧𝑦 (𝑥 ∈ dom (𝑀𝑁) ↔ 𝑧 ∈ dom (𝑀𝑁))))
8584expr 458 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥𝑌𝑎𝐽)) ∧ (𝐹‘(𝑀𝑥)) ∈ 𝑎) → (𝑡 ∈ (𝑆𝑎) → ∃𝑦𝐾 (𝑥𝑦 ∧ ∀𝑧𝑦 (𝑥 ∈ dom (𝑀𝑁) ↔ 𝑧 ∈ dom (𝑀𝑁)))))
8685exlimdv 1937 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥𝑌𝑎𝐽)) ∧ (𝐹‘(𝑀𝑥)) ∈ 𝑎) → (∃𝑡 𝑡 ∈ (𝑆𝑎) → ∃𝑦𝐾 (𝑥𝑦 ∧ ∀𝑧𝑦 (𝑥 ∈ dom (𝑀𝑁) ↔ 𝑧 ∈ dom (𝑀𝑁)))))
8726, 86biimtrid 241 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑥𝑌𝑎𝐽)) ∧ (𝐹‘(𝑀𝑥)) ∈ 𝑎) → ((𝑆𝑎) ≠ ∅ → ∃𝑦𝐾 (𝑥𝑦 ∧ ∀𝑧𝑦 (𝑥 ∈ dom (𝑀𝑁) ↔ 𝑧 ∈ dom (𝑀𝑁)))))
8887expimpd 455 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥𝑌𝑎𝐽)) → (((𝐹‘(𝑀𝑥)) ∈ 𝑎 ∧ (𝑆𝑎) ≠ ∅) → ∃𝑦𝐾 (𝑥𝑦 ∧ ∀𝑧𝑦 (𝑥 ∈ dom (𝑀𝑁) ↔ 𝑧 ∈ dom (𝑀𝑁)))))
8988anassrs 469 . . . . . . . . . . 11 (((𝜑𝑥𝑌) ∧ 𝑎𝐽) → (((𝐹‘(𝑀𝑥)) ∈ 𝑎 ∧ (𝑆𝑎) ≠ ∅) → ∃𝑦𝐾 (𝑥𝑦 ∧ ∀𝑧𝑦 (𝑥 ∈ dom (𝑀𝑁) ↔ 𝑧 ∈ dom (𝑀𝑁)))))
9089rexlimdva 3153 . . . . . . . . . 10 ((𝜑𝑥𝑌) → (∃𝑎𝐽 ((𝐹‘(𝑀𝑥)) ∈ 𝑎 ∧ (𝑆𝑎) ≠ ∅) → ∃𝑦𝐾 (𝑥𝑦 ∧ ∀𝑧𝑦 (𝑥 ∈ dom (𝑀𝑁) ↔ 𝑧 ∈ dom (𝑀𝑁)))))
9125, 90mpd 15 . . . . . . . . 9 ((𝜑𝑥𝑌) → ∃𝑦𝐾 (𝑥𝑦 ∧ ∀𝑧𝑦 (𝑥 ∈ dom (𝑀𝑁) ↔ 𝑧 ∈ dom (𝑀𝑁))))
9291ralrimiva 3144 . . . . . . . 8 (𝜑 → ∀𝑥𝑌𝑦𝐾 (𝑥𝑦 ∧ ∀𝑧𝑦 (𝑥 ∈ dom (𝑀𝑁) ↔ 𝑧 ∈ dom (𝑀𝑁))))
93 conntop 22784 . . . . . . . . . 10 (𝐾 ∈ Conn → 𝐾 ∈ Top)
9411, 93syl 17 . . . . . . . . 9 (𝜑𝐾 ∈ Top)
95 fndmin 7000 . . . . . . . . . . 11 ((𝑀 Fn 𝑌𝑁 Fn 𝑌) → dom (𝑀𝑁) = {𝑥𝑌 ∣ (𝑀𝑥) = (𝑁𝑥)})
966, 10, 95syl2anc 585 . . . . . . . . . 10 (𝜑 → dom (𝑀𝑁) = {𝑥𝑌 ∣ (𝑀𝑥) = (𝑁𝑥)})
97 ssrab2 4042 . . . . . . . . . 10 {𝑥𝑌 ∣ (𝑀𝑥) = (𝑁𝑥)} ⊆ 𝑌
9896, 97eqsstrdi 4003 . . . . . . . . 9 (𝜑 → dom (𝑀𝑁) ⊆ 𝑌)
992isclo 22454 . . . . . . . . 9 ((𝐾 ∈ Top ∧ dom (𝑀𝑁) ⊆ 𝑌) → (dom (𝑀𝑁) ∈ (𝐾 ∩ (Clsd‘𝐾)) ↔ ∀𝑥𝑌𝑦𝐾 (𝑥𝑦 ∧ ∀𝑧𝑦 (𝑥 ∈ dom (𝑀𝑁) ↔ 𝑧 ∈ dom (𝑀𝑁)))))
10094, 98, 99syl2anc 585 . . . . . . . 8 (𝜑 → (dom (𝑀𝑁) ∈ (𝐾 ∩ (Clsd‘𝐾)) ↔ ∀𝑥𝑌𝑦𝐾 (𝑥𝑦 ∧ ∀𝑧𝑦 (𝑥 ∈ dom (𝑀𝑁) ↔ 𝑧 ∈ dom (𝑀𝑁)))))
10192, 100mpbird 257 . . . . . . 7 (𝜑 → dom (𝑀𝑁) ∈ (𝐾 ∩ (Clsd‘𝐾)))
10212, 101sselid 3947 . . . . . 6 (𝜑 → dom (𝑀𝑁) ∈ 𝐾)
103 fveq2 6847 . . . . . . . . . . 11 (𝑥 = 𝑂 → (𝑀𝑥) = (𝑀𝑂))
104 fveq2 6847 . . . . . . . . . . 11 (𝑥 = 𝑂 → (𝑁𝑥) = (𝑁𝑂))
105103, 104eqeq12d 2753 . . . . . . . . . 10 (𝑥 = 𝑂 → ((𝑀𝑥) = (𝑁𝑥) ↔ (𝑀𝑂) = (𝑁𝑂)))
106105elrab 3650 . . . . . . . . 9 (𝑂 ∈ {𝑥𝑌 ∣ (𝑀𝑥) = (𝑁𝑥)} ↔ (𝑂𝑌 ∧ (𝑀𝑂) = (𝑁𝑂)))
10752, 54, 106sylanbrc 584 . . . . . . . 8 (𝜑𝑂 ∈ {𝑥𝑌 ∣ (𝑀𝑥) = (𝑁𝑥)})
108107, 96eleqtrrd 2841 . . . . . . 7 (𝜑𝑂 ∈ dom (𝑀𝑁))
109108ne0d 4300 . . . . . 6 (𝜑 → dom (𝑀𝑁) ≠ ∅)
110 inss2 4194 . . . . . . 7 (𝐾 ∩ (Clsd‘𝐾)) ⊆ (Clsd‘𝐾)
111110, 101sselid 3947 . . . . . 6 (𝜑 → dom (𝑀𝑁) ∈ (Clsd‘𝐾))
1122, 11, 102, 109, 111connclo 22782 . . . . 5 (𝜑 → dom (𝑀𝑁) = 𝑌)
113112, 96eqtr3d 2779 . . . 4 (𝜑𝑌 = {𝑥𝑌 ∣ (𝑀𝑥) = (𝑁𝑥)})
114 rabid2 3439 . . . 4 (𝑌 = {𝑥𝑌 ∣ (𝑀𝑥) = (𝑁𝑥)} ↔ ∀𝑥𝑌 (𝑀𝑥) = (𝑁𝑥))
115113, 114sylib 217 . . 3 (𝜑 → ∀𝑥𝑌 (𝑀𝑥) = (𝑁𝑥))
116115r19.21bi 3237 . 2 ((𝜑𝑥𝑌) → (𝑀𝑥) = (𝑁𝑥))
1176, 10, 116eqfnfvd 6990 1 (𝜑𝑀 = 𝑁)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 397  w3a 1088   = wceq 1542  wex 1782  wcel 2107  wne 2944  wral 3065  wrex 3074  {crab 3410  cdif 3912  cin 3914  wss 3915  c0 4287  𝒫 cpw 4565  {csn 4591   cuni 4870  cmpt 5193  ccnv 5637  dom cdm 5638  cres 5640  cima 5641  ccom 5642   Fn wfn 6496  wf 6497  cfv 6501  crio 7317  (class class class)co 7362  t crest 17309  Topctop 22258  Clsdccld 22383   Cn ccn 22591  Conncconn 22778  𝑛-Locally cnlly 22832  Homeochmeo 23120   CovMap ccvm 33889
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-rep 5247  ax-sep 5261  ax-nul 5268  ax-pow 5325  ax-pr 5389  ax-un 7677
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ne 2945  df-ral 3066  df-rex 3075  df-rmo 3356  df-reu 3357  df-rab 3411  df-v 3450  df-sbc 3745  df-csb 3861  df-dif 3918  df-un 3920  df-in 3922  df-ss 3932  df-pss 3934  df-nul 4288  df-if 4492  df-pw 4567  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-int 4913  df-iun 4961  df-br 5111  df-opab 5173  df-mpt 5194  df-tr 5228  df-id 5536  df-eprel 5542  df-po 5550  df-so 5551  df-fr 5593  df-we 5595  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-ord 6325  df-on 6326  df-lim 6327  df-suc 6328  df-iota 6453  df-fun 6503  df-fn 6504  df-f 6505  df-f1 6506  df-fo 6507  df-f1o 6508  df-fv 6509  df-riota 7318  df-ov 7365  df-oprab 7366  df-mpo 7367  df-om 7808  df-1st 7926  df-2nd 7927  df-map 8774  df-en 8891  df-fin 8894  df-fi 9354  df-rest 17311  df-topgen 17332  df-top 22259  df-topon 22276  df-bases 22312  df-cld 22386  df-nei 22465  df-cn 22594  df-conn 22779  df-nlly 22834  df-hmeo 23122  df-cvm 33890
This theorem is referenced by:  cvmliftmoi  33917
  Copyright terms: Public domain W3C validator