cvmlift2lem9a

	Ref	Expression
Hypotheses	cvmlift2lem9a.b	$⊢ B = ⋃ C$
	cvmlift2lem9a.y	$⊢ Y = ⋃ K$
	cvmlift2lem9a.s	$⊢ S = (k \in J ⟼ \{s \in (𝒫 C ∖ \{\emptyset\}) \| (⋃ s = F^{-1} [k] \land \forall c \in s (\forall d \in (s ∖ \{c\}) c \cap d = \emptyset \land {F ↾}_{c} \in ((C ↾_{𝑡} c) Homeo (J ↾_{𝑡} k))))\})$
	cvmlift2lem9a.f	$⊢ φ \to F \in (C CovMap J)$
	cvmlift2lem9a.h	$⊢ φ \to H : Y ⟶ B$
	cvmlift2lem9a.g	$⊢ φ \to F \circ H \in (K Cn J)$
	cvmlift2lem9a.k	$⊢ φ \to K \in Top$
	cvmlift2lem9a.1	$⊢ φ \to X \in Y$
	cvmlift2lem9a.2	$⊢ φ \to T \in S (A)$
	cvmlift2lem9a.3	$⊢ φ \to (W \in T \land H (X) \in W)$
	cvmlift2lem9a.4	$⊢ φ \to M \subseteq Y$
	cvmlift2lem9a.6	$⊢ φ \to H [M] \subseteq W$
Assertion	cvmlift2lem9a	$⊢ φ \to {H ↾}_{M} \in ((K ↾_{𝑡} M) Cn C)$

Proof

Step	Hyp	Ref	Expression
1		cvmlift2lem9a.b	$⊢ B = ⋃ C$
2		cvmlift2lem9a.y	$⊢ Y = ⋃ K$
3		cvmlift2lem9a.s	$⊢ S = (k \in J ⟼ \{s \in (𝒫 C ∖ \{\emptyset\}) \| (⋃ s = F^{-1} [k] \land \forall c \in s (\forall d \in (s ∖ \{c\}) c \cap d = \emptyset \land {F ↾}_{c} \in ((C ↾_{𝑡} c) Homeo (J ↾_{𝑡} k))))\})$
4		cvmlift2lem9a.f	$⊢ φ \to F \in (C CovMap J)$
5		cvmlift2lem9a.h	$⊢ φ \to H : Y ⟶ B$
6		cvmlift2lem9a.g	$⊢ φ \to F \circ H \in (K Cn J)$
7		cvmlift2lem9a.k	$⊢ φ \to K \in Top$
8		cvmlift2lem9a.1	$⊢ φ \to X \in Y$
9		cvmlift2lem9a.2	$⊢ φ \to T \in S (A)$
10		cvmlift2lem9a.3	$⊢ φ \to (W \in T \land H (X) \in W)$
11		cvmlift2lem9a.4	$⊢ φ \to M \subseteq Y$
12		cvmlift2lem9a.6	$⊢ φ \to H [M] \subseteq W$
13		cvmtop1	$⊢ F \in (C CovMap J) \to C \in Top$
14	4 13	syl	$⊢ φ \to C \in Top$
15		cnrest2r	$⊢ C \in Top \to (K ↾_{𝑡} M) Cn (C ↾_{𝑡} W) \subseteq (K ↾_{𝑡} M) Cn C$
16	14 15	syl	$⊢ φ \to (K ↾_{𝑡} M) Cn (C ↾_{𝑡} W) \subseteq (K ↾_{𝑡} M) Cn C$
17	5	ffnd	$⊢ φ \to H Fn Y$
18		fnssres	$⊢ (H Fn Y \land M \subseteq Y) \to ({H ↾}_{M}) Fn M$
19	17 11 18	syl2anc	$⊢ φ \to ({H ↾}_{M}) Fn M$
20		df-ima	$⊢ H [M] = ran ({H ↾}_{M})$
21	20 12	eqsstrrid	$⊢ φ \to ran ({H ↾}_{M}) \subseteq W$
22		df-f	$⊢ ({H ↾}_{M}) : M ⟶ W \leftrightarrow (({H ↾}_{M}) Fn M \land ran ({H ↾}_{M}) \subseteq W)$
23	19 21 22	sylanbrc	$⊢ φ \to ({H ↾}_{M}) : M ⟶ W$
24	10	simpld	$⊢ φ \to W \in T$
25	3	cvmsf1o	$⊢ (F \in (C CovMap J) \land T \in S (A) \land W \in T) \to ({F ↾}_{W}) : W \underset{1-1 onto}{⟶} A$
26	4 9 24 25	syl3anc	$⊢ φ \to ({F ↾}_{W}) : W \underset{1-1 onto}{⟶} A$
27	26	adantr	$⊢ (φ \land x \in (C ↾_{𝑡} W)) \to ({F ↾}_{W}) : W \underset{1-1 onto}{⟶} A$
28		f1of1	$⊢ ({F ↾}_{W}) : W \underset{1-1 onto}{⟶} A \to ({F ↾}_{W}) : W \underset{1-1}{⟶} A$
29	27 28	syl	$⊢ (φ \land x \in (C ↾_{𝑡} W)) \to ({F ↾}_{W}) : W \underset{1-1}{⟶} A$
30	1	toptopon	$⊢ C \in Top \leftrightarrow C \in TopOn (B)$
31	14 30	sylib	$⊢ φ \to C \in TopOn (B)$
32	3	cvmsss	$⊢ T \in S (A) \to T \subseteq C$
33	9 32	syl	$⊢ φ \to T \subseteq C$
34	33 24	sseldd	$⊢ φ \to W \in C$
35		toponss	$⊢ (C \in TopOn (B) \land W \in C) \to W \subseteq B$
36	31 34 35	syl2anc	$⊢ φ \to W \subseteq B$
37		resttopon	$⊢ (C \in TopOn (B) \land W \subseteq B) \to C ↾_{𝑡} W \in TopOn (W)$
38	31 36 37	syl2anc	$⊢ φ \to C ↾_{𝑡} W \in TopOn (W)$
39		toponss	$⊢ (C ↾_{𝑡} W \in TopOn (W) \land x \in (C ↾_{𝑡} W)) \to x \subseteq W$
40	38 39	sylan	$⊢ (φ \land x \in (C ↾_{𝑡} W)) \to x \subseteq W$
41		f1imacnv	$⊢ (({F ↾}_{W}) : W \underset{1-1}{⟶} A \land x \subseteq W) \to {({F ↾}_{W})}^{-1} [({F ↾}_{W}) [x]] = x$
42	29 40 41	syl2anc	$⊢ (φ \land x \in (C ↾_{𝑡} W)) \to {({F ↾}_{W})}^{-1} [({F ↾}_{W}) [x]] = x$
43	42	imaeq2d	$⊢ (φ \land x \in (C ↾_{𝑡} W)) \to {({H ↾}_{M})}^{-1} [{({F ↾}_{W})}^{-1} [({F ↾}_{W}) [x]]] = {({H ↾}_{M})}^{-1} [x]$
44		imaco	$⊢ ({({H ↾}_{M})}^{-1} \circ {({F ↾}_{W})}^{-1}) [({F ↾}_{W}) [x]] = {({H ↾}_{M})}^{-1} [{({F ↾}_{W})}^{-1} [({F ↾}_{W}) [x]]]$
45		cnvco	$⊢ {(({F ↾}_{W}) \circ ({H ↾}_{M}))}^{-1} = {({H ↾}_{M})}^{-1} \circ {({F ↾}_{W})}^{-1}$
46		cores	$⊢ ran ({H ↾}_{M}) \subseteq W \to ({F ↾}_{W}) \circ ({H ↾}_{M}) = F \circ ({H ↾}_{M})$
47	21 46	syl	$⊢ φ \to ({F ↾}_{W}) \circ ({H ↾}_{M}) = F \circ ({H ↾}_{M})$
48		resco	$⊢ {(F \circ H) ↾}_{M} = F \circ ({H ↾}_{M})$
49	47 48	eqtr4di	$⊢ φ \to ({F ↾}_{W}) \circ ({H ↾}_{M}) = {(F \circ H) ↾}_{M}$
50	49	adantr	$⊢ (φ \land x \in (C ↾_{𝑡} W)) \to ({F ↾}_{W}) \circ ({H ↾}_{M}) = {(F \circ H) ↾}_{M}$
51	50	cnveqd	$⊢ (φ \land x \in (C ↾_{𝑡} W)) \to {(({F ↾}_{W}) \circ ({H ↾}_{M}))}^{-1} = {({(F \circ H) ↾}_{M})}^{-1}$
52	45 51	eqtr3id	$⊢ (φ \land x \in (C ↾_{𝑡} W)) \to {({H ↾}_{M})}^{-1} \circ {({F ↾}_{W})}^{-1} = {({(F \circ H) ↾}_{M})}^{-1}$
53	52	imaeq1d	$⊢ (φ \land x \in (C ↾_{𝑡} W)) \to ({({H ↾}_{M})}^{-1} \circ {({F ↾}_{W})}^{-1}) [({F ↾}_{W}) [x]] = {({(F \circ H) ↾}_{M})}^{-1} [({F ↾}_{W}) [x]]$
54	44 53	eqtr3id	$⊢ (φ \land x \in (C ↾_{𝑡} W)) \to {({H ↾}_{M})}^{-1} [{({F ↾}_{W})}^{-1} [({F ↾}_{W}) [x]]] = {({(F \circ H) ↾}_{M})}^{-1} [({F ↾}_{W}) [x]]$
55	43 54	eqtr3d	$⊢ (φ \land x \in (C ↾_{𝑡} W)) \to {({H ↾}_{M})}^{-1} [x] = {({(F \circ H) ↾}_{M})}^{-1} [({F ↾}_{W}) [x]]$
56	2	cnrest	$⊢ (F \circ H \in (K Cn J) \land M \subseteq Y) \to {(F \circ H) ↾}_{M} \in ((K ↾_{𝑡} M) Cn J)$
57	6 11 56	syl2anc	$⊢ φ \to {(F \circ H) ↾}_{M} \in ((K ↾_{𝑡} M) Cn J)$
58	57	adantr	$⊢ (φ \land x \in (C ↾_{𝑡} W)) \to {(F \circ H) ↾}_{M} \in ((K ↾_{𝑡} M) Cn J)$
59		resima2	$⊢ x \subseteq W \to ({F ↾}_{W}) [x] = F [x]$
60	40 59	syl	$⊢ (φ \land x \in (C ↾_{𝑡} W)) \to ({F ↾}_{W}) [x] = F [x]$
61	4	adantr	$⊢ (φ \land x \in (C ↾_{𝑡} W)) \to F \in (C CovMap J)$
62		restopn2	$⊢ (C \in Top \land W \in C) \to (x \in (C ↾_{𝑡} W) \leftrightarrow (x \in C \land x \subseteq W))$
63	14 34 62	syl2anc	$⊢ φ \to (x \in (C ↾_{𝑡} W) \leftrightarrow (x \in C \land x \subseteq W))$
64	63	simprbda	$⊢ (φ \land x \in (C ↾_{𝑡} W)) \to x \in C$
65		cvmopn	$⊢ (F \in (C CovMap J) \land x \in C) \to F [x] \in J$
66	61 64 65	syl2anc	$⊢ (φ \land x \in (C ↾_{𝑡} W)) \to F [x] \in J$
67	60 66	eqeltrd	$⊢ (φ \land x \in (C ↾_{𝑡} W)) \to ({F ↾}_{W}) [x] \in J$
68		cnima	$⊢ ({(F \circ H) ↾}_{M} \in ((K ↾_{𝑡} M) Cn J) \land ({F ↾}_{W}) [x] \in J) \to {({(F \circ H) ↾}_{M})}^{-1} [({F ↾}_{W}) [x]] \in (K ↾_{𝑡} M)$
69	58 67 68	syl2anc	$⊢ (φ \land x \in (C ↾_{𝑡} W)) \to {({(F \circ H) ↾}_{M})}^{-1} [({F ↾}_{W}) [x]] \in (K ↾_{𝑡} M)$
70	55 69	eqeltrd	$⊢ (φ \land x \in (C ↾_{𝑡} W)) \to {({H ↾}_{M})}^{-1} [x] \in (K ↾_{𝑡} M)$
71	70	ralrimiva	$⊢ φ \to \forall x \in (C ↾_{𝑡} W) {({H ↾}_{M})}^{-1} [x] \in (K ↾_{𝑡} M)$
72	2	toptopon	$⊢ K \in Top \leftrightarrow K \in TopOn (Y)$
73	7 72	sylib	$⊢ φ \to K \in TopOn (Y)$
74		resttopon	$⊢ (K \in TopOn (Y) \land M \subseteq Y) \to K ↾_{𝑡} M \in TopOn (M)$
75	73 11 74	syl2anc	$⊢ φ \to K ↾_{𝑡} M \in TopOn (M)$
76		iscn	$⊢ (K ↾_{𝑡} M \in TopOn (M) \land C ↾_{𝑡} W \in TopOn (W)) \to ({H ↾}_{M} \in ((K ↾_{𝑡} M) Cn (C ↾_{𝑡} W)) \leftrightarrow (({H ↾}_{M}) : M ⟶ W \land \forall x \in (C ↾_{𝑡} W) {({H ↾}_{M})}^{-1} [x] \in (K ↾_{𝑡} M)))$
77	75 38 76	syl2anc	$⊢ φ \to ({H ↾}_{M} \in ((K ↾_{𝑡} M) Cn (C ↾_{𝑡} W)) \leftrightarrow (({H ↾}_{M}) : M ⟶ W \land \forall x \in (C ↾_{𝑡} W) {({H ↾}_{M})}^{-1} [x] \in (K ↾_{𝑡} M)))$
78	23 71 77	mpbir2and	$⊢ φ \to {H ↾}_{M} \in ((K ↾_{𝑡} M) Cn (C ↾_{𝑡} W))$
79	16 78	sseldd	$⊢ φ \to {H ↾}_{M} \in ((K ↾_{𝑡} M) Cn C)$

Metamath Proof Explorer

Theorem cvmlift2lem9a

Proof