cvmliftmolem1

	Ref	Expression
Hypotheses	cvmliftmo.b	$⊢ B = ⋃ C$
	cvmliftmo.y	$⊢ Y = ⋃ K$
	cvmliftmo.f	$⊢ φ \to F \in (C CovMap J)$
	cvmliftmo.k	$⊢ φ \to K \in Conn$
	cvmliftmo.l	$⊢ φ \to K \in N-LocallyConn$
	cvmliftmo.o	$⊢ φ \to O \in Y$
	cvmliftmoi.m	$⊢ φ \to M \in (K Cn C)$
	cvmliftmoi.n	$⊢ φ \to N \in (K Cn C)$
	cvmliftmoi.g	$⊢ φ \to F \circ M = F \circ N$
	cvmliftmoi.p	$⊢ φ \to M (O) = N (O)$
	cvmliftmolem.1	$⊢ S = (k \in J ⟼ \{s \in (𝒫 C ∖ \{\emptyset\}) \| (⋃ s = F^{-1} [k] \land \forall u \in s (\forall v \in (s ∖ \{u\}) u \cap v = \emptyset \land {F ↾}_{u} \in ((C ↾_{𝑡} u) Homeo (J ↾_{𝑡} k))))\})$
	cvmliftmolem.2	$⊢ (φ \land ψ) \to T \in S (U)$
	cvmliftmolem.3	$⊢ (φ \land ψ) \to W \in T$
	cvmliftmolem.4	$⊢ (φ \land ψ) \to I \subseteq M^{-1} [W]$
	cvmliftmolem.5	$⊢ (φ \land ψ) \to K ↾_{𝑡} I \in Conn$
	cvmliftmolem.6	$⊢ (φ \land ψ) \to X \in I$
	cvmliftmolem.7	$⊢ (φ \land ψ) \to Q \in I$
	cvmliftmolem.8	$⊢ (φ \land ψ) \to R \in I$
	cvmliftmolem.9	$⊢ (φ \land ψ) \to F (M (X)) \in U$
Assertion	cvmliftmolem1	$⊢ (φ \land ψ) \to (Q \in dom (M \cap N) \to R \in dom (M \cap N))$

Proof

Step	Hyp	Ref	Expression
1		cvmliftmo.b	$⊢ B = ⋃ C$
2		cvmliftmo.y	$⊢ Y = ⋃ K$
3		cvmliftmo.f	$⊢ φ \to F \in (C CovMap J)$
4		cvmliftmo.k	$⊢ φ \to K \in Conn$
5		cvmliftmo.l	$⊢ φ \to K \in N-LocallyConn$
6		cvmliftmo.o	$⊢ φ \to O \in Y$
7		cvmliftmoi.m	$⊢ φ \to M \in (K Cn C)$
8		cvmliftmoi.n	$⊢ φ \to N \in (K Cn C)$
9		cvmliftmoi.g	$⊢ φ \to F \circ M = F \circ N$
10		cvmliftmoi.p	$⊢ φ \to M (O) = N (O)$
11		cvmliftmolem.1	$⊢ S = (k \in J ⟼ \{s \in (𝒫 C ∖ \{\emptyset\}) \| (⋃ s = F^{-1} [k] \land \forall u \in s (\forall v \in (s ∖ \{u\}) u \cap v = \emptyset \land {F ↾}_{u} \in ((C ↾_{𝑡} u) Homeo (J ↾_{𝑡} k))))\})$
12		cvmliftmolem.2	$⊢ (φ \land ψ) \to T \in S (U)$
13		cvmliftmolem.3	$⊢ (φ \land ψ) \to W \in T$
14		cvmliftmolem.4	$⊢ (φ \land ψ) \to I \subseteq M^{-1} [W]$
15		cvmliftmolem.5	$⊢ (φ \land ψ) \to K ↾_{𝑡} I \in Conn$
16		cvmliftmolem.6	$⊢ (φ \land ψ) \to X \in I$
17		cvmliftmolem.7	$⊢ (φ \land ψ) \to Q \in I$
18		cvmliftmolem.8	$⊢ (φ \land ψ) \to R \in I$
19		cvmliftmolem.9	$⊢ (φ \land ψ) \to F (M (X)) \in U$
20	9	adantr	$⊢ (φ \land ψ) \to F \circ M = F \circ N$
21	20	fveq1d	$⊢ (φ \land ψ) \to (F \circ M) (R) = (F \circ N) (R)$
22	14 18	sseldd	$⊢ (φ \land ψ) \to R \in M^{-1} [W]$
23	2 1	cnf	$⊢ M \in (K Cn C) \to M : Y ⟶ B$
24	7 23	syl	$⊢ φ \to M : Y ⟶ B$
25	24	ffnd	$⊢ φ \to M Fn Y$
26		elpreima	$⊢ M Fn Y \to (R \in M^{-1} [W] \leftrightarrow (R \in Y \land M (R) \in W))$
27	25 26	syl	$⊢ φ \to (R \in M^{-1} [W] \leftrightarrow (R \in Y \land M (R) \in W))$
28	27	simprbda	$⊢ (φ \land R \in M^{-1} [W]) \to R \in Y$
29	22 28	syldan	$⊢ (φ \land ψ) \to R \in Y$
30		fvco3	$⊢ (M : Y ⟶ B \land R \in Y) \to (F \circ M) (R) = F (M (R))$
31	24 30	sylan	$⊢ (φ \land R \in Y) \to (F \circ M) (R) = F (M (R))$
32	29 31	syldan	$⊢ (φ \land ψ) \to (F \circ M) (R) = F (M (R))$
33	2 1	cnf	$⊢ N \in (K Cn C) \to N : Y ⟶ B$
34	8 33	syl	$⊢ φ \to N : Y ⟶ B$
35		fvco3	$⊢ (N : Y ⟶ B \land R \in Y) \to (F \circ N) (R) = F (N (R))$
36	34 35	sylan	$⊢ (φ \land R \in Y) \to (F \circ N) (R) = F (N (R))$
37	29 36	syldan	$⊢ (φ \land ψ) \to (F \circ N) (R) = F (N (R))$
38	21 32 37	3eqtr3d	$⊢ (φ \land ψ) \to F (M (R)) = F (N (R))$
39	38	adantr	$⊢ ((φ \land ψ) \land M (Q) = N (Q)) \to F (M (R)) = F (N (R))$
40	27	simplbda	$⊢ (φ \land R \in M^{-1} [W]) \to M (R) \in W$
41	22 40	syldan	$⊢ (φ \land ψ) \to M (R) \in W$
42	41	adantr	$⊢ ((φ \land ψ) \land M (Q) = N (Q)) \to M (R) \in W$
43		fvres	$⊢ M (R) \in W \to ({F ↾}_{W}) (M (R)) = F (M (R))$
44	42 43	syl	$⊢ ((φ \land ψ) \land M (Q) = N (Q)) \to ({F ↾}_{W}) (M (R)) = F (M (R))$
45	18	adantr	$⊢ ((φ \land ψ) \land M (Q) = N (Q)) \to R \in I$
46		fvres	$⊢ R \in I \to ({N ↾}_{I}) (R) = N (R)$
47	45 46	syl	$⊢ ((φ \land ψ) \land M (Q) = N (Q)) \to ({N ↾}_{I}) (R) = N (R)$
48		eqid	$⊢ ⋃ (K ↾_{𝑡} I) = ⋃ (K ↾_{𝑡} I)$
49	15	adantr	$⊢ ((φ \land ψ) \land M (Q) = N (Q)) \to K ↾_{𝑡} I \in Conn$
50	8	adantr	$⊢ (φ \land ψ) \to N \in (K Cn C)$
51		cnvimass	$⊢ M^{-1} [W] \subseteq dom M$
52	51 24	fssdm	$⊢ φ \to M^{-1} [W] \subseteq Y$
53	52	adantr	$⊢ (φ \land ψ) \to M^{-1} [W] \subseteq Y$
54	14 53	sstrd	$⊢ (φ \land ψ) \to I \subseteq Y$
55	2	cnrest	$⊢ (N \in (K Cn C) \land I \subseteq Y) \to {N ↾}_{I} \in ((K ↾_{𝑡} I) Cn C)$
56	50 54 55	syl2anc	$⊢ (φ \land ψ) \to {N ↾}_{I} \in ((K ↾_{𝑡} I) Cn C)$
57	3	adantr	$⊢ (φ \land ψ) \to F \in (C CovMap J)$
58		cvmtop1	$⊢ F \in (C CovMap J) \to C \in Top$
59	57 58	syl	$⊢ (φ \land ψ) \to C \in Top$
60	1	toptopon	$⊢ C \in Top \leftrightarrow C \in TopOn (B)$
61	59 60	sylib	$⊢ (φ \land ψ) \to C \in TopOn (B)$
62		df-ima	$⊢ N [I] = ran ({N ↾}_{I})$
63		elssuni	$⊢ W \in T \to W \subseteq ⋃ T$
64	13 63	syl	$⊢ (φ \land ψ) \to W \subseteq ⋃ T$
65	11	cvmsuni	$⊢ T \in S (U) \to ⋃ T = F^{-1} [U]$
66	12 65	syl	$⊢ (φ \land ψ) \to ⋃ T = F^{-1} [U]$
67	64 66	sseqtrd	$⊢ (φ \land ψ) \to W \subseteq F^{-1} [U]$
68		imass2	$⊢ W \subseteq F^{-1} [U] \to M^{-1} [W] \subseteq M^{-1} [F^{-1} [U]]$
69	67 68	syl	$⊢ (φ \land ψ) \to M^{-1} [W] \subseteq M^{-1} [F^{-1} [U]]$
70	14 69	sstrd	$⊢ (φ \land ψ) \to I \subseteq M^{-1} [F^{-1} [U]]$
71	20	cnveqd	$⊢ (φ \land ψ) \to {(F \circ M)}^{-1} = {(F \circ N)}^{-1}$
72		cnvco	$⊢ {(F \circ M)}^{-1} = M^{-1} \circ F^{-1}$
73		cnvco	$⊢ {(F \circ N)}^{-1} = N^{-1} \circ F^{-1}$
74	71 72 73	3eqtr3g	$⊢ (φ \land ψ) \to M^{-1} \circ F^{-1} = N^{-1} \circ F^{-1}$
75	74	imaeq1d	$⊢ (φ \land ψ) \to (M^{-1} \circ F^{-1}) [U] = (N^{-1} \circ F^{-1}) [U]$
76		imaco	$⊢ (M^{-1} \circ F^{-1}) [U] = M^{-1} [F^{-1} [U]]$
77		imaco	$⊢ (N^{-1} \circ F^{-1}) [U] = N^{-1} [F^{-1} [U]]$
78	75 76 77	3eqtr3g	$⊢ (φ \land ψ) \to M^{-1} [F^{-1} [U]] = N^{-1} [F^{-1} [U]]$
79	70 78	sseqtrd	$⊢ (φ \land ψ) \to I \subseteq N^{-1} [F^{-1} [U]]$
80	34	adantr	$⊢ (φ \land ψ) \to N : Y ⟶ B$
81	80	ffund	$⊢ (φ \land ψ) \to Fun N$
82	80	fdmd	$⊢ (φ \land ψ) \to dom N = Y$
83	54 82	sseqtrrd	$⊢ (φ \land ψ) \to I \subseteq dom N$
84		funimass3	$⊢ (Fun N \land I \subseteq dom N) \to (N [I] \subseteq F^{-1} [U] \leftrightarrow I \subseteq N^{-1} [F^{-1} [U]])$
85	81 83 84	syl2anc	$⊢ (φ \land ψ) \to (N [I] \subseteq F^{-1} [U] \leftrightarrow I \subseteq N^{-1} [F^{-1} [U]])$
86	79 85	mpbird	$⊢ (φ \land ψ) \to N [I] \subseteq F^{-1} [U]$
87	62 86	eqsstrrid	$⊢ (φ \land ψ) \to ran ({N ↾}_{I}) \subseteq F^{-1} [U]$
88		cnvimass	$⊢ F^{-1} [U] \subseteq dom F$
89		cvmcn	$⊢ F \in (C CovMap J) \to F \in (C Cn J)$
90	3 89	syl	$⊢ φ \to F \in (C Cn J)$
91		eqid	$⊢ ⋃ J = ⋃ J$
92	1 91	cnf	$⊢ F \in (C Cn J) \to F : B ⟶ ⋃ J$
93	90 92	syl	$⊢ φ \to F : B ⟶ ⋃ J$
94	93	fdmd	$⊢ φ \to dom F = B$
95	94	adantr	$⊢ (φ \land ψ) \to dom F = B$
96	88 95	sseqtrid	$⊢ (φ \land ψ) \to F^{-1} [U] \subseteq B$
97		cnrest2	$⊢ (C \in TopOn (B) \land ran ({N ↾}_{I}) \subseteq F^{-1} [U] \land F^{-1} [U] \subseteq B) \to ({N ↾}_{I} \in ((K ↾_{𝑡} I) Cn C) \leftrightarrow {N ↾}_{I} \in ((K ↾_{𝑡} I) Cn (C ↾_{𝑡} F^{-1} [U])))$
98	61 87 96 97	syl3anc	$⊢ (φ \land ψ) \to ({N ↾}_{I} \in ((K ↾_{𝑡} I) Cn C) \leftrightarrow {N ↾}_{I} \in ((K ↾_{𝑡} I) Cn (C ↾_{𝑡} F^{-1} [U])))$
99	56 98	mpbid	$⊢ (φ \land ψ) \to {N ↾}_{I} \in ((K ↾_{𝑡} I) Cn (C ↾_{𝑡} F^{-1} [U]))$
100	99	adantr	$⊢ ((φ \land ψ) \land M (Q) = N (Q)) \to {N ↾}_{I} \in ((K ↾_{𝑡} I) Cn (C ↾_{𝑡} F^{-1} [U]))$
101		dfss2	$⊢ W \subseteq F^{-1} [U] \leftrightarrow W \cap F^{-1} [U] = W$
102	67 101	sylib	$⊢ (φ \land ψ) \to W \cap F^{-1} [U] = W$
103	1	topopn	$⊢ C \in Top \to B \in C$
104	59 103	syl	$⊢ (φ \land ψ) \to B \in C$
105	104 96	ssexd	$⊢ (φ \land ψ) \to F^{-1} [U] \in V$
106	11	cvmsss	$⊢ T \in S (U) \to T \subseteq C$
107	12 106	syl	$⊢ (φ \land ψ) \to T \subseteq C$
108	107 13	sseldd	$⊢ (φ \land ψ) \to W \in C$
109		elrestr	$⊢ (C \in Top \land F^{-1} [U] \in V \land W \in C) \to W \cap F^{-1} [U] \in (C ↾_{𝑡} F^{-1} [U])$
110	59 105 108 109	syl3anc	$⊢ (φ \land ψ) \to W \cap F^{-1} [U] \in (C ↾_{𝑡} F^{-1} [U])$
111	102 110	eqeltrrd	$⊢ (φ \land ψ) \to W \in (C ↾_{𝑡} F^{-1} [U])$
112	111	adantr	$⊢ ((φ \land ψ) \land M (Q) = N (Q)) \to W \in (C ↾_{𝑡} F^{-1} [U])$
113	11	cvmscld	$⊢ (F \in (C CovMap J) \land T \in S (U) \land W \in T) \to W \in Clsd (C ↾_{𝑡} F^{-1} [U])$
114	57 12 13 113	syl3anc	$⊢ (φ \land ψ) \to W \in Clsd (C ↾_{𝑡} F^{-1} [U])$
115	114	adantr	$⊢ ((φ \land ψ) \land M (Q) = N (Q)) \to W \in Clsd (C ↾_{𝑡} F^{-1} [U])$
116		conntop	$⊢ K \in Conn \to K \in Top$
117	4 116	syl	$⊢ φ \to K \in Top$
118	117	adantr	$⊢ (φ \land ψ) \to K \in Top$
119	2	restuni	$⊢ (K \in Top \land I \subseteq Y) \to I = ⋃ (K ↾_{𝑡} I)$
120	118 54 119	syl2anc	$⊢ (φ \land ψ) \to I = ⋃ (K ↾_{𝑡} I)$
121	17 120	eleqtrd	$⊢ (φ \land ψ) \to Q \in ⋃ (K ↾_{𝑡} I)$
122	121	adantr	$⊢ ((φ \land ψ) \land M (Q) = N (Q)) \to Q \in ⋃ (K ↾_{𝑡} I)$
123	17	adantr	$⊢ ((φ \land ψ) \land M (Q) = N (Q)) \to Q \in I$
124		fvres	$⊢ Q \in I \to ({N ↾}_{I}) (Q) = N (Q)$
125	123 124	syl	$⊢ ((φ \land ψ) \land M (Q) = N (Q)) \to ({N ↾}_{I}) (Q) = N (Q)$
126		simpr	$⊢ ((φ \land ψ) \land M (Q) = N (Q)) \to M (Q) = N (Q)$
127	14 17	sseldd	$⊢ (φ \land ψ) \to Q \in M^{-1} [W]$
128		elpreima	$⊢ M Fn Y \to (Q \in M^{-1} [W] \leftrightarrow (Q \in Y \land M (Q) \in W))$
129	25 128	syl	$⊢ φ \to (Q \in M^{-1} [W] \leftrightarrow (Q \in Y \land M (Q) \in W))$
130	129	simplbda	$⊢ (φ \land Q \in M^{-1} [W]) \to M (Q) \in W$
131	127 130	syldan	$⊢ (φ \land ψ) \to M (Q) \in W$
132	131	adantr	$⊢ ((φ \land ψ) \land M (Q) = N (Q)) \to M (Q) \in W$
133	126 132	eqeltrrd	$⊢ ((φ \land ψ) \land M (Q) = N (Q)) \to N (Q) \in W$
134	125 133	eqeltrd	$⊢ ((φ \land ψ) \land M (Q) = N (Q)) \to ({N ↾}_{I}) (Q) \in W$
135	48 49 100 112 115 122 134	conncn	$⊢ ((φ \land ψ) \land M (Q) = N (Q)) \to ({N ↾}_{I}) : ⋃ (K ↾_{𝑡} I) ⟶ W$
136	120	adantr	$⊢ ((φ \land ψ) \land M (Q) = N (Q)) \to I = ⋃ (K ↾_{𝑡} I)$
137	136	feq2d	$⊢ ((φ \land ψ) \land M (Q) = N (Q)) \to (({N ↾}_{I}) : I ⟶ W \leftrightarrow ({N ↾}_{I}) : ⋃ (K ↾_{𝑡} I) ⟶ W)$
138	135 137	mpbird	$⊢ ((φ \land ψ) \land M (Q) = N (Q)) \to ({N ↾}_{I}) : I ⟶ W$
139	138 45	ffvelcdmd	$⊢ ((φ \land ψ) \land M (Q) = N (Q)) \to ({N ↾}_{I}) (R) \in W$
140	47 139	eqeltrrd	$⊢ ((φ \land ψ) \land M (Q) = N (Q)) \to N (R) \in W$
141		fvres	$⊢ N (R) \in W \to ({F ↾}_{W}) (N (R)) = F (N (R))$
142	140 141	syl	$⊢ ((φ \land ψ) \land M (Q) = N (Q)) \to ({F ↾}_{W}) (N (R)) = F (N (R))$
143	39 44 142	3eqtr4d	$⊢ ((φ \land ψ) \land M (Q) = N (Q)) \to ({F ↾}_{W}) (M (R)) = ({F ↾}_{W}) (N (R))$
144	11	cvmsf1o	$⊢ (F \in (C CovMap J) \land T \in S (U) \land W \in T) \to ({F ↾}_{W}) : W \underset{1-1 onto}{⟶} U$
145	57 12 13 144	syl3anc	$⊢ (φ \land ψ) \to ({F ↾}_{W}) : W \underset{1-1 onto}{⟶} U$
146		f1of1	$⊢ ({F ↾}_{W}) : W \underset{1-1 onto}{⟶} U \to ({F ↾}_{W}) : W \underset{1-1}{⟶} U$
147	145 146	syl	$⊢ (φ \land ψ) \to ({F ↾}_{W}) : W \underset{1-1}{⟶} U$
148	147	adantr	$⊢ ((φ \land ψ) \land M (Q) = N (Q)) \to ({F ↾}_{W}) : W \underset{1-1}{⟶} U$
149		f1fveq	$⊢ (({F ↾}_{W}) : W \underset{1-1}{⟶} U \land (M (R) \in W \land N (R) \in W)) \to (({F ↾}_{W}) (M (R)) = ({F ↾}_{W}) (N (R)) \leftrightarrow M (R) = N (R))$
150	148 42 140 149	syl12anc	$⊢ ((φ \land ψ) \land M (Q) = N (Q)) \to (({F ↾}_{W}) (M (R)) = ({F ↾}_{W}) (N (R)) \leftrightarrow M (R) = N (R))$
151	143 150	mpbid	$⊢ ((φ \land ψ) \land M (Q) = N (Q)) \to M (R) = N (R)$
152	151	ex	$⊢ (φ \land ψ) \to (M (Q) = N (Q) \to M (R) = N (R))$
153	129	simprbda	$⊢ (φ \land Q \in M^{-1} [W]) \to Q \in Y$
154	127 153	syldan	$⊢ (φ \land ψ) \to Q \in Y$
155		fveq2	$⊢ x = Q \to M (x) = M (Q)$
156		fveq2	$⊢ x = Q \to N (x) = N (Q)$
157	155 156	eqeq12d	$⊢ x = Q \to (M (x) = N (x) \leftrightarrow M (Q) = N (Q))$
158	157	elrab3	$⊢ Q \in Y \to (Q \in \{x \in Y \| M (x) = N (x)\} \leftrightarrow M (Q) = N (Q))$
159	154 158	syl	$⊢ (φ \land ψ) \to (Q \in \{x \in Y \| M (x) = N (x)\} \leftrightarrow M (Q) = N (Q))$
160		fveq2	$⊢ x = R \to M (x) = M (R)$
161		fveq2	$⊢ x = R \to N (x) = N (R)$
162	160 161	eqeq12d	$⊢ x = R \to (M (x) = N (x) \leftrightarrow M (R) = N (R))$
163	162	elrab3	$⊢ R \in Y \to (R \in \{x \in Y \| M (x) = N (x)\} \leftrightarrow M (R) = N (R))$
164	29 163	syl	$⊢ (φ \land ψ) \to (R \in \{x \in Y \| M (x) = N (x)\} \leftrightarrow M (R) = N (R))$
165	152 159 164	3imtr4d	$⊢ (φ \land ψ) \to (Q \in \{x \in Y \| M (x) = N (x)\} \to R \in \{x \in Y \| M (x) = N (x)\})$
166	34	ffnd	$⊢ φ \to N Fn Y$
167		fndmin	$⊢ (M Fn Y \land N Fn Y) \to dom (M \cap N) = \{x \in Y \| M (x) = N (x)\}$
168	25 166 167	syl2anc	$⊢ φ \to dom (M \cap N) = \{x \in Y \| M (x) = N (x)\}$
169	168	adantr	$⊢ (φ \land ψ) \to dom (M \cap N) = \{x \in Y \| M (x) = N (x)\}$
170	169	eleq2d	$⊢ (φ \land ψ) \to (Q \in dom (M \cap N) \leftrightarrow Q \in \{x \in Y \| M (x) = N (x)\})$
171	169	eleq2d	$⊢ (φ \land ψ) \to (R \in dom (M \cap N) \leftrightarrow R \in \{x \in Y \| M (x) = N (x)\})$
172	165 170 171	3imtr4d	$⊢ (φ \land ψ) \to (Q \in dom (M \cap N) \to R \in dom (M \cap N))$

Metamath Proof Explorer

Theorem cvmliftmolem1

Proof