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 31596
Description: Lemma for cvmliftmo 31598. (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 21270 . . 3 (𝑀 ∈ (𝐾 Cn 𝐶) → 𝑀:𝑌𝐵)
5 ffn 6185 . . 3 (𝑀:𝑌𝐵𝑀 Fn 𝑌)
61, 4, 53syl 18 . 2 (𝜑𝑀 Fn 𝑌)
7 cvmliftmoi.n . . 3 (𝜑𝑁 ∈ (𝐾 Cn 𝐶))
82, 3cnf 21270 . . 3 (𝑁 ∈ (𝐾 Cn 𝐶) → 𝑁:𝑌𝐵)
9 ffn 6185 . . 3 (𝑁:𝑌𝐵𝑁 Fn 𝑌)
107, 8, 93syl 18 . 2 (𝜑𝑁 Fn 𝑌)
11 cvmliftmo.k . . . . . 6 (𝜑𝐾 ∈ Conn)
12 inss1 3979 . . . . . . 7 (𝐾 ∩ (Clsd‘𝐾)) ⊆ 𝐾
13 cvmliftmo.f . . . . . . . . . . . 12 (𝜑𝐹 ∈ (𝐶 CovMap 𝐽))
1413adantr 466 . . . . . . . . . . 11 ((𝜑𝑥𝑌) → 𝐹 ∈ (𝐶 CovMap 𝐽))
151, 4syl 17 . . . . . . . . . . . . 13 (𝜑𝑀:𝑌𝐵)
1615ffvelrnda 6502 . . . . . . . . . . . 12 ((𝜑𝑥𝑌) → (𝑀𝑥) ∈ 𝐵)
17 cvmcn 31576 . . . . . . . . . . . . . 14 (𝐹 ∈ (𝐶 CovMap 𝐽) → 𝐹 ∈ (𝐶 Cn 𝐽))
18 eqid 2770 . . . . . . . . . . . . . . 15 𝐽 = 𝐽
193, 18cnf 21270 . . . . . . . . . . . . . 14 (𝐹 ∈ (𝐶 Cn 𝐽) → 𝐹:𝐵 𝐽)
2013, 17, 193syl 18 . . . . . . . . . . . . 13 (𝜑𝐹:𝐵 𝐽)
2120ffvelrnda 6502 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑀𝑥) ∈ 𝐵) → (𝐹‘(𝑀𝑥)) ∈ 𝐽)
2216, 21syldan 571 . . . . . . . . . . 11 ((𝜑𝑥𝑌) → (𝐹‘(𝑀𝑥)) ∈ 𝐽)
23 cvmliftmolem.1 . . . . . . . . . . . 12 𝑆 = (𝑘𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ ( 𝑠 = (𝐹𝑘) ∧ ∀𝑢𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢𝑣) = ∅ ∧ (𝐹𝑢) ∈ ((𝐶t 𝑢)Homeo(𝐽t 𝑘))))})
2423, 18cvmcov 31577 . . . . . . . . . . 11 ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ (𝐹‘(𝑀𝑥)) ∈ 𝐽) → ∃𝑎𝐽 ((𝐹‘(𝑀𝑥)) ∈ 𝑎 ∧ (𝑆𝑎) ≠ ∅))
2514, 22, 24syl2anc 565 . . . . . . . . . 10 ((𝜑𝑥𝑌) → ∃𝑎𝐽 ((𝐹‘(𝑀𝑥)) ∈ 𝑎 ∧ (𝑆𝑎) ≠ ∅))
26 n0 4076 . . . . . . . . . . . . . 14 ((𝑆𝑎) ≠ ∅ ↔ ∃𝑡 𝑡 ∈ (𝑆𝑎))
27 cvmliftmo.l . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐾 ∈ 𝑛-Locally Conn)
2827adantr 466 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ ((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎)))) → 𝐾 ∈ 𝑛-Locally Conn)
291adantr 466 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ ((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎)))) → 𝑀 ∈ (𝐾 Cn 𝐶))
30 simprrr 759 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ ((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎)))) → 𝑡 ∈ (𝑆𝑎))
3123cvmsss 31581 . . . . . . . . . . . . . . . . . . . . . 22 (𝑡 ∈ (𝑆𝑎) → 𝑡𝐶)
3230, 31syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ ((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎)))) → 𝑡𝐶)
3313adantr 466 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ ((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎)))) → 𝐹 ∈ (𝐶 CovMap 𝐽))
3415adantr 466 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ ((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎)))) → 𝑀:𝑌𝐵)
35 simprll 756 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ ((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎)))) → 𝑥𝑌)
3634, 35ffvelrnd 6503 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ ((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎)))) → (𝑀𝑥) ∈ 𝐵)
37 simprrl 758 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ ((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎)))) → (𝐹‘(𝑀𝑥)) ∈ 𝑎)
38 eqid 2770 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑏𝑡 (𝑀𝑥) ∈ 𝑏) = (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)
3923, 3, 38cvmsiota 31591 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ (𝑡 ∈ (𝑆𝑎) ∧ (𝑀𝑥) ∈ 𝐵 ∧ (𝐹‘(𝑀𝑥)) ∈ 𝑎)) → ((𝑏𝑡 (𝑀𝑥) ∈ 𝑏) ∈ 𝑡 ∧ (𝑀𝑥) ∈ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)))
4033, 30, 36, 37, 39syl13anc 1477 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ ((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎)))) → ((𝑏𝑡 (𝑀𝑥) ∈ 𝑏) ∈ 𝑡 ∧ (𝑀𝑥) ∈ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)))
4140simpld 476 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ ((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎)))) → (𝑏𝑡 (𝑀𝑥) ∈ 𝑏) ∈ 𝑡)
4232, 41sseldd 3751 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ ((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎)))) → (𝑏𝑡 (𝑀𝑥) ∈ 𝑏) ∈ 𝐶)
43 cnima 21289 . . . . . . . . . . . . . . . . . . . 20 ((𝑀 ∈ (𝐾 Cn 𝐶) ∧ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏) ∈ 𝐶) → (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)) ∈ 𝐾)
4429, 42, 43syl2anc 565 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ ((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎)))) → (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)) ∈ 𝐾)
4540simprd 477 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ ((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎)))) → (𝑀𝑥) ∈ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏))
46 elpreima 6480 . . . . . . . . . . . . . . . . . . . . 21 (𝑀 Fn 𝑌 → (𝑥 ∈ (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)) ↔ (𝑥𝑌 ∧ (𝑀𝑥) ∈ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏))))
4734, 5, 463syl 18 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ ((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎)))) → (𝑥 ∈ (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)) ↔ (𝑥𝑌 ∧ (𝑀𝑥) ∈ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏))))
4835, 45, 47mpbir2and 684 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ ((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎)))) → 𝑥 ∈ (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)))
49 nlly2i 21499 . . . . . . . . . . . . . . . . . . 19 ((𝐾 ∈ 𝑛-Locally Conn ∧ (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)) ∈ 𝐾𝑥 ∈ (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏))) → ∃𝑠 ∈ 𝒫 (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏))∃𝑦𝐾 (𝑥𝑦𝑦𝑠 ∧ (𝐾t 𝑠) ∈ Conn))
5028, 44, 48, 49syl3anc 1475 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ ((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎)))) → ∃𝑠 ∈ 𝒫 (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏))∃𝑦𝐾 (𝑥𝑦𝑦𝑠 ∧ (𝐾t 𝑠) ∈ Conn))
51 simprr1 1271 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ ((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎)))) ∧ ((𝑠 ∈ 𝒫 (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)) ∧ 𝑦𝐾) ∧ (𝑥𝑦𝑦𝑠 ∧ (𝐾t 𝑠) ∈ Conn))) → 𝑥𝑦)
52 cvmliftmo.o . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑𝑂𝑌)
53 cvmliftmoi.g . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → (𝐹𝑀) = (𝐹𝑁))
54 cvmliftmoi.p . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → (𝑀𝑂) = (𝑁𝑂))
55 simplrr 755 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎))) ∧ (((𝑠 ∈ 𝒫 (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)) ∧ 𝑦𝐾) ∧ (𝑥𝑦𝑦𝑠 ∧ (𝐾t 𝑠) ∈ Conn)) ∧ 𝑧𝑦)) → 𝑡 ∈ (𝑆𝑎))
5655adantl 467 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑 ∧ (((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎))) ∧ (((𝑠 ∈ 𝒫 (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)) ∧ 𝑦𝐾) ∧ (𝑥𝑦𝑦𝑠 ∧ (𝐾t 𝑠) ∈ Conn)) ∧ 𝑧𝑦))) → 𝑡 ∈ (𝑆𝑎))
5741adantrr 688 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑 ∧ (((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎))) ∧ (((𝑠 ∈ 𝒫 (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)) ∧ 𝑦𝐾) ∧ (𝑥𝑦𝑦𝑠 ∧ (𝐾t 𝑠) ∈ Conn)) ∧ 𝑧𝑦))) → (𝑏𝑡 (𝑀𝑥) ∈ 𝑏) ∈ 𝑡)
58 simplll 750 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝑠 ∈ 𝒫 (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)) ∧ 𝑦𝐾) ∧ (𝑥𝑦𝑦𝑠 ∧ (𝐾t 𝑠) ∈ Conn)) ∧ 𝑧𝑦) → 𝑠 ∈ 𝒫 (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)))
5958ad2antll 700 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑 ∧ (((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎))) ∧ (((𝑠 ∈ 𝒫 (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)) ∧ 𝑦𝐾) ∧ (𝑥𝑦𝑦𝑠 ∧ (𝐾t 𝑠) ∈ Conn)) ∧ 𝑧𝑦))) → 𝑠 ∈ 𝒫 (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)))
6059elpwid 4307 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑 ∧ (((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎))) ∧ (((𝑠 ∈ 𝒫 (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)) ∧ 𝑦𝐾) ∧ (𝑥𝑦𝑦𝑠 ∧ (𝐾t 𝑠) ∈ Conn)) ∧ 𝑧𝑦))) → 𝑠 ⊆ (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)))
61 simplr3 1263 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝑠 ∈ 𝒫 (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)) ∧ 𝑦𝐾) ∧ (𝑥𝑦𝑦𝑠 ∧ (𝐾t 𝑠) ∈ Conn)) ∧ 𝑧𝑦) → (𝐾t 𝑠) ∈ Conn)
6261ad2antll 700 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑 ∧ (((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎))) ∧ (((𝑠 ∈ 𝒫 (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)) ∧ 𝑦𝐾) ∧ (𝑥𝑦𝑦𝑠 ∧ (𝐾t 𝑠) ∈ Conn)) ∧ 𝑧𝑦))) → (𝐾t 𝑠) ∈ Conn)
63 simplr2 1261 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝑠 ∈ 𝒫 (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)) ∧ 𝑦𝐾) ∧ (𝑥𝑦𝑦𝑠 ∧ (𝐾t 𝑠) ∈ Conn)) ∧ 𝑧𝑦) → 𝑦𝑠)
6463ad2antll 700 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑 ∧ (((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎))) ∧ (((𝑠 ∈ 𝒫 (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)) ∧ 𝑦𝐾) ∧ (𝑥𝑦𝑦𝑠 ∧ (𝐾t 𝑠) ∈ Conn)) ∧ 𝑧𝑦))) → 𝑦𝑠)
65 simprr1 1271 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎))) ∧ ((𝑠 ∈ 𝒫 (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)) ∧ 𝑦𝐾) ∧ (𝑥𝑦𝑦𝑠 ∧ (𝐾t 𝑠) ∈ Conn))) → 𝑥𝑦)
6665adantl 467 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑 ∧ (((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎))) ∧ ((𝑠 ∈ 𝒫 (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)) ∧ 𝑦𝐾) ∧ (𝑥𝑦𝑦𝑠 ∧ (𝐾t 𝑠) ∈ Conn)))) → 𝑥𝑦)
6766adantrrr 696 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑 ∧ (((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎))) ∧ (((𝑠 ∈ 𝒫 (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)) ∧ 𝑦𝐾) ∧ (𝑥𝑦𝑦𝑠 ∧ (𝐾t 𝑠) ∈ Conn)) ∧ 𝑧𝑦))) → 𝑥𝑦)
6864, 67sseldd 3751 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑 ∧ (((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎))) ∧ (((𝑠 ∈ 𝒫 (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)) ∧ 𝑦𝐾) ∧ (𝑥𝑦𝑦𝑠 ∧ (𝐾t 𝑠) ∈ Conn)) ∧ 𝑧𝑦))) → 𝑥𝑠)
69 simprrr 759 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑 ∧ (((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎))) ∧ (((𝑠 ∈ 𝒫 (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)) ∧ 𝑦𝐾) ∧ (𝑥𝑦𝑦𝑠 ∧ (𝐾t 𝑠) ∈ Conn)) ∧ 𝑧𝑦))) → 𝑧𝑦)
7064, 69sseldd 3751 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑 ∧ (((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎))) ∧ (((𝑠 ∈ 𝒫 (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)) ∧ 𝑦𝐾) ∧ (𝑥𝑦𝑦𝑠 ∧ (𝐾t 𝑠) ∈ Conn)) ∧ 𝑧𝑦))) → 𝑧𝑠)
7137adantrr 688 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑 ∧ (((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎))) ∧ (((𝑠 ∈ 𝒫 (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)) ∧ 𝑦𝐾) ∧ (𝑥𝑦𝑦𝑠 ∧ (𝐾t 𝑠) ∈ Conn)) ∧ 𝑧𝑦))) → (𝐹‘(𝑀𝑥)) ∈ 𝑎)
723, 2, 13, 11, 27, 52, 1, 7, 53, 54, 23, 56, 57, 60, 62, 68, 68, 70, 71cvmliftmolem1 31595 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑 ∧ (((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎))) ∧ (((𝑠 ∈ 𝒫 (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)) ∧ 𝑦𝐾) ∧ (𝑥𝑦𝑦𝑠 ∧ (𝐾t 𝑠) ∈ Conn)) ∧ 𝑧𝑦))) → (𝑥 ∈ dom (𝑀𝑁) → 𝑧 ∈ dom (𝑀𝑁)))
733, 2, 13, 11, 27, 52, 1, 7, 53, 54, 23, 56, 57, 60, 62, 68, 70, 68, 71cvmliftmolem1 31595 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑 ∧ (((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎))) ∧ (((𝑠 ∈ 𝒫 (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)) ∧ 𝑦𝐾) ∧ (𝑥𝑦𝑦𝑠 ∧ (𝐾t 𝑠) ∈ Conn)) ∧ 𝑧𝑦))) → (𝑧 ∈ dom (𝑀𝑁) → 𝑥 ∈ dom (𝑀𝑁)))
7472, 73impbid 202 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∧ (((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎))) ∧ (((𝑠 ∈ 𝒫 (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)) ∧ 𝑦𝐾) ∧ (𝑥𝑦𝑦𝑠 ∧ (𝐾t 𝑠) ∈ Conn)) ∧ 𝑧𝑦))) → (𝑥 ∈ dom (𝑀𝑁) ↔ 𝑧 ∈ dom (𝑀𝑁)))
7574anassrs 458 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ ((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎)))) ∧ (((𝑠 ∈ 𝒫 (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)) ∧ 𝑦𝐾) ∧ (𝑥𝑦𝑦𝑠 ∧ (𝐾t 𝑠) ∈ Conn)) ∧ 𝑧𝑦)) → (𝑥 ∈ dom (𝑀𝑁) ↔ 𝑧 ∈ dom (𝑀𝑁)))
7675anassrs 458 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ ((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎)))) ∧ ((𝑠 ∈ 𝒫 (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)) ∧ 𝑦𝐾) ∧ (𝑥𝑦𝑦𝑠 ∧ (𝐾t 𝑠) ∈ Conn))) ∧ 𝑧𝑦) → (𝑥 ∈ dom (𝑀𝑁) ↔ 𝑧 ∈ dom (𝑀𝑁)))
7776ralrimiva 3114 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ ((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎)))) ∧ ((𝑠 ∈ 𝒫 (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)) ∧ 𝑦𝐾) ∧ (𝑥𝑦𝑦𝑠 ∧ (𝐾t 𝑠) ∈ Conn))) → ∀𝑧𝑦 (𝑥 ∈ dom (𝑀𝑁) ↔ 𝑧 ∈ dom (𝑀𝑁)))
7851, 77jca 495 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ ((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎)))) ∧ ((𝑠 ∈ 𝒫 (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)) ∧ 𝑦𝐾) ∧ (𝑥𝑦𝑦𝑠 ∧ (𝐾t 𝑠) ∈ Conn))) → (𝑥𝑦 ∧ ∀𝑧𝑦 (𝑥 ∈ dom (𝑀𝑁) ↔ 𝑧 ∈ dom (𝑀𝑁))))
7978expr 444 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ ((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎)))) ∧ (𝑠 ∈ 𝒫 (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)) ∧ 𝑦𝐾)) → ((𝑥𝑦𝑦𝑠 ∧ (𝐾t 𝑠) ∈ Conn) → (𝑥𝑦 ∧ ∀𝑧𝑦 (𝑥 ∈ dom (𝑀𝑁) ↔ 𝑧 ∈ dom (𝑀𝑁)))))
8079anassrs 458 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ ((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎)))) ∧ 𝑠 ∈ 𝒫 (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏))) ∧ 𝑦𝐾) → ((𝑥𝑦𝑦𝑠 ∧ (𝐾t 𝑠) ∈ Conn) → (𝑥𝑦 ∧ ∀𝑧𝑦 (𝑥 ∈ dom (𝑀𝑁) ↔ 𝑧 ∈ dom (𝑀𝑁)))))
8180reximdva 3164 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ ((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎)))) ∧ 𝑠 ∈ 𝒫 (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏))) → (∃𝑦𝐾 (𝑥𝑦𝑦𝑠 ∧ (𝐾t 𝑠) ∈ Conn) → ∃𝑦𝐾 (𝑥𝑦 ∧ ∀𝑧𝑦 (𝑥 ∈ dom (𝑀𝑁) ↔ 𝑧 ∈ dom (𝑀𝑁)))))
8281rexlimdva 3178 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ ((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎)))) → (∃𝑠 ∈ 𝒫 (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏))∃𝑦𝐾 (𝑥𝑦𝑦𝑠 ∧ (𝐾t 𝑠) ∈ Conn) → ∃𝑦𝐾 (𝑥𝑦 ∧ ∀𝑧𝑦 (𝑥 ∈ dom (𝑀𝑁) ↔ 𝑧 ∈ dom (𝑀𝑁)))))
8350, 82mpd 15 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎)))) → ∃𝑦𝐾 (𝑥𝑦 ∧ ∀𝑧𝑦 (𝑥 ∈ dom (𝑀𝑁) ↔ 𝑧 ∈ dom (𝑀𝑁))))
8483anassrs 458 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥𝑌𝑎𝐽)) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎))) → ∃𝑦𝐾 (𝑥𝑦 ∧ ∀𝑧𝑦 (𝑥 ∈ dom (𝑀𝑁) ↔ 𝑧 ∈ dom (𝑀𝑁))))
8584expr 444 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥𝑌𝑎𝐽)) ∧ (𝐹‘(𝑀𝑥)) ∈ 𝑎) → (𝑡 ∈ (𝑆𝑎) → ∃𝑦𝐾 (𝑥𝑦 ∧ ∀𝑧𝑦 (𝑥 ∈ dom (𝑀𝑁) ↔ 𝑧 ∈ dom (𝑀𝑁)))))
8685exlimdv 2012 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥𝑌𝑎𝐽)) ∧ (𝐹‘(𝑀𝑥)) ∈ 𝑎) → (∃𝑡 𝑡 ∈ (𝑆𝑎) → ∃𝑦𝐾 (𝑥𝑦 ∧ ∀𝑧𝑦 (𝑥 ∈ dom (𝑀𝑁) ↔ 𝑧 ∈ dom (𝑀𝑁)))))
8726, 86syl5bi 232 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑥𝑌𝑎𝐽)) ∧ (𝐹‘(𝑀𝑥)) ∈ 𝑎) → ((𝑆𝑎) ≠ ∅ → ∃𝑦𝐾 (𝑥𝑦 ∧ ∀𝑧𝑦 (𝑥 ∈ dom (𝑀𝑁) ↔ 𝑧 ∈ dom (𝑀𝑁)))))
8887expimpd 441 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥𝑌𝑎𝐽)) → (((𝐹‘(𝑀𝑥)) ∈ 𝑎 ∧ (𝑆𝑎) ≠ ∅) → ∃𝑦𝐾 (𝑥𝑦 ∧ ∀𝑧𝑦 (𝑥 ∈ dom (𝑀𝑁) ↔ 𝑧 ∈ dom (𝑀𝑁)))))
8988anassrs 458 . . . . . . . . . . 11 (((𝜑𝑥𝑌) ∧ 𝑎𝐽) → (((𝐹‘(𝑀𝑥)) ∈ 𝑎 ∧ (𝑆𝑎) ≠ ∅) → ∃𝑦𝐾 (𝑥𝑦 ∧ ∀𝑧𝑦 (𝑥 ∈ dom (𝑀𝑁) ↔ 𝑧 ∈ dom (𝑀𝑁)))))
9089rexlimdva 3178 . . . . . . . . . 10 ((𝜑𝑥𝑌) → (∃𝑎𝐽 ((𝐹‘(𝑀𝑥)) ∈ 𝑎 ∧ (𝑆𝑎) ≠ ∅) → ∃𝑦𝐾 (𝑥𝑦 ∧ ∀𝑧𝑦 (𝑥 ∈ dom (𝑀𝑁) ↔ 𝑧 ∈ dom (𝑀𝑁)))))
9125, 90mpd 15 . . . . . . . . 9 ((𝜑𝑥𝑌) → ∃𝑦𝐾 (𝑥𝑦 ∧ ∀𝑧𝑦 (𝑥 ∈ dom (𝑀𝑁) ↔ 𝑧 ∈ dom (𝑀𝑁))))
9291ralrimiva 3114 . . . . . . . 8 (𝜑 → ∀𝑥𝑌𝑦𝐾 (𝑥𝑦 ∧ ∀𝑧𝑦 (𝑥 ∈ dom (𝑀𝑁) ↔ 𝑧 ∈ dom (𝑀𝑁))))
93 conntop 21440 . . . . . . . . . 10 (𝐾 ∈ Conn → 𝐾 ∈ Top)
9411, 93syl 17 . . . . . . . . 9 (𝜑𝐾 ∈ Top)
95 fndmin 6467 . . . . . . . . . . 11 ((𝑀 Fn 𝑌𝑁 Fn 𝑌) → dom (𝑀𝑁) = {𝑥𝑌 ∣ (𝑀𝑥) = (𝑁𝑥)})
966, 10, 95syl2anc 565 . . . . . . . . . 10 (𝜑 → dom (𝑀𝑁) = {𝑥𝑌 ∣ (𝑀𝑥) = (𝑁𝑥)})
97 ssrab2 3834 . . . . . . . . . 10 {𝑥𝑌 ∣ (𝑀𝑥) = (𝑁𝑥)} ⊆ 𝑌
9896, 97syl6eqss 3802 . . . . . . . . 9 (𝜑 → dom (𝑀𝑁) ⊆ 𝑌)
992isclo 21111 . . . . . . . . 9 ((𝐾 ∈ Top ∧ dom (𝑀𝑁) ⊆ 𝑌) → (dom (𝑀𝑁) ∈ (𝐾 ∩ (Clsd‘𝐾)) ↔ ∀𝑥𝑌𝑦𝐾 (𝑥𝑦 ∧ ∀𝑧𝑦 (𝑥 ∈ dom (𝑀𝑁) ↔ 𝑧 ∈ dom (𝑀𝑁)))))
10094, 98, 99syl2anc 565 . . . . . . . 8 (𝜑 → (dom (𝑀𝑁) ∈ (𝐾 ∩ (Clsd‘𝐾)) ↔ ∀𝑥𝑌𝑦𝐾 (𝑥𝑦 ∧ ∀𝑧𝑦 (𝑥 ∈ dom (𝑀𝑁) ↔ 𝑧 ∈ dom (𝑀𝑁)))))
10192, 100mpbird 247 . . . . . . 7 (𝜑 → dom (𝑀𝑁) ∈ (𝐾 ∩ (Clsd‘𝐾)))
10212, 101sseldi 3748 . . . . . 6 (𝜑 → dom (𝑀𝑁) ∈ 𝐾)
103 fveq2 6332 . . . . . . . . . . 11 (𝑥 = 𝑂 → (𝑀𝑥) = (𝑀𝑂))
104 fveq2 6332 . . . . . . . . . . 11 (𝑥 = 𝑂 → (𝑁𝑥) = (𝑁𝑂))
105103, 104eqeq12d 2785 . . . . . . . . . 10 (𝑥 = 𝑂 → ((𝑀𝑥) = (𝑁𝑥) ↔ (𝑀𝑂) = (𝑁𝑂)))
106105elrab 3513 . . . . . . . . 9 (𝑂 ∈ {𝑥𝑌 ∣ (𝑀𝑥) = (𝑁𝑥)} ↔ (𝑂𝑌 ∧ (𝑀𝑂) = (𝑁𝑂)))
10752, 54, 106sylanbrc 564 . . . . . . . 8 (𝜑𝑂 ∈ {𝑥𝑌 ∣ (𝑀𝑥) = (𝑁𝑥)})
108107, 96eleqtrrd 2852 . . . . . . 7 (𝜑𝑂 ∈ dom (𝑀𝑁))
109 ne0i 4067 . . . . . . 7 (𝑂 ∈ dom (𝑀𝑁) → dom (𝑀𝑁) ≠ ∅)
110108, 109syl 17 . . . . . 6 (𝜑 → dom (𝑀𝑁) ≠ ∅)
111 inss2 3980 . . . . . . 7 (𝐾 ∩ (Clsd‘𝐾)) ⊆ (Clsd‘𝐾)
112111, 101sseldi 3748 . . . . . 6 (𝜑 → dom (𝑀𝑁) ∈ (Clsd‘𝐾))
1132, 11, 102, 110, 112connclo 21438 . . . . 5 (𝜑 → dom (𝑀𝑁) = 𝑌)
114113, 96eqtr3d 2806 . . . 4 (𝜑𝑌 = {𝑥𝑌 ∣ (𝑀𝑥) = (𝑁𝑥)})
115 rabid2 3266 . . . 4 (𝑌 = {𝑥𝑌 ∣ (𝑀𝑥) = (𝑁𝑥)} ↔ ∀𝑥𝑌 (𝑀𝑥) = (𝑁𝑥))
116114, 115sylib 208 . . 3 (𝜑 → ∀𝑥𝑌 (𝑀𝑥) = (𝑁𝑥))
117116r19.21bi 3080 . 2 ((𝜑𝑥𝑌) → (𝑀𝑥) = (𝑁𝑥))
1186, 10, 117eqfnfvd 6457 1 (𝜑𝑀 = 𝑁)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 382  w3a 1070   = wceq 1630  wex 1851  wcel 2144  wne 2942  wral 3060  wrex 3061  {crab 3064  cdif 3718  cin 3720  wss 3721  c0 4061  𝒫 cpw 4295  {csn 4314   cuni 4572  cmpt 4861  ccnv 5248  dom cdm 5249  cres 5251  cima 5252  ccom 5253   Fn wfn 6026  wf 6027  cfv 6031  crio 6752  (class class class)co 6792  t crest 16288  Topctop 20917  Clsdccld 21040   Cn ccn 21248  Conncconn 21434  𝑛-Locally cnlly 21488  Homeochmeo 21776   CovMap ccvm 31569
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1990  ax-6 2056  ax-7 2092  ax-8 2146  ax-9 2153  ax-10 2173  ax-11 2189  ax-12 2202  ax-13 2407  ax-ext 2750  ax-rep 4902  ax-sep 4912  ax-nul 4920  ax-pow 4971  ax-pr 5034  ax-un 7095
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 827  df-3or 1071  df-3an 1072  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2049  df-eu 2621  df-mo 2622  df-clab 2757  df-cleq 2763  df-clel 2766  df-nfc 2901  df-ne 2943  df-ral 3065  df-rex 3066  df-reu 3067  df-rmo 3068  df-rab 3069  df-v 3351  df-sbc 3586  df-csb 3681  df-dif 3724  df-un 3726  df-in 3728  df-ss 3735  df-pss 3737  df-nul 4062  df-if 4224  df-pw 4297  df-sn 4315  df-pr 4317  df-tp 4319  df-op 4321  df-uni 4573  df-int 4610  df-iun 4654  df-br 4785  df-opab 4845  df-mpt 4862  df-tr 4885  df-id 5157  df-eprel 5162  df-po 5170  df-so 5171  df-fr 5208  df-we 5210  df-xp 5255  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-rn 5260  df-res 5261  df-ima 5262  df-pred 5823  df-ord 5869  df-on 5870  df-lim 5871  df-suc 5872  df-iota 5994  df-fun 6033  df-fn 6034  df-f 6035  df-f1 6036  df-fo 6037  df-f1o 6038  df-fv 6039  df-riota 6753  df-ov 6795  df-oprab 6796  df-mpt2 6797  df-om 7212  df-1st 7314  df-2nd 7315  df-wrecs 7558  df-recs 7620  df-rdg 7658  df-oadd 7716  df-er 7895  df-map 8010  df-en 8109  df-fin 8112  df-fi 8472  df-rest 16290  df-topgen 16311  df-top 20918  df-topon 20935  df-bases 20970  df-cld 21043  df-nei 21122  df-cn 21251  df-conn 21435  df-nlly 21490  df-hmeo 21778  df-cvm 31570
This theorem is referenced by:  cvmliftmoi  31597
  Copyright terms: Public domain W3C validator