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 34828
Description: Lemma for cvmliftmo 34830. (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 23137 . . 3 (𝑀 ∈ (𝐾 Cn 𝐶) → 𝑀:𝑌𝐵)
5 ffn 6716 . . 3 (𝑀:𝑌𝐵𝑀 Fn 𝑌)
61, 4, 53syl 18 . 2 (𝜑𝑀 Fn 𝑌)
7 cvmliftmoi.n . . 3 (𝜑𝑁 ∈ (𝐾 Cn 𝐶))
82, 3cnf 23137 . . 3 (𝑁 ∈ (𝐾 Cn 𝐶) → 𝑁:𝑌𝐵)
9 ffn 6716 . . 3 (𝑁:𝑌𝐵𝑁 Fn 𝑌)
107, 8, 93syl 18 . 2 (𝜑𝑁 Fn 𝑌)
11 cvmliftmo.k . . . . . 6 (𝜑𝐾 ∈ Conn)
12 inss1 4224 . . . . . . 7 (𝐾 ∩ (Clsd‘𝐾)) ⊆ 𝐾
13 cvmliftmo.f . . . . . . . . . . . 12 (𝜑𝐹 ∈ (𝐶 CovMap 𝐽))
1413adantr 480 . . . . . . . . . . 11 ((𝜑𝑥𝑌) → 𝐹 ∈ (𝐶 CovMap 𝐽))
151, 4syl 17 . . . . . . . . . . . . 13 (𝜑𝑀:𝑌𝐵)
1615ffvelcdmda 7088 . . . . . . . . . . . 12 ((𝜑𝑥𝑌) → (𝑀𝑥) ∈ 𝐵)
17 cvmcn 34808 . . . . . . . . . . . . . 14 (𝐹 ∈ (𝐶 CovMap 𝐽) → 𝐹 ∈ (𝐶 Cn 𝐽))
18 eqid 2727 . . . . . . . . . . . . . . 15 𝐽 = 𝐽
193, 18cnf 23137 . . . . . . . . . . . . . 14 (𝐹 ∈ (𝐶 Cn 𝐽) → 𝐹:𝐵 𝐽)
2013, 17, 193syl 18 . . . . . . . . . . . . 13 (𝜑𝐹:𝐵 𝐽)
2120ffvelcdmda 7088 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑀𝑥) ∈ 𝐵) → (𝐹‘(𝑀𝑥)) ∈ 𝐽)
2216, 21syldan 590 . . . . . . . . . . 11 ((𝜑𝑥𝑌) → (𝐹‘(𝑀𝑥)) ∈ 𝐽)
23 cvmliftmolem.1 . . . . . . . . . . . 12 𝑆 = (𝑘𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ ( 𝑠 = (𝐹𝑘) ∧ ∀𝑢𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢𝑣) = ∅ ∧ (𝐹𝑢) ∈ ((𝐶t 𝑢)Homeo(𝐽t 𝑘))))})
2423, 18cvmcov 34809 . . . . . . . . . . 11 ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ (𝐹‘(𝑀𝑥)) ∈ 𝐽) → ∃𝑎𝐽 ((𝐹‘(𝑀𝑥)) ∈ 𝑎 ∧ (𝑆𝑎) ≠ ∅))
2514, 22, 24syl2anc 583 . . . . . . . . . 10 ((𝜑𝑥𝑌) → ∃𝑎𝐽 ((𝐹‘(𝑀𝑥)) ∈ 𝑎 ∧ (𝑆𝑎) ≠ ∅))
26 n0 4342 . . . . . . . . . . . . . 14 ((𝑆𝑎) ≠ ∅ ↔ ∃𝑡 𝑡 ∈ (𝑆𝑎))
27 cvmliftmo.l . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐾 ∈ 𝑛-Locally Conn)
2827adantr 480 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ ((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎)))) → 𝐾 ∈ 𝑛-Locally Conn)
291adantr 480 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ ((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎)))) → 𝑀 ∈ (𝐾 Cn 𝐶))
30 simprrr 781 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ ((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎)))) → 𝑡 ∈ (𝑆𝑎))
3123cvmsss 34813 . . . . . . . . . . . . . . . . . . . . . 22 (𝑡 ∈ (𝑆𝑎) → 𝑡𝐶)
3230, 31syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ ((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎)))) → 𝑡𝐶)
3313adantr 480 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ ((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎)))) → 𝐹 ∈ (𝐶 CovMap 𝐽))
3415adantr 480 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ ((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎)))) → 𝑀:𝑌𝐵)
35 simprll 778 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ ((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎)))) → 𝑥𝑌)
3634, 35ffvelcdmd 7089 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ ((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎)))) → (𝑀𝑥) ∈ 𝐵)
37 simprrl 780 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ ((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎)))) → (𝐹‘(𝑀𝑥)) ∈ 𝑎)
38 eqid 2727 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑏𝑡 (𝑀𝑥) ∈ 𝑏) = (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)
3923, 3, 38cvmsiota 34823 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ (𝑡 ∈ (𝑆𝑎) ∧ (𝑀𝑥) ∈ 𝐵 ∧ (𝐹‘(𝑀𝑥)) ∈ 𝑎)) → ((𝑏𝑡 (𝑀𝑥) ∈ 𝑏) ∈ 𝑡 ∧ (𝑀𝑥) ∈ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)))
4033, 30, 36, 37, 39syl13anc 1370 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ ((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎)))) → ((𝑏𝑡 (𝑀𝑥) ∈ 𝑏) ∈ 𝑡 ∧ (𝑀𝑥) ∈ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)))
4140simpld 494 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ ((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎)))) → (𝑏𝑡 (𝑀𝑥) ∈ 𝑏) ∈ 𝑡)
4232, 41sseldd 3979 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ ((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎)))) → (𝑏𝑡 (𝑀𝑥) ∈ 𝑏) ∈ 𝐶)
43 cnima 23156 . . . . . . . . . . . . . . . . . . . 20 ((𝑀 ∈ (𝐾 Cn 𝐶) ∧ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏) ∈ 𝐶) → (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)) ∈ 𝐾)
4429, 42, 43syl2anc 583 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ ((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎)))) → (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)) ∈ 𝐾)
4540simprd 495 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ ((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎)))) → (𝑀𝑥) ∈ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏))
46 elpreima 7061 . . . . . . . . . . . . . . . . . . . . 21 (𝑀 Fn 𝑌 → (𝑥 ∈ (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)) ↔ (𝑥𝑌 ∧ (𝑀𝑥) ∈ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏))))
4734, 5, 463syl 18 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ ((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎)))) → (𝑥 ∈ (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)) ↔ (𝑥𝑌 ∧ (𝑀𝑥) ∈ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏))))
4835, 45, 47mpbir2and 712 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ ((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎)))) → 𝑥 ∈ (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)))
49 nlly2i 23367 . . . . . . . . . . . . . . . . . . 19 ((𝐾 ∈ 𝑛-Locally Conn ∧ (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)) ∈ 𝐾𝑥 ∈ (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏))) → ∃𝑠 ∈ 𝒫 (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏))∃𝑦𝐾 (𝑥𝑦𝑦𝑠 ∧ (𝐾t 𝑠) ∈ Conn))
5028, 44, 48, 49syl3anc 1369 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ ((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎)))) → ∃𝑠 ∈ 𝒫 (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏))∃𝑦𝐾 (𝑥𝑦𝑦𝑠 ∧ (𝐾t 𝑠) ∈ Conn))
51 simprr1 1219 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ ((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎)))) ∧ ((𝑠 ∈ 𝒫 (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)) ∧ 𝑦𝐾) ∧ (𝑥𝑦𝑦𝑠 ∧ (𝐾t 𝑠) ∈ Conn))) → 𝑥𝑦)
52 cvmliftmo.o . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑𝑂𝑌)
53 cvmliftmoi.g . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → (𝐹𝑀) = (𝐹𝑁))
54 cvmliftmoi.p . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → (𝑀𝑂) = (𝑁𝑂))
55 simplrr 777 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎))) ∧ (((𝑠 ∈ 𝒫 (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)) ∧ 𝑦𝐾) ∧ (𝑥𝑦𝑦𝑠 ∧ (𝐾t 𝑠) ∈ Conn)) ∧ 𝑧𝑦)) → 𝑡 ∈ (𝑆𝑎))
5655adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑 ∧ (((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎))) ∧ (((𝑠 ∈ 𝒫 (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)) ∧ 𝑦𝐾) ∧ (𝑥𝑦𝑦𝑠 ∧ (𝐾t 𝑠) ∈ Conn)) ∧ 𝑧𝑦))) → 𝑡 ∈ (𝑆𝑎))
5741adantrr 716 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑 ∧ (((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎))) ∧ (((𝑠 ∈ 𝒫 (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)) ∧ 𝑦𝐾) ∧ (𝑥𝑦𝑦𝑠 ∧ (𝐾t 𝑠) ∈ Conn)) ∧ 𝑧𝑦))) → (𝑏𝑡 (𝑀𝑥) ∈ 𝑏) ∈ 𝑡)
58 simplll 774 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝑠 ∈ 𝒫 (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)) ∧ 𝑦𝐾) ∧ (𝑥𝑦𝑦𝑠 ∧ (𝐾t 𝑠) ∈ Conn)) ∧ 𝑧𝑦) → 𝑠 ∈ 𝒫 (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)))
5958ad2antll 728 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑 ∧ (((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎))) ∧ (((𝑠 ∈ 𝒫 (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)) ∧ 𝑦𝐾) ∧ (𝑥𝑦𝑦𝑠 ∧ (𝐾t 𝑠) ∈ Conn)) ∧ 𝑧𝑦))) → 𝑠 ∈ 𝒫 (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)))
6059elpwid 4607 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑 ∧ (((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎))) ∧ (((𝑠 ∈ 𝒫 (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)) ∧ 𝑦𝐾) ∧ (𝑥𝑦𝑦𝑠 ∧ (𝐾t 𝑠) ∈ Conn)) ∧ 𝑧𝑦))) → 𝑠 ⊆ (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)))
61 simplr3 1215 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝑠 ∈ 𝒫 (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)) ∧ 𝑦𝐾) ∧ (𝑥𝑦𝑦𝑠 ∧ (𝐾t 𝑠) ∈ Conn)) ∧ 𝑧𝑦) → (𝐾t 𝑠) ∈ Conn)
6261ad2antll 728 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑 ∧ (((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎))) ∧ (((𝑠 ∈ 𝒫 (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)) ∧ 𝑦𝐾) ∧ (𝑥𝑦𝑦𝑠 ∧ (𝐾t 𝑠) ∈ Conn)) ∧ 𝑧𝑦))) → (𝐾t 𝑠) ∈ Conn)
63 simplr2 1214 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝑠 ∈ 𝒫 (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)) ∧ 𝑦𝐾) ∧ (𝑥𝑦𝑦𝑠 ∧ (𝐾t 𝑠) ∈ Conn)) ∧ 𝑧𝑦) → 𝑦𝑠)
6463ad2antll 728 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑 ∧ (((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎))) ∧ (((𝑠 ∈ 𝒫 (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)) ∧ 𝑦𝐾) ∧ (𝑥𝑦𝑦𝑠 ∧ (𝐾t 𝑠) ∈ Conn)) ∧ 𝑧𝑦))) → 𝑦𝑠)
65 simprr1 1219 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎))) ∧ ((𝑠 ∈ 𝒫 (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)) ∧ 𝑦𝐾) ∧ (𝑥𝑦𝑦𝑠 ∧ (𝐾t 𝑠) ∈ Conn))) → 𝑥𝑦)
6665adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑 ∧ (((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎))) ∧ ((𝑠 ∈ 𝒫 (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)) ∧ 𝑦𝐾) ∧ (𝑥𝑦𝑦𝑠 ∧ (𝐾t 𝑠) ∈ Conn)))) → 𝑥𝑦)
6766adantrrr 724 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑 ∧ (((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎))) ∧ (((𝑠 ∈ 𝒫 (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)) ∧ 𝑦𝐾) ∧ (𝑥𝑦𝑦𝑠 ∧ (𝐾t 𝑠) ∈ Conn)) ∧ 𝑧𝑦))) → 𝑥𝑦)
6864, 67sseldd 3979 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑 ∧ (((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎))) ∧ (((𝑠 ∈ 𝒫 (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)) ∧ 𝑦𝐾) ∧ (𝑥𝑦𝑦𝑠 ∧ (𝐾t 𝑠) ∈ Conn)) ∧ 𝑧𝑦))) → 𝑥𝑠)
69 simprrr 781 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑 ∧ (((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎))) ∧ (((𝑠 ∈ 𝒫 (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)) ∧ 𝑦𝐾) ∧ (𝑥𝑦𝑦𝑠 ∧ (𝐾t 𝑠) ∈ Conn)) ∧ 𝑧𝑦))) → 𝑧𝑦)
7064, 69sseldd 3979 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 34827 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑 ∧ (((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎))) ∧ (((𝑠 ∈ 𝒫 (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)) ∧ 𝑦𝐾) ∧ (𝑥𝑦𝑦𝑠 ∧ (𝐾t 𝑠) ∈ Conn)) ∧ 𝑧𝑦))) → (𝑥 ∈ dom (𝑀𝑁) → 𝑧 ∈ dom (𝑀𝑁)))
733, 2, 13, 11, 27, 52, 1, 7, 53, 54, 23, 56, 57, 60, 62, 68, 70, 68, 71cvmliftmolem1 34827 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑 ∧ (((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎))) ∧ (((𝑠 ∈ 𝒫 (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)) ∧ 𝑦𝐾) ∧ (𝑥𝑦𝑦𝑠 ∧ (𝐾t 𝑠) ∈ Conn)) ∧ 𝑧𝑦))) → (𝑧 ∈ dom (𝑀𝑁) → 𝑥 ∈ dom (𝑀𝑁)))
7472, 73impbid 211 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∧ (((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎))) ∧ (((𝑠 ∈ 𝒫 (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)) ∧ 𝑦𝐾) ∧ (𝑥𝑦𝑦𝑠 ∧ (𝐾t 𝑠) ∈ Conn)) ∧ 𝑧𝑦))) → (𝑥 ∈ dom (𝑀𝑁) ↔ 𝑧 ∈ dom (𝑀𝑁)))
7574anassrs 467 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ ((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎)))) ∧ (((𝑠 ∈ 𝒫 (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)) ∧ 𝑦𝐾) ∧ (𝑥𝑦𝑦𝑠 ∧ (𝐾t 𝑠) ∈ Conn)) ∧ 𝑧𝑦)) → (𝑥 ∈ dom (𝑀𝑁) ↔ 𝑧 ∈ dom (𝑀𝑁)))
7675anassrs 467 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ ((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎)))) ∧ ((𝑠 ∈ 𝒫 (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)) ∧ 𝑦𝐾) ∧ (𝑥𝑦𝑦𝑠 ∧ (𝐾t 𝑠) ∈ Conn))) ∧ 𝑧𝑦) → (𝑥 ∈ dom (𝑀𝑁) ↔ 𝑧 ∈ dom (𝑀𝑁)))
7776ralrimiva 3141 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ ((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎)))) ∧ ((𝑠 ∈ 𝒫 (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)) ∧ 𝑦𝐾) ∧ (𝑥𝑦𝑦𝑠 ∧ (𝐾t 𝑠) ∈ Conn))) → ∀𝑧𝑦 (𝑥 ∈ dom (𝑀𝑁) ↔ 𝑧 ∈ dom (𝑀𝑁)))
7851, 77jca 511 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ ((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎)))) ∧ ((𝑠 ∈ 𝒫 (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)) ∧ 𝑦𝐾) ∧ (𝑥𝑦𝑦𝑠 ∧ (𝐾t 𝑠) ∈ Conn))) → (𝑥𝑦 ∧ ∀𝑧𝑦 (𝑥 ∈ dom (𝑀𝑁) ↔ 𝑧 ∈ dom (𝑀𝑁))))
7978expr 456 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ ((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎)))) ∧ (𝑠 ∈ 𝒫 (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)) ∧ 𝑦𝐾)) → ((𝑥𝑦𝑦𝑠 ∧ (𝐾t 𝑠) ∈ Conn) → (𝑥𝑦 ∧ ∀𝑧𝑦 (𝑥 ∈ dom (𝑀𝑁) ↔ 𝑧 ∈ dom (𝑀𝑁)))))
8079anassrs 467 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ ((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎)))) ∧ 𝑠 ∈ 𝒫 (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏))) ∧ 𝑦𝐾) → ((𝑥𝑦𝑦𝑠 ∧ (𝐾t 𝑠) ∈ Conn) → (𝑥𝑦 ∧ ∀𝑧𝑦 (𝑥 ∈ dom (𝑀𝑁) ↔ 𝑧 ∈ dom (𝑀𝑁)))))
8180reximdva 3163 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ ((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎)))) ∧ 𝑠 ∈ 𝒫 (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏))) → (∃𝑦𝐾 (𝑥𝑦𝑦𝑠 ∧ (𝐾t 𝑠) ∈ Conn) → ∃𝑦𝐾 (𝑥𝑦 ∧ ∀𝑧𝑦 (𝑥 ∈ dom (𝑀𝑁) ↔ 𝑧 ∈ dom (𝑀𝑁)))))
8281rexlimdva 3150 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ ((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎)))) → (∃𝑠 ∈ 𝒫 (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏))∃𝑦𝐾 (𝑥𝑦𝑦𝑠 ∧ (𝐾t 𝑠) ∈ Conn) → ∃𝑦𝐾 (𝑥𝑦 ∧ ∀𝑧𝑦 (𝑥 ∈ dom (𝑀𝑁) ↔ 𝑧 ∈ dom (𝑀𝑁)))))
8350, 82mpd 15 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎)))) → ∃𝑦𝐾 (𝑥𝑦 ∧ ∀𝑧𝑦 (𝑥 ∈ dom (𝑀𝑁) ↔ 𝑧 ∈ dom (𝑀𝑁))))
8483anassrs 467 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥𝑌𝑎𝐽)) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎))) → ∃𝑦𝐾 (𝑥𝑦 ∧ ∀𝑧𝑦 (𝑥 ∈ dom (𝑀𝑁) ↔ 𝑧 ∈ dom (𝑀𝑁))))
8584expr 456 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥𝑌𝑎𝐽)) ∧ (𝐹‘(𝑀𝑥)) ∈ 𝑎) → (𝑡 ∈ (𝑆𝑎) → ∃𝑦𝐾 (𝑥𝑦 ∧ ∀𝑧𝑦 (𝑥 ∈ dom (𝑀𝑁) ↔ 𝑧 ∈ dom (𝑀𝑁)))))
8685exlimdv 1929 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥𝑌𝑎𝐽)) ∧ (𝐹‘(𝑀𝑥)) ∈ 𝑎) → (∃𝑡 𝑡 ∈ (𝑆𝑎) → ∃𝑦𝐾 (𝑥𝑦 ∧ ∀𝑧𝑦 (𝑥 ∈ dom (𝑀𝑁) ↔ 𝑧 ∈ dom (𝑀𝑁)))))
8726, 86biimtrid 241 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑥𝑌𝑎𝐽)) ∧ (𝐹‘(𝑀𝑥)) ∈ 𝑎) → ((𝑆𝑎) ≠ ∅ → ∃𝑦𝐾 (𝑥𝑦 ∧ ∀𝑧𝑦 (𝑥 ∈ dom (𝑀𝑁) ↔ 𝑧 ∈ dom (𝑀𝑁)))))
8887expimpd 453 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥𝑌𝑎𝐽)) → (((𝐹‘(𝑀𝑥)) ∈ 𝑎 ∧ (𝑆𝑎) ≠ ∅) → ∃𝑦𝐾 (𝑥𝑦 ∧ ∀𝑧𝑦 (𝑥 ∈ dom (𝑀𝑁) ↔ 𝑧 ∈ dom (𝑀𝑁)))))
8988anassrs 467 . . . . . . . . . . 11 (((𝜑𝑥𝑌) ∧ 𝑎𝐽) → (((𝐹‘(𝑀𝑥)) ∈ 𝑎 ∧ (𝑆𝑎) ≠ ∅) → ∃𝑦𝐾 (𝑥𝑦 ∧ ∀𝑧𝑦 (𝑥 ∈ dom (𝑀𝑁) ↔ 𝑧 ∈ dom (𝑀𝑁)))))
9089rexlimdva 3150 . . . . . . . . . 10 ((𝜑𝑥𝑌) → (∃𝑎𝐽 ((𝐹‘(𝑀𝑥)) ∈ 𝑎 ∧ (𝑆𝑎) ≠ ∅) → ∃𝑦𝐾 (𝑥𝑦 ∧ ∀𝑧𝑦 (𝑥 ∈ dom (𝑀𝑁) ↔ 𝑧 ∈ dom (𝑀𝑁)))))
9125, 90mpd 15 . . . . . . . . 9 ((𝜑𝑥𝑌) → ∃𝑦𝐾 (𝑥𝑦 ∧ ∀𝑧𝑦 (𝑥 ∈ dom (𝑀𝑁) ↔ 𝑧 ∈ dom (𝑀𝑁))))
9291ralrimiva 3141 . . . . . . . 8 (𝜑 → ∀𝑥𝑌𝑦𝐾 (𝑥𝑦 ∧ ∀𝑧𝑦 (𝑥 ∈ dom (𝑀𝑁) ↔ 𝑧 ∈ dom (𝑀𝑁))))
93 conntop 23308 . . . . . . . . . 10 (𝐾 ∈ Conn → 𝐾 ∈ Top)
9411, 93syl 17 . . . . . . . . 9 (𝜑𝐾 ∈ Top)
95 fndmin 7048 . . . . . . . . . . 11 ((𝑀 Fn 𝑌𝑁 Fn 𝑌) → dom (𝑀𝑁) = {𝑥𝑌 ∣ (𝑀𝑥) = (𝑁𝑥)})
966, 10, 95syl2anc 583 . . . . . . . . . 10 (𝜑 → dom (𝑀𝑁) = {𝑥𝑌 ∣ (𝑀𝑥) = (𝑁𝑥)})
97 ssrab2 4073 . . . . . . . . . 10 {𝑥𝑌 ∣ (𝑀𝑥) = (𝑁𝑥)} ⊆ 𝑌
9896, 97eqsstrdi 4032 . . . . . . . . 9 (𝜑 → dom (𝑀𝑁) ⊆ 𝑌)
992isclo 22978 . . . . . . . . 9 ((𝐾 ∈ Top ∧ dom (𝑀𝑁) ⊆ 𝑌) → (dom (𝑀𝑁) ∈ (𝐾 ∩ (Clsd‘𝐾)) ↔ ∀𝑥𝑌𝑦𝐾 (𝑥𝑦 ∧ ∀𝑧𝑦 (𝑥 ∈ dom (𝑀𝑁) ↔ 𝑧 ∈ dom (𝑀𝑁)))))
10094, 98, 99syl2anc 583 . . . . . . . 8 (𝜑 → (dom (𝑀𝑁) ∈ (𝐾 ∩ (Clsd‘𝐾)) ↔ ∀𝑥𝑌𝑦𝐾 (𝑥𝑦 ∧ ∀𝑧𝑦 (𝑥 ∈ dom (𝑀𝑁) ↔ 𝑧 ∈ dom (𝑀𝑁)))))
10192, 100mpbird 257 . . . . . . 7 (𝜑 → dom (𝑀𝑁) ∈ (𝐾 ∩ (Clsd‘𝐾)))
10212, 101sselid 3976 . . . . . 6 (𝜑 → dom (𝑀𝑁) ∈ 𝐾)
103 fveq2 6891 . . . . . . . . . . 11 (𝑥 = 𝑂 → (𝑀𝑥) = (𝑀𝑂))
104 fveq2 6891 . . . . . . . . . . 11 (𝑥 = 𝑂 → (𝑁𝑥) = (𝑁𝑂))
105103, 104eqeq12d 2743 . . . . . . . . . 10 (𝑥 = 𝑂 → ((𝑀𝑥) = (𝑁𝑥) ↔ (𝑀𝑂) = (𝑁𝑂)))
106105elrab 3680 . . . . . . . . 9 (𝑂 ∈ {𝑥𝑌 ∣ (𝑀𝑥) = (𝑁𝑥)} ↔ (𝑂𝑌 ∧ (𝑀𝑂) = (𝑁𝑂)))
10752, 54, 106sylanbrc 582 . . . . . . . 8 (𝜑𝑂 ∈ {𝑥𝑌 ∣ (𝑀𝑥) = (𝑁𝑥)})
108107, 96eleqtrrd 2831 . . . . . . 7 (𝜑𝑂 ∈ dom (𝑀𝑁))
109108ne0d 4331 . . . . . 6 (𝜑 → dom (𝑀𝑁) ≠ ∅)
110 inss2 4225 . . . . . . 7 (𝐾 ∩ (Clsd‘𝐾)) ⊆ (Clsd‘𝐾)
111110, 101sselid 3976 . . . . . 6 (𝜑 → dom (𝑀𝑁) ∈ (Clsd‘𝐾))
1122, 11, 102, 109, 111connclo 23306 . . . . 5 (𝜑 → dom (𝑀𝑁) = 𝑌)
113112, 96eqtr3d 2769 . . . 4 (𝜑𝑌 = {𝑥𝑌 ∣ (𝑀𝑥) = (𝑁𝑥)})
114 rabid2 3459 . . . 4 (𝑌 = {𝑥𝑌 ∣ (𝑀𝑥) = (𝑁𝑥)} ↔ ∀𝑥𝑌 (𝑀𝑥) = (𝑁𝑥))
115113, 114sylib 217 . . 3 (𝜑 → ∀𝑥𝑌 (𝑀𝑥) = (𝑁𝑥))
116115r19.21bi 3243 . 2 ((𝜑𝑥𝑌) → (𝑀𝑥) = (𝑁𝑥))
1176, 10, 116eqfnfvd 7037 1 (𝜑𝑀 = 𝑁)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 395  w3a 1085   = wceq 1534  wex 1774  wcel 2099  wne 2935  wral 3056  wrex 3065  {crab 3427  cdif 3941  cin 3943  wss 3944  c0 4318  𝒫 cpw 4598  {csn 4624   cuni 4903  cmpt 5225  ccnv 5671  dom cdm 5672  cres 5674  cima 5675  ccom 5676   Fn wfn 6537  wf 6538  cfv 6542  crio 7369  (class class class)co 7414  t crest 17393  Topctop 22782  Clsdccld 22907   Cn ccn 23115  Conncconn 23302  𝑛-Locally cnlly 23356  Homeochmeo 23644   CovMap ccvm 34801
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2164  ax-ext 2698  ax-rep 5279  ax-sep 5293  ax-nul 5300  ax-pow 5359  ax-pr 5423  ax-un 7734
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3or 1086  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2705  df-cleq 2719  df-clel 2805  df-nfc 2880  df-ne 2936  df-ral 3057  df-rex 3066  df-rmo 3371  df-reu 3372  df-rab 3428  df-v 3471  df-sbc 3775  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-pss 3963  df-nul 4319  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-op 4631  df-uni 4904  df-int 4945  df-iun 4993  df-br 5143  df-opab 5205  df-mpt 5226  df-tr 5260  df-id 5570  df-eprel 5576  df-po 5584  df-so 5585  df-fr 5627  df-we 5629  df-xp 5678  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-rn 5683  df-res 5684  df-ima 5685  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-riota 7370  df-ov 7417  df-oprab 7418  df-mpo 7419  df-om 7865  df-1st 7987  df-2nd 7988  df-map 8838  df-en 8956  df-fin 8959  df-fi 9426  df-rest 17395  df-topgen 17416  df-top 22783  df-topon 22800  df-bases 22836  df-cld 22910  df-nei 22989  df-cn 23118  df-conn 23303  df-nlly 23358  df-hmeo 23646  df-cvm 34802
This theorem is referenced by:  cvmliftmoi  34829
  Copyright terms: Public domain W3C validator