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 34737
Description: Lemma for cvmliftmo 34739. (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 23070 . . 3 (𝑀 ∈ (𝐾 Cn 𝐶) → 𝑀:𝑌𝐵)
5 ffn 6717 . . 3 (𝑀:𝑌𝐵𝑀 Fn 𝑌)
61, 4, 53syl 18 . 2 (𝜑𝑀 Fn 𝑌)
7 cvmliftmoi.n . . 3 (𝜑𝑁 ∈ (𝐾 Cn 𝐶))
82, 3cnf 23070 . . 3 (𝑁 ∈ (𝐾 Cn 𝐶) → 𝑁:𝑌𝐵)
9 ffn 6717 . . 3 (𝑁:𝑌𝐵𝑁 Fn 𝑌)
107, 8, 93syl 18 . 2 (𝜑𝑁 Fn 𝑌)
11 cvmliftmo.k . . . . . 6 (𝜑𝐾 ∈ Conn)
12 inss1 4228 . . . . . . 7 (𝐾 ∩ (Clsd‘𝐾)) ⊆ 𝐾
13 cvmliftmo.f . . . . . . . . . . . 12 (𝜑𝐹 ∈ (𝐶 CovMap 𝐽))
1413adantr 480 . . . . . . . . . . 11 ((𝜑𝑥𝑌) → 𝐹 ∈ (𝐶 CovMap 𝐽))
151, 4syl 17 . . . . . . . . . . . . 13 (𝜑𝑀:𝑌𝐵)
1615ffvelcdmda 7086 . . . . . . . . . . . 12 ((𝜑𝑥𝑌) → (𝑀𝑥) ∈ 𝐵)
17 cvmcn 34717 . . . . . . . . . . . . . 14 (𝐹 ∈ (𝐶 CovMap 𝐽) → 𝐹 ∈ (𝐶 Cn 𝐽))
18 eqid 2731 . . . . . . . . . . . . . . 15 𝐽 = 𝐽
193, 18cnf 23070 . . . . . . . . . . . . . 14 (𝐹 ∈ (𝐶 Cn 𝐽) → 𝐹:𝐵 𝐽)
2013, 17, 193syl 18 . . . . . . . . . . . . 13 (𝜑𝐹:𝐵 𝐽)
2120ffvelcdmda 7086 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑀𝑥) ∈ 𝐵) → (𝐹‘(𝑀𝑥)) ∈ 𝐽)
2216, 21syldan 590 . . . . . . . . . . 11 ((𝜑𝑥𝑌) → (𝐹‘(𝑀𝑥)) ∈ 𝐽)
23 cvmliftmolem.1 . . . . . . . . . . . 12 𝑆 = (𝑘𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ ( 𝑠 = (𝐹𝑘) ∧ ∀𝑢𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢𝑣) = ∅ ∧ (𝐹𝑢) ∈ ((𝐶t 𝑢)Homeo(𝐽t 𝑘))))})
2423, 18cvmcov 34718 . . . . . . . . . . 11 ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ (𝐹‘(𝑀𝑥)) ∈ 𝐽) → ∃𝑎𝐽 ((𝐹‘(𝑀𝑥)) ∈ 𝑎 ∧ (𝑆𝑎) ≠ ∅))
2514, 22, 24syl2anc 583 . . . . . . . . . 10 ((𝜑𝑥𝑌) → ∃𝑎𝐽 ((𝐹‘(𝑀𝑥)) ∈ 𝑎 ∧ (𝑆𝑎) ≠ ∅))
26 n0 4346 . . . . . . . . . . . . . 14 ((𝑆𝑎) ≠ ∅ ↔ ∃𝑡 𝑡 ∈ (𝑆𝑎))
27 cvmliftmo.l . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐾 ∈ 𝑛-Locally Conn)
2827adantr 480 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ ((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎)))) → 𝐾 ∈ 𝑛-Locally Conn)
291adantr 480 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ ((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎)))) → 𝑀 ∈ (𝐾 Cn 𝐶))
30 simprrr 779 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ ((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎)))) → 𝑡 ∈ (𝑆𝑎))
3123cvmsss 34722 . . . . . . . . . . . . . . . . . . . . . 22 (𝑡 ∈ (𝑆𝑎) → 𝑡𝐶)
3230, 31syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ ((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎)))) → 𝑡𝐶)
3313adantr 480 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ ((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎)))) → 𝐹 ∈ (𝐶 CovMap 𝐽))
3415adantr 480 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ ((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎)))) → 𝑀:𝑌𝐵)
35 simprll 776 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ ((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎)))) → 𝑥𝑌)
3634, 35ffvelcdmd 7087 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ ((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎)))) → (𝑀𝑥) ∈ 𝐵)
37 simprrl 778 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ ((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎)))) → (𝐹‘(𝑀𝑥)) ∈ 𝑎)
38 eqid 2731 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑏𝑡 (𝑀𝑥) ∈ 𝑏) = (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)
3923, 3, 38cvmsiota 34732 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ (𝑡 ∈ (𝑆𝑎) ∧ (𝑀𝑥) ∈ 𝐵 ∧ (𝐹‘(𝑀𝑥)) ∈ 𝑎)) → ((𝑏𝑡 (𝑀𝑥) ∈ 𝑏) ∈ 𝑡 ∧ (𝑀𝑥) ∈ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)))
4033, 30, 36, 37, 39syl13anc 1371 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ ((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎)))) → ((𝑏𝑡 (𝑀𝑥) ∈ 𝑏) ∈ 𝑡 ∧ (𝑀𝑥) ∈ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)))
4140simpld 494 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ ((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎)))) → (𝑏𝑡 (𝑀𝑥) ∈ 𝑏) ∈ 𝑡)
4232, 41sseldd 3983 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ ((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎)))) → (𝑏𝑡 (𝑀𝑥) ∈ 𝑏) ∈ 𝐶)
43 cnima 23089 . . . . . . . . . . . . . . . . . . . 20 ((𝑀 ∈ (𝐾 Cn 𝐶) ∧ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏) ∈ 𝐶) → (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)) ∈ 𝐾)
4429, 42, 43syl2anc 583 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ ((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎)))) → (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)) ∈ 𝐾)
4540simprd 495 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ ((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎)))) → (𝑀𝑥) ∈ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏))
46 elpreima 7059 . . . . . . . . . . . . . . . . . . . . 21 (𝑀 Fn 𝑌 → (𝑥 ∈ (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)) ↔ (𝑥𝑌 ∧ (𝑀𝑥) ∈ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏))))
4734, 5, 463syl 18 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ ((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎)))) → (𝑥 ∈ (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)) ↔ (𝑥𝑌 ∧ (𝑀𝑥) ∈ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏))))
4835, 45, 47mpbir2and 710 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ ((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎)))) → 𝑥 ∈ (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)))
49 nlly2i 23300 . . . . . . . . . . . . . . . . . . 19 ((𝐾 ∈ 𝑛-Locally Conn ∧ (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)) ∈ 𝐾𝑥 ∈ (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏))) → ∃𝑠 ∈ 𝒫 (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏))∃𝑦𝐾 (𝑥𝑦𝑦𝑠 ∧ (𝐾t 𝑠) ∈ Conn))
5028, 44, 48, 49syl3anc 1370 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ ((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎)))) → ∃𝑠 ∈ 𝒫 (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏))∃𝑦𝐾 (𝑥𝑦𝑦𝑠 ∧ (𝐾t 𝑠) ∈ Conn))
51 simprr1 1220 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ ((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎)))) ∧ ((𝑠 ∈ 𝒫 (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)) ∧ 𝑦𝐾) ∧ (𝑥𝑦𝑦𝑠 ∧ (𝐾t 𝑠) ∈ Conn))) → 𝑥𝑦)
52 cvmliftmo.o . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑𝑂𝑌)
53 cvmliftmoi.g . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → (𝐹𝑀) = (𝐹𝑁))
54 cvmliftmoi.p . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → (𝑀𝑂) = (𝑁𝑂))
55 simplrr 775 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎))) ∧ (((𝑠 ∈ 𝒫 (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)) ∧ 𝑦𝐾) ∧ (𝑥𝑦𝑦𝑠 ∧ (𝐾t 𝑠) ∈ Conn)) ∧ 𝑧𝑦)) → 𝑡 ∈ (𝑆𝑎))
5655adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑 ∧ (((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎))) ∧ (((𝑠 ∈ 𝒫 (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)) ∧ 𝑦𝐾) ∧ (𝑥𝑦𝑦𝑠 ∧ (𝐾t 𝑠) ∈ Conn)) ∧ 𝑧𝑦))) → 𝑡 ∈ (𝑆𝑎))
5741adantrr 714 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑 ∧ (((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎))) ∧ (((𝑠 ∈ 𝒫 (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)) ∧ 𝑦𝐾) ∧ (𝑥𝑦𝑦𝑠 ∧ (𝐾t 𝑠) ∈ Conn)) ∧ 𝑧𝑦))) → (𝑏𝑡 (𝑀𝑥) ∈ 𝑏) ∈ 𝑡)
58 simplll 772 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝑠 ∈ 𝒫 (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)) ∧ 𝑦𝐾) ∧ (𝑥𝑦𝑦𝑠 ∧ (𝐾t 𝑠) ∈ Conn)) ∧ 𝑧𝑦) → 𝑠 ∈ 𝒫 (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)))
5958ad2antll 726 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑 ∧ (((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎))) ∧ (((𝑠 ∈ 𝒫 (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)) ∧ 𝑦𝐾) ∧ (𝑥𝑦𝑦𝑠 ∧ (𝐾t 𝑠) ∈ Conn)) ∧ 𝑧𝑦))) → 𝑠 ∈ 𝒫 (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)))
6059elpwid 4611 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑 ∧ (((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎))) ∧ (((𝑠 ∈ 𝒫 (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)) ∧ 𝑦𝐾) ∧ (𝑥𝑦𝑦𝑠 ∧ (𝐾t 𝑠) ∈ Conn)) ∧ 𝑧𝑦))) → 𝑠 ⊆ (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)))
61 simplr3 1216 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝑠 ∈ 𝒫 (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)) ∧ 𝑦𝐾) ∧ (𝑥𝑦𝑦𝑠 ∧ (𝐾t 𝑠) ∈ Conn)) ∧ 𝑧𝑦) → (𝐾t 𝑠) ∈ Conn)
6261ad2antll 726 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑 ∧ (((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎))) ∧ (((𝑠 ∈ 𝒫 (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)) ∧ 𝑦𝐾) ∧ (𝑥𝑦𝑦𝑠 ∧ (𝐾t 𝑠) ∈ Conn)) ∧ 𝑧𝑦))) → (𝐾t 𝑠) ∈ Conn)
63 simplr2 1215 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝑠 ∈ 𝒫 (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)) ∧ 𝑦𝐾) ∧ (𝑥𝑦𝑦𝑠 ∧ (𝐾t 𝑠) ∈ Conn)) ∧ 𝑧𝑦) → 𝑦𝑠)
6463ad2antll 726 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑 ∧ (((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎))) ∧ (((𝑠 ∈ 𝒫 (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)) ∧ 𝑦𝐾) ∧ (𝑥𝑦𝑦𝑠 ∧ (𝐾t 𝑠) ∈ Conn)) ∧ 𝑧𝑦))) → 𝑦𝑠)
65 simprr1 1220 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎))) ∧ ((𝑠 ∈ 𝒫 (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)) ∧ 𝑦𝐾) ∧ (𝑥𝑦𝑦𝑠 ∧ (𝐾t 𝑠) ∈ Conn))) → 𝑥𝑦)
6665adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑 ∧ (((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎))) ∧ ((𝑠 ∈ 𝒫 (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)) ∧ 𝑦𝐾) ∧ (𝑥𝑦𝑦𝑠 ∧ (𝐾t 𝑠) ∈ Conn)))) → 𝑥𝑦)
6766adantrrr 722 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑 ∧ (((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎))) ∧ (((𝑠 ∈ 𝒫 (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)) ∧ 𝑦𝐾) ∧ (𝑥𝑦𝑦𝑠 ∧ (𝐾t 𝑠) ∈ Conn)) ∧ 𝑧𝑦))) → 𝑥𝑦)
6864, 67sseldd 3983 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑 ∧ (((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎))) ∧ (((𝑠 ∈ 𝒫 (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)) ∧ 𝑦𝐾) ∧ (𝑥𝑦𝑦𝑠 ∧ (𝐾t 𝑠) ∈ Conn)) ∧ 𝑧𝑦))) → 𝑥𝑠)
69 simprrr 779 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑 ∧ (((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎))) ∧ (((𝑠 ∈ 𝒫 (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)) ∧ 𝑦𝐾) ∧ (𝑥𝑦𝑦𝑠 ∧ (𝐾t 𝑠) ∈ Conn)) ∧ 𝑧𝑦))) → 𝑧𝑦)
7064, 69sseldd 3983 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑 ∧ (((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎))) ∧ (((𝑠 ∈ 𝒫 (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)) ∧ 𝑦𝐾) ∧ (𝑥𝑦𝑦𝑠 ∧ (𝐾t 𝑠) ∈ Conn)) ∧ 𝑧𝑦))) → 𝑧𝑠)
7137adantrr 714 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑 ∧ (((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎))) ∧ (((𝑠 ∈ 𝒫 (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)) ∧ 𝑦𝐾) ∧ (𝑥𝑦𝑦𝑠 ∧ (𝐾t 𝑠) ∈ Conn)) ∧ 𝑧𝑦))) → (𝐹‘(𝑀𝑥)) ∈ 𝑎)
723, 2, 13, 11, 27, 52, 1, 7, 53, 54, 23, 56, 57, 60, 62, 68, 68, 70, 71cvmliftmolem1 34736 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑 ∧ (((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎))) ∧ (((𝑠 ∈ 𝒫 (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)) ∧ 𝑦𝐾) ∧ (𝑥𝑦𝑦𝑠 ∧ (𝐾t 𝑠) ∈ Conn)) ∧ 𝑧𝑦))) → (𝑥 ∈ dom (𝑀𝑁) → 𝑧 ∈ dom (𝑀𝑁)))
733, 2, 13, 11, 27, 52, 1, 7, 53, 54, 23, 56, 57, 60, 62, 68, 70, 68, 71cvmliftmolem1 34736 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3145 . . . . . . . . . . . . . . . . . . . . . . 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 3167 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ ((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎)))) ∧ 𝑠 ∈ 𝒫 (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏))) → (∃𝑦𝐾 (𝑥𝑦𝑦𝑠 ∧ (𝐾t 𝑠) ∈ Conn) → ∃𝑦𝐾 (𝑥𝑦 ∧ ∀𝑧𝑦 (𝑥 ∈ dom (𝑀𝑁) ↔ 𝑧 ∈ dom (𝑀𝑁)))))
8281rexlimdva 3154 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ ((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎)))) → (∃𝑠 ∈ 𝒫 (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏))∃𝑦𝐾 (𝑥𝑦𝑦𝑠 ∧ (𝐾t 𝑠) ∈ Conn) → ∃𝑦𝐾 (𝑥𝑦 ∧ ∀𝑧𝑦 (𝑥 ∈ dom (𝑀𝑁) ↔ 𝑧 ∈ dom (𝑀𝑁)))))
8350, 82mpd 15 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎)))) → ∃𝑦𝐾 (𝑥𝑦 ∧ ∀𝑧𝑦 (𝑥 ∈ dom (𝑀𝑁) ↔ 𝑧 ∈ dom (𝑀𝑁))))
8483anassrs 467 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥𝑌𝑎𝐽)) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎))) → ∃𝑦𝐾 (𝑥𝑦 ∧ ∀𝑧𝑦 (𝑥 ∈ dom (𝑀𝑁) ↔ 𝑧 ∈ dom (𝑀𝑁))))
8584expr 456 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥𝑌𝑎𝐽)) ∧ (𝐹‘(𝑀𝑥)) ∈ 𝑎) → (𝑡 ∈ (𝑆𝑎) → ∃𝑦𝐾 (𝑥𝑦 ∧ ∀𝑧𝑦 (𝑥 ∈ dom (𝑀𝑁) ↔ 𝑧 ∈ dom (𝑀𝑁)))))
8685exlimdv 1935 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥𝑌𝑎𝐽)) ∧ (𝐹‘(𝑀𝑥)) ∈ 𝑎) → (∃𝑡 𝑡 ∈ (𝑆𝑎) → ∃𝑦𝐾 (𝑥𝑦 ∧ ∀𝑧𝑦 (𝑥 ∈ dom (𝑀𝑁) ↔ 𝑧 ∈ dom (𝑀𝑁)))))
8726, 86biimtrid 241 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑥𝑌𝑎𝐽)) ∧ (𝐹‘(𝑀𝑥)) ∈ 𝑎) → ((𝑆𝑎) ≠ ∅ → ∃𝑦𝐾 (𝑥𝑦 ∧ ∀𝑧𝑦 (𝑥 ∈ dom (𝑀𝑁) ↔ 𝑧 ∈ dom (𝑀𝑁)))))
8887expimpd 453 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥𝑌𝑎𝐽)) → (((𝐹‘(𝑀𝑥)) ∈ 𝑎 ∧ (𝑆𝑎) ≠ ∅) → ∃𝑦𝐾 (𝑥𝑦 ∧ ∀𝑧𝑦 (𝑥 ∈ dom (𝑀𝑁) ↔ 𝑧 ∈ dom (𝑀𝑁)))))
8988anassrs 467 . . . . . . . . . . 11 (((𝜑𝑥𝑌) ∧ 𝑎𝐽) → (((𝐹‘(𝑀𝑥)) ∈ 𝑎 ∧ (𝑆𝑎) ≠ ∅) → ∃𝑦𝐾 (𝑥𝑦 ∧ ∀𝑧𝑦 (𝑥 ∈ dom (𝑀𝑁) ↔ 𝑧 ∈ dom (𝑀𝑁)))))
9089rexlimdva 3154 . . . . . . . . . 10 ((𝜑𝑥𝑌) → (∃𝑎𝐽 ((𝐹‘(𝑀𝑥)) ∈ 𝑎 ∧ (𝑆𝑎) ≠ ∅) → ∃𝑦𝐾 (𝑥𝑦 ∧ ∀𝑧𝑦 (𝑥 ∈ dom (𝑀𝑁) ↔ 𝑧 ∈ dom (𝑀𝑁)))))
9125, 90mpd 15 . . . . . . . . 9 ((𝜑𝑥𝑌) → ∃𝑦𝐾 (𝑥𝑦 ∧ ∀𝑧𝑦 (𝑥 ∈ dom (𝑀𝑁) ↔ 𝑧 ∈ dom (𝑀𝑁))))
9291ralrimiva 3145 . . . . . . . 8 (𝜑 → ∀𝑥𝑌𝑦𝐾 (𝑥𝑦 ∧ ∀𝑧𝑦 (𝑥 ∈ dom (𝑀𝑁) ↔ 𝑧 ∈ dom (𝑀𝑁))))
93 conntop 23241 . . . . . . . . . 10 (𝐾 ∈ Conn → 𝐾 ∈ Top)
9411, 93syl 17 . . . . . . . . 9 (𝜑𝐾 ∈ Top)
95 fndmin 7046 . . . . . . . . . . 11 ((𝑀 Fn 𝑌𝑁 Fn 𝑌) → dom (𝑀𝑁) = {𝑥𝑌 ∣ (𝑀𝑥) = (𝑁𝑥)})
966, 10, 95syl2anc 583 . . . . . . . . . 10 (𝜑 → dom (𝑀𝑁) = {𝑥𝑌 ∣ (𝑀𝑥) = (𝑁𝑥)})
97 ssrab2 4077 . . . . . . . . . 10 {𝑥𝑌 ∣ (𝑀𝑥) = (𝑁𝑥)} ⊆ 𝑌
9896, 97eqsstrdi 4036 . . . . . . . . 9 (𝜑 → dom (𝑀𝑁) ⊆ 𝑌)
992isclo 22911 . . . . . . . . 9 ((𝐾 ∈ Top ∧ dom (𝑀𝑁) ⊆ 𝑌) → (dom (𝑀𝑁) ∈ (𝐾 ∩ (Clsd‘𝐾)) ↔ ∀𝑥𝑌𝑦𝐾 (𝑥𝑦 ∧ ∀𝑧𝑦 (𝑥 ∈ dom (𝑀𝑁) ↔ 𝑧 ∈ dom (𝑀𝑁)))))
10094, 98, 99syl2anc 583 . . . . . . . 8 (𝜑 → (dom (𝑀𝑁) ∈ (𝐾 ∩ (Clsd‘𝐾)) ↔ ∀𝑥𝑌𝑦𝐾 (𝑥𝑦 ∧ ∀𝑧𝑦 (𝑥 ∈ dom (𝑀𝑁) ↔ 𝑧 ∈ dom (𝑀𝑁)))))
10192, 100mpbird 257 . . . . . . 7 (𝜑 → dom (𝑀𝑁) ∈ (𝐾 ∩ (Clsd‘𝐾)))
10212, 101sselid 3980 . . . . . 6 (𝜑 → dom (𝑀𝑁) ∈ 𝐾)
103 fveq2 6891 . . . . . . . . . . 11 (𝑥 = 𝑂 → (𝑀𝑥) = (𝑀𝑂))
104 fveq2 6891 . . . . . . . . . . 11 (𝑥 = 𝑂 → (𝑁𝑥) = (𝑁𝑂))
105103, 104eqeq12d 2747 . . . . . . . . . 10 (𝑥 = 𝑂 → ((𝑀𝑥) = (𝑁𝑥) ↔ (𝑀𝑂) = (𝑁𝑂)))
106105elrab 3683 . . . . . . . . 9 (𝑂 ∈ {𝑥𝑌 ∣ (𝑀𝑥) = (𝑁𝑥)} ↔ (𝑂𝑌 ∧ (𝑀𝑂) = (𝑁𝑂)))
10752, 54, 106sylanbrc 582 . . . . . . . 8 (𝜑𝑂 ∈ {𝑥𝑌 ∣ (𝑀𝑥) = (𝑁𝑥)})
108107, 96eleqtrrd 2835 . . . . . . 7 (𝜑𝑂 ∈ dom (𝑀𝑁))
109108ne0d 4335 . . . . . 6 (𝜑 → dom (𝑀𝑁) ≠ ∅)
110 inss2 4229 . . . . . . 7 (𝐾 ∩ (Clsd‘𝐾)) ⊆ (Clsd‘𝐾)
111110, 101sselid 3980 . . . . . 6 (𝜑 → dom (𝑀𝑁) ∈ (Clsd‘𝐾))
1122, 11, 102, 109, 111connclo 23239 . . . . 5 (𝜑 → dom (𝑀𝑁) = 𝑌)
113112, 96eqtr3d 2773 . . . 4 (𝜑𝑌 = {𝑥𝑌 ∣ (𝑀𝑥) = (𝑁𝑥)})
114 rabid2 3463 . . . 4 (𝑌 = {𝑥𝑌 ∣ (𝑀𝑥) = (𝑁𝑥)} ↔ ∀𝑥𝑌 (𝑀𝑥) = (𝑁𝑥))
115113, 114sylib 217 . . 3 (𝜑 → ∀𝑥𝑌 (𝑀𝑥) = (𝑁𝑥))
116115r19.21bi 3247 . 2 ((𝜑𝑥𝑌) → (𝑀𝑥) = (𝑁𝑥))
1176, 10, 116eqfnfvd 7035 1 (𝜑𝑀 = 𝑁)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 395  w3a 1086   = wceq 1540  wex 1780  wcel 2105  wne 2939  wral 3060  wrex 3069  {crab 3431  cdif 3945  cin 3947  wss 3948  c0 4322  𝒫 cpw 4602  {csn 4628   cuni 4908  cmpt 5231  ccnv 5675  dom cdm 5676  cres 5678  cima 5679  ccom 5680   Fn wfn 6538  wf 6539  cfv 6543  crio 7367  (class class class)co 7412  t crest 17373  Topctop 22715  Clsdccld 22840   Cn ccn 23048  Conncconn 23235  𝑛-Locally cnlly 23289  Homeochmeo 23577   CovMap ccvm 34710
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2702  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7729
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-ral 3061  df-rex 3070  df-rmo 3375  df-reu 3376  df-rab 3432  df-v 3475  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-int 4951  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-riota 7368  df-ov 7415  df-oprab 7416  df-mpo 7417  df-om 7860  df-1st 7979  df-2nd 7980  df-map 8828  df-en 8946  df-fin 8949  df-fi 9412  df-rest 17375  df-topgen 17396  df-top 22716  df-topon 22733  df-bases 22769  df-cld 22843  df-nei 22922  df-cn 23051  df-conn 23236  df-nlly 23291  df-hmeo 23579  df-cvm 34711
This theorem is referenced by:  cvmliftmoi  34738
  Copyright terms: Public domain W3C validator