Theorem cvmliftmolem1 36015

Description: Lemma for cvmliftmo 36018. (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 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝜓) → (𝐹 ∘ 𝑀) = (𝐹 ∘ 𝑁))
3	2	fveq1d 6879	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝜓) → ((𝐹 ∘ 𝑀)‘𝑅) = ((𝐹 ∘ 𝑁)‘𝑅))
4		cvmliftmolem.4	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜓) → 𝐼 ⊆ (◡𝑀 “ 𝑊))
5		cvmliftmolem.8	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜓) → 𝑅 ∈ 𝐼)
6	4, 5	sseldd 3932	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝜓) → 𝑅 ∈ (◡𝑀 “ 𝑊))
7		cvmliftmoi.m	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑀 ∈ (𝐾 Cn 𝐶))
8		cvmliftmo.y	. . . . . . . . . . . . . . 15 ⊢ 𝑌 = ∪ 𝐾
9		cvmliftmo.b	. . . . . . . . . . . . . . 15 ⊢ 𝐵 = ∪ 𝐶
10	8, 9	cnf 23544	. . . . . . . . . . . . . 14 ⊢ (𝑀 ∈ (𝐾 Cn 𝐶) → 𝑀:𝑌⟶𝐵)
11	7, 10	syl 18	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑀:𝑌⟶𝐵)
12	11	ffnd 6702	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑀 Fn 𝑌)
13		elpreima 7049	. . . . . . . . . . . 12 ⊢ (𝑀 Fn 𝑌 → (𝑅 ∈ (◡𝑀 “ 𝑊) ↔ (𝑅 ∈ 𝑌 ∧ (𝑀‘𝑅) ∈ 𝑊)))
14	12, 13	syl 18	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑅 ∈ (◡𝑀 “ 𝑊) ↔ (𝑅 ∈ 𝑌 ∧ (𝑀‘𝑅) ∈ 𝑊)))
15	14	simprbda 504	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑅 ∈ (◡𝑀 “ 𝑊)) → 𝑅 ∈ 𝑌)
16	6, 15	syldan 603	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝜓) → 𝑅 ∈ 𝑌)
17		fvco3 6977	. . . . . . . . . 10 ⊢ ((𝑀:𝑌⟶𝐵 ∧ 𝑅 ∈ 𝑌) → ((𝐹 ∘ 𝑀)‘𝑅) = (𝐹‘(𝑀‘𝑅)))
18	11, 17	sylan 592	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑅 ∈ 𝑌) → ((𝐹 ∘ 𝑀)‘𝑅) = (𝐹‘(𝑀‘𝑅)))
19	16, 18	syldan 603	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝜓) → ((𝐹 ∘ 𝑀)‘𝑅) = (𝐹‘(𝑀‘𝑅)))
20		cvmliftmoi.n	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑁 ∈ (𝐾 Cn 𝐶))
21	8, 9	cnf 23544	. . . . . . . . . . 11 ⊢ (𝑁 ∈ (𝐾 Cn 𝐶) → 𝑁:𝑌⟶𝐵)
22	20, 21	syl 18	. . . . . . . . . 10 ⊢ (𝜑 → 𝑁:𝑌⟶𝐵)
23		fvco3 6977	. . . . . . . . . 10 ⊢ ((𝑁:𝑌⟶𝐵 ∧ 𝑅 ∈ 𝑌) → ((𝐹 ∘ 𝑁)‘𝑅) = (𝐹‘(𝑁‘𝑅)))
24	22, 23	sylan 592	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑅 ∈ 𝑌) → ((𝐹 ∘ 𝑁)‘𝑅) = (𝐹‘(𝑁‘𝑅)))
25	16, 24	syldan 603	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝜓) → ((𝐹 ∘ 𝑁)‘𝑅) = (𝐹‘(𝑁‘𝑅)))
26	3, 19, 25	3eqtr3d 2804	. . . . . . 7 ⊢ ((𝜑 ∧ 𝜓) → (𝐹‘(𝑀‘𝑅)) = (𝐹‘(𝑁‘𝑅)))
27	26	adantr 486	. . . . . 6 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → (𝐹‘(𝑀‘𝑅)) = (𝐹‘(𝑁‘𝑅)))
28	14	simplbda 505	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑅 ∈ (◡𝑀 “ 𝑊)) → (𝑀‘𝑅) ∈ 𝑊)
29	6, 28	syldan 603	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝜓) → (𝑀‘𝑅) ∈ 𝑊)
30	29	adantr 486	. . . . . . 7 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → (𝑀‘𝑅) ∈ 𝑊)
31		fvres 6896	. . . . . . 7 ⊢ ((𝑀‘𝑅) ∈ 𝑊 → ((𝐹 ↾ 𝑊)‘(𝑀‘𝑅)) = (𝐹‘(𝑀‘𝑅)))
32	30, 31	syl 18	. . . . . 6 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → ((𝐹 ↾ 𝑊)‘(𝑀‘𝑅)) = (𝐹‘(𝑀‘𝑅)))
33	5	adantr 486	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → 𝑅 ∈ 𝐼)
34		fvres 6896	. . . . . . . . 9 ⊢ (𝑅 ∈ 𝐼 → ((𝑁 ↾ 𝐼)‘𝑅) = (𝑁‘𝑅))
35	33, 34	syl 18	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → ((𝑁 ↾ 𝐼)‘𝑅) = (𝑁‘𝑅))
36		eqid 2761	. . . . . . . . . . 11 ⊢ ∪ (𝐾 ↾t 𝐼) = ∪ (𝐾 ↾t 𝐼)
37		cvmliftmolem.5	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝜓) → (𝐾 ↾t 𝐼) ∈ Conn)
38	37	adantr 486	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → (𝐾 ↾t 𝐼) ∈ Conn)
39	20	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜓) → 𝑁 ∈ (𝐾 Cn 𝐶))
40		cnvimass 6076	. . . . . . . . . . . . . . . . 17 ⊢ (◡𝑀 “ 𝑊) ⊆ dom 𝑀
41	40, 11	fssdm 6721	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (◡𝑀 “ 𝑊) ⊆ 𝑌)
42	41	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝜓) → (◡𝑀 “ 𝑊) ⊆ 𝑌)
43	4, 42	sstrd 3941	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜓) → 𝐼 ⊆ 𝑌)
44	8	cnrest 23583	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ (𝐾 Cn 𝐶) ∧ 𝐼 ⊆ 𝑌) → (𝑁 ↾ 𝐼) ∈ ((𝐾 ↾t 𝐼) Cn 𝐶))
45	39, 43, 44	syl2anc 596	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝜓) → (𝑁 ↾ 𝐼) ∈ ((𝐾 ↾t 𝐼) Cn 𝐶))
46		cvmliftmo.f	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐹 ∈ (𝐶 CovMap 𝐽))
47	46	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝜓) → 𝐹 ∈ (𝐶 CovMap 𝐽))
48		cvmtop1 35994	. . . . . . . . . . . . . . . 16 ⊢ (𝐹 ∈ (𝐶 CovMap 𝐽) → 𝐶 ∈ Top)
49	47, 48	syl 18	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝜓) → 𝐶 ∈ Top)
50	9	toptopon 23215	. . . . . . . . . . . . . . 15 ⊢ (𝐶 ∈ Top ↔ 𝐶 ∈ (TopOn‘𝐵))
51	49, 50	sylib 221	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜓) → 𝐶 ∈ (TopOn‘𝐵))
52		df-ima 5664	. . . . . . . . . . . . . . 15 ⊢ (𝑁 “ 𝐼) = ran (𝑁 ↾ 𝐼)
53		cvmliftmolem.3	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝜓) → 𝑊 ∈ 𝑇)
54		elssuni 4899	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑊 ∈ 𝑇 → 𝑊 ⊆ ∪ 𝑇)
55	53, 54	syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝜓) → 𝑊 ⊆ ∪ 𝑇)
56		cvmliftmolem.2	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝜓) → 𝑇 ∈ (𝑆‘𝑈))
57		cvmliftmolem.1	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾t 𝑢)Homeo(𝐽 ↾t 𝑘))))})
58	57	cvmsuni 36003	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑇 ∈ (𝑆‘𝑈) → ∪ 𝑇 = (◡𝐹 “ 𝑈))
59	56, 58	syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝜓) → ∪ 𝑇 = (◡𝐹 “ 𝑈))
60	55, 59	sseqtrd 3967	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝜓) → 𝑊 ⊆ (◡𝐹 “ 𝑈))
61		imass2 6096	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑊 ⊆ (◡𝐹 “ 𝑈) → (◡𝑀 “ 𝑊) ⊆ (◡𝑀 “ (◡𝐹 “ 𝑈)))
62	60, 61	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝜓) → (◡𝑀 “ 𝑊) ⊆ (◡𝑀 “ (◡𝐹 “ 𝑈)))
63	4, 62	sstrd 3941	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝜓) → 𝐼 ⊆ (◡𝑀 “ (◡𝐹 “ 𝑈)))
64	2	cnveqd 5853	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝜓) → ◡(𝐹 ∘ 𝑀) = ◡(𝐹 ∘ 𝑁))
65		cnvco 5867	. . . . . . . . . . . . . . . . . . . 20 ⊢ ◡(𝐹 ∘ 𝑀) = (◡𝑀 ∘ ◡𝐹)
66		cnvco 5867	. . . . . . . . . . . . . . . . . . . 20 ⊢ ◡(𝐹 ∘ 𝑁) = (◡𝑁 ∘ ◡𝐹)
67	64, 65, 66	3eqtr3g 2819	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝜓) → (◡𝑀 ∘ ◡𝐹) = (◡𝑁 ∘ ◡𝐹))
68	67	imaeq1d 6053	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝜓) → ((◡𝑀 ∘ ◡𝐹) “ 𝑈) = ((◡𝑁 ∘ ◡𝐹) “ 𝑈))
69		imaco 6245	. . . . . . . . . . . . . . . . . 18 ⊢ ((◡𝑀 ∘ ◡𝐹) “ 𝑈) = (◡𝑀 “ (◡𝐹 “ 𝑈))
70		imaco 6245	. . . . . . . . . . . . . . . . . 18 ⊢ ((◡𝑁 ∘ ◡𝐹) “ 𝑈) = (◡𝑁 “ (◡𝐹 “ 𝑈))
71	68, 69, 70	3eqtr3g 2819	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝜓) → (◡𝑀 “ (◡𝐹 “ 𝑈)) = (◡𝑁 “ (◡𝐹 “ 𝑈)))
72	63, 71	sseqtrd 3967	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝜓) → 𝐼 ⊆ (◡𝑁 “ (◡𝐹 “ 𝑈)))
73	22	adantr 486	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝜓) → 𝑁:𝑌⟶𝐵)
74	73	ffund 6706	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝜓) → Fun 𝑁)
75	73	fdmd 6712	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝜓) → dom 𝑁 = 𝑌)
76	43, 75	sseqtrrd 3968	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝜓) → 𝐼 ⊆ dom 𝑁)
77		funimass3 7045	. . . . . . . . . . . . . . . . 17 ⊢ ((Fun 𝑁 ∧ 𝐼 ⊆ dom 𝑁) → ((𝑁 “ 𝐼) ⊆ (◡𝐹 “ 𝑈) ↔ 𝐼 ⊆ (◡𝑁 “ (◡𝐹 “ 𝑈))))
78	74, 76, 77	syl2anc 596	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝜓) → ((𝑁 “ 𝐼) ⊆ (◡𝐹 “ 𝑈) ↔ 𝐼 ⊆ (◡𝑁 “ (◡𝐹 “ 𝑈))))
79	72, 78	mpbird 260	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝜓) → (𝑁 “ 𝐼) ⊆ (◡𝐹 “ 𝑈))
80	52, 79	eqsstrrid 3970	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜓) → ran (𝑁 ↾ 𝐼) ⊆ (◡𝐹 “ 𝑈))
81		cnvimass 6076	. . . . . . . . . . . . . . 15 ⊢ (◡𝐹 “ 𝑈) ⊆ dom 𝐹
82		cvmcn 35996	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐹 ∈ (𝐶 CovMap 𝐽) → 𝐹 ∈ (𝐶 Cn 𝐽))
83	46, 82	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐹 ∈ (𝐶 Cn 𝐽))
84		eqid 2761	. . . . . . . . . . . . . . . . . . 19 ⊢ ∪ 𝐽 = ∪ 𝐽
85	9, 84	cnf 23544	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐹 ∈ (𝐶 Cn 𝐽) → 𝐹:𝐵⟶∪ 𝐽)
86	83, 85	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐹:𝐵⟶∪ 𝐽)
87	86	fdmd 6712	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → dom 𝐹 = 𝐵)
88	87	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝜓) → dom 𝐹 = 𝐵)
89	81, 88	sseqtrid 3973	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜓) → (◡𝐹 “ 𝑈) ⊆ 𝐵)
90		cnrest2 23584	. . . . . . . . . . . . . 14 ⊢ ((𝐶 ∈ (TopOn‘𝐵) ∧ ran (𝑁 ↾ 𝐼) ⊆ (◡𝐹 “ 𝑈) ∧ (◡𝐹 “ 𝑈) ⊆ 𝐵) → ((𝑁 ↾ 𝐼) ∈ ((𝐾 ↾t 𝐼) Cn 𝐶) ↔ (𝑁 ↾ 𝐼) ∈ ((𝐾 ↾t 𝐼) Cn (𝐶 ↾t (◡𝐹 “ 𝑈)))))
91	51, 80, 89, 90	syl3anc 1398	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝜓) → ((𝑁 ↾ 𝐼) ∈ ((𝐾 ↾t 𝐼) Cn 𝐶) ↔ (𝑁 ↾ 𝐼) ∈ ((𝐾 ↾t 𝐼) Cn (𝐶 ↾t (◡𝐹 “ 𝑈)))))
92	45, 91	mpbid 235	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝜓) → (𝑁 ↾ 𝐼) ∈ ((𝐾 ↾t 𝐼) Cn (𝐶 ↾t (◡𝐹 “ 𝑈))))
93	92	adantr 486	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → (𝑁 ↾ 𝐼) ∈ ((𝐾 ↾t 𝐼) Cn (𝐶 ↾t (◡𝐹 “ 𝑈))))
94		dfss2 3917	. . . . . . . . . . . . . 14 ⊢ (𝑊 ⊆ (◡𝐹 “ 𝑈) ↔ (𝑊 ∩ (◡𝐹 “ 𝑈)) = 𝑊)
95	60, 94	sylib 221	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝜓) → (𝑊 ∩ (◡𝐹 “ 𝑈)) = 𝑊)
96	9	topopn 23204	. . . . . . . . . . . . . . . 16 ⊢ (𝐶 ∈ Top → 𝐵 ∈ 𝐶)
97	49, 96	syl 18	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝜓) → 𝐵 ∈ 𝐶)
98	97, 89	ssexd 5286	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜓) → (◡𝐹 “ 𝑈) ∈ V)
99	57	cvmsss 36001	. . . . . . . . . . . . . . . 16 ⊢ (𝑇 ∈ (𝑆‘𝑈) → 𝑇 ⊆ 𝐶)
100	56, 99	syl 18	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝜓) → 𝑇 ⊆ 𝐶)
101	100, 53	sseldd 3932	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜓) → 𝑊 ∈ 𝐶)
102		elrestr 17579	. . . . . . . . . . . . . 14 ⊢ ((𝐶 ∈ Top ∧ (◡𝐹 “ 𝑈) ∈ V ∧ 𝑊 ∈ 𝐶) → (𝑊 ∩ (◡𝐹 “ 𝑈)) ∈ (𝐶 ↾t (◡𝐹 “ 𝑈)))
103	49, 98, 101, 102	syl3anc 1398	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝜓) → (𝑊 ∩ (◡𝐹 “ 𝑈)) ∈ (𝐶 ↾t (◡𝐹 “ 𝑈)))
104	95, 103	eqeltrrd 2862	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝜓) → 𝑊 ∈ (𝐶 ↾t (◡𝐹 “ 𝑈)))
105	104	adantr 486	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → 𝑊 ∈ (𝐶 ↾t (◡𝐹 “ 𝑈)))
106	57	cvmscld 36007	. . . . . . . . . . . . 13 ⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑇 ∈ (𝑆‘𝑈) ∧ 𝑊 ∈ 𝑇) → 𝑊 ∈ (Clsd‘(𝐶 ↾t (◡𝐹 “ 𝑈))))
107	47, 56, 53, 106	syl3anc 1398	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝜓) → 𝑊 ∈ (Clsd‘(𝐶 ↾t (◡𝐹 “ 𝑈))))
108	107	adantr 486	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → 𝑊 ∈ (Clsd‘(𝐶 ↾t (◡𝐹 “ 𝑈))))
109		cvmliftmolem.7	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝜓) → 𝑄 ∈ 𝐼)
110		cvmliftmo.k	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐾 ∈ Conn)
111		conntop 23715	. . . . . . . . . . . . . . . 16 ⊢ (𝐾 ∈ Conn → 𝐾 ∈ Top)
112	110, 111	syl 18	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐾 ∈ Top)
113	112	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜓) → 𝐾 ∈ Top)
114	8	restuni 23460	. . . . . . . . . . . . . 14 ⊢ ((𝐾 ∈ Top ∧ 𝐼 ⊆ 𝑌) → 𝐼 = ∪ (𝐾 ↾t 𝐼))
115	113, 43, 114	syl2anc 596	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝜓) → 𝐼 = ∪ (𝐾 ↾t 𝐼))
116	109, 115	eleqtrd 2863	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝜓) → 𝑄 ∈ ∪ (𝐾 ↾t 𝐼))
117	116	adantr 486	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → 𝑄 ∈ ∪ (𝐾 ↾t 𝐼))
118	109	adantr 486	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → 𝑄 ∈ 𝐼)
119		fvres 6896	. . . . . . . . . . . . 13 ⊢ (𝑄 ∈ 𝐼 → ((𝑁 ↾ 𝐼)‘𝑄) = (𝑁‘𝑄))
120	118, 119	syl 18	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → ((𝑁 ↾ 𝐼)‘𝑄) = (𝑁‘𝑄))
121		simpr 490	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → (𝑀‘𝑄) = (𝑁‘𝑄))
122	4, 109	sseldd 3932	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝜓) → 𝑄 ∈ (◡𝑀 “ 𝑊))
123		elpreima 7049	. . . . . . . . . . . . . . . . 17 ⊢ (𝑀 Fn 𝑌 → (𝑄 ∈ (◡𝑀 “ 𝑊) ↔ (𝑄 ∈ 𝑌 ∧ (𝑀‘𝑄) ∈ 𝑊)))
124	12, 123	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑄 ∈ (◡𝑀 “ 𝑊) ↔ (𝑄 ∈ 𝑌 ∧ (𝑀‘𝑄) ∈ 𝑊)))
125	124	simplbda 505	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑄 ∈ (◡𝑀 “ 𝑊)) → (𝑀‘𝑄) ∈ 𝑊)
126	122, 125	syldan 603	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜓) → (𝑀‘𝑄) ∈ 𝑊)
127	126	adantr 486	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → (𝑀‘𝑄) ∈ 𝑊)
128	121, 127	eqeltrrd 2862	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → (𝑁‘𝑄) ∈ 𝑊)
129	120, 128	eqeltrd 2861	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → ((𝑁 ↾ 𝐼)‘𝑄) ∈ 𝑊)
130	36, 38, 93, 105, 108, 117, 129	conncn 23724	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → (𝑁 ↾ 𝐼):∪ (𝐾 ↾t 𝐼)⟶𝑊)
131	115	adantr 486	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → 𝐼 = ∪ (𝐾 ↾t 𝐼))
132	131	feq2d 6685	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → ((𝑁 ↾ 𝐼):𝐼⟶𝑊 ↔ (𝑁 ↾ 𝐼):∪ (𝐾 ↾t 𝐼)⟶𝑊))
133	130, 132	mpbird 260	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → (𝑁 ↾ 𝐼):𝐼⟶𝑊)
134	133, 33	ffvelcdmd 7077	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → ((𝑁 ↾ 𝐼)‘𝑅) ∈ 𝑊)
135	35, 134	eqeltrrd 2862	. . . . . . 7 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → (𝑁‘𝑅) ∈ 𝑊)
136		fvres 6896	. . . . . . 7 ⊢ ((𝑁‘𝑅) ∈ 𝑊 → ((𝐹 ↾ 𝑊)‘(𝑁‘𝑅)) = (𝐹‘(𝑁‘𝑅)))
137	135, 136	syl 18	. . . . . 6 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → ((𝐹 ↾ 𝑊)‘(𝑁‘𝑅)) = (𝐹‘(𝑁‘𝑅)))
138	27, 32, 137	3eqtr4d 2806	. . . . 5 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → ((𝐹 ↾ 𝑊)‘(𝑀‘𝑅)) = ((𝐹 ↾ 𝑊)‘(𝑁‘𝑅)))
139	57	cvmsf1o 36006	. . . . . . . . 9 ⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑇 ∈ (𝑆‘𝑈) ∧ 𝑊 ∈ 𝑇) → (𝐹 ↾ 𝑊):𝑊–1-1-onto→𝑈)
140	47, 56, 53, 139	syl3anc 1398	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝜓) → (𝐹 ↾ 𝑊):𝑊–1-1-onto→𝑈)
141		f1of1 6815	. . . . . . . 8 ⊢ ((𝐹 ↾ 𝑊):𝑊–1-1-onto→𝑈 → (𝐹 ↾ 𝑊):𝑊–1-1→𝑈)
142	140, 141	syl 18	. . . . . . 7 ⊢ ((𝜑 ∧ 𝜓) → (𝐹 ↾ 𝑊):𝑊–1-1→𝑈)
143	142	adantr 486	. . . . . 6 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → (𝐹 ↾ 𝑊):𝑊–1-1→𝑈)
144		f1fveq 7258	. . . . . 6 ⊢ (((𝐹 ↾ 𝑊):𝑊–1-1→𝑈 ∧ ((𝑀‘𝑅) ∈ 𝑊 ∧ (𝑁‘𝑅) ∈ 𝑊)) → (((𝐹 ↾ 𝑊)‘(𝑀‘𝑅)) = ((𝐹 ↾ 𝑊)‘(𝑁‘𝑅)) ↔ (𝑀‘𝑅) = (𝑁‘𝑅)))
145	143, 30, 135, 144	syl12anc 850	. . . . 5 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → (((𝐹 ↾ 𝑊)‘(𝑀‘𝑅)) = ((𝐹 ↾ 𝑊)‘(𝑁‘𝑅)) ↔ (𝑀‘𝑅) = (𝑁‘𝑅)))
146	138, 145	mpbid 235	. . . 4 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → (𝑀‘𝑅) = (𝑁‘𝑅))
147	146	ex 418	. . 3 ⊢ ((𝜑 ∧ 𝜓) → ((𝑀‘𝑄) = (𝑁‘𝑄) → (𝑀‘𝑅) = (𝑁‘𝑅)))
148	124	simprbda 504	. . . . 5 ⊢ ((𝜑 ∧ 𝑄 ∈ (◡𝑀 “ 𝑊)) → 𝑄 ∈ 𝑌)
149	122, 148	syldan 603	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝑄 ∈ 𝑌)
150		fveq2 6877	. . . . . 6 ⊢ (𝑥 = 𝑄 → (𝑀‘𝑥) = (𝑀‘𝑄))
151		fveq2 6877	. . . . . 6 ⊢ (𝑥 = 𝑄 → (𝑁‘𝑥) = (𝑁‘𝑄))
152	150, 151	eqeq12d 2777	. . . . 5 ⊢ (𝑥 = 𝑄 → ((𝑀‘𝑥) = (𝑁‘𝑥) ↔ (𝑀‘𝑄) = (𝑁‘𝑄)))
153	152	elrab3 3646	. . . 4 ⊢ (𝑄 ∈ 𝑌 → (𝑄 ∈ {𝑥 ∈ 𝑌 ∣ (𝑀‘𝑥) = (𝑁‘𝑥)} ↔ (𝑀‘𝑄) = (𝑁‘𝑄)))
154	149, 153	syl 18	. . 3 ⊢ ((𝜑 ∧ 𝜓) → (𝑄 ∈ {𝑥 ∈ 𝑌 ∣ (𝑀‘𝑥) = (𝑁‘𝑥)} ↔ (𝑀‘𝑄) = (𝑁‘𝑄)))
155		fveq2 6877	. . . . . 6 ⊢ (𝑥 = 𝑅 → (𝑀‘𝑥) = (𝑀‘𝑅))
156		fveq2 6877	. . . . . 6 ⊢ (𝑥 = 𝑅 → (𝑁‘𝑥) = (𝑁‘𝑅))
157	155, 156	eqeq12d 2777	. . . . 5 ⊢ (𝑥 = 𝑅 → ((𝑀‘𝑥) = (𝑁‘𝑥) ↔ (𝑀‘𝑅) = (𝑁‘𝑅)))
158	157	elrab3 3646	. . . 4 ⊢ (𝑅 ∈ 𝑌 → (𝑅 ∈ {𝑥 ∈ 𝑌 ∣ (𝑀‘𝑥) = (𝑁‘𝑥)} ↔ (𝑀‘𝑅) = (𝑁‘𝑅)))
159	16, 158	syl 18	. . 3 ⊢ ((𝜑 ∧ 𝜓) → (𝑅 ∈ {𝑥 ∈ 𝑌 ∣ (𝑀‘𝑥) = (𝑁‘𝑥)} ↔ (𝑀‘𝑅) = (𝑁‘𝑅)))
160	147, 154, 159	3imtr4d 297	. 2 ⊢ ((𝜑 ∧ 𝜓) → (𝑄 ∈ {𝑥 ∈ 𝑌 ∣ (𝑀‘𝑥) = (𝑁‘𝑥)} → 𝑅 ∈ {𝑥 ∈ 𝑌 ∣ (𝑀‘𝑥) = (𝑁‘𝑥)}))
161	22	ffnd 6702	. . . . 5 ⊢ (𝜑 → 𝑁 Fn 𝑌)
162		fndmin 7036	. . . . 5 ⊢ ((𝑀 Fn 𝑌 ∧ 𝑁 Fn 𝑌) → dom (𝑀 ∩ 𝑁) = {𝑥 ∈ 𝑌 ∣ (𝑀‘𝑥) = (𝑁‘𝑥)})
163	12, 161, 162	syl2anc 596	. . . 4 ⊢ (𝜑 → dom (𝑀 ∩ 𝑁) = {𝑥 ∈ 𝑌 ∣ (𝑀‘𝑥) = (𝑁‘𝑥)})
164	163	adantr 486	. . 3 ⊢ ((𝜑 ∧ 𝜓) → dom (𝑀 ∩ 𝑁) = {𝑥 ∈ 𝑌 ∣ (𝑀‘𝑥) = (𝑁‘𝑥)})
165	164	eleq2d 2847	. 2 ⊢ ((𝜑 ∧ 𝜓) → (𝑄 ∈ dom (𝑀 ∩ 𝑁) ↔ 𝑄 ∈ {𝑥 ∈ 𝑌 ∣ (𝑀‘𝑥) = (𝑁‘𝑥)}))
166	164	eleq2d 2847	. 2 ⊢ ((𝜑 ∧ 𝜓) → (𝑅 ∈ dom (𝑀 ∩ 𝑁) ↔ 𝑅 ∈ {𝑥 ∈ 𝑌 ∣ (𝑀‘𝑥) = (𝑁‘𝑥)}))
167	160, 165, 166	3imtr4d 297	1 ⊢ ((𝜑 ∧ 𝜓) → (𝑄 ∈ dom (𝑀 ∩ 𝑁) → 𝑅 ∈ dom (𝑀 ∩ 𝑁)))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570   ∈ wcel 2145  ∀wral 3077  {crab 3413  Vcvv 3451   ∖ cdif 3896   ∩ cin 3898   ⊆ wss 3899  ∅c0 4279  𝒫 cpw 4557  {csn 4584  ∪ cuni 4867   ↦ cmpt 5186  ^◡ccnv 5650  dom cdm 5651  ran crn 5652   ↾ cres 5653   “ cima 5654   ∘ ccom 5655  Fun wfun 6525   Fn wfn 6526  ⟶wf 6527  –1-1→wf1 6528  –1-1-onto→wf1o 6530  ‘cfv 6531  (class class class)co 7412   ↾_t crest 17571  Topctop 23191  TopOnctopon 23208  Clsdccld 23314   Cn ccn 23522  Conncconn 23709  𝑛-Locally cnlly 23764  Homeochmeo 24052   CovMap ccvm 35989

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-rep 5232  ax-sep 5249  ax-nul 5260  ax-pow 5327  ax-pr 5391  ax-un 7740

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3078  df-rex 3088  df-reu 3367  df-rab 3414  df-v 3453  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-int 4908  df-iun 4953  df-br 5104  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5546  df-eprel 5551  df-po 5559  df-so 5560  df-fr 5604  df-we 5606  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-ord 6358  df-on 6359  df-lim 6360  df-suc 6361  df-iota 6487  df-fun 6533  df-fn 6534  df-f 6535  df-f1 6536  df-fo 6537  df-f1o 6538  df-fv 6539  df-ov 7415  df-oprab 7416  df-mpo 7417  df-om 7867  df-1st 7990  df-2nd 7991  df-map 8833  df-en 8958  df-fin 8961  df-fi 9387  df-rest 17573  df-topgen 17594  df-top 23192  df-topon 23209  df-bases 23244  df-cld 23317  df-cn 23525  df-conn 23710  df-hmeo 24054  df-cvm 35990

This theorem is used by:  cvmliftmolem2  36016