Theorem cvmliftmolem1 35266

Description: Lemma for cvmliftmo 35269. (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 𝑘))))})
cvmliftmolem.2	⊢ ((𝜑 ∧ 𝜓) → 𝑇 ∈ (𝑆‘𝑈))
cvmliftmolem.3	⊢ ((𝜑 ∧ 𝜓) → 𝑊 ∈ 𝑇)
cvmliftmolem.4	⊢ ((𝜑 ∧ 𝜓) → 𝐼 ⊆ (◡𝑀 “ 𝑊))
cvmliftmolem.5	⊢ ((𝜑 ∧ 𝜓) → (𝐾 ↾t 𝐼) ∈ Conn)
cvmliftmolem.6	⊢ ((𝜑 ∧ 𝜓) → 𝑋 ∈ 𝐼)
cvmliftmolem.7	⊢ ((𝜑 ∧ 𝜓) → 𝑄 ∈ 𝐼)
cvmliftmolem.8	⊢ ((𝜑 ∧ 𝜓) → 𝑅 ∈ 𝐼)
cvmliftmolem.9	⊢ ((𝜑 ∧ 𝜓) → (𝐹‘(𝑀‘𝑋)) ∈ 𝑈)

Assertion

Ref	Expression
cvmliftmolem1	⊢ ((𝜑 ∧ 𝜓) → (𝑄 ∈ dom (𝑀 ∩ 𝑁) → 𝑅 ∈ dom (𝑀 ∩ 𝑁)))

Distinct variable groups:   𝑘,𝑠,𝑢,𝑣,𝐶   𝑘,𝐽,𝑠,𝑢,𝑣   𝑣,𝐵   𝐾,𝑠   𝑘,𝑀,𝑠,𝑢,𝑣   𝑁,𝑠   𝜑,𝑠   𝑘,𝐹,𝑠,𝑢,𝑣   𝑆,𝑠   𝑈,𝑘,𝑠,𝑢,𝑣   𝑇,𝑠,𝑢,𝑣   𝑢,𝑊,𝑣   𝑌,𝑠

Allowed substitution hints:   𝜑(𝑣,𝑢,𝑘)   𝜓(𝑣,𝑢,𝑘,𝑠)   𝐵(𝑢,𝑘,𝑠)   𝑄(𝑣,𝑢,𝑘,𝑠)   𝑅(𝑣,𝑢,𝑘,𝑠)   𝑆(𝑣,𝑢,𝑘)   𝑇(𝑘)   𝐼(𝑣,𝑢,𝑘,𝑠)   𝐾(𝑣,𝑢,𝑘)   𝑁(𝑣,𝑢,𝑘)   𝑂(𝑣,𝑢,𝑘,𝑠)   𝑊(𝑘,𝑠)   𝑋(𝑣,𝑢,𝑘,𝑠)   𝑌(𝑣,𝑢,𝑘)

Proof of Theorem cvmliftmolem1

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		cvmliftmoi.g	. . . . . . . . . 10 ⊢ (𝜑 → (𝐹 ∘ 𝑀) = (𝐹 ∘ 𝑁))
2	1	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝜓) → (𝐹 ∘ 𝑀) = (𝐹 ∘ 𝑁))
3	2	fveq1d 6909	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝜓) → ((𝐹 ∘ 𝑀)‘𝑅) = ((𝐹 ∘ 𝑁)‘𝑅))
4		cvmliftmolem.4	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜓) → 𝐼 ⊆ (◡𝑀 “ 𝑊))
5		cvmliftmolem.8	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜓) → 𝑅 ∈ 𝐼)
6	4, 5	sseldd 3996	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝜓) → 𝑅 ∈ (◡𝑀 “ 𝑊))
7		cvmliftmoi.m	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑀 ∈ (𝐾 Cn 𝐶))
8		cvmliftmo.y	. . . . . . . . . . . . . . 15 ⊢ 𝑌 = ∪ 𝐾
9		cvmliftmo.b	. . . . . . . . . . . . . . 15 ⊢ 𝐵 = ∪ 𝐶
10	8, 9	cnf 23270	. . . . . . . . . . . . . 14 ⊢ (𝑀 ∈ (𝐾 Cn 𝐶) → 𝑀:𝑌⟶𝐵)
11	7, 10	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑀:𝑌⟶𝐵)
12	11	ffnd 6738	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑀 Fn 𝑌)
13		elpreima 7078	. . . . . . . . . . . 12 ⊢ (𝑀 Fn 𝑌 → (𝑅 ∈ (◡𝑀 “ 𝑊) ↔ (𝑅 ∈ 𝑌 ∧ (𝑀‘𝑅) ∈ 𝑊)))
14	12, 13	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑅 ∈ (◡𝑀 “ 𝑊) ↔ (𝑅 ∈ 𝑌 ∧ (𝑀‘𝑅) ∈ 𝑊)))
15	14	simprbda 498	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑅 ∈ (◡𝑀 “ 𝑊)) → 𝑅 ∈ 𝑌)
16	6, 15	syldan 591	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝜓) → 𝑅 ∈ 𝑌)
17		fvco3 7008	. . . . . . . . . 10 ⊢ ((𝑀:𝑌⟶𝐵 ∧ 𝑅 ∈ 𝑌) → ((𝐹 ∘ 𝑀)‘𝑅) = (𝐹‘(𝑀‘𝑅)))
18	11, 17	sylan 580	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑅 ∈ 𝑌) → ((𝐹 ∘ 𝑀)‘𝑅) = (𝐹‘(𝑀‘𝑅)))
19	16, 18	syldan 591	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝜓) → ((𝐹 ∘ 𝑀)‘𝑅) = (𝐹‘(𝑀‘𝑅)))
20		cvmliftmoi.n	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑁 ∈ (𝐾 Cn 𝐶))
21	8, 9	cnf 23270	. . . . . . . . . . 11 ⊢ (𝑁 ∈ (𝐾 Cn 𝐶) → 𝑁:𝑌⟶𝐵)
22	20, 21	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝑁:𝑌⟶𝐵)
23		fvco3 7008	. . . . . . . . . 10 ⊢ ((𝑁:𝑌⟶𝐵 ∧ 𝑅 ∈ 𝑌) → ((𝐹 ∘ 𝑁)‘𝑅) = (𝐹‘(𝑁‘𝑅)))
24	22, 23	sylan 580	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑅 ∈ 𝑌) → ((𝐹 ∘ 𝑁)‘𝑅) = (𝐹‘(𝑁‘𝑅)))
25	16, 24	syldan 591	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝜓) → ((𝐹 ∘ 𝑁)‘𝑅) = (𝐹‘(𝑁‘𝑅)))
26	3, 19, 25	3eqtr3d 2783	. . . . . . 7 ⊢ ((𝜑 ∧ 𝜓) → (𝐹‘(𝑀‘𝑅)) = (𝐹‘(𝑁‘𝑅)))
27	26	adantr 480	. . . . . 6 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → (𝐹‘(𝑀‘𝑅)) = (𝐹‘(𝑁‘𝑅)))
28	14	simplbda 499	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑅 ∈ (◡𝑀 “ 𝑊)) → (𝑀‘𝑅) ∈ 𝑊)
29	6, 28	syldan 591	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝜓) → (𝑀‘𝑅) ∈ 𝑊)
30	29	adantr 480	. . . . . . 7 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → (𝑀‘𝑅) ∈ 𝑊)
31		fvres 6926	. . . . . . 7 ⊢ ((𝑀‘𝑅) ∈ 𝑊 → ((𝐹 ↾ 𝑊)‘(𝑀‘𝑅)) = (𝐹‘(𝑀‘𝑅)))
32	30, 31	syl 17	. . . . . 6 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → ((𝐹 ↾ 𝑊)‘(𝑀‘𝑅)) = (𝐹‘(𝑀‘𝑅)))
33	5	adantr 480	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → 𝑅 ∈ 𝐼)
34		fvres 6926	. . . . . . . . 9 ⊢ (𝑅 ∈ 𝐼 → ((𝑁 ↾ 𝐼)‘𝑅) = (𝑁‘𝑅))
35	33, 34	syl 17	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → ((𝑁 ↾ 𝐼)‘𝑅) = (𝑁‘𝑅))
36		eqid 2735	. . . . . . . . . . 11 ⊢ ∪ (𝐾 ↾t 𝐼) = ∪ (𝐾 ↾t 𝐼)
37		cvmliftmolem.5	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝜓) → (𝐾 ↾t 𝐼) ∈ Conn)
38	37	adantr 480	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → (𝐾 ↾t 𝐼) ∈ Conn)
39	20	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜓) → 𝑁 ∈ (𝐾 Cn 𝐶))
40		cnvimass 6102	. . . . . . . . . . . . . . . . 17 ⊢ (◡𝑀 “ 𝑊) ⊆ dom 𝑀
41	40, 11	fssdm 6756	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (◡𝑀 “ 𝑊) ⊆ 𝑌)
42	41	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝜓) → (◡𝑀 “ 𝑊) ⊆ 𝑌)
43	4, 42	sstrd 4006	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜓) → 𝐼 ⊆ 𝑌)
44	8	cnrest 23309	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ (𝐾 Cn 𝐶) ∧ 𝐼 ⊆ 𝑌) → (𝑁 ↾ 𝐼) ∈ ((𝐾 ↾t 𝐼) Cn 𝐶))
45	39, 43, 44	syl2anc 584	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝜓) → (𝑁 ↾ 𝐼) ∈ ((𝐾 ↾t 𝐼) Cn 𝐶))
46		cvmliftmo.f	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐹 ∈ (𝐶 CovMap 𝐽))
47	46	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝜓) → 𝐹 ∈ (𝐶 CovMap 𝐽))
48		cvmtop1 35245	. . . . . . . . . . . . . . . 16 ⊢ (𝐹 ∈ (𝐶 CovMap 𝐽) → 𝐶 ∈ Top)
49	47, 48	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝜓) → 𝐶 ∈ Top)
50	9	toptopon 22939	. . . . . . . . . . . . . . 15 ⊢ (𝐶 ∈ Top ↔ 𝐶 ∈ (TopOn‘𝐵))
51	49, 50	sylib 218	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜓) → 𝐶 ∈ (TopOn‘𝐵))
52		df-ima 5702	. . . . . . . . . . . . . . 15 ⊢ (𝑁 “ 𝐼) = ran (𝑁 ↾ 𝐼)
53		cvmliftmolem.3	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝜓) → 𝑊 ∈ 𝑇)
54		elssuni 4942	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑊 ∈ 𝑇 → 𝑊 ⊆ ∪ 𝑇)
55	53, 54	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝜓) → 𝑊 ⊆ ∪ 𝑇)
56		cvmliftmolem.2	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝜓) → 𝑇 ∈ (𝑆‘𝑈))
57		cvmliftmolem.1	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾t 𝑢)Homeo(𝐽 ↾t 𝑘))))})
58	57	cvmsuni 35254	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑇 ∈ (𝑆‘𝑈) → ∪ 𝑇 = (◡𝐹 “ 𝑈))
59	56, 58	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝜓) → ∪ 𝑇 = (◡𝐹 “ 𝑈))
60	55, 59	sseqtrd 4036	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝜓) → 𝑊 ⊆ (◡𝐹 “ 𝑈))
61		imass2 6123	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑊 ⊆ (◡𝐹 “ 𝑈) → (◡𝑀 “ 𝑊) ⊆ (◡𝑀 “ (◡𝐹 “ 𝑈)))
62	60, 61	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝜓) → (◡𝑀 “ 𝑊) ⊆ (◡𝑀 “ (◡𝐹 “ 𝑈)))
63	4, 62	sstrd 4006	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝜓) → 𝐼 ⊆ (◡𝑀 “ (◡𝐹 “ 𝑈)))
64	2	cnveqd 5889	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝜓) → ◡(𝐹 ∘ 𝑀) = ◡(𝐹 ∘ 𝑁))
65		cnvco 5899	. . . . . . . . . . . . . . . . . . . 20 ⊢ ◡(𝐹 ∘ 𝑀) = (◡𝑀 ∘ ◡𝐹)
66		cnvco 5899	. . . . . . . . . . . . . . . . . . . 20 ⊢ ◡(𝐹 ∘ 𝑁) = (◡𝑁 ∘ ◡𝐹)
67	64, 65, 66	3eqtr3g 2798	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝜓) → (◡𝑀 ∘ ◡𝐹) = (◡𝑁 ∘ ◡𝐹))
68	67	imaeq1d 6079	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝜓) → ((◡𝑀 ∘ ◡𝐹) “ 𝑈) = ((◡𝑁 ∘ ◡𝐹) “ 𝑈))
69		imaco 6273	. . . . . . . . . . . . . . . . . 18 ⊢ ((◡𝑀 ∘ ◡𝐹) “ 𝑈) = (◡𝑀 “ (◡𝐹 “ 𝑈))
70		imaco 6273	. . . . . . . . . . . . . . . . . 18 ⊢ ((◡𝑁 ∘ ◡𝐹) “ 𝑈) = (◡𝑁 “ (◡𝐹 “ 𝑈))
71	68, 69, 70	3eqtr3g 2798	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝜓) → (◡𝑀 “ (◡𝐹 “ 𝑈)) = (◡𝑁 “ (◡𝐹 “ 𝑈)))
72	63, 71	sseqtrd 4036	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝜓) → 𝐼 ⊆ (◡𝑁 “ (◡𝐹 “ 𝑈)))
73	22	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝜓) → 𝑁:𝑌⟶𝐵)
74	73	ffund 6741	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝜓) → Fun 𝑁)
75	73	fdmd 6747	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝜓) → dom 𝑁 = 𝑌)
76	43, 75	sseqtrrd 4037	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝜓) → 𝐼 ⊆ dom 𝑁)
77		funimass3 7074	. . . . . . . . . . . . . . . . 17 ⊢ ((Fun 𝑁 ∧ 𝐼 ⊆ dom 𝑁) → ((𝑁 “ 𝐼) ⊆ (◡𝐹 “ 𝑈) ↔ 𝐼 ⊆ (◡𝑁 “ (◡𝐹 “ 𝑈))))
78	74, 76, 77	syl2anc 584	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝜓) → ((𝑁 “ 𝐼) ⊆ (◡𝐹 “ 𝑈) ↔ 𝐼 ⊆ (◡𝑁 “ (◡𝐹 “ 𝑈))))
79	72, 78	mpbird 257	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝜓) → (𝑁 “ 𝐼) ⊆ (◡𝐹 “ 𝑈))
80	52, 79	eqsstrrid 4045	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜓) → ran (𝑁 ↾ 𝐼) ⊆ (◡𝐹 “ 𝑈))
81		cnvimass 6102	. . . . . . . . . . . . . . 15 ⊢ (◡𝐹 “ 𝑈) ⊆ dom 𝐹
82		cvmcn 35247	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐹 ∈ (𝐶 CovMap 𝐽) → 𝐹 ∈ (𝐶 Cn 𝐽))
83	46, 82	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐹 ∈ (𝐶 Cn 𝐽))
84		eqid 2735	. . . . . . . . . . . . . . . . . . 19 ⊢ ∪ 𝐽 = ∪ 𝐽
85	9, 84	cnf 23270	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐹 ∈ (𝐶 Cn 𝐽) → 𝐹:𝐵⟶∪ 𝐽)
86	83, 85	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐹:𝐵⟶∪ 𝐽)
87	86	fdmd 6747	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → dom 𝐹 = 𝐵)
88	87	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝜓) → dom 𝐹 = 𝐵)
89	81, 88	sseqtrid 4048	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜓) → (◡𝐹 “ 𝑈) ⊆ 𝐵)
90		cnrest2 23310	. . . . . . . . . . . . . 14 ⊢ ((𝐶 ∈ (TopOn‘𝐵) ∧ ran (𝑁 ↾ 𝐼) ⊆ (◡𝐹 “ 𝑈) ∧ (◡𝐹 “ 𝑈) ⊆ 𝐵) → ((𝑁 ↾ 𝐼) ∈ ((𝐾 ↾t 𝐼) Cn 𝐶) ↔ (𝑁 ↾ 𝐼) ∈ ((𝐾 ↾t 𝐼) Cn (𝐶 ↾t (◡𝐹 “ 𝑈)))))
91	51, 80, 89, 90	syl3anc 1370	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝜓) → ((𝑁 ↾ 𝐼) ∈ ((𝐾 ↾t 𝐼) Cn 𝐶) ↔ (𝑁 ↾ 𝐼) ∈ ((𝐾 ↾t 𝐼) Cn (𝐶 ↾t (◡𝐹 “ 𝑈)))))
92	45, 91	mpbid 232	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝜓) → (𝑁 ↾ 𝐼) ∈ ((𝐾 ↾t 𝐼) Cn (𝐶 ↾t (◡𝐹 “ 𝑈))))
93	92	adantr 480	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → (𝑁 ↾ 𝐼) ∈ ((𝐾 ↾t 𝐼) Cn (𝐶 ↾t (◡𝐹 “ 𝑈))))
94		dfss2 3981	. . . . . . . . . . . . . 14 ⊢ (𝑊 ⊆ (◡𝐹 “ 𝑈) ↔ (𝑊 ∩ (◡𝐹 “ 𝑈)) = 𝑊)
95	60, 94	sylib 218	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝜓) → (𝑊 ∩ (◡𝐹 “ 𝑈)) = 𝑊)
96	9	topopn 22928	. . . . . . . . . . . . . . . 16 ⊢ (𝐶 ∈ Top → 𝐵 ∈ 𝐶)
97	49, 96	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝜓) → 𝐵 ∈ 𝐶)
98	97, 89	ssexd 5330	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜓) → (◡𝐹 “ 𝑈) ∈ V)
99	57	cvmsss 35252	. . . . . . . . . . . . . . . 16 ⊢ (𝑇 ∈ (𝑆‘𝑈) → 𝑇 ⊆ 𝐶)
100	56, 99	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝜓) → 𝑇 ⊆ 𝐶)
101	100, 53	sseldd 3996	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜓) → 𝑊 ∈ 𝐶)
102		elrestr 17475	. . . . . . . . . . . . . 14 ⊢ ((𝐶 ∈ Top ∧ (◡𝐹 “ 𝑈) ∈ V ∧ 𝑊 ∈ 𝐶) → (𝑊 ∩ (◡𝐹 “ 𝑈)) ∈ (𝐶 ↾t (◡𝐹 “ 𝑈)))
103	49, 98, 101, 102	syl3anc 1370	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝜓) → (𝑊 ∩ (◡𝐹 “ 𝑈)) ∈ (𝐶 ↾t (◡𝐹 “ 𝑈)))
104	95, 103	eqeltrrd 2840	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝜓) → 𝑊 ∈ (𝐶 ↾t (◡𝐹 “ 𝑈)))
105	104	adantr 480	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → 𝑊 ∈ (𝐶 ↾t (◡𝐹 “ 𝑈)))
106	57	cvmscld 35258	. . . . . . . . . . . . 13 ⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑇 ∈ (𝑆‘𝑈) ∧ 𝑊 ∈ 𝑇) → 𝑊 ∈ (Clsd‘(𝐶 ↾t (◡𝐹 “ 𝑈))))
107	47, 56, 53, 106	syl3anc 1370	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝜓) → 𝑊 ∈ (Clsd‘(𝐶 ↾t (◡𝐹 “ 𝑈))))
108	107	adantr 480	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → 𝑊 ∈ (Clsd‘(𝐶 ↾t (◡𝐹 “ 𝑈))))
109		cvmliftmolem.7	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝜓) → 𝑄 ∈ 𝐼)
110		cvmliftmo.k	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐾 ∈ Conn)
111		conntop 23441	. . . . . . . . . . . . . . . 16 ⊢ (𝐾 ∈ Conn → 𝐾 ∈ Top)
112	110, 111	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐾 ∈ Top)
113	112	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜓) → 𝐾 ∈ Top)
114	8	restuni 23186	. . . . . . . . . . . . . 14 ⊢ ((𝐾 ∈ Top ∧ 𝐼 ⊆ 𝑌) → 𝐼 = ∪ (𝐾 ↾t 𝐼))
115	113, 43, 114	syl2anc 584	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝜓) → 𝐼 = ∪ (𝐾 ↾t 𝐼))
116	109, 115	eleqtrd 2841	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝜓) → 𝑄 ∈ ∪ (𝐾 ↾t 𝐼))
117	116	adantr 480	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → 𝑄 ∈ ∪ (𝐾 ↾t 𝐼))
118	109	adantr 480	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → 𝑄 ∈ 𝐼)
119		fvres 6926	. . . . . . . . . . . . 13 ⊢ (𝑄 ∈ 𝐼 → ((𝑁 ↾ 𝐼)‘𝑄) = (𝑁‘𝑄))
120	118, 119	syl 17	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → ((𝑁 ↾ 𝐼)‘𝑄) = (𝑁‘𝑄))
121		simpr 484	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → (𝑀‘𝑄) = (𝑁‘𝑄))
122	4, 109	sseldd 3996	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝜓) → 𝑄 ∈ (◡𝑀 “ 𝑊))
123		elpreima 7078	. . . . . . . . . . . . . . . . 17 ⊢ (𝑀 Fn 𝑌 → (𝑄 ∈ (◡𝑀 “ 𝑊) ↔ (𝑄 ∈ 𝑌 ∧ (𝑀‘𝑄) ∈ 𝑊)))
124	12, 123	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑄 ∈ (◡𝑀 “ 𝑊) ↔ (𝑄 ∈ 𝑌 ∧ (𝑀‘𝑄) ∈ 𝑊)))
125	124	simplbda 499	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑄 ∈ (◡𝑀 “ 𝑊)) → (𝑀‘𝑄) ∈ 𝑊)
126	122, 125	syldan 591	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜓) → (𝑀‘𝑄) ∈ 𝑊)
127	126	adantr 480	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → (𝑀‘𝑄) ∈ 𝑊)
128	121, 127	eqeltrrd 2840	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → (𝑁‘𝑄) ∈ 𝑊)
129	120, 128	eqeltrd 2839	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → ((𝑁 ↾ 𝐼)‘𝑄) ∈ 𝑊)
130	36, 38, 93, 105, 108, 117, 129	conncn 23450	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → (𝑁 ↾ 𝐼):∪ (𝐾 ↾t 𝐼)⟶𝑊)
131	115	adantr 480	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → 𝐼 = ∪ (𝐾 ↾t 𝐼))
132	131	feq2d 6723	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → ((𝑁 ↾ 𝐼):𝐼⟶𝑊 ↔ (𝑁 ↾ 𝐼):∪ (𝐾 ↾t 𝐼)⟶𝑊))
133	130, 132	mpbird 257	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → (𝑁 ↾ 𝐼):𝐼⟶𝑊)
134	133, 33	ffvelcdmd 7105	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → ((𝑁 ↾ 𝐼)‘𝑅) ∈ 𝑊)
135	35, 134	eqeltrrd 2840	. . . . . . 7 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → (𝑁‘𝑅) ∈ 𝑊)
136		fvres 6926	. . . . . . 7 ⊢ ((𝑁‘𝑅) ∈ 𝑊 → ((𝐹 ↾ 𝑊)‘(𝑁‘𝑅)) = (𝐹‘(𝑁‘𝑅)))
137	135, 136	syl 17	. . . . . 6 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → ((𝐹 ↾ 𝑊)‘(𝑁‘𝑅)) = (𝐹‘(𝑁‘𝑅)))
138	27, 32, 137	3eqtr4d 2785	. . . . 5 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → ((𝐹 ↾ 𝑊)‘(𝑀‘𝑅)) = ((𝐹 ↾ 𝑊)‘(𝑁‘𝑅)))
139	57	cvmsf1o 35257	. . . . . . . . 9 ⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑇 ∈ (𝑆‘𝑈) ∧ 𝑊 ∈ 𝑇) → (𝐹 ↾ 𝑊):𝑊–1-1-onto→𝑈)
140	47, 56, 53, 139	syl3anc 1370	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝜓) → (𝐹 ↾ 𝑊):𝑊–1-1-onto→𝑈)
141		f1of1 6848	. . . . . . . 8 ⊢ ((𝐹 ↾ 𝑊):𝑊–1-1-onto→𝑈 → (𝐹 ↾ 𝑊):𝑊–1-1→𝑈)
142	140, 141	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ 𝜓) → (𝐹 ↾ 𝑊):𝑊–1-1→𝑈)
143	142	adantr 480	. . . . . 6 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → (𝐹 ↾ 𝑊):𝑊–1-1→𝑈)
144		f1fveq 7282	. . . . . 6 ⊢ (((𝐹 ↾ 𝑊):𝑊–1-1→𝑈 ∧ ((𝑀‘𝑅) ∈ 𝑊 ∧ (𝑁‘𝑅) ∈ 𝑊)) → (((𝐹 ↾ 𝑊)‘(𝑀‘𝑅)) = ((𝐹 ↾ 𝑊)‘(𝑁‘𝑅)) ↔ (𝑀‘𝑅) = (𝑁‘𝑅)))
145	143, 30, 135, 144	syl12anc 837	. . . . 5 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → (((𝐹 ↾ 𝑊)‘(𝑀‘𝑅)) = ((𝐹 ↾ 𝑊)‘(𝑁‘𝑅)) ↔ (𝑀‘𝑅) = (𝑁‘𝑅)))
146	138, 145	mpbid 232	. . . 4 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → (𝑀‘𝑅) = (𝑁‘𝑅))
147	146	ex 412	. . 3 ⊢ ((𝜑 ∧ 𝜓) → ((𝑀‘𝑄) = (𝑁‘𝑄) → (𝑀‘𝑅) = (𝑁‘𝑅)))
148	124	simprbda 498	. . . . 5 ⊢ ((𝜑 ∧ 𝑄 ∈ (◡𝑀 “ 𝑊)) → 𝑄 ∈ 𝑌)
149	122, 148	syldan 591	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝑄 ∈ 𝑌)
150		fveq2 6907	. . . . . 6 ⊢ (𝑥 = 𝑄 → (𝑀‘𝑥) = (𝑀‘𝑄))
151		fveq2 6907	. . . . . 6 ⊢ (𝑥 = 𝑄 → (𝑁‘𝑥) = (𝑁‘𝑄))
152	150, 151	eqeq12d 2751	. . . . 5 ⊢ (𝑥 = 𝑄 → ((𝑀‘𝑥) = (𝑁‘𝑥) ↔ (𝑀‘𝑄) = (𝑁‘𝑄)))
153	152	elrab3 3696	. . . 4 ⊢ (𝑄 ∈ 𝑌 → (𝑄 ∈ {𝑥 ∈ 𝑌 ∣ (𝑀‘𝑥) = (𝑁‘𝑥)} ↔ (𝑀‘𝑄) = (𝑁‘𝑄)))
154	149, 153	syl 17	. . 3 ⊢ ((𝜑 ∧ 𝜓) → (𝑄 ∈ {𝑥 ∈ 𝑌 ∣ (𝑀‘𝑥) = (𝑁‘𝑥)} ↔ (𝑀‘𝑄) = (𝑁‘𝑄)))
155		fveq2 6907	. . . . . 6 ⊢ (𝑥 = 𝑅 → (𝑀‘𝑥) = (𝑀‘𝑅))
156		fveq2 6907	. . . . . 6 ⊢ (𝑥 = 𝑅 → (𝑁‘𝑥) = (𝑁‘𝑅))
157	155, 156	eqeq12d 2751	. . . . 5 ⊢ (𝑥 = 𝑅 → ((𝑀‘𝑥) = (𝑁‘𝑥) ↔ (𝑀‘𝑅) = (𝑁‘𝑅)))
158	157	elrab3 3696	. . . 4 ⊢ (𝑅 ∈ 𝑌 → (𝑅 ∈ {𝑥 ∈ 𝑌 ∣ (𝑀‘𝑥) = (𝑁‘𝑥)} ↔ (𝑀‘𝑅) = (𝑁‘𝑅)))
159	16, 158	syl 17	. . 3 ⊢ ((𝜑 ∧ 𝜓) → (𝑅 ∈ {𝑥 ∈ 𝑌 ∣ (𝑀‘𝑥) = (𝑁‘𝑥)} ↔ (𝑀‘𝑅) = (𝑁‘𝑅)))
160	147, 154, 159	3imtr4d 294	. 2 ⊢ ((𝜑 ∧ 𝜓) → (𝑄 ∈ {𝑥 ∈ 𝑌 ∣ (𝑀‘𝑥) = (𝑁‘𝑥)} → 𝑅 ∈ {𝑥 ∈ 𝑌 ∣ (𝑀‘𝑥) = (𝑁‘𝑥)}))
161	22	ffnd 6738	. . . . 5 ⊢ (𝜑 → 𝑁 Fn 𝑌)
162		fndmin 7065	. . . . 5 ⊢ ((𝑀 Fn 𝑌 ∧ 𝑁 Fn 𝑌) → dom (𝑀 ∩ 𝑁) = {𝑥 ∈ 𝑌 ∣ (𝑀‘𝑥) = (𝑁‘𝑥)})
163	12, 161, 162	syl2anc 584	. . . 4 ⊢ (𝜑 → dom (𝑀 ∩ 𝑁) = {𝑥 ∈ 𝑌 ∣ (𝑀‘𝑥) = (𝑁‘𝑥)})
164	163	adantr 480	. . 3 ⊢ ((𝜑 ∧ 𝜓) → dom (𝑀 ∩ 𝑁) = {𝑥 ∈ 𝑌 ∣ (𝑀‘𝑥) = (𝑁‘𝑥)})
165	164	eleq2d 2825	. 2 ⊢ ((𝜑 ∧ 𝜓) → (𝑄 ∈ dom (𝑀 ∩ 𝑁) ↔ 𝑄 ∈ {𝑥 ∈ 𝑌 ∣ (𝑀‘𝑥) = (𝑁‘𝑥)}))
166	164	eleq2d 2825	. 2 ⊢ ((𝜑 ∧ 𝜓) → (𝑅 ∈ dom (𝑀 ∩ 𝑁) ↔ 𝑅 ∈ {𝑥 ∈ 𝑌 ∣ (𝑀‘𝑥) = (𝑁‘𝑥)}))
167	160, 165, 166	3imtr4d 294	1 ⊢ ((𝜑 ∧ 𝜓) → (𝑄 ∈ dom (𝑀 ∩ 𝑁) → 𝑅 ∈ dom (𝑀 ∩ 𝑁)))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1537   ∈ wcel 2106  ∀wral 3059  {crab 3433  Vcvv 3478   ∖ cdif 3960   ∩ cin 3962   ⊆ wss 3963  ∅c0 4339  𝒫 cpw 4605  {csn 4631  ∪ cuni 4912   ↦ cmpt 5231  ^◡ccnv 5688  dom cdm 5689  ran crn 5690   ↾ cres 5691   “ cima 5692   ∘ ccom 5693  Fun wfun 6557   Fn wfn 6558  ⟶wf 6559  –1-1→wf1 6560  –1-1-onto→wf1o 6562  ‘cfv 6563  (class class class)co 7431   ↾_t crest 17467  Topctop 22915  TopOnctopon 22932  Clsdccld 23040   Cn ccn 23248  Conncconn 23435  𝑛-Locally cnlly 23489  Homeochmeo 23777   CovMap ccvm 35240

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-rep 5285  ax-sep 5302  ax-nul 5312  ax-pow 5371  ax-pr 5438  ax-un 7754

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ne 2939  df-ral 3060  df-rex 3069  df-reu 3379  df-rab 3434  df-v 3480  df-sbc 3792  df-csb 3909  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-pss 3983  df-nul 4340  df-if 4532  df-pw 4607  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-int 4952  df-iun 4998  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5583  df-eprel 5589  df-po 5597  df-so 5598  df-fr 5641  df-we 5643  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-res 5701  df-ima 5702  df-ord 6389  df-on 6390  df-lim 6391  df-suc 6392  df-iota 6516  df-fun 6565  df-fn 6566  df-f 6567  df-f1 6568  df-fo 6569  df-f1o 6570  df-fv 6571  df-ov 7434  df-oprab 7435  df-mpo 7436  df-om 7888  df-1st 8013  df-2nd 8014  df-map 8867  df-en 8985  df-fin 8988  df-fi 9449  df-rest 17469  df-topgen 17490  df-top 22916  df-topon 22933  df-bases 22969  df-cld 23043  df-cn 23251  df-conn 23436  df-hmeo 23779  df-cvm 35241

This theorem is referenced by:  cvmliftmolem2  35267