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

Theorem cvmliftmolem2 30518
 Description: Lemma for cvmliftmo 30520. (Contributed by Mario Carneiro, 10-Mar-2015.)
Hypotheses
Ref Expression
cvmliftmo.b 𝐵 = 𝐶
cvmliftmo.y 𝑌 = 𝐾
cvmliftmo.f (𝜑𝐹 ∈ (𝐶 CovMap 𝐽))
cvmliftmo.k (𝜑𝐾 ∈ Con)
cvmliftmo.l (𝜑𝐾 ∈ 𝑛-Locally Con)
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 20860 . . 3 (𝑀 ∈ (𝐾 Cn 𝐶) → 𝑀:𝑌𝐵)
5 ffn 5958 . . 3 (𝑀:𝑌𝐵𝑀 Fn 𝑌)
61, 4, 53syl 18 . 2 (𝜑𝑀 Fn 𝑌)
7 cvmliftmoi.n . . 3 (𝜑𝑁 ∈ (𝐾 Cn 𝐶))
82, 3cnf 20860 . . 3 (𝑁 ∈ (𝐾 Cn 𝐶) → 𝑁:𝑌𝐵)
9 ffn 5958 . . 3 (𝑁:𝑌𝐵𝑁 Fn 𝑌)
107, 8, 93syl 18 . 2 (𝜑𝑁 Fn 𝑌)
11 cvmliftmo.k . . . . . 6 (𝜑𝐾 ∈ Con)
12 inss1 3795 . . . . . . 7 (𝐾 ∩ (Clsd‘𝐾)) ⊆ 𝐾
13 cvmliftmo.f . . . . . . . . . . . 12 (𝜑𝐹 ∈ (𝐶 CovMap 𝐽))
1413adantr 480 . . . . . . . . . . 11 ((𝜑𝑥𝑌) → 𝐹 ∈ (𝐶 CovMap 𝐽))
151, 4syl 17 . . . . . . . . . . . . 13 (𝜑𝑀:𝑌𝐵)
1615ffvelrnda 6267 . . . . . . . . . . . 12 ((𝜑𝑥𝑌) → (𝑀𝑥) ∈ 𝐵)
17 cvmcn 30498 . . . . . . . . . . . . . 14 (𝐹 ∈ (𝐶 CovMap 𝐽) → 𝐹 ∈ (𝐶 Cn 𝐽))
18 eqid 2610 . . . . . . . . . . . . . . 15 𝐽 = 𝐽
193, 18cnf 20860 . . . . . . . . . . . . . 14 (𝐹 ∈ (𝐶 Cn 𝐽) → 𝐹:𝐵 𝐽)
2013, 17, 193syl 18 . . . . . . . . . . . . 13 (𝜑𝐹:𝐵 𝐽)
2120ffvelrnda 6267 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑀𝑥) ∈ 𝐵) → (𝐹‘(𝑀𝑥)) ∈ 𝐽)
2216, 21syldan 486 . . . . . . . . . . 11 ((𝜑𝑥𝑌) → (𝐹‘(𝑀𝑥)) ∈ 𝐽)
23 cvmliftmolem.1 . . . . . . . . . . . 12 𝑆 = (𝑘𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ ( 𝑠 = (𝐹𝑘) ∧ ∀𝑢𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢𝑣) = ∅ ∧ (𝐹𝑢) ∈ ((𝐶t 𝑢)Homeo(𝐽t 𝑘))))})
2423, 18cvmcov 30499 . . . . . . . . . . 11 ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ (𝐹‘(𝑀𝑥)) ∈ 𝐽) → ∃𝑎𝐽 ((𝐹‘(𝑀𝑥)) ∈ 𝑎 ∧ (𝑆𝑎) ≠ ∅))
2514, 22, 24syl2anc 691 . . . . . . . . . 10 ((𝜑𝑥𝑌) → ∃𝑎𝐽 ((𝐹‘(𝑀𝑥)) ∈ 𝑎 ∧ (𝑆𝑎) ≠ ∅))
26 n0 3890 . . . . . . . . . . . . . 14 ((𝑆𝑎) ≠ ∅ ↔ ∃𝑡 𝑡 ∈ (𝑆𝑎))
27 cvmliftmo.l . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐾 ∈ 𝑛-Locally Con)
2827adantr 480 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ ((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎)))) → 𝐾 ∈ 𝑛-Locally Con)
291adantr 480 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ ((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎)))) → 𝑀 ∈ (𝐾 Cn 𝐶))
30 simprrr 801 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ ((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎)))) → 𝑡 ∈ (𝑆𝑎))
3123cvmsss 30503 . . . . . . . . . . . . . . . . . . . . . 22 (𝑡 ∈ (𝑆𝑎) → 𝑡𝐶)
3230, 31syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ ((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎)))) → 𝑡𝐶)
3313adantr 480 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ ((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎)))) → 𝐹 ∈ (𝐶 CovMap 𝐽))
3415adantr 480 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ ((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎)))) → 𝑀:𝑌𝐵)
35 simprll 798 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ ((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎)))) → 𝑥𝑌)
3634, 35ffvelrnd 6268 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ ((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎)))) → (𝑀𝑥) ∈ 𝐵)
37 simprrl 800 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ ((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎)))) → (𝐹‘(𝑀𝑥)) ∈ 𝑎)
38 eqid 2610 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑏𝑡 (𝑀𝑥) ∈ 𝑏) = (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)
3923, 3, 38cvmsiota 30513 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ (𝑡 ∈ (𝑆𝑎) ∧ (𝑀𝑥) ∈ 𝐵 ∧ (𝐹‘(𝑀𝑥)) ∈ 𝑎)) → ((𝑏𝑡 (𝑀𝑥) ∈ 𝑏) ∈ 𝑡 ∧ (𝑀𝑥) ∈ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)))
4033, 30, 36, 37, 39syl13anc 1320 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ ((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎)))) → ((𝑏𝑡 (𝑀𝑥) ∈ 𝑏) ∈ 𝑡 ∧ (𝑀𝑥) ∈ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)))
4140simpld 474 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ ((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎)))) → (𝑏𝑡 (𝑀𝑥) ∈ 𝑏) ∈ 𝑡)
4232, 41sseldd 3569 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ ((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎)))) → (𝑏𝑡 (𝑀𝑥) ∈ 𝑏) ∈ 𝐶)
43 cnima 20879 . . . . . . . . . . . . . . . . . . . 20 ((𝑀 ∈ (𝐾 Cn 𝐶) ∧ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏) ∈ 𝐶) → (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)) ∈ 𝐾)
4429, 42, 43syl2anc 691 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ ((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎)))) → (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)) ∈ 𝐾)
4540simprd 478 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ ((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎)))) → (𝑀𝑥) ∈ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏))
46 elpreima 6245 . . . . . . . . . . . . . . . . . . . . 21 (𝑀 Fn 𝑌 → (𝑥 ∈ (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)) ↔ (𝑥𝑌 ∧ (𝑀𝑥) ∈ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏))))
4734, 5, 463syl 18 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ ((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎)))) → (𝑥 ∈ (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)) ↔ (𝑥𝑌 ∧ (𝑀𝑥) ∈ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏))))
4835, 45, 47mpbir2and 959 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ ((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎)))) → 𝑥 ∈ (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)))
49 nlly2i 21089 . . . . . . . . . . . . . . . . . . 19 ((𝐾 ∈ 𝑛-Locally Con ∧ (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)) ∈ 𝐾𝑥 ∈ (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏))) → ∃𝑠 ∈ 𝒫 (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏))∃𝑦𝐾 (𝑥𝑦𝑦𝑠 ∧ (𝐾t 𝑠) ∈ Con))
5028, 44, 48, 49syl3anc 1318 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ ((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎)))) → ∃𝑠 ∈ 𝒫 (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏))∃𝑦𝐾 (𝑥𝑦𝑦𝑠 ∧ (𝐾t 𝑠) ∈ Con))
51 simprr1 1102 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ ((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎)))) ∧ ((𝑠 ∈ 𝒫 (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)) ∧ 𝑦𝐾) ∧ (𝑥𝑦𝑦𝑠 ∧ (𝐾t 𝑠) ∈ Con))) → 𝑥𝑦)
52 cvmliftmo.o . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑𝑂𝑌)
53 cvmliftmoi.g . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → (𝐹𝑀) = (𝐹𝑁))
54 cvmliftmoi.p . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → (𝑀𝑂) = (𝑁𝑂))
55 simplrr 797 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎))) ∧ (((𝑠 ∈ 𝒫 (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)) ∧ 𝑦𝐾) ∧ (𝑥𝑦𝑦𝑠 ∧ (𝐾t 𝑠) ∈ Con)) ∧ 𝑧𝑦)) → 𝑡 ∈ (𝑆𝑎))
5655adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑 ∧ (((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎))) ∧ (((𝑠 ∈ 𝒫 (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)) ∧ 𝑦𝐾) ∧ (𝑥𝑦𝑦𝑠 ∧ (𝐾t 𝑠) ∈ Con)) ∧ 𝑧𝑦))) → 𝑡 ∈ (𝑆𝑎))
5741adantrr 749 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑 ∧ (((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎))) ∧ (((𝑠 ∈ 𝒫 (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)) ∧ 𝑦𝐾) ∧ (𝑥𝑦𝑦𝑠 ∧ (𝐾t 𝑠) ∈ Con)) ∧ 𝑧𝑦))) → (𝑏𝑡 (𝑀𝑥) ∈ 𝑏) ∈ 𝑡)
58 simplll 794 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝑠 ∈ 𝒫 (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)) ∧ 𝑦𝐾) ∧ (𝑥𝑦𝑦𝑠 ∧ (𝐾t 𝑠) ∈ Con)) ∧ 𝑧𝑦) → 𝑠 ∈ 𝒫 (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)))
5958ad2antll 761 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑 ∧ (((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎))) ∧ (((𝑠 ∈ 𝒫 (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)) ∧ 𝑦𝐾) ∧ (𝑥𝑦𝑦𝑠 ∧ (𝐾t 𝑠) ∈ Con)) ∧ 𝑧𝑦))) → 𝑠 ∈ 𝒫 (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)))
6059elpwid 4118 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑 ∧ (((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎))) ∧ (((𝑠 ∈ 𝒫 (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)) ∧ 𝑦𝐾) ∧ (𝑥𝑦𝑦𝑠 ∧ (𝐾t 𝑠) ∈ Con)) ∧ 𝑧𝑦))) → 𝑠 ⊆ (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)))
61 simplr3 1098 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝑠 ∈ 𝒫 (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)) ∧ 𝑦𝐾) ∧ (𝑥𝑦𝑦𝑠 ∧ (𝐾t 𝑠) ∈ Con)) ∧ 𝑧𝑦) → (𝐾t 𝑠) ∈ Con)
6261ad2antll 761 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑 ∧ (((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎))) ∧ (((𝑠 ∈ 𝒫 (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)) ∧ 𝑦𝐾) ∧ (𝑥𝑦𝑦𝑠 ∧ (𝐾t 𝑠) ∈ Con)) ∧ 𝑧𝑦))) → (𝐾t 𝑠) ∈ Con)
63 simplr2 1097 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝑠 ∈ 𝒫 (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)) ∧ 𝑦𝐾) ∧ (𝑥𝑦𝑦𝑠 ∧ (𝐾t 𝑠) ∈ Con)) ∧ 𝑧𝑦) → 𝑦𝑠)
6463ad2antll 761 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑 ∧ (((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎))) ∧ (((𝑠 ∈ 𝒫 (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)) ∧ 𝑦𝐾) ∧ (𝑥𝑦𝑦𝑠 ∧ (𝐾t 𝑠) ∈ Con)) ∧ 𝑧𝑦))) → 𝑦𝑠)
65 simprr1 1102 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎))) ∧ ((𝑠 ∈ 𝒫 (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)) ∧ 𝑦𝐾) ∧ (𝑥𝑦𝑦𝑠 ∧ (𝐾t 𝑠) ∈ Con))) → 𝑥𝑦)
6665adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑 ∧ (((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎))) ∧ ((𝑠 ∈ 𝒫 (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)) ∧ 𝑦𝐾) ∧ (𝑥𝑦𝑦𝑠 ∧ (𝐾t 𝑠) ∈ Con)))) → 𝑥𝑦)
6766adantrrr 757 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑 ∧ (((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎))) ∧ (((𝑠 ∈ 𝒫 (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)) ∧ 𝑦𝐾) ∧ (𝑥𝑦𝑦𝑠 ∧ (𝐾t 𝑠) ∈ Con)) ∧ 𝑧𝑦))) → 𝑥𝑦)
6864, 67sseldd 3569 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑 ∧ (((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎))) ∧ (((𝑠 ∈ 𝒫 (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)) ∧ 𝑦𝐾) ∧ (𝑥𝑦𝑦𝑠 ∧ (𝐾t 𝑠) ∈ Con)) ∧ 𝑧𝑦))) → 𝑥𝑠)
69 simprrr 801 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑 ∧ (((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎))) ∧ (((𝑠 ∈ 𝒫 (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)) ∧ 𝑦𝐾) ∧ (𝑥𝑦𝑦𝑠 ∧ (𝐾t 𝑠) ∈ Con)) ∧ 𝑧𝑦))) → 𝑧𝑦)
7064, 69sseldd 3569 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑 ∧ (((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎))) ∧ (((𝑠 ∈ 𝒫 (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)) ∧ 𝑦𝐾) ∧ (𝑥𝑦𝑦𝑠 ∧ (𝐾t 𝑠) ∈ Con)) ∧ 𝑧𝑦))) → 𝑧𝑠)
7137adantrr 749 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑 ∧ (((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎))) ∧ (((𝑠 ∈ 𝒫 (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)) ∧ 𝑦𝐾) ∧ (𝑥𝑦𝑦𝑠 ∧ (𝐾t 𝑠) ∈ Con)) ∧ 𝑧𝑦))) → (𝐹‘(𝑀𝑥)) ∈ 𝑎)
723, 2, 13, 11, 27, 52, 1, 7, 53, 54, 23, 56, 57, 60, 62, 68, 68, 70, 71cvmliftmolem1 30517 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑 ∧ (((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎))) ∧ (((𝑠 ∈ 𝒫 (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)) ∧ 𝑦𝐾) ∧ (𝑥𝑦𝑦𝑠 ∧ (𝐾t 𝑠) ∈ Con)) ∧ 𝑧𝑦))) → (𝑥 ∈ dom (𝑀𝑁) → 𝑧 ∈ dom (𝑀𝑁)))
733, 2, 13, 11, 27, 52, 1, 7, 53, 54, 23, 56, 57, 60, 62, 68, 70, 68, 71cvmliftmolem1 30517 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑 ∧ (((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎))) ∧ (((𝑠 ∈ 𝒫 (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)) ∧ 𝑦𝐾) ∧ (𝑥𝑦𝑦𝑠 ∧ (𝐾t 𝑠) ∈ Con)) ∧ 𝑧𝑦))) → (𝑧 ∈ dom (𝑀𝑁) → 𝑥 ∈ dom (𝑀𝑁)))
7472, 73impbid 201 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∧ (((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎))) ∧ (((𝑠 ∈ 𝒫 (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)) ∧ 𝑦𝐾) ∧ (𝑥𝑦𝑦𝑠 ∧ (𝐾t 𝑠) ∈ Con)) ∧ 𝑧𝑦))) → (𝑥 ∈ dom (𝑀𝑁) ↔ 𝑧 ∈ dom (𝑀𝑁)))
7574anassrs 678 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ ((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎)))) ∧ (((𝑠 ∈ 𝒫 (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)) ∧ 𝑦𝐾) ∧ (𝑥𝑦𝑦𝑠 ∧ (𝐾t 𝑠) ∈ Con)) ∧ 𝑧𝑦)) → (𝑥 ∈ dom (𝑀𝑁) ↔ 𝑧 ∈ dom (𝑀𝑁)))
7675anassrs 678 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ ((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎)))) ∧ ((𝑠 ∈ 𝒫 (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)) ∧ 𝑦𝐾) ∧ (𝑥𝑦𝑦𝑠 ∧ (𝐾t 𝑠) ∈ Con))) ∧ 𝑧𝑦) → (𝑥 ∈ dom (𝑀𝑁) ↔ 𝑧 ∈ dom (𝑀𝑁)))
7776ralrimiva 2949 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ ((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎)))) ∧ ((𝑠 ∈ 𝒫 (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)) ∧ 𝑦𝐾) ∧ (𝑥𝑦𝑦𝑠 ∧ (𝐾t 𝑠) ∈ Con))) → ∀𝑧𝑦 (𝑥 ∈ dom (𝑀𝑁) ↔ 𝑧 ∈ dom (𝑀𝑁)))
7851, 77jca 553 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ ((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎)))) ∧ ((𝑠 ∈ 𝒫 (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)) ∧ 𝑦𝐾) ∧ (𝑥𝑦𝑦𝑠 ∧ (𝐾t 𝑠) ∈ Con))) → (𝑥𝑦 ∧ ∀𝑧𝑦 (𝑥 ∈ dom (𝑀𝑁) ↔ 𝑧 ∈ dom (𝑀𝑁))))
7978expr 641 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ ((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎)))) ∧ (𝑠 ∈ 𝒫 (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏)) ∧ 𝑦𝐾)) → ((𝑥𝑦𝑦𝑠 ∧ (𝐾t 𝑠) ∈ Con) → (𝑥𝑦 ∧ ∀𝑧𝑦 (𝑥 ∈ dom (𝑀𝑁) ↔ 𝑧 ∈ dom (𝑀𝑁)))))
8079anassrs 678 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ ((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎)))) ∧ 𝑠 ∈ 𝒫 (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏))) ∧ 𝑦𝐾) → ((𝑥𝑦𝑦𝑠 ∧ (𝐾t 𝑠) ∈ Con) → (𝑥𝑦 ∧ ∀𝑧𝑦 (𝑥 ∈ dom (𝑀𝑁) ↔ 𝑧 ∈ dom (𝑀𝑁)))))
8180reximdva 3000 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ ((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎)))) ∧ 𝑠 ∈ 𝒫 (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏))) → (∃𝑦𝐾 (𝑥𝑦𝑦𝑠 ∧ (𝐾t 𝑠) ∈ Con) → ∃𝑦𝐾 (𝑥𝑦 ∧ ∀𝑧𝑦 (𝑥 ∈ dom (𝑀𝑁) ↔ 𝑧 ∈ dom (𝑀𝑁)))))
8281rexlimdva 3013 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ ((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎)))) → (∃𝑠 ∈ 𝒫 (𝑀 “ (𝑏𝑡 (𝑀𝑥) ∈ 𝑏))∃𝑦𝐾 (𝑥𝑦𝑦𝑠 ∧ (𝐾t 𝑠) ∈ Con) → ∃𝑦𝐾 (𝑥𝑦 ∧ ∀𝑧𝑦 (𝑥 ∈ dom (𝑀𝑁) ↔ 𝑧 ∈ dom (𝑀𝑁)))))
8350, 82mpd 15 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ((𝑥𝑌𝑎𝐽) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎)))) → ∃𝑦𝐾 (𝑥𝑦 ∧ ∀𝑧𝑦 (𝑥 ∈ dom (𝑀𝑁) ↔ 𝑧 ∈ dom (𝑀𝑁))))
8483anassrs 678 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥𝑌𝑎𝐽)) ∧ ((𝐹‘(𝑀𝑥)) ∈ 𝑎𝑡 ∈ (𝑆𝑎))) → ∃𝑦𝐾 (𝑥𝑦 ∧ ∀𝑧𝑦 (𝑥 ∈ dom (𝑀𝑁) ↔ 𝑧 ∈ dom (𝑀𝑁))))
8584expr 641 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥𝑌𝑎𝐽)) ∧ (𝐹‘(𝑀𝑥)) ∈ 𝑎) → (𝑡 ∈ (𝑆𝑎) → ∃𝑦𝐾 (𝑥𝑦 ∧ ∀𝑧𝑦 (𝑥 ∈ dom (𝑀𝑁) ↔ 𝑧 ∈ dom (𝑀𝑁)))))
8685exlimdv 1848 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥𝑌𝑎𝐽)) ∧ (𝐹‘(𝑀𝑥)) ∈ 𝑎) → (∃𝑡 𝑡 ∈ (𝑆𝑎) → ∃𝑦𝐾 (𝑥𝑦 ∧ ∀𝑧𝑦 (𝑥 ∈ dom (𝑀𝑁) ↔ 𝑧 ∈ dom (𝑀𝑁)))))
8726, 86syl5bi 231 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑥𝑌𝑎𝐽)) ∧ (𝐹‘(𝑀𝑥)) ∈ 𝑎) → ((𝑆𝑎) ≠ ∅ → ∃𝑦𝐾 (𝑥𝑦 ∧ ∀𝑧𝑦 (𝑥 ∈ dom (𝑀𝑁) ↔ 𝑧 ∈ dom (𝑀𝑁)))))
8887expimpd 627 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥𝑌𝑎𝐽)) → (((𝐹‘(𝑀𝑥)) ∈ 𝑎 ∧ (𝑆𝑎) ≠ ∅) → ∃𝑦𝐾 (𝑥𝑦 ∧ ∀𝑧𝑦 (𝑥 ∈ dom (𝑀𝑁) ↔ 𝑧 ∈ dom (𝑀𝑁)))))
8988anassrs 678 . . . . . . . . . . 11 (((𝜑𝑥𝑌) ∧ 𝑎𝐽) → (((𝐹‘(𝑀𝑥)) ∈ 𝑎 ∧ (𝑆𝑎) ≠ ∅) → ∃𝑦𝐾 (𝑥𝑦 ∧ ∀𝑧𝑦 (𝑥 ∈ dom (𝑀𝑁) ↔ 𝑧 ∈ dom (𝑀𝑁)))))
9089rexlimdva 3013 . . . . . . . . . 10 ((𝜑𝑥𝑌) → (∃𝑎𝐽 ((𝐹‘(𝑀𝑥)) ∈ 𝑎 ∧ (𝑆𝑎) ≠ ∅) → ∃𝑦𝐾 (𝑥𝑦 ∧ ∀𝑧𝑦 (𝑥 ∈ dom (𝑀𝑁) ↔ 𝑧 ∈ dom (𝑀𝑁)))))
9125, 90mpd 15 . . . . . . . . 9 ((𝜑𝑥𝑌) → ∃𝑦𝐾 (𝑥𝑦 ∧ ∀𝑧𝑦 (𝑥 ∈ dom (𝑀𝑁) ↔ 𝑧 ∈ dom (𝑀𝑁))))
9291ralrimiva 2949 . . . . . . . 8 (𝜑 → ∀𝑥𝑌𝑦𝐾 (𝑥𝑦 ∧ ∀𝑧𝑦 (𝑥 ∈ dom (𝑀𝑁) ↔ 𝑧 ∈ dom (𝑀𝑁))))
93 contop 21030 . . . . . . . . . 10 (𝐾 ∈ Con → 𝐾 ∈ Top)
9411, 93syl 17 . . . . . . . . 9 (𝜑𝐾 ∈ Top)
95 fndmin 6232 . . . . . . . . . . 11 ((𝑀 Fn 𝑌𝑁 Fn 𝑌) → dom (𝑀𝑁) = {𝑥𝑌 ∣ (𝑀𝑥) = (𝑁𝑥)})
966, 10, 95syl2anc 691 . . . . . . . . . 10 (𝜑 → dom (𝑀𝑁) = {𝑥𝑌 ∣ (𝑀𝑥) = (𝑁𝑥)})
97 ssrab2 3650 . . . . . . . . . 10 {𝑥𝑌 ∣ (𝑀𝑥) = (𝑁𝑥)} ⊆ 𝑌
9896, 97syl6eqss 3618 . . . . . . . . 9 (𝜑 → dom (𝑀𝑁) ⊆ 𝑌)
992isclo 20701 . . . . . . . . 9 ((𝐾 ∈ Top ∧ dom (𝑀𝑁) ⊆ 𝑌) → (dom (𝑀𝑁) ∈ (𝐾 ∩ (Clsd‘𝐾)) ↔ ∀𝑥𝑌𝑦𝐾 (𝑥𝑦 ∧ ∀𝑧𝑦 (𝑥 ∈ dom (𝑀𝑁) ↔ 𝑧 ∈ dom (𝑀𝑁)))))
10094, 98, 99syl2anc 691 . . . . . . . 8 (𝜑 → (dom (𝑀𝑁) ∈ (𝐾 ∩ (Clsd‘𝐾)) ↔ ∀𝑥𝑌𝑦𝐾 (𝑥𝑦 ∧ ∀𝑧𝑦 (𝑥 ∈ dom (𝑀𝑁) ↔ 𝑧 ∈ dom (𝑀𝑁)))))
10192, 100mpbird 246 . . . . . . 7 (𝜑 → dom (𝑀𝑁) ∈ (𝐾 ∩ (Clsd‘𝐾)))
10212, 101sseldi 3566 . . . . . 6 (𝜑 → dom (𝑀𝑁) ∈ 𝐾)
103 fveq2 6103 . . . . . . . . . . 11 (𝑥 = 𝑂 → (𝑀𝑥) = (𝑀𝑂))
104 fveq2 6103 . . . . . . . . . . 11 (𝑥 = 𝑂 → (𝑁𝑥) = (𝑁𝑂))
105103, 104eqeq12d 2625 . . . . . . . . . 10 (𝑥 = 𝑂 → ((𝑀𝑥) = (𝑁𝑥) ↔ (𝑀𝑂) = (𝑁𝑂)))
106105elrab 3331 . . . . . . . . 9 (𝑂 ∈ {𝑥𝑌 ∣ (𝑀𝑥) = (𝑁𝑥)} ↔ (𝑂𝑌 ∧ (𝑀𝑂) = (𝑁𝑂)))
10752, 54, 106sylanbrc 695 . . . . . . . 8 (𝜑𝑂 ∈ {𝑥𝑌 ∣ (𝑀𝑥) = (𝑁𝑥)})
108107, 96eleqtrrd 2691 . . . . . . 7 (𝜑𝑂 ∈ dom (𝑀𝑁))
109 ne0i 3880 . . . . . . 7 (𝑂 ∈ dom (𝑀𝑁) → dom (𝑀𝑁) ≠ ∅)
110108, 109syl 17 . . . . . 6 (𝜑 → dom (𝑀𝑁) ≠ ∅)
111 inss2 3796 . . . . . . 7 (𝐾 ∩ (Clsd‘𝐾)) ⊆ (Clsd‘𝐾)
112111, 101sseldi 3566 . . . . . 6 (𝜑 → dom (𝑀𝑁) ∈ (Clsd‘𝐾))
1132, 11, 102, 110, 112conclo 21028 . . . . 5 (𝜑 → dom (𝑀𝑁) = 𝑌)
114113, 96eqtr3d 2646 . . . 4 (𝜑𝑌 = {𝑥𝑌 ∣ (𝑀𝑥) = (𝑁𝑥)})
115 rabid2 3096 . . . 4 (𝑌 = {𝑥𝑌 ∣ (𝑀𝑥) = (𝑁𝑥)} ↔ ∀𝑥𝑌 (𝑀𝑥) = (𝑁𝑥))
116114, 115sylib 207 . . 3 (𝜑 → ∀𝑥𝑌 (𝑀𝑥) = (𝑁𝑥))
117116r19.21bi 2916 . 2 ((𝜑𝑥𝑌) → (𝑀𝑥) = (𝑁𝑥))
1186, 10, 117eqfnfvd 6222 1 (𝜑𝑀 = 𝑁)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383   ∧ w3a 1031   = wceq 1475  ∃wex 1695   ∈ wcel 1977   ≠ wne 2780  ∀wral 2896  ∃wrex 2897  {crab 2900   ∖ cdif 3537   ∩ cin 3539   ⊆ wss 3540  ∅c0 3874  𝒫 cpw 4108  {csn 4125  ∪ cuni 4372   ↦ cmpt 4643  ◡ccnv 5037  dom cdm 5038   ↾ cres 5040   “ cima 5041   ∘ ccom 5042   Fn wfn 5799  ⟶wf 5800  ‘cfv 5804  ℩crio 6510  (class class class)co 6549   ↾t crest 15904  Topctop 20517  Clsdccld 20630   Cn ccn 20838  Conccon 21024  𝑛-Locally cnlly 21078  Homeochmeo 21366   CovMap ccvm 30491 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-int 4411  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-om 6958  df-1st 7059  df-2nd 7060  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-oadd 7451  df-er 7629  df-map 7746  df-en 7842  df-fin 7845  df-fi 8200  df-rest 15906  df-topgen 15927  df-top 20521  df-bases 20522  df-topon 20523  df-cld 20633  df-nei 20712  df-cn 20841  df-con 21025  df-nlly 21080  df-hmeo 21368  df-cvm 30492 This theorem is referenced by:  cvmliftmoi  30519
 Copyright terms: Public domain W3C validator