cvmliftmolem1 - Mathbox for Mario Carneiro

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

Theorem cvmliftmolem1 31601

Description: Lemma for cvmliftmo 31604. (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 466	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝜓) → (𝐹 ∘ 𝑀) = (𝐹 ∘ 𝑁))
3	2	fveq1d 6334	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝜓) → ((𝐹 ∘ 𝑀)‘𝑅) = ((𝐹 ∘ 𝑁)‘𝑅))
4		cvmliftmolem.4	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜓) → 𝐼 ⊆ (^◡𝑀 “ 𝑊))
5		cvmliftmolem.8	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜓) → 𝑅 ∈ 𝐼)
6	4, 5	sseldd 3753	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝜓) → 𝑅 ∈ (^◡𝑀 “ 𝑊))
7		cvmliftmoi.m	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑀 ∈ (𝐾 Cn 𝐶))
8		cvmliftmo.y	. . . . . . . . . . . . . . 15 ⊢ 𝑌 = ∪ 𝐾
9		cvmliftmo.b	. . . . . . . . . . . . . . 15 ⊢ 𝐵 = ∪ 𝐶
10	8, 9	cnf 21271	. . . . . . . . . . . . . 14 ⊢ (𝑀 ∈ (𝐾 Cn 𝐶) → 𝑀:𝑌⟶𝐵)
11	7, 10	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑀:𝑌⟶𝐵)
12		ffn 6185	. . . . . . . . . . . . 13 ⊢ (𝑀:𝑌⟶𝐵 → 𝑀 Fn 𝑌)
13	11, 12	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑀 Fn 𝑌)
14		elpreima 6480	. . . . . . . . . . . 12 ⊢ (𝑀 Fn 𝑌 → (𝑅 ∈ (^◡𝑀 “ 𝑊) ↔ (𝑅 ∈ 𝑌 ∧ (𝑀‘𝑅) ∈ 𝑊)))
15	13, 14	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑅 ∈ (^◡𝑀 “ 𝑊) ↔ (𝑅 ∈ 𝑌 ∧ (𝑀‘𝑅) ∈ 𝑊)))
16	15	simprbda 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑅 ∈ (^◡𝑀 “ 𝑊)) → 𝑅 ∈ 𝑌)
17	6, 16	syldan 579	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝜓) → 𝑅 ∈ 𝑌)
18		fvco3 6417	. . . . . . . . . 10 ⊢ ((𝑀:𝑌⟶𝐵 ∧ 𝑅 ∈ 𝑌) → ((𝐹 ∘ 𝑀)‘𝑅) = (𝐹‘(𝑀‘𝑅)))
19	11, 18	sylan 569	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑅 ∈ 𝑌) → ((𝐹 ∘ 𝑀)‘𝑅) = (𝐹‘(𝑀‘𝑅)))
20	17, 19	syldan 579	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝜓) → ((𝐹 ∘ 𝑀)‘𝑅) = (𝐹‘(𝑀‘𝑅)))
21		cvmliftmoi.n	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑁 ∈ (𝐾 Cn 𝐶))
22	8, 9	cnf 21271	. . . . . . . . . . 11 ⊢ (𝑁 ∈ (𝐾 Cn 𝐶) → 𝑁:𝑌⟶𝐵)
23	21, 22	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝑁:𝑌⟶𝐵)
24		fvco3 6417	. . . . . . . . . 10 ⊢ ((𝑁:𝑌⟶𝐵 ∧ 𝑅 ∈ 𝑌) → ((𝐹 ∘ 𝑁)‘𝑅) = (𝐹‘(𝑁‘𝑅)))
25	23, 24	sylan 569	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑅 ∈ 𝑌) → ((𝐹 ∘ 𝑁)‘𝑅) = (𝐹‘(𝑁‘𝑅)))
26	17, 25	syldan 579	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝜓) → ((𝐹 ∘ 𝑁)‘𝑅) = (𝐹‘(𝑁‘𝑅)))
27	3, 20, 26	3eqtr3d 2813	. . . . . . 7 ⊢ ((𝜑 ∧ 𝜓) → (𝐹‘(𝑀‘𝑅)) = (𝐹‘(𝑁‘𝑅)))
28	27	adantr 466	. . . . . 6 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → (𝐹‘(𝑀‘𝑅)) = (𝐹‘(𝑁‘𝑅)))
29	15	simplbda 487	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑅 ∈ (^◡𝑀 “ 𝑊)) → (𝑀‘𝑅) ∈ 𝑊)
30	6, 29	syldan 579	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝜓) → (𝑀‘𝑅) ∈ 𝑊)
31	30	adantr 466	. . . . . . 7 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → (𝑀‘𝑅) ∈ 𝑊)
32		fvres 6348	. . . . . . 7 ⊢ ((𝑀‘𝑅) ∈ 𝑊 → ((𝐹 ↾ 𝑊)‘(𝑀‘𝑅)) = (𝐹‘(𝑀‘𝑅)))
33	31, 32	syl 17	. . . . . 6 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → ((𝐹 ↾ 𝑊)‘(𝑀‘𝑅)) = (𝐹‘(𝑀‘𝑅)))
34	5	adantr 466	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → 𝑅 ∈ 𝐼)
35		fvres 6348	. . . . . . . . 9 ⊢ (𝑅 ∈ 𝐼 → ((𝑁 ↾ 𝐼)‘𝑅) = (𝑁‘𝑅))
36	34, 35	syl 17	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → ((𝑁 ↾ 𝐼)‘𝑅) = (𝑁‘𝑅))
37		eqid 2771	. . . . . . . . . . 11 ⊢ ∪ (𝐾 ↾_t 𝐼) = ∪ (𝐾 ↾_t 𝐼)
38		cvmliftmolem.5	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝜓) → (𝐾 ↾_t 𝐼) ∈ Conn)
39	38	adantr 466	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → (𝐾 ↾_t 𝐼) ∈ Conn)
40	21	adantr 466	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜓) → 𝑁 ∈ (𝐾 Cn 𝐶))
41		cnvimass 5626	. . . . . . . . . . . . . . . . 17 ⊢ (^◡𝑀 “ 𝑊) ⊆ dom 𝑀
42		fdm 6191	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑀:𝑌⟶𝐵 → dom 𝑀 = 𝑌)
43	11, 42	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → dom 𝑀 = 𝑌)
44	41, 43	syl5sseq 3802	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (^◡𝑀 “ 𝑊) ⊆ 𝑌)
45	44	adantr 466	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝜓) → (^◡𝑀 “ 𝑊) ⊆ 𝑌)
46	4, 45	sstrd 3762	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜓) → 𝐼 ⊆ 𝑌)
47	8	cnrest 21310	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ (𝐾 Cn 𝐶) ∧ 𝐼 ⊆ 𝑌) → (𝑁 ↾ 𝐼) ∈ ((𝐾 ↾_t 𝐼) Cn 𝐶))
48	40, 46, 47	syl2anc 573	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝜓) → (𝑁 ↾ 𝐼) ∈ ((𝐾 ↾_t 𝐼) Cn 𝐶))
49		cvmliftmo.f	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐹 ∈ (𝐶 CovMap 𝐽))
50	49	adantr 466	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝜓) → 𝐹 ∈ (𝐶 CovMap 𝐽))
51		cvmtop1 31580	. . . . . . . . . . . . . . . 16 ⊢ (𝐹 ∈ (𝐶 CovMap 𝐽) → 𝐶 ∈ Top)
52	50, 51	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝜓) → 𝐶 ∈ Top)
53	9	toptopon 20942	. . . . . . . . . . . . . . 15 ⊢ (𝐶 ∈ Top ↔ 𝐶 ∈ (TopOn‘𝐵))
54	52, 53	sylib 208	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜓) → 𝐶 ∈ (TopOn‘𝐵))
55		df-ima 5262	. . . . . . . . . . . . . . 15 ⊢ (𝑁 “ 𝐼) = ran (𝑁 ↾ 𝐼)
56		cvmliftmolem.3	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝜓) → 𝑊 ∈ 𝑇)
57		elssuni 4603	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑊 ∈ 𝑇 → 𝑊 ⊆ ∪ 𝑇)
58	56, 57	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝜓) → 𝑊 ⊆ ∪ 𝑇)
59		cvmliftmolem.2	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝜓) → 𝑇 ∈ (𝑆‘𝑈))
60		cvmliftmolem.1	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (^◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾_t 𝑢)Homeo(𝐽 ↾_t 𝑘))))})
61	60	cvmsuni 31589	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑇 ∈ (𝑆‘𝑈) → ∪ 𝑇 = (^◡𝐹 “ 𝑈))
62	59, 61	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝜓) → ∪ 𝑇 = (^◡𝐹 “ 𝑈))
63	58, 62	sseqtrd 3790	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝜓) → 𝑊 ⊆ (^◡𝐹 “ 𝑈))
64		imass2 5642	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑊 ⊆ (^◡𝐹 “ 𝑈) → (^◡𝑀 “ 𝑊) ⊆ (^◡𝑀 “ (^◡𝐹 “ 𝑈)))
65	63, 64	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝜓) → (^◡𝑀 “ 𝑊) ⊆ (^◡𝑀 “ (^◡𝐹 “ 𝑈)))
66	4, 65	sstrd 3762	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝜓) → 𝐼 ⊆ (^◡𝑀 “ (^◡𝐹 “ 𝑈)))
67	2	cnveqd 5436	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝜓) → ^◡(𝐹 ∘ 𝑀) = ^◡(𝐹 ∘ 𝑁))
68		cnvco 5446	. . . . . . . . . . . . . . . . . . . 20 ⊢ ^◡(𝐹 ∘ 𝑀) = (^◡𝑀 ∘ ^◡𝐹)
69		cnvco 5446	. . . . . . . . . . . . . . . . . . . 20 ⊢ ^◡(𝐹 ∘ 𝑁) = (^◡𝑁 ∘ ^◡𝐹)
70	67, 68, 69	3eqtr3g 2828	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝜓) → (^◡𝑀 ∘ ^◡𝐹) = (^◡𝑁 ∘ ^◡𝐹))
71	70	imaeq1d 5606	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝜓) → ((^◡𝑀 ∘ ^◡𝐹) “ 𝑈) = ((^◡𝑁 ∘ ^◡𝐹) “ 𝑈))
72		imaco 5784	. . . . . . . . . . . . . . . . . 18 ⊢ ((^◡𝑀 ∘ ^◡𝐹) “ 𝑈) = (^◡𝑀 “ (^◡𝐹 “ 𝑈))
73		imaco 5784	. . . . . . . . . . . . . . . . . 18 ⊢ ((^◡𝑁 ∘ ^◡𝐹) “ 𝑈) = (^◡𝑁 “ (^◡𝐹 “ 𝑈))
74	71, 72, 73	3eqtr3g 2828	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝜓) → (^◡𝑀 “ (^◡𝐹 “ 𝑈)) = (^◡𝑁 “ (^◡𝐹 “ 𝑈)))
75	66, 74	sseqtrd 3790	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝜓) → 𝐼 ⊆ (^◡𝑁 “ (^◡𝐹 “ 𝑈)))
76	23	adantr 466	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝜓) → 𝑁:𝑌⟶𝐵)
77		ffun 6188	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑁:𝑌⟶𝐵 → Fun 𝑁)
78	76, 77	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝜓) → Fun 𝑁)
79		fdm 6191	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑁:𝑌⟶𝐵 → dom 𝑁 = 𝑌)
80	76, 79	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝜓) → dom 𝑁 = 𝑌)
81	46, 80	sseqtr4d 3791	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝜓) → 𝐼 ⊆ dom 𝑁)
82		funimass3 6476	. . . . . . . . . . . . . . . . 17 ⊢ ((Fun 𝑁 ∧ 𝐼 ⊆ dom 𝑁) → ((𝑁 “ 𝐼) ⊆ (^◡𝐹 “ 𝑈) ↔ 𝐼 ⊆ (^◡𝑁 “ (^◡𝐹 “ 𝑈))))
83	78, 81, 82	syl2anc 573	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝜓) → ((𝑁 “ 𝐼) ⊆ (^◡𝐹 “ 𝑈) ↔ 𝐼 ⊆ (^◡𝑁 “ (^◡𝐹 “ 𝑈))))
84	75, 83	mpbird 247	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝜓) → (𝑁 “ 𝐼) ⊆ (^◡𝐹 “ 𝑈))
85	55, 84	syl5eqssr 3799	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜓) → ran (𝑁 ↾ 𝐼) ⊆ (^◡𝐹 “ 𝑈))
86		cnvimass 5626	. . . . . . . . . . . . . . 15 ⊢ (^◡𝐹 “ 𝑈) ⊆ dom 𝐹
87		cvmcn 31582	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐹 ∈ (𝐶 CovMap 𝐽) → 𝐹 ∈ (𝐶 Cn 𝐽))
88	49, 87	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐹 ∈ (𝐶 Cn 𝐽))
89		eqid 2771	. . . . . . . . . . . . . . . . . . 19 ⊢ ∪ 𝐽 = ∪ 𝐽
90	9, 89	cnf 21271	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐹 ∈ (𝐶 Cn 𝐽) → 𝐹:𝐵⟶∪ 𝐽)
91	88, 90	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐹:𝐵⟶∪ 𝐽)
92		fdm 6191	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹:𝐵⟶∪ 𝐽 → dom 𝐹 = 𝐵)
93	91, 92	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → dom 𝐹 = 𝐵)
94	93	adantr 466	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝜓) → dom 𝐹 = 𝐵)
95	86, 94	syl5sseq 3802	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜓) → (^◡𝐹 “ 𝑈) ⊆ 𝐵)
96		cnrest2 21311	. . . . . . . . . . . . . 14 ⊢ ((𝐶 ∈ (TopOn‘𝐵) ∧ ran (𝑁 ↾ 𝐼) ⊆ (^◡𝐹 “ 𝑈) ∧ (^◡𝐹 “ 𝑈) ⊆ 𝐵) → ((𝑁 ↾ 𝐼) ∈ ((𝐾 ↾_t 𝐼) Cn 𝐶) ↔ (𝑁 ↾ 𝐼) ∈ ((𝐾 ↾_t 𝐼) Cn (𝐶 ↾_t (^◡𝐹 “ 𝑈)))))
97	54, 85, 95, 96	syl3anc 1476	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝜓) → ((𝑁 ↾ 𝐼) ∈ ((𝐾 ↾_t 𝐼) Cn 𝐶) ↔ (𝑁 ↾ 𝐼) ∈ ((𝐾 ↾_t 𝐼) Cn (𝐶 ↾_t (^◡𝐹 “ 𝑈)))))
98	48, 97	mpbid 222	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝜓) → (𝑁 ↾ 𝐼) ∈ ((𝐾 ↾_t 𝐼) Cn (𝐶 ↾_t (^◡𝐹 “ 𝑈))))
99	98	adantr 466	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → (𝑁 ↾ 𝐼) ∈ ((𝐾 ↾_t 𝐼) Cn (𝐶 ↾_t (^◡𝐹 “ 𝑈))))
100		df-ss 3737	. . . . . . . . . . . . . 14 ⊢ (𝑊 ⊆ (^◡𝐹 “ 𝑈) ↔ (𝑊 ∩ (^◡𝐹 “ 𝑈)) = 𝑊)
101	63, 100	sylib 208	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝜓) → (𝑊 ∩ (^◡𝐹 “ 𝑈)) = 𝑊)
102	9	topopn 20931	. . . . . . . . . . . . . . . 16 ⊢ (𝐶 ∈ Top → 𝐵 ∈ 𝐶)
103	52, 102	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝜓) → 𝐵 ∈ 𝐶)
104	103, 95	ssexd 4939	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜓) → (^◡𝐹 “ 𝑈) ∈ V)
105	60	cvmsss 31587	. . . . . . . . . . . . . . . 16 ⊢ (𝑇 ∈ (𝑆‘𝑈) → 𝑇 ⊆ 𝐶)
106	59, 105	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝜓) → 𝑇 ⊆ 𝐶)
107	106, 56	sseldd 3753	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜓) → 𝑊 ∈ 𝐶)
108		elrestr 16297	. . . . . . . . . . . . . 14 ⊢ ((𝐶 ∈ Top ∧ (^◡𝐹 “ 𝑈) ∈ V ∧ 𝑊 ∈ 𝐶) → (𝑊 ∩ (^◡𝐹 “ 𝑈)) ∈ (𝐶 ↾_t (^◡𝐹 “ 𝑈)))
109	52, 104, 107, 108	syl3anc 1476	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝜓) → (𝑊 ∩ (^◡𝐹 “ 𝑈)) ∈ (𝐶 ↾_t (^◡𝐹 “ 𝑈)))
110	101, 109	eqeltrrd 2851	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝜓) → 𝑊 ∈ (𝐶 ↾_t (^◡𝐹 “ 𝑈)))
111	110	adantr 466	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → 𝑊 ∈ (𝐶 ↾_t (^◡𝐹 “ 𝑈)))
112	60	cvmscld 31593	. . . . . . . . . . . . 13 ⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑇 ∈ (𝑆‘𝑈) ∧ 𝑊 ∈ 𝑇) → 𝑊 ∈ (Clsd‘(𝐶 ↾_t (^◡𝐹 “ 𝑈))))
113	50, 59, 56, 112	syl3anc 1476	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝜓) → 𝑊 ∈ (Clsd‘(𝐶 ↾_t (^◡𝐹 “ 𝑈))))
114	113	adantr 466	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → 𝑊 ∈ (Clsd‘(𝐶 ↾_t (^◡𝐹 “ 𝑈))))
115		cvmliftmolem.7	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝜓) → 𝑄 ∈ 𝐼)
116		cvmliftmo.k	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐾 ∈ Conn)
117		conntop 21441	. . . . . . . . . . . . . . . 16 ⊢ (𝐾 ∈ Conn → 𝐾 ∈ Top)
118	116, 117	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐾 ∈ Top)
119	118	adantr 466	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜓) → 𝐾 ∈ Top)
120	8	restuni 21187	. . . . . . . . . . . . . 14 ⊢ ((𝐾 ∈ Top ∧ 𝐼 ⊆ 𝑌) → 𝐼 = ∪ (𝐾 ↾_t 𝐼))
121	119, 46, 120	syl2anc 573	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝜓) → 𝐼 = ∪ (𝐾 ↾_t 𝐼))
122	115, 121	eleqtrd 2852	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝜓) → 𝑄 ∈ ∪ (𝐾 ↾_t 𝐼))
123	122	adantr 466	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → 𝑄 ∈ ∪ (𝐾 ↾_t 𝐼))
124	115	adantr 466	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → 𝑄 ∈ 𝐼)
125		fvres 6348	. . . . . . . . . . . . 13 ⊢ (𝑄 ∈ 𝐼 → ((𝑁 ↾ 𝐼)‘𝑄) = (𝑁‘𝑄))
126	124, 125	syl 17	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → ((𝑁 ↾ 𝐼)‘𝑄) = (𝑁‘𝑄))
127		simpr 471	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → (𝑀‘𝑄) = (𝑁‘𝑄))
128	4, 115	sseldd 3753	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝜓) → 𝑄 ∈ (^◡𝑀 “ 𝑊))
129		elpreima 6480	. . . . . . . . . . . . . . . . 17 ⊢ (𝑀 Fn 𝑌 → (𝑄 ∈ (^◡𝑀 “ 𝑊) ↔ (𝑄 ∈ 𝑌 ∧ (𝑀‘𝑄) ∈ 𝑊)))
130	13, 129	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑄 ∈ (^◡𝑀 “ 𝑊) ↔ (𝑄 ∈ 𝑌 ∧ (𝑀‘𝑄) ∈ 𝑊)))
131	130	simplbda 487	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑄 ∈ (^◡𝑀 “ 𝑊)) → (𝑀‘𝑄) ∈ 𝑊)
132	128, 131	syldan 579	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜓) → (𝑀‘𝑄) ∈ 𝑊)
133	132	adantr 466	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → (𝑀‘𝑄) ∈ 𝑊)
134	127, 133	eqeltrrd 2851	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → (𝑁‘𝑄) ∈ 𝑊)
135	126, 134	eqeltrd 2850	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → ((𝑁 ↾ 𝐼)‘𝑄) ∈ 𝑊)
136	37, 39, 99, 111, 114, 123, 135	conncn 21450	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → (𝑁 ↾ 𝐼):∪ (𝐾 ↾_t 𝐼)⟶𝑊)
137	121	adantr 466	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → 𝐼 = ∪ (𝐾 ↾_t 𝐼))
138	137	feq2d 6171	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → ((𝑁 ↾ 𝐼):𝐼⟶𝑊 ↔ (𝑁 ↾ 𝐼):∪ (𝐾 ↾_t 𝐼)⟶𝑊))
139	136, 138	mpbird 247	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → (𝑁 ↾ 𝐼):𝐼⟶𝑊)
140	139, 34	ffvelrnd 6503	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → ((𝑁 ↾ 𝐼)‘𝑅) ∈ 𝑊)
141	36, 140	eqeltrrd 2851	. . . . . . 7 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → (𝑁‘𝑅) ∈ 𝑊)
142		fvres 6348	. . . . . . 7 ⊢ ((𝑁‘𝑅) ∈ 𝑊 → ((𝐹 ↾ 𝑊)‘(𝑁‘𝑅)) = (𝐹‘(𝑁‘𝑅)))
143	141, 142	syl 17	. . . . . 6 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → ((𝐹 ↾ 𝑊)‘(𝑁‘𝑅)) = (𝐹‘(𝑁‘𝑅)))
144	28, 33, 143	3eqtr4d 2815	. . . . 5 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → ((𝐹 ↾ 𝑊)‘(𝑀‘𝑅)) = ((𝐹 ↾ 𝑊)‘(𝑁‘𝑅)))
145	60	cvmsf1o 31592	. . . . . . . . 9 ⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑇 ∈ (𝑆‘𝑈) ∧ 𝑊 ∈ 𝑇) → (𝐹 ↾ 𝑊):𝑊–1-1-onto→𝑈)
146	50, 59, 56, 145	syl3anc 1476	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝜓) → (𝐹 ↾ 𝑊):𝑊–1-1-onto→𝑈)
147		f1of1 6277	. . . . . . . 8 ⊢ ((𝐹 ↾ 𝑊):𝑊–1-1-onto→𝑈 → (𝐹 ↾ 𝑊):𝑊–1-1→𝑈)
148	146, 147	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ 𝜓) → (𝐹 ↾ 𝑊):𝑊–1-1→𝑈)
149	148	adantr 466	. . . . . 6 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → (𝐹 ↾ 𝑊):𝑊–1-1→𝑈)
150		f1fveq 6662	. . . . . 6 ⊢ (((𝐹 ↾ 𝑊):𝑊–1-1→𝑈 ∧ ((𝑀‘𝑅) ∈ 𝑊 ∧ (𝑁‘𝑅) ∈ 𝑊)) → (((𝐹 ↾ 𝑊)‘(𝑀‘𝑅)) = ((𝐹 ↾ 𝑊)‘(𝑁‘𝑅)) ↔ (𝑀‘𝑅) = (𝑁‘𝑅)))
151	149, 31, 141, 150	syl12anc 1474	. . . . 5 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → (((𝐹 ↾ 𝑊)‘(𝑀‘𝑅)) = ((𝐹 ↾ 𝑊)‘(𝑁‘𝑅)) ↔ (𝑀‘𝑅) = (𝑁‘𝑅)))
152	144, 151	mpbid 222	. . . 4 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝑀‘𝑄) = (𝑁‘𝑄)) → (𝑀‘𝑅) = (𝑁‘𝑅))
153	152	ex 397	. . 3 ⊢ ((𝜑 ∧ 𝜓) → ((𝑀‘𝑄) = (𝑁‘𝑄) → (𝑀‘𝑅) = (𝑁‘𝑅)))
154	130	simprbda 486	. . . . 5 ⊢ ((𝜑 ∧ 𝑄 ∈ (^◡𝑀 “ 𝑊)) → 𝑄 ∈ 𝑌)
155	128, 154	syldan 579	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝑄 ∈ 𝑌)
156		fveq2 6332	. . . . . 6 ⊢ (𝑥 = 𝑄 → (𝑀‘𝑥) = (𝑀‘𝑄))
157		fveq2 6332	. . . . . 6 ⊢ (𝑥 = 𝑄 → (𝑁‘𝑥) = (𝑁‘𝑄))
158	156, 157	eqeq12d 2786	. . . . 5 ⊢ (𝑥 = 𝑄 → ((𝑀‘𝑥) = (𝑁‘𝑥) ↔ (𝑀‘𝑄) = (𝑁‘𝑄)))
159	158	elrab3 3516	. . . 4 ⊢ (𝑄 ∈ 𝑌 → (𝑄 ∈ {𝑥 ∈ 𝑌 ∣ (𝑀‘𝑥) = (𝑁‘𝑥)} ↔ (𝑀‘𝑄) = (𝑁‘𝑄)))
160	155, 159	syl 17	. . 3 ⊢ ((𝜑 ∧ 𝜓) → (𝑄 ∈ {𝑥 ∈ 𝑌 ∣ (𝑀‘𝑥) = (𝑁‘𝑥)} ↔ (𝑀‘𝑄) = (𝑁‘𝑄)))
161		fveq2 6332	. . . . . 6 ⊢ (𝑥 = 𝑅 → (𝑀‘𝑥) = (𝑀‘𝑅))
162		fveq2 6332	. . . . . 6 ⊢ (𝑥 = 𝑅 → (𝑁‘𝑥) = (𝑁‘𝑅))
163	161, 162	eqeq12d 2786	. . . . 5 ⊢ (𝑥 = 𝑅 → ((𝑀‘𝑥) = (𝑁‘𝑥) ↔ (𝑀‘𝑅) = (𝑁‘𝑅)))
164	163	elrab3 3516	. . . 4 ⊢ (𝑅 ∈ 𝑌 → (𝑅 ∈ {𝑥 ∈ 𝑌 ∣ (𝑀‘𝑥) = (𝑁‘𝑥)} ↔ (𝑀‘𝑅) = (𝑁‘𝑅)))
165	17, 164	syl 17	. . 3 ⊢ ((𝜑 ∧ 𝜓) → (𝑅 ∈ {𝑥 ∈ 𝑌 ∣ (𝑀‘𝑥) = (𝑁‘𝑥)} ↔ (𝑀‘𝑅) = (𝑁‘𝑅)))
166	153, 160, 165	3imtr4d 283	. 2 ⊢ ((𝜑 ∧ 𝜓) → (𝑄 ∈ {𝑥 ∈ 𝑌 ∣ (𝑀‘𝑥) = (𝑁‘𝑥)} → 𝑅 ∈ {𝑥 ∈ 𝑌 ∣ (𝑀‘𝑥) = (𝑁‘𝑥)}))
167		ffn 6185	. . . . . 6 ⊢ (𝑁:𝑌⟶𝐵 → 𝑁 Fn 𝑌)
168	23, 167	syl 17	. . . . 5 ⊢ (𝜑 → 𝑁 Fn 𝑌)
169		fndmin 6467	. . . . 5 ⊢ ((𝑀 Fn 𝑌 ∧ 𝑁 Fn 𝑌) → dom (𝑀 ∩ 𝑁) = {𝑥 ∈ 𝑌 ∣ (𝑀‘𝑥) = (𝑁‘𝑥)})
170	13, 168, 169	syl2anc 573	. . . 4 ⊢ (𝜑 → dom (𝑀 ∩ 𝑁) = {𝑥 ∈ 𝑌 ∣ (𝑀‘𝑥) = (𝑁‘𝑥)})
171	170	adantr 466	. . 3 ⊢ ((𝜑 ∧ 𝜓) → dom (𝑀 ∩ 𝑁) = {𝑥 ∈ 𝑌 ∣ (𝑀‘𝑥) = (𝑁‘𝑥)})
172	171	eleq2d 2836	. 2 ⊢ ((𝜑 ∧ 𝜓) → (𝑄 ∈ dom (𝑀 ∩ 𝑁) ↔ 𝑄 ∈ {𝑥 ∈ 𝑌 ∣ (𝑀‘𝑥) = (𝑁‘𝑥)}))
173	171	eleq2d 2836	. 2 ⊢ ((𝜑 ∧ 𝜓) → (𝑅 ∈ dom (𝑀 ∩ 𝑁) ↔ 𝑅 ∈ {𝑥 ∈ 𝑌 ∣ (𝑀‘𝑥) = (𝑁‘𝑥)}))
174	166, 172, 173	3imtr4d 283	1 ⊢ ((𝜑 ∧ 𝜓) → (𝑄 ∈ dom (𝑀 ∩ 𝑁) → 𝑅 ∈ dom (𝑀 ∩ 𝑁)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 196 ∧ wa 382 = wceq 1631 ∈ wcel 2145 ∀wral 3061 {crab 3065 Vcvv 3351 ∖ cdif 3720 ∩ cin 3722 ⊆ wss 3723 ∅c0 4063 𝒫 cpw 4297 {csn 4316 ∪ cuni 4574 ↦ cmpt 4863 ^◡ccnv 5248 dom cdm 5249 ran crn 5250 ↾ cres 5251 “ cima 5252 ∘ ccom 5253 Fun wfun 6025 Fn wfn 6026 ⟶wf 6027 –1-1→wf1 6028 –1-1-onto→wf1o 6030 ‘cfv 6031 (class class class)co 6793 ↾_t crest 16289 Topctop 20918 TopOnctopon 20935 Clsdccld 21041 Cn ccn 21249 Conncconn 21435 𝑛-Locally cnlly 21489 Homeochmeo 21777 CovMap ccvm 31575

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1870 ax-4 1885 ax-5 1991 ax-6 2057 ax-7 2093 ax-8 2147 ax-9 2154 ax-10 2174 ax-11 2190 ax-12 2203 ax-13 2408 ax-ext 2751 ax-rep 4904 ax-sep 4915 ax-nul 4923 ax-pow 4974 ax-pr 5034 ax-un 7096

This theorem depends on definitions: df-bi 197 df-an 383 df-or 837 df-3or 1072 df-3an 1073 df-tru 1634 df-ex 1853 df-nf 1858 df-sb 2050 df-eu 2622 df-mo 2623 df-clab 2758 df-cleq 2764 df-clel 2767 df-nfc 2902 df-ne 2944 df-ral 3066 df-rex 3067 df-reu 3068 df-rab 3070 df-v 3353 df-sbc 3588 df-csb 3683 df-dif 3726 df-un 3728 df-in 3730 df-ss 3737 df-pss 3739 df-nul 4064 df-if 4226 df-pw 4299 df-sn 4317 df-pr 4319 df-tp 4321 df-op 4323 df-uni 4575 df-int 4612 df-iun 4656 df-br 4787 df-opab 4847 df-mpt 4864 df-tr 4887 df-id 5157 df-eprel 5162 df-po 5170 df-so 5171 df-fr 5208 df-we 5210 df-xp 5255 df-rel 5256 df-cnv 5257 df-co 5258 df-dm 5259 df-rn 5260 df-res 5261 df-ima 5262 df-pred 5823 df-ord 5869 df-on 5870 df-lim 5871 df-suc 5872 df-iota 5994 df-fun 6033 df-fn 6034 df-f 6035 df-f1 6036 df-fo 6037 df-f1o 6038 df-fv 6039 df-ov 6796 df-oprab 6797 df-mpt2 6798 df-om 7213 df-1st 7315 df-2nd 7316 df-wrecs 7559 df-recs 7621 df-rdg 7659 df-oadd 7717 df-er 7896 df-map 8011 df-en 8110 df-fin 8113 df-fi 8473 df-rest 16291 df-topgen 16312 df-top 20919 df-topon 20936 df-bases 20971 df-cld 21044 df-cn 21252 df-conn 21436 df-hmeo 21779 df-cvm 31576

This theorem is referenced by: cvmliftmolem2 31602

W3C validator