Theorem cvmliftmolem1 35644

Description: Lemma for cvmliftmo 35647. (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 485	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝜓) → (𝐹 ∘ 𝑀) = (𝐹 ∘ 𝑁))
3	2	fveq1d 6873	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝜓) → ((𝐹 ∘ 𝑀)‘𝑅) = ((𝐹 ∘ 𝑁)‘𝑅))
4		cvmliftmolem.4	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜓) → 𝐼 ⊆ (◡𝑀 “ 𝑊))
5		cvmliftmolem.8	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜓) → 𝑅 ∈ 𝐼)
6	4, 5	sseldd 3940	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝜓) → 𝑅 ∈ (◡𝑀 “ 𝑊))
7		cvmliftmoi.m	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑀 ∈ (𝐾 Cn 𝐶))
8		cvmliftmo.y	. . . . . . . . . . . . . . 15 ⊢ 𝑌 = ∪ 𝐾
9		cvmliftmo.b	. . . . . . . . . . . . . . 15 ⊢ 𝐵 = ∪ 𝐶
10	8, 9	cnf 23364	. . . . . . . . . . . . . 14 ⊢ (𝑀 ∈ (𝐾 Cn 𝐶) → 𝑀:𝑌⟶𝐵)
11	7, 10	syl 18	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑀:𝑌⟶𝐵)
12	11	ffnd 6696	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑀 Fn 𝑌)
13		elpreima 7043	. . . . . . . . . . . 12 ⊢ (𝑀 Fn 𝑌 → (𝑅 ∈ (◡𝑀 “ 𝑊) ↔ (𝑅 ∈ 𝑌 ∧ (𝑀‘𝑅) ∈ 𝑊)))
14	12, 13	syl 18	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑅 ∈ (◡𝑀 “ 𝑊) ↔ (𝑅 ∈ 𝑌 ∧ (𝑀‘𝑅) ∈ 𝑊)))
15	14	simprbda 503	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑅 ∈ (◡𝑀 “ 𝑊)) → 𝑅 ∈ 𝑌)
16	6, 15	syldan 602	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝜓) → 𝑅 ∈ 𝑌)
17		fvco3 6971	. . . . . . . . . 10 ⊢ ((𝑀:𝑌⟶𝐵 ∧ 𝑅 ∈ 𝑌) → ((𝐹 ∘ 𝑀)‘𝑅) = (𝐹‘(𝑀‘𝑅)))
18	11, 17	sylan 591	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑅 ∈ 𝑌) → ((𝐹 ∘ 𝑀)‘𝑅) = (𝐹‘(𝑀‘𝑅)))
19	16, 18	syldan 602	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝜓) → ((𝐹 ∘ 𝑀)‘𝑅) = (𝐹‘(𝑀‘𝑅)))
20		cvmliftmoi.n	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑁 ∈ (𝐾 Cn 𝐶))
21	8, 9	cnf 23364	. . . . . . . . . . 11 ⊢ (𝑁 ∈ (𝐾 Cn 𝐶) → 𝑁:𝑌⟶𝐵)
22	20, 21	syl 18	. . . . . . . . . 10 ⊢ (𝜑 → 𝑁:𝑌⟶𝐵)
23		fvco3 6971	. . . . . . . . . 10 ⊢ ((𝑁:𝑌⟶𝐵 ∧ 𝑅 ∈ 𝑌) → ((𝐹 ∘ 𝑁)‘𝑅) = (𝐹‘(𝑁‘𝑅)))
24	22, 23	sylan 591	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑅 ∈ 𝑌) → ((𝐹 ∘ 𝑁)‘𝑅) = (𝐹‘(𝑁‘𝑅)))
25	16, 24	syldan 602	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝜓) → ((𝐹 ∘ 𝑁)‘𝑅) = (𝐹‘(𝑁‘𝑅)))
26	3, 19, 25	3eqtr3d 2808	. . . . . . 7 ⊢ ((𝜑 ∧ 𝜓) → (𝐹‘(𝑀‘𝑅)) = (𝐹‘(𝑁‘𝑅)))
27	26	adantr 485	. . . . . 6 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → (𝐹‘(𝑀‘𝑅)) = (𝐹‘(𝑁‘𝑅)))
28	14	simplbda 504	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑅 ∈ (◡𝑀 “ 𝑊)) → (𝑀‘𝑅) ∈ 𝑊)
29	6, 28	syldan 602	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝜓) → (𝑀‘𝑅) ∈ 𝑊)
30	29	adantr 485	. . . . . . 7 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → (𝑀‘𝑅) ∈ 𝑊)
31		fvres 6890	. . . . . . 7 ⊢ ((𝑀‘𝑅) ∈ 𝑊 → ((𝐹 ↾ 𝑊)‘(𝑀‘𝑅)) = (𝐹‘(𝑀‘𝑅)))
32	30, 31	syl 18	. . . . . 6 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → ((𝐹 ↾ 𝑊)‘(𝑀‘𝑅)) = (𝐹‘(𝑀‘𝑅)))
33	5	adantr 485	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → 𝑅 ∈ 𝐼)
34		fvres 6890	. . . . . . . . 9 ⊢ (𝑅 ∈ 𝐼 → ((𝑁 ↾ 𝐼)‘𝑅) = (𝑁‘𝑅))
35	33, 34	syl 18	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → ((𝑁 ↾ 𝐼)‘𝑅) = (𝑁‘𝑅))
36		eqid 2765	. . . . . . . . . . 11 ⊢ ∪ (𝐾 ↾t 𝐼) = ∪ (𝐾 ↾t 𝐼)
37		cvmliftmolem.5	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝜓) → (𝐾 ↾t 𝐼) ∈ Conn)
38	37	adantr 485	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → (𝐾 ↾t 𝐼) ∈ Conn)
39	20	adantr 485	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜓) → 𝑁 ∈ (𝐾 Cn 𝐶))
40		cnvimass 6075	. . . . . . . . . . . . . . . . 17 ⊢ (◡𝑀 “ 𝑊) ⊆ dom 𝑀
41	40, 11	fssdm 6715	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (◡𝑀 “ 𝑊) ⊆ 𝑌)
42	41	adantr 485	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝜓) → (◡𝑀 “ 𝑊) ⊆ 𝑌)
43	4, 42	sstrd 3949	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜓) → 𝐼 ⊆ 𝑌)
44	8	cnrest 23403	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ (𝐾 Cn 𝐶) ∧ 𝐼 ⊆ 𝑌) → (𝑁 ↾ 𝐼) ∈ ((𝐾 ↾t 𝐼) Cn 𝐶))
45	39, 43, 44	syl2anc 595	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝜓) → (𝑁 ↾ 𝐼) ∈ ((𝐾 ↾t 𝐼) Cn 𝐶))
46		cvmliftmo.f	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐹 ∈ (𝐶 CovMap 𝐽))
47	46	adantr 485	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝜓) → 𝐹 ∈ (𝐶 CovMap 𝐽))
48		cvmtop1 35623	. . . . . . . . . . . . . . . 16 ⊢ (𝐹 ∈ (𝐶 CovMap 𝐽) → 𝐶 ∈ Top)
49	47, 48	syl 18	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝜓) → 𝐶 ∈ Top)
50	9	toptopon 23035	. . . . . . . . . . . . . . 15 ⊢ (𝐶 ∈ Top ↔ 𝐶 ∈ (TopOn‘𝐵))
51	49, 50	sylib 221	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜓) → 𝐶 ∈ (TopOn‘𝐵))
52		df-ima 5665	. . . . . . . . . . . . . . 15 ⊢ (𝑁 “ 𝐼) = ran (𝑁 ↾ 𝐼)
53		cvmliftmolem.3	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝜓) → 𝑊 ∈ 𝑇)
54		elssuni 4900	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑊 ∈ 𝑇 → 𝑊 ⊆ ∪ 𝑇)
55	53, 54	syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝜓) → 𝑊 ⊆ ∪ 𝑇)
56		cvmliftmolem.2	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝜓) → 𝑇 ∈ (𝑆‘𝑈))
57		cvmliftmolem.1	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾t 𝑢)Homeo(𝐽 ↾t 𝑘))))})
58	57	cvmsuni 35632	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑇 ∈ (𝑆‘𝑈) → ∪ 𝑇 = (◡𝐹 “ 𝑈))
59	56, 58	syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝜓) → ∪ 𝑇 = (◡𝐹 “ 𝑈))
60	55, 59	sseqtrd 3975	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝜓) → 𝑊 ⊆ (◡𝐹 “ 𝑈))
61		imass2 6095	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑊 ⊆ (◡𝐹 “ 𝑈) → (◡𝑀 “ 𝑊) ⊆ (◡𝑀 “ (◡𝐹 “ 𝑈)))
62	60, 61	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝜓) → (◡𝑀 “ 𝑊) ⊆ (◡𝑀 “ (◡𝐹 “ 𝑈)))
63	4, 62	sstrd 3949	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝜓) → 𝐼 ⊆ (◡𝑀 “ (◡𝐹 “ 𝑈)))
64	2	cnveqd 5852	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝜓) → ◡(𝐹 ∘ 𝑀) = ◡(𝐹 ∘ 𝑁))
65		cnvco 5866	. . . . . . . . . . . . . . . . . . . 20 ⊢ ◡(𝐹 ∘ 𝑀) = (◡𝑀 ∘ ◡𝐹)
66		cnvco 5866	. . . . . . . . . . . . . . . . . . . 20 ⊢ ◡(𝐹 ∘ 𝑁) = (◡𝑁 ∘ ◡𝐹)
67	64, 65, 66	3eqtr3g 2823	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝜓) → (◡𝑀 ∘ ◡𝐹) = (◡𝑁 ∘ ◡𝐹))
68	67	imaeq1d 6052	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝜓) → ((◡𝑀 ∘ ◡𝐹) “ 𝑈) = ((◡𝑁 ∘ ◡𝐹) “ 𝑈))
69		imaco 6242	. . . . . . . . . . . . . . . . . 18 ⊢ ((◡𝑀 ∘ ◡𝐹) “ 𝑈) = (◡𝑀 “ (◡𝐹 “ 𝑈))
70		imaco 6242	. . . . . . . . . . . . . . . . . 18 ⊢ ((◡𝑁 ∘ ◡𝐹) “ 𝑈) = (◡𝑁 “ (◡𝐹 “ 𝑈))
71	68, 69, 70	3eqtr3g 2823	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝜓) → (◡𝑀 “ (◡𝐹 “ 𝑈)) = (◡𝑁 “ (◡𝐹 “ 𝑈)))
72	63, 71	sseqtrd 3975	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝜓) → 𝐼 ⊆ (◡𝑁 “ (◡𝐹 “ 𝑈)))
73	22	adantr 485	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝜓) → 𝑁:𝑌⟶𝐵)
74	73	ffund 6700	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝜓) → Fun 𝑁)
75	73	fdmd 6706	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝜓) → dom 𝑁 = 𝑌)
76	43, 75	sseqtrrd 3976	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝜓) → 𝐼 ⊆ dom 𝑁)
77		funimass3 7039	. . . . . . . . . . . . . . . . 17 ⊢ ((Fun 𝑁 ∧ 𝐼 ⊆ dom 𝑁) → ((𝑁 “ 𝐼) ⊆ (◡𝐹 “ 𝑈) ↔ 𝐼 ⊆ (◡𝑁 “ (◡𝐹 “ 𝑈))))
78	74, 76, 77	syl2anc 595	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝜓) → ((𝑁 “ 𝐼) ⊆ (◡𝐹 “ 𝑈) ↔ 𝐼 ⊆ (◡𝑁 “ (◡𝐹 “ 𝑈))))
79	72, 78	mpbird 260	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝜓) → (𝑁 “ 𝐼) ⊆ (◡𝐹 “ 𝑈))
80	52, 79	eqsstrrid 3978	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜓) → ran (𝑁 ↾ 𝐼) ⊆ (◡𝐹 “ 𝑈))
81		cnvimass 6075	. . . . . . . . . . . . . . 15 ⊢ (◡𝐹 “ 𝑈) ⊆ dom 𝐹
82		cvmcn 35625	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐹 ∈ (𝐶 CovMap 𝐽) → 𝐹 ∈ (𝐶 Cn 𝐽))
83	46, 82	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐹 ∈ (𝐶 Cn 𝐽))
84		eqid 2765	. . . . . . . . . . . . . . . . . . 19 ⊢ ∪ 𝐽 = ∪ 𝐽
85	9, 84	cnf 23364	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐹 ∈ (𝐶 Cn 𝐽) → 𝐹:𝐵⟶∪ 𝐽)
86	83, 85	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐹:𝐵⟶∪ 𝐽)
87	86	fdmd 6706	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → dom 𝐹 = 𝐵)
88	87	adantr 485	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝜓) → dom 𝐹 = 𝐵)
89	81, 88	sseqtrid 3981	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜓) → (◡𝐹 “ 𝑈) ⊆ 𝐵)
90		cnrest2 23404	. . . . . . . . . . . . . 14 ⊢ ((𝐶 ∈ (TopOn‘𝐵) ∧ ran (𝑁 ↾ 𝐼) ⊆ (◡𝐹 “ 𝑈) ∧ (◡𝐹 “ 𝑈) ⊆ 𝐵) → ((𝑁 ↾ 𝐼) ∈ ((𝐾 ↾t 𝐼) Cn 𝐶) ↔ (𝑁 ↾ 𝐼) ∈ ((𝐾 ↾t 𝐼) Cn (𝐶 ↾t (◡𝐹 “ 𝑈)))))
91	51, 80, 89, 90	syl3anc 1394	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝜓) → ((𝑁 ↾ 𝐼) ∈ ((𝐾 ↾t 𝐼) Cn 𝐶) ↔ (𝑁 ↾ 𝐼) ∈ ((𝐾 ↾t 𝐼) Cn (𝐶 ↾t (◡𝐹 “ 𝑈)))))
92	45, 91	mpbid 235	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝜓) → (𝑁 ↾ 𝐼) ∈ ((𝐾 ↾t 𝐼) Cn (𝐶 ↾t (◡𝐹 “ 𝑈))))
93	92	adantr 485	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → (𝑁 ↾ 𝐼) ∈ ((𝐾 ↾t 𝐼) Cn (𝐶 ↾t (◡𝐹 “ 𝑈))))
94		dfss2 3925	. . . . . . . . . . . . . 14 ⊢ (𝑊 ⊆ (◡𝐹 “ 𝑈) ↔ (𝑊 ∩ (◡𝐹 “ 𝑈)) = 𝑊)
95	60, 94	sylib 221	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝜓) → (𝑊 ∩ (◡𝐹 “ 𝑈)) = 𝑊)
96	9	topopn 23024	. . . . . . . . . . . . . . . 16 ⊢ (𝐶 ∈ Top → 𝐵 ∈ 𝐶)
97	49, 96	syl 18	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝜓) → 𝐵 ∈ 𝐶)
98	97, 89	ssexd 5285	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜓) → (◡𝐹 “ 𝑈) ∈ V)
99	57	cvmsss 35630	. . . . . . . . . . . . . . . 16 ⊢ (𝑇 ∈ (𝑆‘𝑈) → 𝑇 ⊆ 𝐶)
100	56, 99	syl 18	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝜓) → 𝑇 ⊆ 𝐶)
101	100, 53	sseldd 3940	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜓) → 𝑊 ∈ 𝐶)
102		elrestr 17471	. . . . . . . . . . . . . 14 ⊢ ((𝐶 ∈ Top ∧ (◡𝐹 “ 𝑈) ∈ V ∧ 𝑊 ∈ 𝐶) → (𝑊 ∩ (◡𝐹 “ 𝑈)) ∈ (𝐶 ↾t (◡𝐹 “ 𝑈)))
103	49, 98, 101, 102	syl3anc 1394	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝜓) → (𝑊 ∩ (◡𝐹 “ 𝑈)) ∈ (𝐶 ↾t (◡𝐹 “ 𝑈)))
104	95, 103	eqeltrrd 2866	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝜓) → 𝑊 ∈ (𝐶 ↾t (◡𝐹 “ 𝑈)))
105	104	adantr 485	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → 𝑊 ∈ (𝐶 ↾t (◡𝐹 “ 𝑈)))
106	57	cvmscld 35636	. . . . . . . . . . . . 13 ⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑇 ∈ (𝑆‘𝑈) ∧ 𝑊 ∈ 𝑇) → 𝑊 ∈ (Clsd‘(𝐶 ↾t (◡𝐹 “ 𝑈))))
107	47, 56, 53, 106	syl3anc 1394	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝜓) → 𝑊 ∈ (Clsd‘(𝐶 ↾t (◡𝐹 “ 𝑈))))
108	107	adantr 485	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → 𝑊 ∈ (Clsd‘(𝐶 ↾t (◡𝐹 “ 𝑈))))
109		cvmliftmolem.7	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝜓) → 𝑄 ∈ 𝐼)
110		cvmliftmo.k	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐾 ∈ Conn)
111		conntop 23535	. . . . . . . . . . . . . . . 16 ⊢ (𝐾 ∈ Conn → 𝐾 ∈ Top)
112	110, 111	syl 18	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐾 ∈ Top)
113	112	adantr 485	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜓) → 𝐾 ∈ Top)
114	8	restuni 23280	. . . . . . . . . . . . . 14 ⊢ ((𝐾 ∈ Top ∧ 𝐼 ⊆ 𝑌) → 𝐼 = ∪ (𝐾 ↾t 𝐼))
115	113, 43, 114	syl2anc 595	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝜓) → 𝐼 = ∪ (𝐾 ↾t 𝐼))
116	109, 115	eleqtrd 2867	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝜓) → 𝑄 ∈ ∪ (𝐾 ↾t 𝐼))
117	116	adantr 485	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → 𝑄 ∈ ∪ (𝐾 ↾t 𝐼))
118	109	adantr 485	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → 𝑄 ∈ 𝐼)
119		fvres 6890	. . . . . . . . . . . . 13 ⊢ (𝑄 ∈ 𝐼 → ((𝑁 ↾ 𝐼)‘𝑄) = (𝑁‘𝑄))
120	118, 119	syl 18	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → ((𝑁 ↾ 𝐼)‘𝑄) = (𝑁‘𝑄))
121		simpr 489	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → (𝑀‘𝑄) = (𝑁‘𝑄))
122	4, 109	sseldd 3940	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝜓) → 𝑄 ∈ (◡𝑀 “ 𝑊))
123		elpreima 7043	. . . . . . . . . . . . . . . . 17 ⊢ (𝑀 Fn 𝑌 → (𝑄 ∈ (◡𝑀 “ 𝑊) ↔ (𝑄 ∈ 𝑌 ∧ (𝑀‘𝑄) ∈ 𝑊)))
124	12, 123	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑄 ∈ (◡𝑀 “ 𝑊) ↔ (𝑄 ∈ 𝑌 ∧ (𝑀‘𝑄) ∈ 𝑊)))
125	124	simplbda 504	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑄 ∈ (◡𝑀 “ 𝑊)) → (𝑀‘𝑄) ∈ 𝑊)
126	122, 125	syldan 602	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜓) → (𝑀‘𝑄) ∈ 𝑊)
127	126	adantr 485	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → (𝑀‘𝑄) ∈ 𝑊)
128	121, 127	eqeltrrd 2866	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → (𝑁‘𝑄) ∈ 𝑊)
129	120, 128	eqeltrd 2865	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → ((𝑁 ↾ 𝐼)‘𝑄) ∈ 𝑊)
130	36, 38, 93, 105, 108, 117, 129	conncn 23544	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → (𝑁 ↾ 𝐼):∪ (𝐾 ↾t 𝐼)⟶𝑊)
131	115	adantr 485	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → 𝐼 = ∪ (𝐾 ↾t 𝐼))
132	131	feq2d 6679	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → ((𝑁 ↾ 𝐼):𝐼⟶𝑊 ↔ (𝑁 ↾ 𝐼):∪ (𝐾 ↾t 𝐼)⟶𝑊))
133	130, 132	mpbird 260	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → (𝑁 ↾ 𝐼):𝐼⟶𝑊)
134	133, 33	ffvelcdmd 7070	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → ((𝑁 ↾ 𝐼)‘𝑅) ∈ 𝑊)
135	35, 134	eqeltrrd 2866	. . . . . . 7 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → (𝑁‘𝑅) ∈ 𝑊)
136		fvres 6890	. . . . . . 7 ⊢ ((𝑁‘𝑅) ∈ 𝑊 → ((𝐹 ↾ 𝑊)‘(𝑁‘𝑅)) = (𝐹‘(𝑁‘𝑅)))
137	135, 136	syl 18	. . . . . 6 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → ((𝐹 ↾ 𝑊)‘(𝑁‘𝑅)) = (𝐹‘(𝑁‘𝑅)))
138	27, 32, 137	3eqtr4d 2810	. . . . 5 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → ((𝐹 ↾ 𝑊)‘(𝑀‘𝑅)) = ((𝐹 ↾ 𝑊)‘(𝑁‘𝑅)))
139	57	cvmsf1o 35635	. . . . . . . . 9 ⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑇 ∈ (𝑆‘𝑈) ∧ 𝑊 ∈ 𝑇) → (𝐹 ↾ 𝑊):𝑊–1-1-onto→𝑈)
140	47, 56, 53, 139	syl3anc 1394	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝜓) → (𝐹 ↾ 𝑊):𝑊–1-1-onto→𝑈)
141		f1of1 6809	. . . . . . . 8 ⊢ ((𝐹 ↾ 𝑊):𝑊–1-1-onto→𝑈 → (𝐹 ↾ 𝑊):𝑊–1-1→𝑈)
142	140, 141	syl 18	. . . . . . 7 ⊢ ((𝜑 ∧ 𝜓) → (𝐹 ↾ 𝑊):𝑊–1-1→𝑈)
143	142	adantr 485	. . . . . 6 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → (𝐹 ↾ 𝑊):𝑊–1-1→𝑈)
144		f1fveq 7250	. . . . . 6 ⊢ (((𝐹 ↾ 𝑊):𝑊–1-1→𝑈 ∧ ((𝑀‘𝑅) ∈ 𝑊 ∧ (𝑁‘𝑅) ∈ 𝑊)) → (((𝐹 ↾ 𝑊)‘(𝑀‘𝑅)) = ((𝐹 ↾ 𝑊)‘(𝑁‘𝑅)) ↔ (𝑀‘𝑅) = (𝑁‘𝑅)))
145	143, 30, 135, 144	syl12anc 849	. . . . 5 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → (((𝐹 ↾ 𝑊)‘(𝑀‘𝑅)) = ((𝐹 ↾ 𝑊)‘(𝑁‘𝑅)) ↔ (𝑀‘𝑅) = (𝑁‘𝑅)))
146	138, 145	mpbid 235	. . . 4 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → (𝑀‘𝑅) = (𝑁‘𝑅))
147	146	ex 417	. . 3 ⊢ ((𝜑 ∧ 𝜓) → ((𝑀‘𝑄) = (𝑁‘𝑄) → (𝑀‘𝑅) = (𝑁‘𝑅)))
148	124	simprbda 503	. . . . 5 ⊢ ((𝜑 ∧ 𝑄 ∈ (◡𝑀 “ 𝑊)) → 𝑄 ∈ 𝑌)
149	122, 148	syldan 602	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝑄 ∈ 𝑌)
150		fveq2 6871	. . . . . 6 ⊢ (𝑥 = 𝑄 → (𝑀‘𝑥) = (𝑀‘𝑄))
151		fveq2 6871	. . . . . 6 ⊢ (𝑥 = 𝑄 → (𝑁‘𝑥) = (𝑁‘𝑄))
152	150, 151	eqeq12d 2781	. . . . 5 ⊢ (𝑥 = 𝑄 → ((𝑀‘𝑥) = (𝑁‘𝑥) ↔ (𝑀‘𝑄) = (𝑁‘𝑄)))
153	152	elrab3 3654	. . . 4 ⊢ (𝑄 ∈ 𝑌 → (𝑄 ∈ {𝑥 ∈ 𝑌 ∣ (𝑀‘𝑥) = (𝑁‘𝑥)} ↔ (𝑀‘𝑄) = (𝑁‘𝑄)))
154	149, 153	syl 18	. . 3 ⊢ ((𝜑 ∧ 𝜓) → (𝑄 ∈ {𝑥 ∈ 𝑌 ∣ (𝑀‘𝑥) = (𝑁‘𝑥)} ↔ (𝑀‘𝑄) = (𝑁‘𝑄)))
155		fveq2 6871	. . . . . 6 ⊢ (𝑥 = 𝑅 → (𝑀‘𝑥) = (𝑀‘𝑅))
156		fveq2 6871	. . . . . 6 ⊢ (𝑥 = 𝑅 → (𝑁‘𝑥) = (𝑁‘𝑅))
157	155, 156	eqeq12d 2781	. . . . 5 ⊢ (𝑥 = 𝑅 → ((𝑀‘𝑥) = (𝑁‘𝑥) ↔ (𝑀‘𝑅) = (𝑁‘𝑅)))
158	157	elrab3 3654	. . . 4 ⊢ (𝑅 ∈ 𝑌 → (𝑅 ∈ {𝑥 ∈ 𝑌 ∣ (𝑀‘𝑥) = (𝑁‘𝑥)} ↔ (𝑀‘𝑅) = (𝑁‘𝑅)))
159	16, 158	syl 18	. . 3 ⊢ ((𝜑 ∧ 𝜓) → (𝑅 ∈ {𝑥 ∈ 𝑌 ∣ (𝑀‘𝑥) = (𝑁‘𝑥)} ↔ (𝑀‘𝑅) = (𝑁‘𝑅)))
160	147, 154, 159	3imtr4d 297	. 2 ⊢ ((𝜑 ∧ 𝜓) → (𝑄 ∈ {𝑥 ∈ 𝑌 ∣ (𝑀‘𝑥) = (𝑁‘𝑥)} → 𝑅 ∈ {𝑥 ∈ 𝑌 ∣ (𝑀‘𝑥) = (𝑁‘𝑥)}))
161	22	ffnd 6696	. . . . 5 ⊢ (𝜑 → 𝑁 Fn 𝑌)
162		fndmin 7030	. . . . 5 ⊢ ((𝑀 Fn 𝑌 ∧ 𝑁 Fn 𝑌) → dom (𝑀 ∩ 𝑁) = {𝑥 ∈ 𝑌 ∣ (𝑀‘𝑥) = (𝑁‘𝑥)})
163	12, 161, 162	syl2anc 595	. . . 4 ⊢ (𝜑 → dom (𝑀 ∩ 𝑁) = {𝑥 ∈ 𝑌 ∣ (𝑀‘𝑥) = (𝑁‘𝑥)})
164	163	adantr 485	. . 3 ⊢ ((𝜑 ∧ 𝜓) → dom (𝑀 ∩ 𝑁) = {𝑥 ∈ 𝑌 ∣ (𝑀‘𝑥) = (𝑁‘𝑥)})
165	164	eleq2d 2851	. 2 ⊢ ((𝜑 ∧ 𝜓) → (𝑄 ∈ dom (𝑀 ∩ 𝑁) ↔ 𝑄 ∈ {𝑥 ∈ 𝑌 ∣ (𝑀‘𝑥) = (𝑁‘𝑥)}))
166	164	eleq2d 2851	. 2 ⊢ ((𝜑 ∧ 𝜓) → (𝑅 ∈ dom (𝑀 ∩ 𝑁) ↔ 𝑅 ∈ {𝑥 ∈ 𝑌 ∣ (𝑀‘𝑥) = (𝑁‘𝑥)}))
167	160, 165, 166	3imtr4d 297	1 ⊢ ((𝜑 ∧ 𝜓) → (𝑄 ∈ dom (𝑀 ∩ 𝑁) → 𝑅 ∈ dom (𝑀 ∩ 𝑁)))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   = wceq 1563   ∈ wcel 2145  ∀wral 3079  {crab 3417  Vcvv 3457   ∖ cdif 3904   ∩ cin 3906   ⊆ wss 3907  ∅c0 4288  𝒫 cpw 4558  {csn 4585  ∪ cuni 4868   ↦ cmpt 5186  ^◡ccnv 5651  dom cdm 5652  ran crn 5653   ↾ cres 5654   “ cima 5655   ∘ ccom 5656  Fun wfun 6519   Fn wfn 6520  ⟶wf 6521  –1-1→wf1 6522  –1-1-onto→wf1o 6524  ‘cfv 6525  (class class class)co 7400   ↾_t crest 17463  Topctop 23011  TopOnctopon 23028  Clsdccld 23134   Cn ccn 23342  Conncconn 23529  𝑛-Locally cnlly 23583  Homeochmeo 23871   CovMap ccvm 35618

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2737  ax-rep 5232  ax-sep 5251  ax-nul 5261  ax-pow 5327  ax-pr 5395  ax-un 7722

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-nf 1807  df-sb 2094  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-ral 3080  df-rex 3090  df-reu 3371  df-rab 3418  df-v 3459  df-sbc 3748  df-csb 3856  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-pss 3927  df-nul 4289  df-if 4484  df-pw 4560  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4869  df-int 4909  df-iun 4954  df-br 5106  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5547  df-eprel 5552  df-po 5560  df-so 5561  df-fr 5605  df-we 5607  df-xp 5658  df-rel 5659  df-cnv 5660  df-co 5661  df-dm 5662  df-rn 5663  df-res 5664  df-ima 5665  df-ord 6353  df-on 6354  df-lim 6355  df-suc 6356  df-iota 6481  df-fun 6527  df-fn 6528  df-f 6529  df-f1 6530  df-fo 6531  df-f1o 6532  df-fv 6533  df-ov 7403  df-oprab 7404  df-mpo 7405  df-om 7851  df-1st 7974  df-2nd 7975  df-map 8814  df-en 8932  df-fin 8935  df-fi 9359  df-rest 17465  df-topgen 17486  df-top 23012  df-topon 23029  df-bases 23064  df-cld 23137  df-cn 23345  df-conn 23530  df-hmeo 23873  df-cvm 35619

This theorem is referenced by:  cvmliftmolem2  35645