cvmlift2lem9

	Ref	Expression
Hypotheses	cvmlift2.b	$⊢ B = ⋃ C$
	cvmlift2.f	$⊢ φ \to F \in (C CovMap J)$
	cvmlift2.g	$⊢ φ \to G \in ((II \times_{t} II) Cn J)$
	cvmlift2.p	$⊢ φ \to P \in B$
	cvmlift2.i	$⊢ φ \to F (P) = 0 G 0$
	cvmlift2.h	$⊢ H = (ι f \in (II Cn C) \| (F \circ f = (z \in [0, 1] ⟼ z G 0) \land f (0) = P))$
	cvmlift2.k	$⊢ K = (x \in [0, 1], y \in [0, 1] ⟼ (ι f \in (II Cn C) \| (F \circ f = (z \in [0, 1] ⟼ x G z) \land f (0) = H (x))) (y))$
	cvmlift2lem10.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))))\})$
	cvmlift2lem9.1	$⊢ φ \to X G Y \in M$
	cvmlift2lem9.2	$⊢ φ \to T \in S (M)$
	cvmlift2lem9.3	$⊢ φ \to U \in II$
	cvmlift2lem9.4	$⊢ φ \to V \in II$
	cvmlift2lem9.5	$⊢ φ \to II ↾_{𝑡} U \in Conn$
	cvmlift2lem9.6	$⊢ φ \to II ↾_{𝑡} V \in Conn$
	cvmlift2lem9.7	$⊢ φ \to X \in U$
	cvmlift2lem9.8	$⊢ φ \to Y \in V$
	cvmlift2lem9.9	$⊢ φ \to U \times V \subseteq G^{-1} [M]$
	cvmlift2lem9.10	$⊢ φ \to Z \in V$
	cvmlift2lem9.11	$⊢ φ \to {K ↾}_{(U \times \{Z\})} \in (((II \times_{t} II) ↾_{𝑡} (U \times \{Z\})) Cn C)$
	cvmlift2lem9.w	$⊢ W = (ι b \in T \| X K Y \in b)$
Assertion	cvmlift2lem9	$⊢ φ \to {K ↾}_{(U \times V)} \in (((II \times_{t} II) ↾_{𝑡} (U \times V)) Cn C)$

Proof

Step	Hyp	Ref	Expression
1		cvmlift2.b	$⊢ B = ⋃ C$
2		cvmlift2.f	$⊢ φ \to F \in (C CovMap J)$
3		cvmlift2.g	$⊢ φ \to G \in ((II \times_{t} II) Cn J)$
4		cvmlift2.p	$⊢ φ \to P \in B$
5		cvmlift2.i	$⊢ φ \to F (P) = 0 G 0$
6		cvmlift2.h	$⊢ H = (ι f \in (II Cn C) \| (F \circ f = (z \in [0, 1] ⟼ z G 0) \land f (0) = P))$
7		cvmlift2.k	$⊢ K = (x \in [0, 1], y \in [0, 1] ⟼ (ι f \in (II Cn C) \| (F \circ f = (z \in [0, 1] ⟼ x G z) \land f (0) = H (x))) (y))$
8		cvmlift2lem10.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))))\})$
9		cvmlift2lem9.1	$⊢ φ \to X G Y \in M$
10		cvmlift2lem9.2	$⊢ φ \to T \in S (M)$
11		cvmlift2lem9.3	$⊢ φ \to U \in II$
12		cvmlift2lem9.4	$⊢ φ \to V \in II$
13		cvmlift2lem9.5	$⊢ φ \to II ↾_{𝑡} U \in Conn$
14		cvmlift2lem9.6	$⊢ φ \to II ↾_{𝑡} V \in Conn$
15		cvmlift2lem9.7	$⊢ φ \to X \in U$
16		cvmlift2lem9.8	$⊢ φ \to Y \in V$
17		cvmlift2lem9.9	$⊢ φ \to U \times V \subseteq G^{-1} [M]$
18		cvmlift2lem9.10	$⊢ φ \to Z \in V$
19		cvmlift2lem9.11	$⊢ φ \to {K ↾}_{(U \times \{Z\})} \in (((II \times_{t} II) ↾_{𝑡} (U \times \{Z\})) Cn C)$
20		cvmlift2lem9.w	$⊢ W = (ι b \in T \| X K Y \in b)$
21		iitop	$⊢ II \in Top$
22		iiuni	$⊢ [0, 1] = ⋃ II$
23	21 21 22 22	txunii	$⊢ [0, 1] \times [0, 1] = ⋃ (II \times_{t} II)$
24	1 2 3 4 5 6 7	cvmlift2lem5	$⊢ φ \to K : [0, 1] \times [0, 1] ⟶ B$
25	1 2 3 4 5 6 7	cvmlift2lem7	$⊢ φ \to F \circ K = G$
26	25 3	eqeltrd	$⊢ φ \to F \circ K \in ((II \times_{t} II) Cn J)$
27	21 21	txtopi	$⊢ II \times_{t} II \in Top$
28	27	a1i	$⊢ φ \to II \times_{t} II \in Top$
29		elssuni	$⊢ U \in II \to U \subseteq ⋃ II$
30	29 22	sseqtrrdi	$⊢ U \in II \to U \subseteq [0, 1]$
31	11 30	syl	$⊢ φ \to U \subseteq [0, 1]$
32	31 15	sseldd	$⊢ φ \to X \in [0, 1]$
33		elssuni	$⊢ V \in II \to V \subseteq ⋃ II$
34	33 22	sseqtrrdi	$⊢ V \in II \to V \subseteq [0, 1]$
35	12 34	syl	$⊢ φ \to V \subseteq [0, 1]$
36	35 16	sseldd	$⊢ φ \to Y \in [0, 1]$
37		opelxpi	$⊢ (X \in [0, 1] \land Y \in [0, 1]) \to ⟨X, Y⟩ \in ([0, 1] \times [0, 1])$
38	32 36 37	syl2anc	$⊢ φ \to ⟨X, Y⟩ \in ([0, 1] \times [0, 1])$
39	24 32 36	fovrnd	$⊢ φ \to X K Y \in B$
40		fvco3	$⊢ (K : [0, 1] \times [0, 1] ⟶ B \land ⟨X, Y⟩ \in ([0, 1] \times [0, 1])) \to (F \circ K) (⟨X, Y⟩) = F (K (⟨X, Y⟩))$
41	24 38 40	syl2anc	$⊢ φ \to (F \circ K) (⟨X, Y⟩) = F (K (⟨X, Y⟩))$
42	25	fveq1d	$⊢ φ \to (F \circ K) (⟨X, Y⟩) = G (⟨X, Y⟩)$
43	41 42	eqtr3d	$⊢ φ \to F (K (⟨X, Y⟩)) = G (⟨X, Y⟩)$
44		df-ov	$⊢ X K Y = K (⟨X, Y⟩)$
45	44	fveq2i	$⊢ F (X K Y) = F (K (⟨X, Y⟩))$
46		df-ov	$⊢ X G Y = G (⟨X, Y⟩)$
47	43 45 46	3eqtr4g	$⊢ φ \to F (X K Y) = X G Y$
48	47 9	eqeltrd	$⊢ φ \to F (X K Y) \in M$
49	8 1 20	cvmsiota	$⊢ (F \in (C CovMap J) \land (T \in S (M) \land X K Y \in B \land F (X K Y) \in M)) \to (W \in T \land X K Y \in W)$
50	2 10 39 48 49	syl13anc	$⊢ φ \to (W \in T \land X K Y \in W)$
51	44	eleq1i	$⊢ X K Y \in W \leftrightarrow K (⟨X, Y⟩) \in W$
52	51	anbi2i	$⊢ (W \in T \land X K Y \in W) \leftrightarrow (W \in T \land K (⟨X, Y⟩) \in W)$
53	50 52	sylib	$⊢ φ \to (W \in T \land K (⟨X, Y⟩) \in W)$
54		xpss12	$⊢ (U \subseteq [0, 1] \land V \subseteq [0, 1]) \to U \times V \subseteq [0, 1] \times [0, 1]$
55	31 35 54	syl2anc	$⊢ φ \to U \times V \subseteq [0, 1] \times [0, 1]$
56		snidg	$⊢ m \in U \to m \in \{m\}$
57	56	ad2antrl	$⊢ (φ \land (m \in U \land n \in V)) \to m \in \{m\}$
58		simprr	$⊢ (φ \land (m \in U \land n \in V)) \to n \in V$
59		ovres	$⊢ (m \in \{m\} \land n \in V) \to m ({K ↾}_{(\{m\} \times V)}) n = m K n$
60	57 58 59	syl2anc	$⊢ (φ \land (m \in U \land n \in V)) \to m ({K ↾}_{(\{m\} \times V)}) n = m K n$
61		eqid	$⊢ ⋃ ((II \times_{t} II) ↾_{𝑡} (\{m\} \times V)) = ⋃ ((II \times_{t} II) ↾_{𝑡} (\{m\} \times V))$
62	21	a1i	$⊢ (φ \land (m \in U \land n \in V)) \to II \in Top$
63		snex	$⊢ \{m\} \in V$
64	63	a1i	$⊢ (φ \land (m \in U \land n \in V)) \to \{m\} \in V$
65	12	adantr	$⊢ (φ \land (m \in U \land n \in V)) \to V \in II$
66		txrest	$⊢ ((II \in Top \land II \in Top) \land (\{m\} \in V \land V \in II)) \to (II \times_{t} II) ↾_{𝑡} (\{m\} \times V) = (II ↾_{𝑡} \{m\}) \times_{t} (II ↾_{𝑡} V)$
67	62 62 64 65 66	syl22anc	$⊢ (φ \land (m \in U \land n \in V)) \to (II \times_{t} II) ↾_{𝑡} (\{m\} \times V) = (II ↾_{𝑡} \{m\}) \times_{t} (II ↾_{𝑡} V)$
68		iitopon	$⊢ II \in TopOn ([0, 1])$
69	31	sselda	$⊢ (φ \land m \in U) \to m \in [0, 1]$
70	69	adantrr	$⊢ (φ \land (m \in U \land n \in V)) \to m \in [0, 1]$
71		restsn2	$⊢ (II \in TopOn ([0, 1]) \land m \in [0, 1]) \to II ↾_{𝑡} \{m\} = 𝒫 \{m\}$
72	68 70 71	sylancr	$⊢ (φ \land (m \in U \land n \in V)) \to II ↾_{𝑡} \{m\} = 𝒫 \{m\}$
73		pwsn	$⊢ 𝒫 \{m\} = \{\emptyset, \{m\}\}$
74		indisconn	$⊢ \{\emptyset, \{m\}\} \in Conn$
75	73 74	eqeltri	$⊢ 𝒫 \{m\} \in Conn$
76	72 75	eqeltrdi	$⊢ (φ \land (m \in U \land n \in V)) \to II ↾_{𝑡} \{m\} \in Conn$
77	14	adantr	$⊢ (φ \land (m \in U \land n \in V)) \to II ↾_{𝑡} V \in Conn$
78		txconn	$⊢ (II ↾_{𝑡} \{m\} \in Conn \land II ↾_{𝑡} V \in Conn) \to (II ↾_{𝑡} \{m\}) \times_{t} (II ↾_{𝑡} V) \in Conn$
79	76 77 78	syl2anc	$⊢ (φ \land (m \in U \land n \in V)) \to (II ↾_{𝑡} \{m\}) \times_{t} (II ↾_{𝑡} V) \in Conn$
80	67 79	eqeltrd	$⊢ (φ \land (m \in U \land n \in V)) \to (II \times_{t} II) ↾_{𝑡} (\{m\} \times V) \in Conn$
81	1 2 3 4 5 6 7	cvmlift2lem6	$⊢ (φ \land m \in [0, 1]) \to {K ↾}_{(\{m\} \times [0, 1])} \in (((II \times_{t} II) ↾_{𝑡} (\{m\} \times [0, 1])) Cn C)$
82	70 81	syldan	$⊢ (φ \land (m \in U \land n \in V)) \to {K ↾}_{(\{m\} \times [0, 1])} \in (((II \times_{t} II) ↾_{𝑡} (\{m\} \times [0, 1])) Cn C)$
83	35	adantr	$⊢ (φ \land (m \in U \land n \in V)) \to V \subseteq [0, 1]$
84		xpss2	$⊢ V \subseteq [0, 1] \to \{m\} \times V \subseteq \{m\} \times [0, 1]$
85	83 84	syl	$⊢ (φ \land (m \in U \land n \in V)) \to \{m\} \times V \subseteq \{m\} \times [0, 1]$
86	70	snssd	$⊢ (φ \land (m \in U \land n \in V)) \to \{m\} \subseteq [0, 1]$
87		xpss1	$⊢ \{m\} \subseteq [0, 1] \to \{m\} \times [0, 1] \subseteq [0, 1] \times [0, 1]$
88	86 87	syl	$⊢ (φ \land (m \in U \land n \in V)) \to \{m\} \times [0, 1] \subseteq [0, 1] \times [0, 1]$
89	23	restuni	$⊢ (II \times_{t} II \in Top \land \{m\} \times [0, 1] \subseteq [0, 1] \times [0, 1]) \to \{m\} \times [0, 1] = ⋃ ((II \times_{t} II) ↾_{𝑡} (\{m\} \times [0, 1]))$
90	27 88 89	sylancr	$⊢ (φ \land (m \in U \land n \in V)) \to \{m\} \times [0, 1] = ⋃ ((II \times_{t} II) ↾_{𝑡} (\{m\} \times [0, 1]))$
91	85 90	sseqtrd	$⊢ (φ \land (m \in U \land n \in V)) \to \{m\} \times V \subseteq ⋃ ((II \times_{t} II) ↾_{𝑡} (\{m\} \times [0, 1]))$
92		eqid	$⊢ ⋃ ((II \times_{t} II) ↾_{𝑡} (\{m\} \times [0, 1])) = ⋃ ((II \times_{t} II) ↾_{𝑡} (\{m\} \times [0, 1]))$
93	92	cnrest	$⊢ ({K ↾}_{(\{m\} \times [0, 1])} \in (((II \times_{t} II) ↾_{𝑡} (\{m\} \times [0, 1])) Cn C) \land \{m\} \times V \subseteq ⋃ ((II \times_{t} II) ↾_{𝑡} (\{m\} \times [0, 1]))) \to {({K ↾}_{(\{m\} \times [0, 1])}) ↾}_{(\{m\} \times V)} \in ((((II \times_{t} II) ↾_{𝑡} (\{m\} \times [0, 1])) ↾_{𝑡} (\{m\} \times V)) Cn C)$
94	82 91 93	syl2anc	$⊢ (φ \land (m \in U \land n \in V)) \to {({K ↾}_{(\{m\} \times [0, 1])}) ↾}_{(\{m\} \times V)} \in ((((II \times_{t} II) ↾_{𝑡} (\{m\} \times [0, 1])) ↾_{𝑡} (\{m\} \times V)) Cn C)$
95	85	resabs1d	$⊢ (φ \land (m \in U \land n \in V)) \to {({K ↾}_{(\{m\} \times [0, 1])}) ↾}_{(\{m\} \times V)} = {K ↾}_{(\{m\} \times V)}$
96	27	a1i	$⊢ (φ \land (m \in U \land n \in V)) \to II \times_{t} II \in Top$
97		ovex	$⊢ [0, 1] \in V$
98	63 97	xpex	$⊢ \{m\} \times [0, 1] \in V$
99	98	a1i	$⊢ (φ \land (m \in U \land n \in V)) \to \{m\} \times [0, 1] \in V$
100		restabs	$⊢ (II \times_{t} II \in Top \land \{m\} \times V \subseteq \{m\} \times [0, 1] \land \{m\} \times [0, 1] \in V) \to ((II \times_{t} II) ↾_{𝑡} (\{m\} \times [0, 1])) ↾_{𝑡} (\{m\} \times V) = (II \times_{t} II) ↾_{𝑡} (\{m\} \times V)$
101	96 85 99 100	syl3anc	$⊢ (φ \land (m \in U \land n \in V)) \to ((II \times_{t} II) ↾_{𝑡} (\{m\} \times [0, 1])) ↾_{𝑡} (\{m\} \times V) = (II \times_{t} II) ↾_{𝑡} (\{m\} \times V)$
102	101	oveq1d	$⊢ (φ \land (m \in U \land n \in V)) \to (((II \times_{t} II) ↾_{𝑡} (\{m\} \times [0, 1])) ↾_{𝑡} (\{m\} \times V)) Cn C = ((II \times_{t} II) ↾_{𝑡} (\{m\} \times V)) Cn C$
103	94 95 102	3eltr3d	$⊢ (φ \land (m \in U \land n \in V)) \to {K ↾}_{(\{m\} \times V)} \in (((II \times_{t} II) ↾_{𝑡} (\{m\} \times V)) Cn C)$
104		cvmtop1	$⊢ F \in (C CovMap J) \to C \in Top$
105	2 104	syl	$⊢ φ \to C \in Top$
106	105	adantr	$⊢ (φ \land (m \in U \land n \in V)) \to C \in Top$
107	1	toptopon	$⊢ C \in Top \leftrightarrow C \in TopOn (B)$
108	106 107	sylib	$⊢ (φ \land (m \in U \land n \in V)) \to C \in TopOn (B)$
109		df-ima	$⊢ K [\{m\} \times V] = ran ({K ↾}_{(\{m\} \times V)})$
110		simprl	$⊢ (φ \land (m \in U \land n \in V)) \to m \in U$
111	110	snssd	$⊢ (φ \land (m \in U \land n \in V)) \to \{m\} \subseteq U$
112		xpss1	$⊢ \{m\} \subseteq U \to \{m\} \times V \subseteq U \times V$
113		imass2	$⊢ \{m\} \times V \subseteq U \times V \to K [\{m\} \times V] \subseteq K [U \times V]$
114	111 112 113	3syl	$⊢ (φ \land (m \in U \land n \in V)) \to K [\{m\} \times V] \subseteq K [U \times V]$
115		imaco	$⊢ (K^{-1} \circ F^{-1}) [M] = K^{-1} [F^{-1} [M]]$
116		cnvco	$⊢ {(F \circ K)}^{-1} = K^{-1} \circ F^{-1}$
117	25	cnveqd	$⊢ φ \to {(F \circ K)}^{-1} = G^{-1}$
118	116 117	eqtr3id	$⊢ φ \to K^{-1} \circ F^{-1} = G^{-1}$
119	118	imaeq1d	$⊢ φ \to (K^{-1} \circ F^{-1}) [M] = G^{-1} [M]$
120	115 119	eqtr3id	$⊢ φ \to K^{-1} [F^{-1} [M]] = G^{-1} [M]$
121	17 120	sseqtrrd	$⊢ φ \to U \times V \subseteq K^{-1} [F^{-1} [M]]$
122	24	ffund	$⊢ φ \to Fun K$
123	24	fdmd	$⊢ φ \to dom K = [0, 1] \times [0, 1]$
124	55 123	sseqtrrd	$⊢ φ \to U \times V \subseteq dom K$
125		funimass3	$⊢ (Fun K \land U \times V \subseteq dom K) \to (K [U \times V] \subseteq F^{-1} [M] \leftrightarrow U \times V \subseteq K^{-1} [F^{-1} [M]])$
126	122 124 125	syl2anc	$⊢ φ \to (K [U \times V] \subseteq F^{-1} [M] \leftrightarrow U \times V \subseteq K^{-1} [F^{-1} [M]])$
127	121 126	mpbird	$⊢ φ \to K [U \times V] \subseteq F^{-1} [M]$
128	127	adantr	$⊢ (φ \land (m \in U \land n \in V)) \to K [U \times V] \subseteq F^{-1} [M]$
129	114 128	sstrd	$⊢ (φ \land (m \in U \land n \in V)) \to K [\{m\} \times V] \subseteq F^{-1} [M]$
130	109 129	eqsstrrid	$⊢ (φ \land (m \in U \land n \in V)) \to ran ({K ↾}_{(\{m\} \times V)}) \subseteq F^{-1} [M]$
131		cnvimass	$⊢ F^{-1} [M] \subseteq dom F$
132		cvmcn	$⊢ F \in (C CovMap J) \to F \in (C Cn J)$
133	2 132	syl	$⊢ φ \to F \in (C Cn J)$
134		eqid	$⊢ ⋃ J = ⋃ J$
135	1 134	cnf	$⊢ F \in (C Cn J) \to F : B ⟶ ⋃ J$
136		fdm	$⊢ F : B ⟶ ⋃ J \to dom F = B$
137	133 135 136	3syl	$⊢ φ \to dom F = B$
138	131 137	sseqtrid	$⊢ φ \to F^{-1} [M] \subseteq B$
139	138	adantr	$⊢ (φ \land (m \in U \land n \in V)) \to F^{-1} [M] \subseteq B$
140		cnrest2	$⊢ (C \in TopOn (B) \land ran ({K ↾}_{(\{m\} \times V)}) \subseteq F^{-1} [M] \land F^{-1} [M] \subseteq B) \to ({K ↾}_{(\{m\} \times V)} \in (((II \times_{t} II) ↾_{𝑡} (\{m\} \times V)) Cn C) \leftrightarrow {K ↾}_{(\{m\} \times V)} \in (((II \times_{t} II) ↾_{𝑡} (\{m\} \times V)) Cn (C ↾_{𝑡} F^{-1} [M])))$
141	108 130 139 140	syl3anc	$⊢ (φ \land (m \in U \land n \in V)) \to ({K ↾}_{(\{m\} \times V)} \in (((II \times_{t} II) ↾_{𝑡} (\{m\} \times V)) Cn C) \leftrightarrow {K ↾}_{(\{m\} \times V)} \in (((II \times_{t} II) ↾_{𝑡} (\{m\} \times V)) Cn (C ↾_{𝑡} F^{-1} [M])))$
142	103 141	mpbid	$⊢ (φ \land (m \in U \land n \in V)) \to {K ↾}_{(\{m\} \times V)} \in (((II \times_{t} II) ↾_{𝑡} (\{m\} \times V)) Cn (C ↾_{𝑡} F^{-1} [M]))$
143	8	cvmsss	$⊢ T \in S (M) \to T \subseteq C$
144	10 143	syl	$⊢ φ \to T \subseteq C$
145	50	simpld	$⊢ φ \to W \in T$
146	144 145	sseldd	$⊢ φ \to W \in C$
147		elssuni	$⊢ W \in T \to W \subseteq ⋃ T$
148	145 147	syl	$⊢ φ \to W \subseteq ⋃ T$
149	8	cvmsuni	$⊢ T \in S (M) \to ⋃ T = F^{-1} [M]$
150	10 149	syl	$⊢ φ \to ⋃ T = F^{-1} [M]$
151	148 150	sseqtrd	$⊢ φ \to W \subseteq F^{-1} [M]$
152	8	cvmsrcl	$⊢ T \in S (M) \to M \in J$
153	10 152	syl	$⊢ φ \to M \in J$
154		cnima	$⊢ (F \in (C Cn J) \land M \in J) \to F^{-1} [M] \in C$
155	133 153 154	syl2anc	$⊢ φ \to F^{-1} [M] \in C$
156		restopn2	$⊢ (C \in Top \land F^{-1} [M] \in C) \to (W \in (C ↾_{𝑡} F^{-1} [M]) \leftrightarrow (W \in C \land W \subseteq F^{-1} [M]))$
157	105 155 156	syl2anc	$⊢ φ \to (W \in (C ↾_{𝑡} F^{-1} [M]) \leftrightarrow (W \in C \land W \subseteq F^{-1} [M]))$
158	146 151 157	mpbir2and	$⊢ φ \to W \in (C ↾_{𝑡} F^{-1} [M])$
159	158	adantr	$⊢ (φ \land (m \in U \land n \in V)) \to W \in (C ↾_{𝑡} F^{-1} [M])$
160	8	cvmscld	$⊢ (F \in (C CovMap J) \land T \in S (M) \land W \in T) \to W \in Clsd (C ↾_{𝑡} F^{-1} [M])$
161	2 10 145 160	syl3anc	$⊢ φ \to W \in Clsd (C ↾_{𝑡} F^{-1} [M])$
162	161	adantr	$⊢ (φ \land (m \in U \land n \in V)) \to W \in Clsd (C ↾_{𝑡} F^{-1} [M])$
163	18	adantr	$⊢ (φ \land (m \in U \land n \in V)) \to Z \in V$
164		opelxpi	$⊢ (m \in \{m\} \land Z \in V) \to ⟨m, Z⟩ \in (\{m\} \times V)$
165	57 163 164	syl2anc	$⊢ (φ \land (m \in U \land n \in V)) \to ⟨m, Z⟩ \in (\{m\} \times V)$
166	85 88	sstrd	$⊢ (φ \land (m \in U \land n \in V)) \to \{m\} \times V \subseteq [0, 1] \times [0, 1]$
167	23	restuni	$⊢ (II \times_{t} II \in Top \land \{m\} \times V \subseteq [0, 1] \times [0, 1]) \to \{m\} \times V = ⋃ ((II \times_{t} II) ↾_{𝑡} (\{m\} \times V))$
168	27 166 167	sylancr	$⊢ (φ \land (m \in U \land n \in V)) \to \{m\} \times V = ⋃ ((II \times_{t} II) ↾_{𝑡} (\{m\} \times V))$
169	165 168	eleqtrd	$⊢ (φ \land (m \in U \land n \in V)) \to ⟨m, Z⟩ \in ⋃ ((II \times_{t} II) ↾_{𝑡} (\{m\} \times V))$
170		df-ov	$⊢ m ({K ↾}_{(\{m\} \times V)}) Z = ({K ↾}_{(\{m\} \times V)}) (⟨m, Z⟩)$
171		ovres	$⊢ (m \in \{m\} \land Z \in V) \to m ({K ↾}_{(\{m\} \times V)}) Z = m K Z$
172	57 163 171	syl2anc	$⊢ (φ \land (m \in U \land n \in V)) \to m ({K ↾}_{(\{m\} \times V)}) Z = m K Z$
173		snidg	$⊢ Z \in V \to Z \in \{Z\}$
174	18 173	syl	$⊢ φ \to Z \in \{Z\}$
175	174	adantr	$⊢ (φ \land (m \in U \land n \in V)) \to Z \in \{Z\}$
176		ovres	$⊢ (m \in U \land Z \in \{Z\}) \to m ({K ↾}_{(U \times \{Z\})}) Z = m K Z$
177	110 175 176	syl2anc	$⊢ (φ \land (m \in U \land n \in V)) \to m ({K ↾}_{(U \times \{Z\})}) Z = m K Z$
178	172 177	eqtr4d	$⊢ (φ \land (m \in U \land n \in V)) \to m ({K ↾}_{(\{m\} \times V)}) Z = m ({K ↾}_{(U \times \{Z\})}) Z$
179	170 178	eqtr3id	$⊢ (φ \land (m \in U \land n \in V)) \to ({K ↾}_{(\{m\} \times V)}) (⟨m, Z⟩) = m ({K ↾}_{(U \times \{Z\})}) Z$
180		eqid	$⊢ ⋃ ((II \times_{t} II) ↾_{𝑡} (U \times \{Z\})) = ⋃ ((II \times_{t} II) ↾_{𝑡} (U \times \{Z\}))$
181	21	a1i	$⊢ φ \to II \in Top$
182		snex	$⊢ \{Z\} \in V$
183	182	a1i	$⊢ φ \to \{Z\} \in V$
184		txrest	$⊢ ((II \in Top \land II \in Top) \land (U \in II \land \{Z\} \in V)) \to (II \times_{t} II) ↾_{𝑡} (U \times \{Z\}) = (II ↾_{𝑡} U) \times_{t} (II ↾_{𝑡} \{Z\})$
185	181 181 11 183 184	syl22anc	$⊢ φ \to (II \times_{t} II) ↾_{𝑡} (U \times \{Z\}) = (II ↾_{𝑡} U) \times_{t} (II ↾_{𝑡} \{Z\})$
186	35 18	sseldd	$⊢ φ \to Z \in [0, 1]$
187		restsn2	$⊢ (II \in TopOn ([0, 1]) \land Z \in [0, 1]) \to II ↾_{𝑡} \{Z\} = 𝒫 \{Z\}$
188	68 186 187	sylancr	$⊢ φ \to II ↾_{𝑡} \{Z\} = 𝒫 \{Z\}$
189		pwsn	$⊢ 𝒫 \{Z\} = \{\emptyset, \{Z\}\}$
190		indisconn	$⊢ \{\emptyset, \{Z\}\} \in Conn$
191	189 190	eqeltri	$⊢ 𝒫 \{Z\} \in Conn$
192	188 191	eqeltrdi	$⊢ φ \to II ↾_{𝑡} \{Z\} \in Conn$
193		txconn	$⊢ (II ↾_{𝑡} U \in Conn \land II ↾_{𝑡} \{Z\} \in Conn) \to (II ↾_{𝑡} U) \times_{t} (II ↾_{𝑡} \{Z\}) \in Conn$
194	13 192 193	syl2anc	$⊢ φ \to (II ↾_{𝑡} U) \times_{t} (II ↾_{𝑡} \{Z\}) \in Conn$
195	185 194	eqeltrd	$⊢ φ \to (II \times_{t} II) ↾_{𝑡} (U \times \{Z\}) \in Conn$
196	105 107	sylib	$⊢ φ \to C \in TopOn (B)$
197		df-ima	$⊢ K [U \times \{Z\}] = ran ({K ↾}_{(U \times \{Z\})})$
198	18	snssd	$⊢ φ \to \{Z\} \subseteq V$
199		xpss2	$⊢ \{Z\} \subseteq V \to U \times \{Z\} \subseteq U \times V$
200		imass2	$⊢ U \times \{Z\} \subseteq U \times V \to K [U \times \{Z\}] \subseteq K [U \times V]$
201	198 199 200	3syl	$⊢ φ \to K [U \times \{Z\}] \subseteq K [U \times V]$
202	201 127	sstrd	$⊢ φ \to K [U \times \{Z\}] \subseteq F^{-1} [M]$
203	197 202	eqsstrrid	$⊢ φ \to ran ({K ↾}_{(U \times \{Z\})}) \subseteq F^{-1} [M]$
204		cnrest2	$⊢ (C \in TopOn (B) \land ran ({K ↾}_{(U \times \{Z\})}) \subseteq F^{-1} [M] \land F^{-1} [M] \subseteq B) \to ({K ↾}_{(U \times \{Z\})} \in (((II \times_{t} II) ↾_{𝑡} (U \times \{Z\})) Cn C) \leftrightarrow {K ↾}_{(U \times \{Z\})} \in (((II \times_{t} II) ↾_{𝑡} (U \times \{Z\})) Cn (C ↾_{𝑡} F^{-1} [M])))$
205	196 203 138 204	syl3anc	$⊢ φ \to ({K ↾}_{(U \times \{Z\})} \in (((II \times_{t} II) ↾_{𝑡} (U \times \{Z\})) Cn C) \leftrightarrow {K ↾}_{(U \times \{Z\})} \in (((II \times_{t} II) ↾_{𝑡} (U \times \{Z\})) Cn (C ↾_{𝑡} F^{-1} [M])))$
206	19 205	mpbid	$⊢ φ \to {K ↾}_{(U \times \{Z\})} \in (((II \times_{t} II) ↾_{𝑡} (U \times \{Z\})) Cn (C ↾_{𝑡} F^{-1} [M]))$
207		opelxpi	$⊢ (X \in U \land Z \in \{Z\}) \to ⟨X, Z⟩ \in (U \times \{Z\})$
208	15 174 207	syl2anc	$⊢ φ \to ⟨X, Z⟩ \in (U \times \{Z\})$
209	186	snssd	$⊢ φ \to \{Z\} \subseteq [0, 1]$
210		xpss12	$⊢ (U \subseteq [0, 1] \land \{Z\} \subseteq [0, 1]) \to U \times \{Z\} \subseteq [0, 1] \times [0, 1]$
211	31 209 210	syl2anc	$⊢ φ \to U \times \{Z\} \subseteq [0, 1] \times [0, 1]$
212	23	restuni	$⊢ (II \times_{t} II \in Top \land U \times \{Z\} \subseteq [0, 1] \times [0, 1]) \to U \times \{Z\} = ⋃ ((II \times_{t} II) ↾_{𝑡} (U \times \{Z\}))$
213	27 211 212	sylancr	$⊢ φ \to U \times \{Z\} = ⋃ ((II \times_{t} II) ↾_{𝑡} (U \times \{Z\}))$
214	208 213	eleqtrd	$⊢ φ \to ⟨X, Z⟩ \in ⋃ ((II \times_{t} II) ↾_{𝑡} (U \times \{Z\}))$
215		df-ov	$⊢ X ({K ↾}_{(U \times \{Z\})}) Z = ({K ↾}_{(U \times \{Z\})}) (⟨X, Z⟩)$
216		ovres	$⊢ (X \in U \land Z \in \{Z\}) \to X ({K ↾}_{(U \times \{Z\})}) Z = X K Z$
217	15 174 216	syl2anc	$⊢ φ \to X ({K ↾}_{(U \times \{Z\})}) Z = X K Z$
218		snidg	$⊢ X \in U \to X \in \{X\}$
219	15 218	syl	$⊢ φ \to X \in \{X\}$
220		ovres	$⊢ (X \in \{X\} \land Z \in V) \to X ({K ↾}_{(\{X\} \times V)}) Z = X K Z$
221	219 18 220	syl2anc	$⊢ φ \to X ({K ↾}_{(\{X\} \times V)}) Z = X K Z$
222	217 221	eqtr4d	$⊢ φ \to X ({K ↾}_{(U \times \{Z\})}) Z = X ({K ↾}_{(\{X\} \times V)}) Z$
223	215 222	eqtr3id	$⊢ φ \to ({K ↾}_{(U \times \{Z\})}) (⟨X, Z⟩) = X ({K ↾}_{(\{X\} \times V)}) Z$
224		eqid	$⊢ ⋃ ((II \times_{t} II) ↾_{𝑡} (\{X\} \times V)) = ⋃ ((II \times_{t} II) ↾_{𝑡} (\{X\} \times V))$
225		snex	$⊢ \{X\} \in V$
226	225	a1i	$⊢ φ \to \{X\} \in V$
227		txrest	$⊢ ((II \in Top \land II \in Top) \land (\{X\} \in V \land V \in II)) \to (II \times_{t} II) ↾_{𝑡} (\{X\} \times V) = (II ↾_{𝑡} \{X\}) \times_{t} (II ↾_{𝑡} V)$
228	181 181 226 12 227	syl22anc	$⊢ φ \to (II \times_{t} II) ↾_{𝑡} (\{X\} \times V) = (II ↾_{𝑡} \{X\}) \times_{t} (II ↾_{𝑡} V)$
229		restsn2	$⊢ (II \in TopOn ([0, 1]) \land X \in [0, 1]) \to II ↾_{𝑡} \{X\} = 𝒫 \{X\}$
230	68 32 229	sylancr	$⊢ φ \to II ↾_{𝑡} \{X\} = 𝒫 \{X\}$
231		pwsn	$⊢ 𝒫 \{X\} = \{\emptyset, \{X\}\}$
232		indisconn	$⊢ \{\emptyset, \{X\}\} \in Conn$
233	231 232	eqeltri	$⊢ 𝒫 \{X\} \in Conn$
234	230 233	eqeltrdi	$⊢ φ \to II ↾_{𝑡} \{X\} \in Conn$
235		txconn	$⊢ (II ↾_{𝑡} \{X\} \in Conn \land II ↾_{𝑡} V \in Conn) \to (II ↾_{𝑡} \{X\}) \times_{t} (II ↾_{𝑡} V) \in Conn$
236	234 14 235	syl2anc	$⊢ φ \to (II ↾_{𝑡} \{X\}) \times_{t} (II ↾_{𝑡} V) \in Conn$
237	228 236	eqeltrd	$⊢ φ \to (II \times_{t} II) ↾_{𝑡} (\{X\} \times V) \in Conn$
238	1 2 3 4 5 6 7	cvmlift2lem6	$⊢ (φ \land X \in [0, 1]) \to {K ↾}_{(\{X\} \times [0, 1])} \in (((II \times_{t} II) ↾_{𝑡} (\{X\} \times [0, 1])) Cn C)$
239	32 238	mpdan	$⊢ φ \to {K ↾}_{(\{X\} \times [0, 1])} \in (((II \times_{t} II) ↾_{𝑡} (\{X\} \times [0, 1])) Cn C)$
240		xpss2	$⊢ V \subseteq [0, 1] \to \{X\} \times V \subseteq \{X\} \times [0, 1]$
241	12 34 240	3syl	$⊢ φ \to \{X\} \times V \subseteq \{X\} \times [0, 1]$
242	32	snssd	$⊢ φ \to \{X\} \subseteq [0, 1]$
243		xpss1	$⊢ \{X\} \subseteq [0, 1] \to \{X\} \times [0, 1] \subseteq [0, 1] \times [0, 1]$
244	242 243	syl	$⊢ φ \to \{X\} \times [0, 1] \subseteq [0, 1] \times [0, 1]$
245	23	restuni	$⊢ (II \times_{t} II \in Top \land \{X\} \times [0, 1] \subseteq [0, 1] \times [0, 1]) \to \{X\} \times [0, 1] = ⋃ ((II \times_{t} II) ↾_{𝑡} (\{X\} \times [0, 1]))$
246	27 244 245	sylancr	$⊢ φ \to \{X\} \times [0, 1] = ⋃ ((II \times_{t} II) ↾_{𝑡} (\{X\} \times [0, 1]))$
247	241 246	sseqtrd	$⊢ φ \to \{X\} \times V \subseteq ⋃ ((II \times_{t} II) ↾_{𝑡} (\{X\} \times [0, 1]))$
248		eqid	$⊢ ⋃ ((II \times_{t} II) ↾_{𝑡} (\{X\} \times [0, 1])) = ⋃ ((II \times_{t} II) ↾_{𝑡} (\{X\} \times [0, 1]))$
249	248	cnrest	$⊢ ({K ↾}_{(\{X\} \times [0, 1])} \in (((II \times_{t} II) ↾_{𝑡} (\{X\} \times [0, 1])) Cn C) \land \{X\} \times V \subseteq ⋃ ((II \times_{t} II) ↾_{𝑡} (\{X\} \times [0, 1]))) \to {({K ↾}_{(\{X\} \times [0, 1])}) ↾}_{(\{X\} \times V)} \in ((((II \times_{t} II) ↾_{𝑡} (\{X\} \times [0, 1])) ↾_{𝑡} (\{X\} \times V)) Cn C)$
250	239 247 249	syl2anc	$⊢ φ \to {({K ↾}_{(\{X\} \times [0, 1])}) ↾}_{(\{X\} \times V)} \in ((((II \times_{t} II) ↾_{𝑡} (\{X\} \times [0, 1])) ↾_{𝑡} (\{X\} \times V)) Cn C)$
251	241	resabs1d	$⊢ φ \to {({K ↾}_{(\{X\} \times [0, 1])}) ↾}_{(\{X\} \times V)} = {K ↾}_{(\{X\} \times V)}$
252	225 97	xpex	$⊢ \{X\} \times [0, 1] \in V$
253	252	a1i	$⊢ φ \to \{X\} \times [0, 1] \in V$
254		restabs	$⊢ (II \times_{t} II \in Top \land \{X\} \times V \subseteq \{X\} \times [0, 1] \land \{X\} \times [0, 1] \in V) \to ((II \times_{t} II) ↾_{𝑡} (\{X\} \times [0, 1])) ↾_{𝑡} (\{X\} \times V) = (II \times_{t} II) ↾_{𝑡} (\{X\} \times V)$
255	28 241 253 254	syl3anc	$⊢ φ \to ((II \times_{t} II) ↾_{𝑡} (\{X\} \times [0, 1])) ↾_{𝑡} (\{X\} \times V) = (II \times_{t} II) ↾_{𝑡} (\{X\} \times V)$
256	255	oveq1d	$⊢ φ \to (((II \times_{t} II) ↾_{𝑡} (\{X\} \times [0, 1])) ↾_{𝑡} (\{X\} \times V)) Cn C = ((II \times_{t} II) ↾_{𝑡} (\{X\} \times V)) Cn C$
257	250 251 256	3eltr3d	$⊢ φ \to {K ↾}_{(\{X\} \times V)} \in (((II \times_{t} II) ↾_{𝑡} (\{X\} \times V)) Cn C)$
258		df-ima	$⊢ K [\{X\} \times V] = ran ({K ↾}_{(\{X\} \times V)})$
259	15	snssd	$⊢ φ \to \{X\} \subseteq U$
260		xpss1	$⊢ \{X\} \subseteq U \to \{X\} \times V \subseteq U \times V$
261		imass2	$⊢ \{X\} \times V \subseteq U \times V \to K [\{X\} \times V] \subseteq K [U \times V]$
262	259 260 261	3syl	$⊢ φ \to K [\{X\} \times V] \subseteq K [U \times V]$
263	262 127	sstrd	$⊢ φ \to K [\{X\} \times V] \subseteq F^{-1} [M]$
264	258 263	eqsstrrid	$⊢ φ \to ran ({K ↾}_{(\{X\} \times V)}) \subseteq F^{-1} [M]$
265		cnrest2	$⊢ (C \in TopOn (B) \land ran ({K ↾}_{(\{X\} \times V)}) \subseteq F^{-1} [M] \land F^{-1} [M] \subseteq B) \to ({K ↾}_{(\{X\} \times V)} \in (((II \times_{t} II) ↾_{𝑡} (\{X\} \times V)) Cn C) \leftrightarrow {K ↾}_{(\{X\} \times V)} \in (((II \times_{t} II) ↾_{𝑡} (\{X\} \times V)) Cn (C ↾_{𝑡} F^{-1} [M])))$
266	196 264 138 265	syl3anc	$⊢ φ \to ({K ↾}_{(\{X\} \times V)} \in (((II \times_{t} II) ↾_{𝑡} (\{X\} \times V)) Cn C) \leftrightarrow {K ↾}_{(\{X\} \times V)} \in (((II \times_{t} II) ↾_{𝑡} (\{X\} \times V)) Cn (C ↾_{𝑡} F^{-1} [M])))$
267	257 266	mpbid	$⊢ φ \to {K ↾}_{(\{X\} \times V)} \in (((II \times_{t} II) ↾_{𝑡} (\{X\} \times V)) Cn (C ↾_{𝑡} F^{-1} [M]))$
268		opelxpi	$⊢ (X \in \{X\} \land Y \in V) \to ⟨X, Y⟩ \in (\{X\} \times V)$
269	219 16 268	syl2anc	$⊢ φ \to ⟨X, Y⟩ \in (\{X\} \times V)$
270	259 260	syl	$⊢ φ \to \{X\} \times V \subseteq U \times V$
271	270 55	sstrd	$⊢ φ \to \{X\} \times V \subseteq [0, 1] \times [0, 1]$
272	23	restuni	$⊢ (II \times_{t} II \in Top \land \{X\} \times V \subseteq [0, 1] \times [0, 1]) \to \{X\} \times V = ⋃ ((II \times_{t} II) ↾_{𝑡} (\{X\} \times V))$
273	27 271 272	sylancr	$⊢ φ \to \{X\} \times V = ⋃ ((II \times_{t} II) ↾_{𝑡} (\{X\} \times V))$
274	269 273	eleqtrd	$⊢ φ \to ⟨X, Y⟩ \in ⋃ ((II \times_{t} II) ↾_{𝑡} (\{X\} \times V))$
275		df-ov	$⊢ X ({K ↾}_{(\{X\} \times V)}) Y = ({K ↾}_{(\{X\} \times V)}) (⟨X, Y⟩)$
276		ovres	$⊢ (X \in \{X\} \land Y \in V) \to X ({K ↾}_{(\{X\} \times V)}) Y = X K Y$
277	219 16 276	syl2anc	$⊢ φ \to X ({K ↾}_{(\{X\} \times V)}) Y = X K Y$
278	275 277	eqtr3id	$⊢ φ \to ({K ↾}_{(\{X\} \times V)}) (⟨X, Y⟩) = X K Y$
279	50	simprd	$⊢ φ \to X K Y \in W$
280	278 279	eqeltrd	$⊢ φ \to ({K ↾}_{(\{X\} \times V)}) (⟨X, Y⟩) \in W$
281	224 237 267 158 161 274 280	conncn	$⊢ φ \to ({K ↾}_{(\{X\} \times V)}) : ⋃ ((II \times_{t} II) ↾_{𝑡} (\{X\} \times V)) ⟶ W$
282	273	feq2d	$⊢ φ \to (({K ↾}_{(\{X\} \times V)}) : \{X\} \times V ⟶ W \leftrightarrow ({K ↾}_{(\{X\} \times V)}) : ⋃ ((II \times_{t} II) ↾_{𝑡} (\{X\} \times V)) ⟶ W)$
283	281 282	mpbird	$⊢ φ \to ({K ↾}_{(\{X\} \times V)}) : \{X\} \times V ⟶ W$
284	283 219 18	fovrnd	$⊢ φ \to X ({K ↾}_{(\{X\} \times V)}) Z \in W$
285	223 284	eqeltrd	$⊢ φ \to ({K ↾}_{(U \times \{Z\})}) (⟨X, Z⟩) \in W$
286	180 195 206 158 161 214 285	conncn	$⊢ φ \to ({K ↾}_{(U \times \{Z\})}) : ⋃ ((II \times_{t} II) ↾_{𝑡} (U \times \{Z\})) ⟶ W$
287	213	feq2d	$⊢ φ \to (({K ↾}_{(U \times \{Z\})}) : U \times \{Z\} ⟶ W \leftrightarrow ({K ↾}_{(U \times \{Z\})}) : ⋃ ((II \times_{t} II) ↾_{𝑡} (U \times \{Z\})) ⟶ W)$
288	286 287	mpbird	$⊢ φ \to ({K ↾}_{(U \times \{Z\})}) : U \times \{Z\} ⟶ W$
289	288	adantr	$⊢ (φ \land (m \in U \land n \in V)) \to ({K ↾}_{(U \times \{Z\})}) : U \times \{Z\} ⟶ W$
290	289 110 175	fovrnd	$⊢ (φ \land (m \in U \land n \in V)) \to m ({K ↾}_{(U \times \{Z\})}) Z \in W$
291	179 290	eqeltrd	$⊢ (φ \land (m \in U \land n \in V)) \to ({K ↾}_{(\{m\} \times V)}) (⟨m, Z⟩) \in W$
292	61 80 142 159 162 169 291	conncn	$⊢ (φ \land (m \in U \land n \in V)) \to ({K ↾}_{(\{m\} \times V)}) : ⋃ ((II \times_{t} II) ↾_{𝑡} (\{m\} \times V)) ⟶ W$
293	168	feq2d	$⊢ (φ \land (m \in U \land n \in V)) \to (({K ↾}_{(\{m\} \times V)}) : \{m\} \times V ⟶ W \leftrightarrow ({K ↾}_{(\{m\} \times V)}) : ⋃ ((II \times_{t} II) ↾_{𝑡} (\{m\} \times V)) ⟶ W)$
294	292 293	mpbird	$⊢ (φ \land (m \in U \land n \in V)) \to ({K ↾}_{(\{m\} \times V)}) : \{m\} \times V ⟶ W$
295	294 57 58	fovrnd	$⊢ (φ \land (m \in U \land n \in V)) \to m ({K ↾}_{(\{m\} \times V)}) n \in W$
296	60 295	eqeltrrd	$⊢ (φ \land (m \in U \land n \in V)) \to m K n \in W$
297	296	ralrimivva	$⊢ φ \to \forall m \in U \forall n \in V m K n \in W$
298		funimassov	$⊢ (Fun K \land U \times V \subseteq dom K) \to (K [U \times V] \subseteq W \leftrightarrow \forall m \in U \forall n \in V m K n \in W)$
299	122 124 298	syl2anc	$⊢ φ \to (K [U \times V] \subseteq W \leftrightarrow \forall m \in U \forall n \in V m K n \in W)$
300	297 299	mpbird	$⊢ φ \to K [U \times V] \subseteq W$
301	1 23 8 2 24 26 28 38 10 53 55 300	cvmlift2lem9a	$⊢ φ \to {K ↾}_{(U \times V)} \in (((II \times_{t} II) ↾_{𝑡} (U \times V)) Cn C)$

Metamath Proof Explorer

Theorem cvmlift2lem9

Proof