Theorem cvmliftmolem1 35308

Description: Lemma for cvmliftmo 35311. (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 6883	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝜓) → ((𝐹 ∘ 𝑀)‘𝑅) = ((𝐹 ∘ 𝑁)‘𝑅))
4		cvmliftmolem.4	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜓) → 𝐼 ⊆ (◡𝑀 “ 𝑊))
5		cvmliftmolem.8	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜓) → 𝑅 ∈ 𝐼)
6	4, 5	sseldd 3964	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝜓) → 𝑅 ∈ (◡𝑀 “ 𝑊))
7		cvmliftmoi.m	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑀 ∈ (𝐾 Cn 𝐶))
8		cvmliftmo.y	. . . . . . . . . . . . . . 15 ⊢ 𝑌 = ∪ 𝐾
9		cvmliftmo.b	. . . . . . . . . . . . . . 15 ⊢ 𝐵 = ∪ 𝐶
10	8, 9	cnf 23189	. . . . . . . . . . . . . 14 ⊢ (𝑀 ∈ (𝐾 Cn 𝐶) → 𝑀:𝑌⟶𝐵)
11	7, 10	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑀:𝑌⟶𝐵)
12	11	ffnd 6712	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑀 Fn 𝑌)
13		elpreima 7053	. . . . . . . . . . . 12 ⊢ (𝑀 Fn 𝑌 → (𝑅 ∈ (◡𝑀 “ 𝑊) ↔ (𝑅 ∈ 𝑌 ∧ (𝑀‘𝑅) ∈ 𝑊)))
14	12, 13	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑅 ∈ (◡𝑀 “ 𝑊) ↔ (𝑅 ∈ 𝑌 ∧ (𝑀‘𝑅) ∈ 𝑊)))
15	14	simprbda 498	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑅 ∈ (◡𝑀 “ 𝑊)) → 𝑅 ∈ 𝑌)
16	6, 15	syldan 591	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝜓) → 𝑅 ∈ 𝑌)
17		fvco3 6983	. . . . . . . . . 10 ⊢ ((𝑀:𝑌⟶𝐵 ∧ 𝑅 ∈ 𝑌) → ((𝐹 ∘ 𝑀)‘𝑅) = (𝐹‘(𝑀‘𝑅)))
18	11, 17	sylan 580	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑅 ∈ 𝑌) → ((𝐹 ∘ 𝑀)‘𝑅) = (𝐹‘(𝑀‘𝑅)))
19	16, 18	syldan 591	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝜓) → ((𝐹 ∘ 𝑀)‘𝑅) = (𝐹‘(𝑀‘𝑅)))
20		cvmliftmoi.n	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑁 ∈ (𝐾 Cn 𝐶))
21	8, 9	cnf 23189	. . . . . . . . . . 11 ⊢ (𝑁 ∈ (𝐾 Cn 𝐶) → 𝑁:𝑌⟶𝐵)
22	20, 21	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝑁:𝑌⟶𝐵)
23		fvco3 6983	. . . . . . . . . 10 ⊢ ((𝑁:𝑌⟶𝐵 ∧ 𝑅 ∈ 𝑌) → ((𝐹 ∘ 𝑁)‘𝑅) = (𝐹‘(𝑁‘𝑅)))
24	22, 23	sylan 580	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑅 ∈ 𝑌) → ((𝐹 ∘ 𝑁)‘𝑅) = (𝐹‘(𝑁‘𝑅)))
25	16, 24	syldan 591	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝜓) → ((𝐹 ∘ 𝑁)‘𝑅) = (𝐹‘(𝑁‘𝑅)))
26	3, 19, 25	3eqtr3d 2779	. . . . . . 7 ⊢ ((𝜑 ∧ 𝜓) → (𝐹‘(𝑀‘𝑅)) = (𝐹‘(𝑁‘𝑅)))
27	26	adantr 480	. . . . . 6 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → (𝐹‘(𝑀‘𝑅)) = (𝐹‘(𝑁‘𝑅)))
28	14	simplbda 499	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑅 ∈ (◡𝑀 “ 𝑊)) → (𝑀‘𝑅) ∈ 𝑊)
29	6, 28	syldan 591	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝜓) → (𝑀‘𝑅) ∈ 𝑊)
30	29	adantr 480	. . . . . . 7 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → (𝑀‘𝑅) ∈ 𝑊)
31		fvres 6900	. . . . . . 7 ⊢ ((𝑀‘𝑅) ∈ 𝑊 → ((𝐹 ↾ 𝑊)‘(𝑀‘𝑅)) = (𝐹‘(𝑀‘𝑅)))
32	30, 31	syl 17	. . . . . 6 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → ((𝐹 ↾ 𝑊)‘(𝑀‘𝑅)) = (𝐹‘(𝑀‘𝑅)))
33	5	adantr 480	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → 𝑅 ∈ 𝐼)
34		fvres 6900	. . . . . . . . 9 ⊢ (𝑅 ∈ 𝐼 → ((𝑁 ↾ 𝐼)‘𝑅) = (𝑁‘𝑅))
35	33, 34	syl 17	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → ((𝑁 ↾ 𝐼)‘𝑅) = (𝑁‘𝑅))
36		eqid 2736	. . . . . . . . . . 11 ⊢ ∪ (𝐾 ↾t 𝐼) = ∪ (𝐾 ↾t 𝐼)
37		cvmliftmolem.5	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝜓) → (𝐾 ↾t 𝐼) ∈ Conn)
38	37	adantr 480	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → (𝐾 ↾t 𝐼) ∈ Conn)
39	20	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜓) → 𝑁 ∈ (𝐾 Cn 𝐶))
40		cnvimass 6074	. . . . . . . . . . . . . . . . 17 ⊢ (◡𝑀 “ 𝑊) ⊆ dom 𝑀
41	40, 11	fssdm 6730	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (◡𝑀 “ 𝑊) ⊆ 𝑌)
42	41	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝜓) → (◡𝑀 “ 𝑊) ⊆ 𝑌)
43	4, 42	sstrd 3974	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜓) → 𝐼 ⊆ 𝑌)
44	8	cnrest 23228	. . . . . . . . . . . . . 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 35287	. . . . . . . . . . . . . . . 16 ⊢ (𝐹 ∈ (𝐶 CovMap 𝐽) → 𝐶 ∈ Top)
49	47, 48	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝜓) → 𝐶 ∈ Top)
50	9	toptopon 22860	. . . . . . . . . . . . . . 15 ⊢ (𝐶 ∈ Top ↔ 𝐶 ∈ (TopOn‘𝐵))
51	49, 50	sylib 218	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜓) → 𝐶 ∈ (TopOn‘𝐵))
52		df-ima 5672	. . . . . . . . . . . . . . 15 ⊢ (𝑁 “ 𝐼) = ran (𝑁 ↾ 𝐼)
53		cvmliftmolem.3	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝜓) → 𝑊 ∈ 𝑇)
54		elssuni 4918	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑊 ∈ 𝑇 → 𝑊 ⊆ ∪ 𝑇)
55	53, 54	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝜓) → 𝑊 ⊆ ∪ 𝑇)
56		cvmliftmolem.2	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝜓) → 𝑇 ∈ (𝑆‘𝑈))
57		cvmliftmolem.1	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾t 𝑢)Homeo(𝐽 ↾t 𝑘))))})
58	57	cvmsuni 35296	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑇 ∈ (𝑆‘𝑈) → ∪ 𝑇 = (◡𝐹 “ 𝑈))
59	56, 58	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝜓) → ∪ 𝑇 = (◡𝐹 “ 𝑈))
60	55, 59	sseqtrd 4000	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝜓) → 𝑊 ⊆ (◡𝐹 “ 𝑈))
61		imass2 6094	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑊 ⊆ (◡𝐹 “ 𝑈) → (◡𝑀 “ 𝑊) ⊆ (◡𝑀 “ (◡𝐹 “ 𝑈)))
62	60, 61	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝜓) → (◡𝑀 “ 𝑊) ⊆ (◡𝑀 “ (◡𝐹 “ 𝑈)))
63	4, 62	sstrd 3974	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝜓) → 𝐼 ⊆ (◡𝑀 “ (◡𝐹 “ 𝑈)))
64	2	cnveqd 5860	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝜓) → ◡(𝐹 ∘ 𝑀) = ◡(𝐹 ∘ 𝑁))
65		cnvco 5870	. . . . . . . . . . . . . . . . . . . 20 ⊢ ◡(𝐹 ∘ 𝑀) = (◡𝑀 ∘ ◡𝐹)
66		cnvco 5870	. . . . . . . . . . . . . . . . . . . 20 ⊢ ◡(𝐹 ∘ 𝑁) = (◡𝑁 ∘ ◡𝐹)
67	64, 65, 66	3eqtr3g 2794	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝜓) → (◡𝑀 ∘ ◡𝐹) = (◡𝑁 ∘ ◡𝐹))
68	67	imaeq1d 6051	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝜓) → ((◡𝑀 ∘ ◡𝐹) “ 𝑈) = ((◡𝑁 ∘ ◡𝐹) “ 𝑈))
69		imaco 6245	. . . . . . . . . . . . . . . . . 18 ⊢ ((◡𝑀 ∘ ◡𝐹) “ 𝑈) = (◡𝑀 “ (◡𝐹 “ 𝑈))
70		imaco 6245	. . . . . . . . . . . . . . . . . 18 ⊢ ((◡𝑁 ∘ ◡𝐹) “ 𝑈) = (◡𝑁 “ (◡𝐹 “ 𝑈))
71	68, 69, 70	3eqtr3g 2794	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝜓) → (◡𝑀 “ (◡𝐹 “ 𝑈)) = (◡𝑁 “ (◡𝐹 “ 𝑈)))
72	63, 71	sseqtrd 4000	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝜓) → 𝐼 ⊆ (◡𝑁 “ (◡𝐹 “ 𝑈)))
73	22	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝜓) → 𝑁:𝑌⟶𝐵)
74	73	ffund 6715	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝜓) → Fun 𝑁)
75	73	fdmd 6721	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝜓) → dom 𝑁 = 𝑌)
76	43, 75	sseqtrrd 4001	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝜓) → 𝐼 ⊆ dom 𝑁)
77		funimass3 7049	. . . . . . . . . . . . . . . . 17 ⊢ ((Fun 𝑁 ∧ 𝐼 ⊆ dom 𝑁) → ((𝑁 “ 𝐼) ⊆ (◡𝐹 “ 𝑈) ↔ 𝐼 ⊆ (◡𝑁 “ (◡𝐹 “ 𝑈))))
78	74, 76, 77	syl2anc 584	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝜓) → ((𝑁 “ 𝐼) ⊆ (◡𝐹 “ 𝑈) ↔ 𝐼 ⊆ (◡𝑁 “ (◡𝐹 “ 𝑈))))
79	72, 78	mpbird 257	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝜓) → (𝑁 “ 𝐼) ⊆ (◡𝐹 “ 𝑈))
80	52, 79	eqsstrrid 4003	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜓) → ran (𝑁 ↾ 𝐼) ⊆ (◡𝐹 “ 𝑈))
81		cnvimass 6074	. . . . . . . . . . . . . . 15 ⊢ (◡𝐹 “ 𝑈) ⊆ dom 𝐹
82		cvmcn 35289	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐹 ∈ (𝐶 CovMap 𝐽) → 𝐹 ∈ (𝐶 Cn 𝐽))
83	46, 82	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐹 ∈ (𝐶 Cn 𝐽))
84		eqid 2736	. . . . . . . . . . . . . . . . . . 19 ⊢ ∪ 𝐽 = ∪ 𝐽
85	9, 84	cnf 23189	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐹 ∈ (𝐶 Cn 𝐽) → 𝐹:𝐵⟶∪ 𝐽)
86	83, 85	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐹:𝐵⟶∪ 𝐽)
87	86	fdmd 6721	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → dom 𝐹 = 𝐵)
88	87	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝜓) → dom 𝐹 = 𝐵)
89	81, 88	sseqtrid 4006	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜓) → (◡𝐹 “ 𝑈) ⊆ 𝐵)
90		cnrest2 23229	. . . . . . . . . . . . . 14 ⊢ ((𝐶 ∈ (TopOn‘𝐵) ∧ ran (𝑁 ↾ 𝐼) ⊆ (◡𝐹 “ 𝑈) ∧ (◡𝐹 “ 𝑈) ⊆ 𝐵) → ((𝑁 ↾ 𝐼) ∈ ((𝐾 ↾t 𝐼) Cn 𝐶) ↔ (𝑁 ↾ 𝐼) ∈ ((𝐾 ↾t 𝐼) Cn (𝐶 ↾t (◡𝐹 “ 𝑈)))))
91	51, 80, 89, 90	syl3anc 1373	. . . . . . . . . . . . 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 3949	. . . . . . . . . . . . . 14 ⊢ (𝑊 ⊆ (◡𝐹 “ 𝑈) ↔ (𝑊 ∩ (◡𝐹 “ 𝑈)) = 𝑊)
95	60, 94	sylib 218	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝜓) → (𝑊 ∩ (◡𝐹 “ 𝑈)) = 𝑊)
96	9	topopn 22849	. . . . . . . . . . . . . . . 16 ⊢ (𝐶 ∈ Top → 𝐵 ∈ 𝐶)
97	49, 96	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝜓) → 𝐵 ∈ 𝐶)
98	97, 89	ssexd 5299	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜓) → (◡𝐹 “ 𝑈) ∈ V)
99	57	cvmsss 35294	. . . . . . . . . . . . . . . 16 ⊢ (𝑇 ∈ (𝑆‘𝑈) → 𝑇 ⊆ 𝐶)
100	56, 99	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝜓) → 𝑇 ⊆ 𝐶)
101	100, 53	sseldd 3964	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜓) → 𝑊 ∈ 𝐶)
102		elrestr 17447	. . . . . . . . . . . . . 14 ⊢ ((𝐶 ∈ Top ∧ (◡𝐹 “ 𝑈) ∈ V ∧ 𝑊 ∈ 𝐶) → (𝑊 ∩ (◡𝐹 “ 𝑈)) ∈ (𝐶 ↾t (◡𝐹 “ 𝑈)))
103	49, 98, 101, 102	syl3anc 1373	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝜓) → (𝑊 ∩ (◡𝐹 “ 𝑈)) ∈ (𝐶 ↾t (◡𝐹 “ 𝑈)))
104	95, 103	eqeltrrd 2836	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝜓) → 𝑊 ∈ (𝐶 ↾t (◡𝐹 “ 𝑈)))
105	104	adantr 480	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → 𝑊 ∈ (𝐶 ↾t (◡𝐹 “ 𝑈)))
106	57	cvmscld 35300	. . . . . . . . . . . . 13 ⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑇 ∈ (𝑆‘𝑈) ∧ 𝑊 ∈ 𝑇) → 𝑊 ∈ (Clsd‘(𝐶 ↾t (◡𝐹 “ 𝑈))))
107	47, 56, 53, 106	syl3anc 1373	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝜓) → 𝑊 ∈ (Clsd‘(𝐶 ↾t (◡𝐹 “ 𝑈))))
108	107	adantr 480	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → 𝑊 ∈ (Clsd‘(𝐶 ↾t (◡𝐹 “ 𝑈))))
109		cvmliftmolem.7	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝜓) → 𝑄 ∈ 𝐼)
110		cvmliftmo.k	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐾 ∈ Conn)
111		conntop 23360	. . . . . . . . . . . . . . . 16 ⊢ (𝐾 ∈ Conn → 𝐾 ∈ Top)
112	110, 111	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐾 ∈ Top)
113	112	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜓) → 𝐾 ∈ Top)
114	8	restuni 23105	. . . . . . . . . . . . . 14 ⊢ ((𝐾 ∈ Top ∧ 𝐼 ⊆ 𝑌) → 𝐼 = ∪ (𝐾 ↾t 𝐼))
115	113, 43, 114	syl2anc 584	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝜓) → 𝐼 = ∪ (𝐾 ↾t 𝐼))
116	109, 115	eleqtrd 2837	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝜓) → 𝑄 ∈ ∪ (𝐾 ↾t 𝐼))
117	116	adantr 480	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → 𝑄 ∈ ∪ (𝐾 ↾t 𝐼))
118	109	adantr 480	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → 𝑄 ∈ 𝐼)
119		fvres 6900	. . . . . . . . . . . . 13 ⊢ (𝑄 ∈ 𝐼 → ((𝑁 ↾ 𝐼)‘𝑄) = (𝑁‘𝑄))
120	118, 119	syl 17	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → ((𝑁 ↾ 𝐼)‘𝑄) = (𝑁‘𝑄))
121		simpr 484	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → (𝑀‘𝑄) = (𝑁‘𝑄))
122	4, 109	sseldd 3964	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝜓) → 𝑄 ∈ (◡𝑀 “ 𝑊))
123		elpreima 7053	. . . . . . . . . . . . . . . . 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 2836	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → (𝑁‘𝑄) ∈ 𝑊)
129	120, 128	eqeltrd 2835	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → ((𝑁 ↾ 𝐼)‘𝑄) ∈ 𝑊)
130	36, 38, 93, 105, 108, 117, 129	conncn 23369	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → (𝑁 ↾ 𝐼):∪ (𝐾 ↾t 𝐼)⟶𝑊)
131	115	adantr 480	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → 𝐼 = ∪ (𝐾 ↾t 𝐼))
132	131	feq2d 6697	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → ((𝑁 ↾ 𝐼):𝐼⟶𝑊 ↔ (𝑁 ↾ 𝐼):∪ (𝐾 ↾t 𝐼)⟶𝑊))
133	130, 132	mpbird 257	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → (𝑁 ↾ 𝐼):𝐼⟶𝑊)
134	133, 33	ffvelcdmd 7080	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → ((𝑁 ↾ 𝐼)‘𝑅) ∈ 𝑊)
135	35, 134	eqeltrrd 2836	. . . . . . 7 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → (𝑁‘𝑅) ∈ 𝑊)
136		fvres 6900	. . . . . . 7 ⊢ ((𝑁‘𝑅) ∈ 𝑊 → ((𝐹 ↾ 𝑊)‘(𝑁‘𝑅)) = (𝐹‘(𝑁‘𝑅)))
137	135, 136	syl 17	. . . . . 6 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → ((𝐹 ↾ 𝑊)‘(𝑁‘𝑅)) = (𝐹‘(𝑁‘𝑅)))
138	27, 32, 137	3eqtr4d 2781	. . . . 5 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → ((𝐹 ↾ 𝑊)‘(𝑀‘𝑅)) = ((𝐹 ↾ 𝑊)‘(𝑁‘𝑅)))
139	57	cvmsf1o 35299	. . . . . . . . 9 ⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑇 ∈ (𝑆‘𝑈) ∧ 𝑊 ∈ 𝑇) → (𝐹 ↾ 𝑊):𝑊–1-1-onto→𝑈)
140	47, 56, 53, 139	syl3anc 1373	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝜓) → (𝐹 ↾ 𝑊):𝑊–1-1-onto→𝑈)
141		f1of1 6822	. . . . . . . 8 ⊢ ((𝐹 ↾ 𝑊):𝑊–1-1-onto→𝑈 → (𝐹 ↾ 𝑊):𝑊–1-1→𝑈)
142	140, 141	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ 𝜓) → (𝐹 ↾ 𝑊):𝑊–1-1→𝑈)
143	142	adantr 480	. . . . . 6 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → (𝐹 ↾ 𝑊):𝑊–1-1→𝑈)
144		f1fveq 7260	. . . . . 6 ⊢ (((𝐹 ↾ 𝑊):𝑊–1-1→𝑈 ∧ ((𝑀‘𝑅) ∈ 𝑊 ∧ (𝑁‘𝑅) ∈ 𝑊)) → (((𝐹 ↾ 𝑊)‘(𝑀‘𝑅)) = ((𝐹 ↾ 𝑊)‘(𝑁‘𝑅)) ↔ (𝑀‘𝑅) = (𝑁‘𝑅)))
145	143, 30, 135, 144	syl12anc 836	. . . . 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 6881	. . . . . 6 ⊢ (𝑥 = 𝑄 → (𝑀‘𝑥) = (𝑀‘𝑄))
151		fveq2 6881	. . . . . 6 ⊢ (𝑥 = 𝑄 → (𝑁‘𝑥) = (𝑁‘𝑄))
152	150, 151	eqeq12d 2752	. . . . 5 ⊢ (𝑥 = 𝑄 → ((𝑀‘𝑥) = (𝑁‘𝑥) ↔ (𝑀‘𝑄) = (𝑁‘𝑄)))
153	152	elrab3 3677	. . . 4 ⊢ (𝑄 ∈ 𝑌 → (𝑄 ∈ {𝑥 ∈ 𝑌 ∣ (𝑀‘𝑥) = (𝑁‘𝑥)} ↔ (𝑀‘𝑄) = (𝑁‘𝑄)))
154	149, 153	syl 17	. . 3 ⊢ ((𝜑 ∧ 𝜓) → (𝑄 ∈ {𝑥 ∈ 𝑌 ∣ (𝑀‘𝑥) = (𝑁‘𝑥)} ↔ (𝑀‘𝑄) = (𝑁‘𝑄)))
155		fveq2 6881	. . . . . 6 ⊢ (𝑥 = 𝑅 → (𝑀‘𝑥) = (𝑀‘𝑅))
156		fveq2 6881	. . . . . 6 ⊢ (𝑥 = 𝑅 → (𝑁‘𝑥) = (𝑁‘𝑅))
157	155, 156	eqeq12d 2752	. . . . 5 ⊢ (𝑥 = 𝑅 → ((𝑀‘𝑥) = (𝑁‘𝑥) ↔ (𝑀‘𝑅) = (𝑁‘𝑅)))
158	157	elrab3 3677	. . . 4 ⊢ (𝑅 ∈ 𝑌 → (𝑅 ∈ {𝑥 ∈ 𝑌 ∣ (𝑀‘𝑥) = (𝑁‘𝑥)} ↔ (𝑀‘𝑅) = (𝑁‘𝑅)))
159	16, 158	syl 17	. . 3 ⊢ ((𝜑 ∧ 𝜓) → (𝑅 ∈ {𝑥 ∈ 𝑌 ∣ (𝑀‘𝑥) = (𝑁‘𝑥)} ↔ (𝑀‘𝑅) = (𝑁‘𝑅)))
160	147, 154, 159	3imtr4d 294	. 2 ⊢ ((𝜑 ∧ 𝜓) → (𝑄 ∈ {𝑥 ∈ 𝑌 ∣ (𝑀‘𝑥) = (𝑁‘𝑥)} → 𝑅 ∈ {𝑥 ∈ 𝑌 ∣ (𝑀‘𝑥) = (𝑁‘𝑥)}))
161	22	ffnd 6712	. . . . 5 ⊢ (𝜑 → 𝑁 Fn 𝑌)
162		fndmin 7040	. . . . 5 ⊢ ((𝑀 Fn 𝑌 ∧ 𝑁 Fn 𝑌) → dom (𝑀 ∩ 𝑁) = {𝑥 ∈ 𝑌 ∣ (𝑀‘𝑥) = (𝑁‘𝑥)})
163	12, 161, 162	syl2anc 584	. . . 4 ⊢ (𝜑 → dom (𝑀 ∩ 𝑁) = {𝑥 ∈ 𝑌 ∣ (𝑀‘𝑥) = (𝑁‘𝑥)})
164	163	adantr 480	. . 3 ⊢ ((𝜑 ∧ 𝜓) → dom (𝑀 ∩ 𝑁) = {𝑥 ∈ 𝑌 ∣ (𝑀‘𝑥) = (𝑁‘𝑥)})
165	164	eleq2d 2821	. 2 ⊢ ((𝜑 ∧ 𝜓) → (𝑄 ∈ dom (𝑀 ∩ 𝑁) ↔ 𝑄 ∈ {𝑥 ∈ 𝑌 ∣ (𝑀‘𝑥) = (𝑁‘𝑥)}))
166	164	eleq2d 2821	. 2 ⊢ ((𝜑 ∧ 𝜓) → (𝑅 ∈ dom (𝑀 ∩ 𝑁) ↔ 𝑅 ∈ {𝑥 ∈ 𝑌 ∣ (𝑀‘𝑥) = (𝑁‘𝑥)}))
167	160, 165, 166	3imtr4d 294	1 ⊢ ((𝜑 ∧ 𝜓) → (𝑄 ∈ dom (𝑀 ∩ 𝑁) → 𝑅 ∈ dom (𝑀 ∩ 𝑁)))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540   ∈ wcel 2109  ∀wral 3052  {crab 3420  Vcvv 3464   ∖ cdif 3928   ∩ cin 3930   ⊆ wss 3931  ∅c0 4313  𝒫 cpw 4580  {csn 4606  ∪ cuni 4888   ↦ cmpt 5206  ^◡ccnv 5658  dom cdm 5659  ran crn 5660   ↾ cres 5661   “ cima 5662   ∘ ccom 5663  Fun wfun 6530   Fn wfn 6531  ⟶wf 6532  –1-1→wf1 6533  –1-1-onto→wf1o 6535  ‘cfv 6536  (class class class)co 7410   ↾_t crest 17439  Topctop 22836  TopOnctopon 22853  Clsdccld 22959   Cn ccn 23167  Conncconn 23354  𝑛-Locally cnlly 23408  Homeochmeo 23696   CovMap ccvm 35282

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2708  ax-rep 5254  ax-sep 5271  ax-nul 5281  ax-pow 5340  ax-pr 5407  ax-un 7734

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2810  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3062  df-reu 3365  df-rab 3421  df-v 3466  df-sbc 3771  df-csb 3880  df-dif 3934  df-un 3936  df-in 3938  df-ss 3948  df-pss 3951  df-nul 4314  df-if 4506  df-pw 4582  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4889  df-int 4928  df-iun 4974  df-br 5125  df-opab 5187  df-mpt 5207  df-tr 5235  df-id 5553  df-eprel 5558  df-po 5566  df-so 5567  df-fr 5611  df-we 5613  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-ord 6360  df-on 6361  df-lim 6362  df-suc 6363  df-iota 6489  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-ov 7413  df-oprab 7414  df-mpo 7415  df-om 7867  df-1st 7993  df-2nd 7994  df-map 8847  df-en 8965  df-fin 8968  df-fi 9428  df-rest 17441  df-topgen 17462  df-top 22837  df-topon 22854  df-bases 22889  df-cld 22962  df-cn 23170  df-conn 23355  df-hmeo 23698  df-cvm 35283

This theorem is referenced by:  cvmliftmolem2  35309