cvmlift2lem12

	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))$
	cvmlift2.m	$⊢ M = \{z \in ([0, 1] \times [0, 1]) \| K \in ((II \times_{t} II) CnP C) (z)\}$
	cvmlift2.a	$⊢ A = \{a \in [0, 1] \| [0, 1] \times \{a\} \subseteq M\}$
	cvmlift2.s	$⊢ S = \{⟨r, t⟩ \| (t \in [0, 1] \land \exists u \in nei (II) (\{r\}) (u \times \{a\} \subseteq M \leftrightarrow u \times \{t\} \subseteq M))\}$
Assertion	cvmlift2lem12	$⊢ φ \to K \in ((II \times_{t} II) 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		cvmlift2.m	$⊢ M = \{z \in ([0, 1] \times [0, 1]) \| K \in ((II \times_{t} II) CnP C) (z)\}$
9		cvmlift2.a	$⊢ A = \{a \in [0, 1] \| [0, 1] \times \{a\} \subseteq M\}$
10		cvmlift2.s	$⊢ S = \{⟨r, t⟩ \| (t \in [0, 1] \land \exists u \in nei (II) (\{r\}) (u \times \{a\} \subseteq M \leftrightarrow u \times \{t\} \subseteq M))\}$
11	1 2 3 4 5 6 7	cvmlift2lem5	$⊢ φ \to K : [0, 1] \times [0, 1] ⟶ B$
12		iunid	$⊢ ⋃_{a \in [0, 1]} \{a\} = [0, 1]$
13	12	xpeq2i	$⊢ [0, 1] \times ⋃_{a \in [0, 1]} \{a\} = [0, 1] \times [0, 1]$
14		xpiundi	$⊢ [0, 1] \times ⋃_{a \in [0, 1]} \{a\} = ⋃_{a \in [0, 1]} ([0, 1] \times \{a\})$
15	13 14	eqtr3i	$⊢ [0, 1] \times [0, 1] = ⋃_{a \in [0, 1]} ([0, 1] \times \{a\})$
16		iiuni	$⊢ [0, 1] = ⋃ II$
17		iiconn	$⊢ II \in Conn$
18	17	a1i	$⊢ φ \to II \in Conn$
19		inss1	$⊢ II \cap Clsd (II) \subseteq II$
20		iicmp	$⊢ II \in Comp$
21	20	a1i	$⊢ (φ \land a \in [0, 1]) \to II \in Comp$
22		iitop	$⊢ II \in Top$
23	22	a1i	$⊢ (φ \land a \in [0, 1]) \to II \in Top$
24	22 22	txtopi	$⊢ II \times_{t} II \in Top$
25	16	neiss2	$⊢ (II \in Top \land u \in nei (II) (\{r\})) \to \{r\} \subseteq [0, 1]$
26	22 25	mpan	$⊢ u \in nei (II) (\{r\}) \to \{r\} \subseteq [0, 1]$
27		vex	$⊢ r \in V$
28	27	snss	$⊢ r \in [0, 1] \leftrightarrow \{r\} \subseteq [0, 1]$
29	26 28	sylibr	$⊢ u \in nei (II) (\{r\}) \to r \in [0, 1]$
30	29	a1d	$⊢ u \in nei (II) (\{r\}) \to ((u \times \{a\} \subseteq M \leftrightarrow u \times \{t\} \subseteq M) \to r \in [0, 1])$
31	30	rexlimiv	$⊢ \exists u \in nei (II) (\{r\}) (u \times \{a\} \subseteq M \leftrightarrow u \times \{t\} \subseteq M) \to r \in [0, 1]$
32	31	adantl	$⊢ (t \in [0, 1] \land \exists u \in nei (II) (\{r\}) (u \times \{a\} \subseteq M \leftrightarrow u \times \{t\} \subseteq M)) \to r \in [0, 1]$
33		simpl	$⊢ (t \in [0, 1] \land \exists u \in nei (II) (\{r\}) (u \times \{a\} \subseteq M \leftrightarrow u \times \{t\} \subseteq M)) \to t \in [0, 1]$
34	32 33	jca	$⊢ (t \in [0, 1] \land \exists u \in nei (II) (\{r\}) (u \times \{a\} \subseteq M \leftrightarrow u \times \{t\} \subseteq M)) \to (r \in [0, 1] \land t \in [0, 1])$
35	34	ssopab2i	$⊢ \{⟨r, t⟩ \| (t \in [0, 1] \land \exists u \in nei (II) (\{r\}) (u \times \{a\} \subseteq M \leftrightarrow u \times \{t\} \subseteq M))\} \subseteq \{⟨r, t⟩ \| (r \in [0, 1] \land t \in [0, 1])\}$
36		df-xp	$⊢ [0, 1] \times [0, 1] = \{⟨r, t⟩ \| (r \in [0, 1] \land t \in [0, 1])\}$
37	35 10 36	3sstr4i	$⊢ S \subseteq [0, 1] \times [0, 1]$
38	22 22 16 16	txunii	$⊢ [0, 1] \times [0, 1] = ⋃ (II \times_{t} II)$
39	38	ntropn	$⊢ (II \times_{t} II \in Top \land S \subseteq [0, 1] \times [0, 1]) \to int (II \times_{t} II) (S) \in (II \times_{t} II)$
40	24 37 39	mp2an	$⊢ int (II \times_{t} II) (S) \in (II \times_{t} II)$
41	40	a1i	$⊢ (φ \land a \in [0, 1]) \to int (II \times_{t} II) (S) \in (II \times_{t} II)$
42	2	adantr	$⊢ (φ \land (a \in [0, 1] \land b \in [0, 1])) \to F \in (C CovMap J)$
43	3	adantr	$⊢ (φ \land (a \in [0, 1] \land b \in [0, 1])) \to G \in ((II \times_{t} II) Cn J)$
44	4	adantr	$⊢ (φ \land (a \in [0, 1] \land b \in [0, 1])) \to P \in B$
45	5	adantr	$⊢ (φ \land (a \in [0, 1] \land b \in [0, 1])) \to F (P) = 0 G 0$
46		eqid	$⊢ (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))))\}) = (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))))\})$
47		simprr	$⊢ (φ \land (a \in [0, 1] \land b \in [0, 1])) \to b \in [0, 1]$
48		simprl	$⊢ (φ \land (a \in [0, 1] \land b \in [0, 1])) \to a \in [0, 1]$
49	1 42 43 44 45 6 7 46 47 48	cvmlift2lem10	$⊢ (φ \land (a \in [0, 1] \land b \in [0, 1])) \to \exists u \in II \exists v \in II (b \in u \land a \in v \land (\exists w \in v {K ↾}_{(u \times \{w\})} \in (((II \times_{t} II) ↾_{𝑡} (u \times \{w\})) Cn C) \to {K ↾}_{(u \times v)} \in (((II \times_{t} II) ↾_{𝑡} (u \times v)) Cn C)))$
50	24	a1i	$⊢ (((φ \land (a \in [0, 1] \land b \in [0, 1])) \land (u \in II \land v \in II)) \land (b \in u \land a \in v \land (\exists w \in v {K ↾}_{(u \times \{w\})} \in (((II \times_{t} II) ↾_{𝑡} (u \times \{w\})) Cn C) \to {K ↾}_{(u \times v)} \in (((II \times_{t} II) ↾_{𝑡} (u \times v)) Cn C)))) \to II \times_{t} II \in Top$
51	37	a1i	$⊢ (((φ \land (a \in [0, 1] \land b \in [0, 1])) \land (u \in II \land v \in II)) \land (b \in u \land a \in v \land (\exists w \in v {K ↾}_{(u \times \{w\})} \in (((II \times_{t} II) ↾_{𝑡} (u \times \{w\})) Cn C) \to {K ↾}_{(u \times v)} \in (((II \times_{t} II) ↾_{𝑡} (u \times v)) Cn C)))) \to S \subseteq [0, 1] \times [0, 1]$
52	22	a1i	$⊢ (((φ \land (a \in [0, 1] \land b \in [0, 1])) \land (u \in II \land v \in II)) \land (b \in u \land a \in v \land (\exists w \in v {K ↾}_{(u \times \{w\})} \in (((II \times_{t} II) ↾_{𝑡} (u \times \{w\})) Cn C) \to {K ↾}_{(u \times v)} \in (((II \times_{t} II) ↾_{𝑡} (u \times v)) Cn C)))) \to II \in Top$
53		simplrl	$⊢ (((φ \land (a \in [0, 1] \land b \in [0, 1])) \land (u \in II \land v \in II)) \land (b \in u \land a \in v \land (\exists w \in v {K ↾}_{(u \times \{w\})} \in (((II \times_{t} II) ↾_{𝑡} (u \times \{w\})) Cn C) \to {K ↾}_{(u \times v)} \in (((II \times_{t} II) ↾_{𝑡} (u \times v)) Cn C)))) \to u \in II$
54		simplrr	$⊢ (((φ \land (a \in [0, 1] \land b \in [0, 1])) \land (u \in II \land v \in II)) \land (b \in u \land a \in v \land (\exists w \in v {K ↾}_{(u \times \{w\})} \in (((II \times_{t} II) ↾_{𝑡} (u \times \{w\})) Cn C) \to {K ↾}_{(u \times v)} \in (((II \times_{t} II) ↾_{𝑡} (u \times v)) Cn C)))) \to v \in II$
55		txopn	$⊢ ((II \in Top \land II \in Top) \land (u \in II \land v \in II)) \to u \times v \in (II \times_{t} II)$
56	52 52 53 54 55	syl22anc	$⊢ (((φ \land (a \in [0, 1] \land b \in [0, 1])) \land (u \in II \land v \in II)) \land (b \in u \land a \in v \land (\exists w \in v {K ↾}_{(u \times \{w\})} \in (((II \times_{t} II) ↾_{𝑡} (u \times \{w\})) Cn C) \to {K ↾}_{(u \times v)} \in (((II \times_{t} II) ↾_{𝑡} (u \times v)) Cn C)))) \to u \times v \in (II \times_{t} II)$
57		simpr	$⊢ (r \in u \land t \in v) \to t \in v$
58		elunii	$⊢ (t \in v \land v \in II) \to t \in ⋃ II$
59	58 16	eleqtrrdi	$⊢ (t \in v \land v \in II) \to t \in [0, 1]$
60	57 54 59	syl2anr	$⊢ ((((φ \land (a \in [0, 1] \land b \in [0, 1])) \land (u \in II \land v \in II)) \land (b \in u \land a \in v \land (\exists w \in v {K ↾}_{(u \times \{w\})} \in (((II \times_{t} II) ↾_{𝑡} (u \times \{w\})) Cn C) \to {K ↾}_{(u \times v)} \in (((II \times_{t} II) ↾_{𝑡} (u \times v)) Cn C)))) \land (r \in u \land t \in v)) \to t \in [0, 1]$
61	22	a1i	$⊢ ((((φ \land (a \in [0, 1] \land b \in [0, 1])) \land (u \in II \land v \in II)) \land (b \in u \land a \in v \land (\exists w \in v {K ↾}_{(u \times \{w\})} \in (((II \times_{t} II) ↾_{𝑡} (u \times \{w\})) Cn C) \to {K ↾}_{(u \times v)} \in (((II \times_{t} II) ↾_{𝑡} (u \times v)) Cn C)))) \land (r \in u \land t \in v)) \to II \in Top$
62	53	adantr	$⊢ ((((φ \land (a \in [0, 1] \land b \in [0, 1])) \land (u \in II \land v \in II)) \land (b \in u \land a \in v \land (\exists w \in v {K ↾}_{(u \times \{w\})} \in (((II \times_{t} II) ↾_{𝑡} (u \times \{w\})) Cn C) \to {K ↾}_{(u \times v)} \in (((II \times_{t} II) ↾_{𝑡} (u \times v)) Cn C)))) \land (r \in u \land t \in v)) \to u \in II$
63		simprl	$⊢ ((((φ \land (a \in [0, 1] \land b \in [0, 1])) \land (u \in II \land v \in II)) \land (b \in u \land a \in v \land (\exists w \in v {K ↾}_{(u \times \{w\})} \in (((II \times_{t} II) ↾_{𝑡} (u \times \{w\})) Cn C) \to {K ↾}_{(u \times v)} \in (((II \times_{t} II) ↾_{𝑡} (u \times v)) Cn C)))) \land (r \in u \land t \in v)) \to r \in u$
64		opnneip	$⊢ (II \in Top \land u \in II \land r \in u) \to u \in nei (II) (\{r\})$
65	61 62 63 64	syl3anc	$⊢ ((((φ \land (a \in [0, 1] \land b \in [0, 1])) \land (u \in II \land v \in II)) \land (b \in u \land a \in v \land (\exists w \in v {K ↾}_{(u \times \{w\})} \in (((II \times_{t} II) ↾_{𝑡} (u \times \{w\})) Cn C) \to {K ↾}_{(u \times v)} \in (((II \times_{t} II) ↾_{𝑡} (u \times v)) Cn C)))) \land (r \in u \land t \in v)) \to u \in nei (II) (\{r\})$
66	42	ad3antrrr	$⊢ ((((φ \land (a \in [0, 1] \land b \in [0, 1])) \land (u \in II \land v \in II)) \land (b \in u \land a \in v \land (\exists w \in v {K ↾}_{(u \times \{w\})} \in (((II \times_{t} II) ↾_{𝑡} (u \times \{w\})) Cn C) \to {K ↾}_{(u \times v)} \in (((II \times_{t} II) ↾_{𝑡} (u \times v)) Cn C)))) \land (r \in u \land t \in v)) \to F \in (C CovMap J)$
67	43	ad3antrrr	$⊢ ((((φ \land (a \in [0, 1] \land b \in [0, 1])) \land (u \in II \land v \in II)) \land (b \in u \land a \in v \land (\exists w \in v {K ↾}_{(u \times \{w\})} \in (((II \times_{t} II) ↾_{𝑡} (u \times \{w\})) Cn C) \to {K ↾}_{(u \times v)} \in (((II \times_{t} II) ↾_{𝑡} (u \times v)) Cn C)))) \land (r \in u \land t \in v)) \to G \in ((II \times_{t} II) Cn J)$
68	44	ad3antrrr	$⊢ ((((φ \land (a \in [0, 1] \land b \in [0, 1])) \land (u \in II \land v \in II)) \land (b \in u \land a \in v \land (\exists w \in v {K ↾}_{(u \times \{w\})} \in (((II \times_{t} II) ↾_{𝑡} (u \times \{w\})) Cn C) \to {K ↾}_{(u \times v)} \in (((II \times_{t} II) ↾_{𝑡} (u \times v)) Cn C)))) \land (r \in u \land t \in v)) \to P \in B$
69	45	ad3antrrr	$⊢ ((((φ \land (a \in [0, 1] \land b \in [0, 1])) \land (u \in II \land v \in II)) \land (b \in u \land a \in v \land (\exists w \in v {K ↾}_{(u \times \{w\})} \in (((II \times_{t} II) ↾_{𝑡} (u \times \{w\})) Cn C) \to {K ↾}_{(u \times v)} \in (((II \times_{t} II) ↾_{𝑡} (u \times v)) Cn C)))) \land (r \in u \land t \in v)) \to F (P) = 0 G 0$
70	54	adantr	$⊢ ((((φ \land (a \in [0, 1] \land b \in [0, 1])) \land (u \in II \land v \in II)) \land (b \in u \land a \in v \land (\exists w \in v {K ↾}_{(u \times \{w\})} \in (((II \times_{t} II) ↾_{𝑡} (u \times \{w\})) Cn C) \to {K ↾}_{(u \times v)} \in (((II \times_{t} II) ↾_{𝑡} (u \times v)) Cn C)))) \land (r \in u \land t \in v)) \to v \in II$
71		simplr2	$⊢ ((((φ \land (a \in [0, 1] \land b \in [0, 1])) \land (u \in II \land v \in II)) \land (b \in u \land a \in v \land (\exists w \in v {K ↾}_{(u \times \{w\})} \in (((II \times_{t} II) ↾_{𝑡} (u \times \{w\})) Cn C) \to {K ↾}_{(u \times v)} \in (((II \times_{t} II) ↾_{𝑡} (u \times v)) Cn C)))) \land (r \in u \land t \in v)) \to a \in v$
72		simprr	$⊢ ((((φ \land (a \in [0, 1] \land b \in [0, 1])) \land (u \in II \land v \in II)) \land (b \in u \land a \in v \land (\exists w \in v {K ↾}_{(u \times \{w\})} \in (((II \times_{t} II) ↾_{𝑡} (u \times \{w\})) Cn C) \to {K ↾}_{(u \times v)} \in (((II \times_{t} II) ↾_{𝑡} (u \times v)) Cn C)))) \land (r \in u \land t \in v)) \to t \in v$
73		sneq	$⊢ c = w \to \{c\} = \{w\}$
74	73	xpeq2d	$⊢ c = w \to u \times \{c\} = u \times \{w\}$
75	74	reseq2d	$⊢ c = w \to {K ↾}_{(u \times \{c\})} = {K ↾}_{(u \times \{w\})}$
76	74	oveq2d	$⊢ c = w \to (II \times_{t} II) ↾_{𝑡} (u \times \{c\}) = (II \times_{t} II) ↾_{𝑡} (u \times \{w\})$
77	76	oveq1d	$⊢ c = w \to ((II \times_{t} II) ↾_{𝑡} (u \times \{c\})) Cn C = ((II \times_{t} II) ↾_{𝑡} (u \times \{w\})) Cn C$
78	75 77	eleq12d	$⊢ c = w \to ({K ↾}_{(u \times \{c\})} \in (((II \times_{t} II) ↾_{𝑡} (u \times \{c\})) Cn C) \leftrightarrow {K ↾}_{(u \times \{w\})} \in (((II \times_{t} II) ↾_{𝑡} (u \times \{w\})) Cn C))$
79	78	cbvrexvw	$⊢ \exists c \in v {K ↾}_{(u \times \{c\})} \in (((II \times_{t} II) ↾_{𝑡} (u \times \{c\})) Cn C) \leftrightarrow \exists w \in v {K ↾}_{(u \times \{w\})} \in (((II \times_{t} II) ↾_{𝑡} (u \times \{w\})) Cn C)$
80		simplr3	$⊢ ((((φ \land (a \in [0, 1] \land b \in [0, 1])) \land (u \in II \land v \in II)) \land (b \in u \land a \in v \land (\exists w \in v {K ↾}_{(u \times \{w\})} \in (((II \times_{t} II) ↾_{𝑡} (u \times \{w\})) Cn C) \to {K ↾}_{(u \times v)} \in (((II \times_{t} II) ↾_{𝑡} (u \times v)) Cn C)))) \land (r \in u \land t \in v)) \to (\exists w \in v {K ↾}_{(u \times \{w\})} \in (((II \times_{t} II) ↾_{𝑡} (u \times \{w\})) Cn C) \to {K ↾}_{(u \times v)} \in (((II \times_{t} II) ↾_{𝑡} (u \times v)) Cn C))$
81	79 80	biimtrid	$⊢ ((((φ \land (a \in [0, 1] \land b \in [0, 1])) \land (u \in II \land v \in II)) \land (b \in u \land a \in v \land (\exists w \in v {K ↾}_{(u \times \{w\})} \in (((II \times_{t} II) ↾_{𝑡} (u \times \{w\})) Cn C) \to {K ↾}_{(u \times v)} \in (((II \times_{t} II) ↾_{𝑡} (u \times v)) Cn C)))) \land (r \in u \land t \in v)) \to (\exists c \in v {K ↾}_{(u \times \{c\})} \in (((II \times_{t} II) ↾_{𝑡} (u \times \{c\})) Cn C) \to {K ↾}_{(u \times v)} \in (((II \times_{t} II) ↾_{𝑡} (u \times v)) Cn C))$
82	1 66 67 68 69 6 7 8 62 70 71 72 81	cvmlift2lem11	$⊢ ((((φ \land (a \in [0, 1] \land b \in [0, 1])) \land (u \in II \land v \in II)) \land (b \in u \land a \in v \land (\exists w \in v {K ↾}_{(u \times \{w\})} \in (((II \times_{t} II) ↾_{𝑡} (u \times \{w\})) Cn C) \to {K ↾}_{(u \times v)} \in (((II \times_{t} II) ↾_{𝑡} (u \times v)) Cn C)))) \land (r \in u \land t \in v)) \to (u \times \{a\} \subseteq M \to u \times \{t\} \subseteq M)$
83	1 66 67 68 69 6 7 8 62 70 72 71 81	cvmlift2lem11	$⊢ ((((φ \land (a \in [0, 1] \land b \in [0, 1])) \land (u \in II \land v \in II)) \land (b \in u \land a \in v \land (\exists w \in v {K ↾}_{(u \times \{w\})} \in (((II \times_{t} II) ↾_{𝑡} (u \times \{w\})) Cn C) \to {K ↾}_{(u \times v)} \in (((II \times_{t} II) ↾_{𝑡} (u \times v)) Cn C)))) \land (r \in u \land t \in v)) \to (u \times \{t\} \subseteq M \to u \times \{a\} \subseteq M)$
84	82 83	impbid	$⊢ ((((φ \land (a \in [0, 1] \land b \in [0, 1])) \land (u \in II \land v \in II)) \land (b \in u \land a \in v \land (\exists w \in v {K ↾}_{(u \times \{w\})} \in (((II \times_{t} II) ↾_{𝑡} (u \times \{w\})) Cn C) \to {K ↾}_{(u \times v)} \in (((II \times_{t} II) ↾_{𝑡} (u \times v)) Cn C)))) \land (r \in u \land t \in v)) \to (u \times \{a\} \subseteq M \leftrightarrow u \times \{t\} \subseteq M)$
85		rspe	$⊢ (u \in nei (II) (\{r\}) \land (u \times \{a\} \subseteq M \leftrightarrow u \times \{t\} \subseteq M)) \to \exists u \in nei (II) (\{r\}) (u \times \{a\} \subseteq M \leftrightarrow u \times \{t\} \subseteq M)$
86	65 84 85	syl2anc	$⊢ ((((φ \land (a \in [0, 1] \land b \in [0, 1])) \land (u \in II \land v \in II)) \land (b \in u \land a \in v \land (\exists w \in v {K ↾}_{(u \times \{w\})} \in (((II \times_{t} II) ↾_{𝑡} (u \times \{w\})) Cn C) \to {K ↾}_{(u \times v)} \in (((II \times_{t} II) ↾_{𝑡} (u \times v)) Cn C)))) \land (r \in u \land t \in v)) \to \exists u \in nei (II) (\{r\}) (u \times \{a\} \subseteq M \leftrightarrow u \times \{t\} \subseteq M)$
87	60 86	jca	$⊢ ((((φ \land (a \in [0, 1] \land b \in [0, 1])) \land (u \in II \land v \in II)) \land (b \in u \land a \in v \land (\exists w \in v {K ↾}_{(u \times \{w\})} \in (((II \times_{t} II) ↾_{𝑡} (u \times \{w\})) Cn C) \to {K ↾}_{(u \times v)} \in (((II \times_{t} II) ↾_{𝑡} (u \times v)) Cn C)))) \land (r \in u \land t \in v)) \to (t \in [0, 1] \land \exists u \in nei (II) (\{r\}) (u \times \{a\} \subseteq M \leftrightarrow u \times \{t\} \subseteq M))$
88	87	ex	$⊢ (((φ \land (a \in [0, 1] \land b \in [0, 1])) \land (u \in II \land v \in II)) \land (b \in u \land a \in v \land (\exists w \in v {K ↾}_{(u \times \{w\})} \in (((II \times_{t} II) ↾_{𝑡} (u \times \{w\})) Cn C) \to {K ↾}_{(u \times v)} \in (((II \times_{t} II) ↾_{𝑡} (u \times v)) Cn C)))) \to ((r \in u \land t \in v) \to (t \in [0, 1] \land \exists u \in nei (II) (\{r\}) (u \times \{a\} \subseteq M \leftrightarrow u \times \{t\} \subseteq M)))$
89	88	alrimivv	$⊢ (((φ \land (a \in [0, 1] \land b \in [0, 1])) \land (u \in II \land v \in II)) \land (b \in u \land a \in v \land (\exists w \in v {K ↾}_{(u \times \{w\})} \in (((II \times_{t} II) ↾_{𝑡} (u \times \{w\})) Cn C) \to {K ↾}_{(u \times v)} \in (((II \times_{t} II) ↾_{𝑡} (u \times v)) Cn C)))) \to \forall r \forall t ((r \in u \land t \in v) \to (t \in [0, 1] \land \exists u \in nei (II) (\{r\}) (u \times \{a\} \subseteq M \leftrightarrow u \times \{t\} \subseteq M)))$
90		df-xp	$⊢ u \times v = \{⟨r, t⟩ \| (r \in u \land t \in v)\}$
91	90 10	sseq12i	$⊢ u \times v \subseteq S \leftrightarrow \{⟨r, t⟩ \| (r \in u \land t \in v)\} \subseteq \{⟨r, t⟩ \| (t \in [0, 1] \land \exists u \in nei (II) (\{r\}) (u \times \{a\} \subseteq M \leftrightarrow u \times \{t\} \subseteq M))\}$
92		ssopab2bw	$⊢ \{⟨r, t⟩ \| (r \in u \land t \in v)\} \subseteq \{⟨r, t⟩ \| (t \in [0, 1] \land \exists u \in nei (II) (\{r\}) (u \times \{a\} \subseteq M \leftrightarrow u \times \{t\} \subseteq M))\} \leftrightarrow \forall r \forall t ((r \in u \land t \in v) \to (t \in [0, 1] \land \exists u \in nei (II) (\{r\}) (u \times \{a\} \subseteq M \leftrightarrow u \times \{t\} \subseteq M)))$
93	91 92	bitri	$⊢ u \times v \subseteq S \leftrightarrow \forall r \forall t ((r \in u \land t \in v) \to (t \in [0, 1] \land \exists u \in nei (II) (\{r\}) (u \times \{a\} \subseteq M \leftrightarrow u \times \{t\} \subseteq M)))$
94	89 93	sylibr	$⊢ (((φ \land (a \in [0, 1] \land b \in [0, 1])) \land (u \in II \land v \in II)) \land (b \in u \land a \in v \land (\exists w \in v {K ↾}_{(u \times \{w\})} \in (((II \times_{t} II) ↾_{𝑡} (u \times \{w\})) Cn C) \to {K ↾}_{(u \times v)} \in (((II \times_{t} II) ↾_{𝑡} (u \times v)) Cn C)))) \to u \times v \subseteq S$
95	38	ssntr	$⊢ ((II \times_{t} II \in Top \land S \subseteq [0, 1] \times [0, 1]) \land (u \times v \in (II \times_{t} II) \land u \times v \subseteq S)) \to u \times v \subseteq int (II \times_{t} II) (S)$
96	50 51 56 94 95	syl22anc	$⊢ (((φ \land (a \in [0, 1] \land b \in [0, 1])) \land (u \in II \land v \in II)) \land (b \in u \land a \in v \land (\exists w \in v {K ↾}_{(u \times \{w\})} \in (((II \times_{t} II) ↾_{𝑡} (u \times \{w\})) Cn C) \to {K ↾}_{(u \times v)} \in (((II \times_{t} II) ↾_{𝑡} (u \times v)) Cn C)))) \to u \times v \subseteq int (II \times_{t} II) (S)$
97		simpr1	$⊢ (((φ \land (a \in [0, 1] \land b \in [0, 1])) \land (u \in II \land v \in II)) \land (b \in u \land a \in v \land (\exists w \in v {K ↾}_{(u \times \{w\})} \in (((II \times_{t} II) ↾_{𝑡} (u \times \{w\})) Cn C) \to {K ↾}_{(u \times v)} \in (((II \times_{t} II) ↾_{𝑡} (u \times v)) Cn C)))) \to b \in u$
98		simpr2	$⊢ (((φ \land (a \in [0, 1] \land b \in [0, 1])) \land (u \in II \land v \in II)) \land (b \in u \land a \in v \land (\exists w \in v {K ↾}_{(u \times \{w\})} \in (((II \times_{t} II) ↾_{𝑡} (u \times \{w\})) Cn C) \to {K ↾}_{(u \times v)} \in (((II \times_{t} II) ↾_{𝑡} (u \times v)) Cn C)))) \to a \in v$
99		opelxpi	$⊢ (b \in u \land a \in v) \to ⟨b, a⟩ \in (u \times v)$
100	97 98 99	syl2anc	$⊢ (((φ \land (a \in [0, 1] \land b \in [0, 1])) \land (u \in II \land v \in II)) \land (b \in u \land a \in v \land (\exists w \in v {K ↾}_{(u \times \{w\})} \in (((II \times_{t} II) ↾_{𝑡} (u \times \{w\})) Cn C) \to {K ↾}_{(u \times v)} \in (((II \times_{t} II) ↾_{𝑡} (u \times v)) Cn C)))) \to ⟨b, a⟩ \in (u \times v)$
101	96 100	sseldd	$⊢ (((φ \land (a \in [0, 1] \land b \in [0, 1])) \land (u \in II \land v \in II)) \land (b \in u \land a \in v \land (\exists w \in v {K ↾}_{(u \times \{w\})} \in (((II \times_{t} II) ↾_{𝑡} (u \times \{w\})) Cn C) \to {K ↾}_{(u \times v)} \in (((II \times_{t} II) ↾_{𝑡} (u \times v)) Cn C)))) \to ⟨b, a⟩ \in int (II \times_{t} II) (S)$
102	101	ex	$⊢ ((φ \land (a \in [0, 1] \land b \in [0, 1])) \land (u \in II \land v \in II)) \to ((b \in u \land a \in v \land (\exists w \in v {K ↾}_{(u \times \{w\})} \in (((II \times_{t} II) ↾_{𝑡} (u \times \{w\})) Cn C) \to {K ↾}_{(u \times v)} \in (((II \times_{t} II) ↾_{𝑡} (u \times v)) Cn C))) \to ⟨b, a⟩ \in int (II \times_{t} II) (S))$
103	102	rexlimdvva	$⊢ (φ \land (a \in [0, 1] \land b \in [0, 1])) \to (\exists u \in II \exists v \in II (b \in u \land a \in v \land (\exists w \in v {K ↾}_{(u \times \{w\})} \in (((II \times_{t} II) ↾_{𝑡} (u \times \{w\})) Cn C) \to {K ↾}_{(u \times v)} \in (((II \times_{t} II) ↾_{𝑡} (u \times v)) Cn C))) \to ⟨b, a⟩ \in int (II \times_{t} II) (S))$
104	49 103	mpd	$⊢ (φ \land (a \in [0, 1] \land b \in [0, 1])) \to ⟨b, a⟩ \in int (II \times_{t} II) (S)$
105		vex	$⊢ a \in V$
106		opeq2	$⊢ w = a \to ⟨b, w⟩ = ⟨b, a⟩$
107	106	eleq1d	$⊢ w = a \to (⟨b, w⟩ \in int (II \times_{t} II) (S) \leftrightarrow ⟨b, a⟩ \in int (II \times_{t} II) (S))$
108	105 107	ralsn	$⊢ \forall w \in \{a\} ⟨b, w⟩ \in int (II \times_{t} II) (S) \leftrightarrow ⟨b, a⟩ \in int (II \times_{t} II) (S)$
109	104 108	sylibr	$⊢ (φ \land (a \in [0, 1] \land b \in [0, 1])) \to \forall w \in \{a\} ⟨b, w⟩ \in int (II \times_{t} II) (S)$
110	109	anassrs	$⊢ ((φ \land a \in [0, 1]) \land b \in [0, 1]) \to \forall w \in \{a\} ⟨b, w⟩ \in int (II \times_{t} II) (S)$
111	110	ralrimiva	$⊢ (φ \land a \in [0, 1]) \to \forall b \in [0, 1] \forall w \in \{a\} ⟨b, w⟩ \in int (II \times_{t} II) (S)$
112		dfss3	$⊢ [0, 1] \times \{a\} \subseteq int (II \times_{t} II) (S) \leftrightarrow \forall u \in ([0, 1] \times \{a\}) u \in int (II \times_{t} II) (S)$
113		eleq1	$⊢ u = ⟨b, w⟩ \to (u \in int (II \times_{t} II) (S) \leftrightarrow ⟨b, w⟩ \in int (II \times_{t} II) (S))$
114	113	ralxp	$⊢ \forall u \in ([0, 1] \times \{a\}) u \in int (II \times_{t} II) (S) \leftrightarrow \forall b \in [0, 1] \forall w \in \{a\} ⟨b, w⟩ \in int (II \times_{t} II) (S)$
115	112 114	bitri	$⊢ [0, 1] \times \{a\} \subseteq int (II \times_{t} II) (S) \leftrightarrow \forall b \in [0, 1] \forall w \in \{a\} ⟨b, w⟩ \in int (II \times_{t} II) (S)$
116	111 115	sylibr	$⊢ (φ \land a \in [0, 1]) \to [0, 1] \times \{a\} \subseteq int (II \times_{t} II) (S)$
117		simpr	$⊢ (φ \land a \in [0, 1]) \to a \in [0, 1]$
118	16 16 21 23 41 116 117	txtube	$⊢ (φ \land a \in [0, 1]) \to \exists v \in II (a \in v \land [0, 1] \times v \subseteq int (II \times_{t} II) (S))$
119	38	ntrss2	$⊢ (II \times_{t} II \in Top \land S \subseteq [0, 1] \times [0, 1]) \to int (II \times_{t} II) (S) \subseteq S$
120	24 37 119	mp2an	$⊢ int (II \times_{t} II) (S) \subseteq S$
121		sstr	$⊢ ([0, 1] \times v \subseteq int (II \times_{t} II) (S) \land int (II \times_{t} II) (S) \subseteq S) \to [0, 1] \times v \subseteq S$
122	120 121	mpan2	$⊢ [0, 1] \times v \subseteq int (II \times_{t} II) (S) \to [0, 1] \times v \subseteq S$
123		df-xp	$⊢ [0, 1] \times v = \{⟨r, t⟩ \| (r \in [0, 1] \land t \in v)\}$
124	123 10	sseq12i	$⊢ [0, 1] \times v \subseteq S \leftrightarrow \{⟨r, t⟩ \| (r \in [0, 1] \land t \in v)\} \subseteq \{⟨r, t⟩ \| (t \in [0, 1] \land \exists u \in nei (II) (\{r\}) (u \times \{a\} \subseteq M \leftrightarrow u \times \{t\} \subseteq M))\}$
125		ssopab2bw	$⊢ \{⟨r, t⟩ \| (r \in [0, 1] \land t \in v)\} \subseteq \{⟨r, t⟩ \| (t \in [0, 1] \land \exists u \in nei (II) (\{r\}) (u \times \{a\} \subseteq M \leftrightarrow u \times \{t\} \subseteq M))\} \leftrightarrow \forall r \forall t ((r \in [0, 1] \land t \in v) \to (t \in [0, 1] \land \exists u \in nei (II) (\{r\}) (u \times \{a\} \subseteq M \leftrightarrow u \times \{t\} \subseteq M)))$
126		r2al	$⊢ \forall r \in [0, 1] \forall t \in v (t \in [0, 1] \land \exists u \in nei (II) (\{r\}) (u \times \{a\} \subseteq M \leftrightarrow u \times \{t\} \subseteq M)) \leftrightarrow \forall r \forall t ((r \in [0, 1] \land t \in v) \to (t \in [0, 1] \land \exists u \in nei (II) (\{r\}) (u \times \{a\} \subseteq M \leftrightarrow u \times \{t\} \subseteq M)))$
127		ralcom	$⊢ \forall r \in [0, 1] \forall t \in v (t \in [0, 1] \land \exists u \in nei (II) (\{r\}) (u \times \{a\} \subseteq M \leftrightarrow u \times \{t\} \subseteq M)) \leftrightarrow \forall t \in v \forall r \in [0, 1] (t \in [0, 1] \land \exists u \in nei (II) (\{r\}) (u \times \{a\} \subseteq M \leftrightarrow u \times \{t\} \subseteq M))$
128	125 126 127	3bitr2i	$⊢ \{⟨r, t⟩ \| (r \in [0, 1] \land t \in v)\} \subseteq \{⟨r, t⟩ \| (t \in [0, 1] \land \exists u \in nei (II) (\{r\}) (u \times \{a\} \subseteq M \leftrightarrow u \times \{t\} \subseteq M))\} \leftrightarrow \forall t \in v \forall r \in [0, 1] (t \in [0, 1] \land \exists u \in nei (II) (\{r\}) (u \times \{a\} \subseteq M \leftrightarrow u \times \{t\} \subseteq M))$
129	124 128	bitri	$⊢ [0, 1] \times v \subseteq S \leftrightarrow \forall t \in v \forall r \in [0, 1] (t \in [0, 1] \land \exists u \in nei (II) (\{r\}) (u \times \{a\} \subseteq M \leftrightarrow u \times \{t\} \subseteq M))$
130	122 129	sylib	$⊢ [0, 1] \times v \subseteq int (II \times_{t} II) (S) \to \forall t \in v \forall r \in [0, 1] (t \in [0, 1] \land \exists u \in nei (II) (\{r\}) (u \times \{a\} \subseteq M \leftrightarrow u \times \{t\} \subseteq M))$
131		simpr	$⊢ (t \in [0, 1] \land \exists u \in nei (II) (\{r\}) (u \times \{a\} \subseteq M \leftrightarrow u \times \{t\} \subseteq M)) \to \exists u \in nei (II) (\{r\}) (u \times \{a\} \subseteq M \leftrightarrow u \times \{t\} \subseteq M)$
132	131	ralimi	$⊢ \forall r \in [0, 1] (t \in [0, 1] \land \exists u \in nei (II) (\{r\}) (u \times \{a\} \subseteq M \leftrightarrow u \times \{t\} \subseteq M)) \to \forall r \in [0, 1] \exists u \in nei (II) (\{r\}) (u \times \{a\} \subseteq M \leftrightarrow u \times \{t\} \subseteq M)$
133		cvmlift2lem1	$⊢ \forall r \in [0, 1] \exists u \in nei (II) (\{r\}) (u \times \{a\} \subseteq M \leftrightarrow u \times \{t\} \subseteq M) \to ([0, 1] \times \{a\} \subseteq M \to [0, 1] \times \{t\} \subseteq M)$
134		bicom	$⊢ (u \times \{a\} \subseteq M \leftrightarrow u \times \{t\} \subseteq M) \leftrightarrow (u \times \{t\} \subseteq M \leftrightarrow u \times \{a\} \subseteq M)$
135	134	rexbii	$⊢ \exists u \in nei (II) (\{r\}) (u \times \{a\} \subseteq M \leftrightarrow u \times \{t\} \subseteq M) \leftrightarrow \exists u \in nei (II) (\{r\}) (u \times \{t\} \subseteq M \leftrightarrow u \times \{a\} \subseteq M)$
136	135	ralbii	$⊢ \forall r \in [0, 1] \exists u \in nei (II) (\{r\}) (u \times \{a\} \subseteq M \leftrightarrow u \times \{t\} \subseteq M) \leftrightarrow \forall r \in [0, 1] \exists u \in nei (II) (\{r\}) (u \times \{t\} \subseteq M \leftrightarrow u \times \{a\} \subseteq M)$
137		cvmlift2lem1	$⊢ \forall r \in [0, 1] \exists u \in nei (II) (\{r\}) (u \times \{t\} \subseteq M \leftrightarrow u \times \{a\} \subseteq M) \to ([0, 1] \times \{t\} \subseteq M \to [0, 1] \times \{a\} \subseteq M)$
138	136 137	sylbi	$⊢ \forall r \in [0, 1] \exists u \in nei (II) (\{r\}) (u \times \{a\} \subseteq M \leftrightarrow u \times \{t\} \subseteq M) \to ([0, 1] \times \{t\} \subseteq M \to [0, 1] \times \{a\} \subseteq M)$
139	133 138	impbid	$⊢ \forall r \in [0, 1] \exists u \in nei (II) (\{r\}) (u \times \{a\} \subseteq M \leftrightarrow u \times \{t\} \subseteq M) \to ([0, 1] \times \{a\} \subseteq M \leftrightarrow [0, 1] \times \{t\} \subseteq M)$
140	132 139	syl	$⊢ \forall r \in [0, 1] (t \in [0, 1] \land \exists u \in nei (II) (\{r\}) (u \times \{a\} \subseteq M \leftrightarrow u \times \{t\} \subseteq M)) \to ([0, 1] \times \{a\} \subseteq M \leftrightarrow [0, 1] \times \{t\} \subseteq M)$
141	9	reqabi	$⊢ a \in A \leftrightarrow (a \in [0, 1] \land [0, 1] \times \{a\} \subseteq M)$
142	141	baib	$⊢ a \in [0, 1] \to (a \in A \leftrightarrow [0, 1] \times \{a\} \subseteq M)$
143	142	ad3antlr	$⊢ (((φ \land a \in [0, 1]) \land v \in II) \land t \in v) \to (a \in A \leftrightarrow [0, 1] \times \{a\} \subseteq M)$
144		elssuni	$⊢ v \in II \to v \subseteq ⋃ II$
145	144 16	sseqtrrdi	$⊢ v \in II \to v \subseteq [0, 1]$
146	145	adantl	$⊢ ((φ \land a \in [0, 1]) \land v \in II) \to v \subseteq [0, 1]$
147	146	sselda	$⊢ (((φ \land a \in [0, 1]) \land v \in II) \land t \in v) \to t \in [0, 1]$
148		sneq	$⊢ a = t \to \{a\} = \{t\}$
149	148	xpeq2d	$⊢ a = t \to [0, 1] \times \{a\} = [0, 1] \times \{t\}$
150	149	sseq1d	$⊢ a = t \to ([0, 1] \times \{a\} \subseteq M \leftrightarrow [0, 1] \times \{t\} \subseteq M)$
151	150 9	elrab2	$⊢ t \in A \leftrightarrow (t \in [0, 1] \land [0, 1] \times \{t\} \subseteq M)$
152	151	baib	$⊢ t \in [0, 1] \to (t \in A \leftrightarrow [0, 1] \times \{t\} \subseteq M)$
153	147 152	syl	$⊢ (((φ \land a \in [0, 1]) \land v \in II) \land t \in v) \to (t \in A \leftrightarrow [0, 1] \times \{t\} \subseteq M)$
154	143 153	bibi12d	$⊢ (((φ \land a \in [0, 1]) \land v \in II) \land t \in v) \to ((a \in A \leftrightarrow t \in A) \leftrightarrow ([0, 1] \times \{a\} \subseteq M \leftrightarrow [0, 1] \times \{t\} \subseteq M))$
155	140 154	imbitrrid	$⊢ (((φ \land a \in [0, 1]) \land v \in II) \land t \in v) \to (\forall r \in [0, 1] (t \in [0, 1] \land \exists u \in nei (II) (\{r\}) (u \times \{a\} \subseteq M \leftrightarrow u \times \{t\} \subseteq M)) \to (a \in A \leftrightarrow t \in A))$
156	155	ralimdva	$⊢ ((φ \land a \in [0, 1]) \land v \in II) \to (\forall t \in v \forall r \in [0, 1] (t \in [0, 1] \land \exists u \in nei (II) (\{r\}) (u \times \{a\} \subseteq M \leftrightarrow u \times \{t\} \subseteq M)) \to \forall t \in v (a \in A \leftrightarrow t \in A))$
157	130 156	syl5	$⊢ ((φ \land a \in [0, 1]) \land v \in II) \to ([0, 1] \times v \subseteq int (II \times_{t} II) (S) \to \forall t \in v (a \in A \leftrightarrow t \in A))$
158	157	anim2d	$⊢ ((φ \land a \in [0, 1]) \land v \in II) \to ((a \in v \land [0, 1] \times v \subseteq int (II \times_{t} II) (S)) \to (a \in v \land \forall t \in v (a \in A \leftrightarrow t \in A)))$
159	158	reximdva	$⊢ (φ \land a \in [0, 1]) \to (\exists v \in II (a \in v \land [0, 1] \times v \subseteq int (II \times_{t} II) (S)) \to \exists v \in II (a \in v \land \forall t \in v (a \in A \leftrightarrow t \in A)))$
160	118 159	mpd	$⊢ (φ \land a \in [0, 1]) \to \exists v \in II (a \in v \land \forall t \in v (a \in A \leftrightarrow t \in A))$
161	160	ralrimiva	$⊢ φ \to \forall a \in [0, 1] \exists v \in II (a \in v \land \forall t \in v (a \in A \leftrightarrow t \in A))$
162		ssrab2	$⊢ \{a \in [0, 1] \| [0, 1] \times \{a\} \subseteq M\} \subseteq [0, 1]$
163	9 162	eqsstri	$⊢ A \subseteq [0, 1]$
164	16	isclo	$⊢ (II \in Top \land A \subseteq [0, 1]) \to (A \in (II \cap Clsd (II)) \leftrightarrow \forall a \in [0, 1] \exists v \in II (a \in v \land \forall t \in v (a \in A \leftrightarrow t \in A)))$
165	22 163 164	mp2an	$⊢ A \in (II \cap Clsd (II)) \leftrightarrow \forall a \in [0, 1] \exists v \in II (a \in v \land \forall t \in v (a \in A \leftrightarrow t \in A))$
166	161 165	sylibr	$⊢ φ \to A \in (II \cap Clsd (II))$
167	19 166	sselid	$⊢ φ \to A \in II$
168		0elunit	$⊢ 0 \in [0, 1]$
169	168	a1i	$⊢ φ \to 0 \in [0, 1]$
170		relxp	$⊢ Rel ([0, 1] \times \{0\})$
171	170	a1i	$⊢ φ \to Rel ([0, 1] \times \{0\})$
172		opelxp	$⊢ ⟨r, a⟩ \in ([0, 1] \times \{0\}) \leftrightarrow (r \in [0, 1] \land a \in \{0\})$
173		id	$⊢ r \in [0, 1] \to r \in [0, 1]$
174		opelxpi	$⊢ (r \in [0, 1] \land 0 \in [0, 1]) \to ⟨r, 0⟩ \in ([0, 1] \times [0, 1])$
175	173 169 174	syl2anr	$⊢ (φ \land r \in [0, 1]) \to ⟨r, 0⟩ \in ([0, 1] \times [0, 1])$
176	2	adantr	$⊢ (φ \land r \in [0, 1]) \to F \in (C CovMap J)$
177	3	adantr	$⊢ (φ \land r \in [0, 1]) \to G \in ((II \times_{t} II) Cn J)$
178	4	adantr	$⊢ (φ \land r \in [0, 1]) \to P \in B$
179	5	adantr	$⊢ (φ \land r \in [0, 1]) \to F (P) = 0 G 0$
180		simpr	$⊢ (φ \land r \in [0, 1]) \to r \in [0, 1]$
181	168	a1i	$⊢ (φ \land r \in [0, 1]) \to 0 \in [0, 1]$
182	1 176 177 178 179 6 7 46 180 181	cvmlift2lem10	$⊢ (φ \land r \in [0, 1]) \to \exists u \in II \exists v \in II (r \in u \land 0 \in v \land (\exists w \in v {K ↾}_{(u \times \{w\})} \in (((II \times_{t} II) ↾_{𝑡} (u \times \{w\})) Cn C) \to {K ↾}_{(u \times v)} \in (((II \times_{t} II) ↾_{𝑡} (u \times v)) Cn C)))$
183		df-3an	$⊢ (r \in u \land 0 \in v \land (\exists w \in v {K ↾}_{(u \times \{w\})} \in (((II \times_{t} II) ↾_{𝑡} (u \times \{w\})) Cn C) \to {K ↾}_{(u \times v)} \in (((II \times_{t} II) ↾_{𝑡} (u \times v)) Cn C))) \leftrightarrow ((r \in u \land 0 \in v) \land (\exists w \in v {K ↾}_{(u \times \{w\})} \in (((II \times_{t} II) ↾_{𝑡} (u \times \{w\})) Cn C) \to {K ↾}_{(u \times v)} \in (((II \times_{t} II) ↾_{𝑡} (u \times v)) Cn C)))$
184		simprr	$⊢ (((φ \land r \in [0, 1]) \land (u \in II \land v \in II)) \land (r \in u \land 0 \in v)) \to 0 \in v$
185	11	ad3antrrr	$⊢ (((φ \land r \in [0, 1]) \land (u \in II \land v \in II)) \land (r \in u \land 0 \in v)) \to K : [0, 1] \times [0, 1] ⟶ B$
186	185	ffnd	$⊢ (((φ \land r \in [0, 1]) \land (u \in II \land v \in II)) \land (r \in u \land 0 \in v)) \to K Fn ([0, 1] \times [0, 1])$
187		fnov	$⊢ K Fn ([0, 1] \times [0, 1]) \leftrightarrow K = (b \in [0, 1], w \in [0, 1] ⟼ b K w)$
188	186 187	sylib	$⊢ (((φ \land r \in [0, 1]) \land (u \in II \land v \in II)) \land (r \in u \land 0 \in v)) \to K = (b \in [0, 1], w \in [0, 1] ⟼ b K w)$
189	188	reseq1d	$⊢ (((φ \land r \in [0, 1]) \land (u \in II \land v \in II)) \land (r \in u \land 0 \in v)) \to {K ↾}_{(u \times \{0\})} = {(b \in [0, 1], w \in [0, 1] ⟼ b K w) ↾}_{(u \times \{0\})}$
190		simplrl	$⊢ (((φ \land r \in [0, 1]) \land (u \in II \land v \in II)) \land (r \in u \land 0 \in v)) \to u \in II$
191		elssuni	$⊢ u \in II \to u \subseteq ⋃ II$
192	191 16	sseqtrrdi	$⊢ u \in II \to u \subseteq [0, 1]$
193	190 192	syl	$⊢ (((φ \land r \in [0, 1]) \land (u \in II \land v \in II)) \land (r \in u \land 0 \in v)) \to u \subseteq [0, 1]$
194	169	snssd	$⊢ φ \to \{0\} \subseteq [0, 1]$
195	194	ad3antrrr	$⊢ (((φ \land r \in [0, 1]) \land (u \in II \land v \in II)) \land (r \in u \land 0 \in v)) \to \{0\} \subseteq [0, 1]$
196		resmpo	$⊢ (u \subseteq [0, 1] \land \{0\} \subseteq [0, 1]) \to {(b \in [0, 1], w \in [0, 1] ⟼ b K w) ↾}_{(u \times \{0\})} = (b \in u, w \in \{0\} ⟼ b K w)$
197	193 195 196	syl2anc	$⊢ (((φ \land r \in [0, 1]) \land (u \in II \land v \in II)) \land (r \in u \land 0 \in v)) \to {(b \in [0, 1], w \in [0, 1] ⟼ b K w) ↾}_{(u \times \{0\})} = (b \in u, w \in \{0\} ⟼ b K w)$
198	193	sselda	$⊢ ((((φ \land r \in [0, 1]) \land (u \in II \land v \in II)) \land (r \in u \land 0 \in v)) \land b \in u) \to b \in [0, 1]$
199		simplll	$⊢ (((φ \land r \in [0, 1]) \land (u \in II \land v \in II)) \land (r \in u \land 0 \in v)) \to φ$
200	1 2 3 4 5 6 7	cvmlift2lem8	$⊢ (φ \land b \in [0, 1]) \to b K 0 = H (b)$
201	199 200	sylan	$⊢ ((((φ \land r \in [0, 1]) \land (u \in II \land v \in II)) \land (r \in u \land 0 \in v)) \land b \in [0, 1]) \to b K 0 = H (b)$
202	198 201	syldan	$⊢ ((((φ \land r \in [0, 1]) \land (u \in II \land v \in II)) \land (r \in u \land 0 \in v)) \land b \in u) \to b K 0 = H (b)$
203		elsni	$⊢ w \in \{0\} \to w = 0$
204	203	oveq2d	$⊢ w \in \{0\} \to b K w = b K 0$
205	204	eqeq1d	$⊢ w \in \{0\} \to (b K w = H (b) \leftrightarrow b K 0 = H (b))$
206	202 205	syl5ibrcom	$⊢ ((((φ \land r \in [0, 1]) \land (u \in II \land v \in II)) \land (r \in u \land 0 \in v)) \land b \in u) \to (w \in \{0\} \to b K w = H (b))$
207	206	3impia	$⊢ ((((φ \land r \in [0, 1]) \land (u \in II \land v \in II)) \land (r \in u \land 0 \in v)) \land b \in u \land w \in \{0\}) \to b K w = H (b)$
208	207	mpoeq3dva	$⊢ (((φ \land r \in [0, 1]) \land (u \in II \land v \in II)) \land (r \in u \land 0 \in v)) \to (b \in u, w \in \{0\} ⟼ b K w) = (b \in u, w \in \{0\} ⟼ H (b))$
209	189 197 208	3eqtrd	$⊢ (((φ \land r \in [0, 1]) \land (u \in II \land v \in II)) \land (r \in u \land 0 \in v)) \to {K ↾}_{(u \times \{0\})} = (b \in u, w \in \{0\} ⟼ H (b))$
210		eqid	$⊢ II ↾_{𝑡} u = II ↾_{𝑡} u$
211		iitopon	$⊢ II \in TopOn ([0, 1])$
212	211	a1i	$⊢ (((φ \land r \in [0, 1]) \land (u \in II \land v \in II)) \land (r \in u \land 0 \in v)) \to II \in TopOn ([0, 1])$
213		eqid	$⊢ II ↾_{𝑡} \{0\} = II ↾_{𝑡} \{0\}$
214	212 212	cnmpt1st	$⊢ (((φ \land r \in [0, 1]) \land (u \in II \land v \in II)) \land (r \in u \land 0 \in v)) \to (b \in [0, 1], w \in [0, 1] ⟼ b) \in ((II \times_{t} II) Cn II)$
215	1 2 3 4 5 6	cvmlift2lem2	$⊢ φ \to (H \in (II Cn C) \land F \circ H = (z \in [0, 1] ⟼ z G 0) \land H (0) = P)$
216	215	simp1d	$⊢ φ \to H \in (II Cn C)$
217	199 216	syl	$⊢ (((φ \land r \in [0, 1]) \land (u \in II \land v \in II)) \land (r \in u \land 0 \in v)) \to H \in (II Cn C)$
218	212 212 214 217	cnmpt21f	$⊢ (((φ \land r \in [0, 1]) \land (u \in II \land v \in II)) \land (r \in u \land 0 \in v)) \to (b \in [0, 1], w \in [0, 1] ⟼ H (b)) \in ((II \times_{t} II) Cn C)$
219	210 212 193 213 212 195 218	cnmpt2res	$⊢ (((φ \land r \in [0, 1]) \land (u \in II \land v \in II)) \land (r \in u \land 0 \in v)) \to (b \in u, w \in \{0\} ⟼ H (b)) \in (((II ↾_{𝑡} u) \times_{t} (II ↾_{𝑡} \{0\})) Cn C)$
220		vex	$⊢ u \in V$
221		snex	$⊢ \{0\} \in V$
222		txrest	$⊢ ((II \in Top \land II \in Top) \land (u \in V \land \{0\} \in V)) \to (II \times_{t} II) ↾_{𝑡} (u \times \{0\}) = (II ↾_{𝑡} u) \times_{t} (II ↾_{𝑡} \{0\})$
223	22 22 220 221 222	mp4an	$⊢ (II \times_{t} II) ↾_{𝑡} (u \times \{0\}) = (II ↾_{𝑡} u) \times_{t} (II ↾_{𝑡} \{0\})$
224	223	oveq1i	$⊢ ((II \times_{t} II) ↾_{𝑡} (u \times \{0\})) Cn C = ((II ↾_{𝑡} u) \times_{t} (II ↾_{𝑡} \{0\})) Cn C$
225	219 224	eleqtrrdi	$⊢ (((φ \land r \in [0, 1]) \land (u \in II \land v \in II)) \land (r \in u \land 0 \in v)) \to (b \in u, w \in \{0\} ⟼ H (b)) \in (((II \times_{t} II) ↾_{𝑡} (u \times \{0\})) Cn C)$
226	209 225	eqeltrd	$⊢ (((φ \land r \in [0, 1]) \land (u \in II \land v \in II)) \land (r \in u \land 0 \in v)) \to {K ↾}_{(u \times \{0\})} \in (((II \times_{t} II) ↾_{𝑡} (u \times \{0\})) Cn C)$
227		sneq	$⊢ w = 0 \to \{w\} = \{0\}$
228	227	xpeq2d	$⊢ w = 0 \to u \times \{w\} = u \times \{0\}$
229	228	reseq2d	$⊢ w = 0 \to {K ↾}_{(u \times \{w\})} = {K ↾}_{(u \times \{0\})}$
230	228	oveq2d	$⊢ w = 0 \to (II \times_{t} II) ↾_{𝑡} (u \times \{w\}) = (II \times_{t} II) ↾_{𝑡} (u \times \{0\})$
231	230	oveq1d	$⊢ w = 0 \to ((II \times_{t} II) ↾_{𝑡} (u \times \{w\})) Cn C = ((II \times_{t} II) ↾_{𝑡} (u \times \{0\})) Cn C$
232	229 231	eleq12d	$⊢ w = 0 \to ({K ↾}_{(u \times \{w\})} \in (((II \times_{t} II) ↾_{𝑡} (u \times \{w\})) Cn C) \leftrightarrow {K ↾}_{(u \times \{0\})} \in (((II \times_{t} II) ↾_{𝑡} (u \times \{0\})) Cn C))$
233	232	rspcev	$⊢ (0 \in v \land {K ↾}_{(u \times \{0\})} \in (((II \times_{t} II) ↾_{𝑡} (u \times \{0\})) Cn C)) \to \exists w \in v {K ↾}_{(u \times \{w\})} \in (((II \times_{t} II) ↾_{𝑡} (u \times \{w\})) Cn C)$
234	184 226 233	syl2anc	$⊢ (((φ \land r \in [0, 1]) \land (u \in II \land v \in II)) \land (r \in u \land 0 \in v)) \to \exists w \in v {K ↾}_{(u \times \{w\})} \in (((II \times_{t} II) ↾_{𝑡} (u \times \{w\})) Cn C)$
235		opelxpi	$⊢ (r \in u \land 0 \in v) \to ⟨r, 0⟩ \in (u \times v)$
236	235	adantl	$⊢ (((φ \land r \in [0, 1]) \land (u \in II \land v \in II)) \land (r \in u \land 0 \in v)) \to ⟨r, 0⟩ \in (u \times v)$
237		simplrr	$⊢ (((φ \land r \in [0, 1]) \land (u \in II \land v \in II)) \land (r \in u \land 0 \in v)) \to v \in II$
238	237 145	syl	$⊢ (((φ \land r \in [0, 1]) \land (u \in II \land v \in II)) \land (r \in u \land 0 \in v)) \to v \subseteq [0, 1]$
239		xpss12	$⊢ (u \subseteq [0, 1] \land v \subseteq [0, 1]) \to u \times v \subseteq [0, 1] \times [0, 1]$
240	193 238 239	syl2anc	$⊢ (((φ \land r \in [0, 1]) \land (u \in II \land v \in II)) \land (r \in u \land 0 \in v)) \to u \times v \subseteq [0, 1] \times [0, 1]$
241	38	restuni	$⊢ (II \times_{t} II \in Top \land u \times v \subseteq [0, 1] \times [0, 1]) \to u \times v = ⋃ ((II \times_{t} II) ↾_{𝑡} (u \times v))$
242	24 240 241	sylancr	$⊢ (((φ \land r \in [0, 1]) \land (u \in II \land v \in II)) \land (r \in u \land 0 \in v)) \to u \times v = ⋃ ((II \times_{t} II) ↾_{𝑡} (u \times v))$
243	236 242	eleqtrd	$⊢ (((φ \land r \in [0, 1]) \land (u \in II \land v \in II)) \land (r \in u \land 0 \in v)) \to ⟨r, 0⟩ \in ⋃ ((II \times_{t} II) ↾_{𝑡} (u \times v))$
244		eqid	$⊢ ⋃ ((II \times_{t} II) ↾_{𝑡} (u \times v)) = ⋃ ((II \times_{t} II) ↾_{𝑡} (u \times v))$
245	244	cncnpi	$⊢ ({K ↾}_{(u \times v)} \in (((II \times_{t} II) ↾_{𝑡} (u \times v)) Cn C) \land ⟨r, 0⟩ \in ⋃ ((II \times_{t} II) ↾_{𝑡} (u \times v))) \to {K ↾}_{(u \times v)} \in (((II \times_{t} II) ↾_{𝑡} (u \times v)) CnP C) (⟨r, 0⟩)$
246	245	expcom	$⊢ ⟨r, 0⟩ \in ⋃ ((II \times_{t} II) ↾_{𝑡} (u \times v)) \to ({K ↾}_{(u \times v)} \in (((II \times_{t} II) ↾_{𝑡} (u \times v)) Cn C) \to {K ↾}_{(u \times v)} \in (((II \times_{t} II) ↾_{𝑡} (u \times v)) CnP C) (⟨r, 0⟩))$
247	243 246	syl	$⊢ (((φ \land r \in [0, 1]) \land (u \in II \land v \in II)) \land (r \in u \land 0 \in v)) \to ({K ↾}_{(u \times v)} \in (((II \times_{t} II) ↾_{𝑡} (u \times v)) Cn C) \to {K ↾}_{(u \times v)} \in (((II \times_{t} II) ↾_{𝑡} (u \times v)) CnP C) (⟨r, 0⟩))$
248	24	a1i	$⊢ (((φ \land r \in [0, 1]) \land (u \in II \land v \in II)) \land (r \in u \land 0 \in v)) \to II \times_{t} II \in Top$
249	22	a1i	$⊢ (((φ \land r \in [0, 1]) \land (u \in II \land v \in II)) \land (r \in u \land 0 \in v)) \to II \in Top$
250	249 249 190 237 55	syl22anc	$⊢ (((φ \land r \in [0, 1]) \land (u \in II \land v \in II)) \land (r \in u \land 0 \in v)) \to u \times v \in (II \times_{t} II)$
251		isopn3i	$⊢ (II \times_{t} II \in Top \land u \times v \in (II \times_{t} II)) \to int (II \times_{t} II) (u \times v) = u \times v$
252	24 250 251	sylancr	$⊢ (((φ \land r \in [0, 1]) \land (u \in II \land v \in II)) \land (r \in u \land 0 \in v)) \to int (II \times_{t} II) (u \times v) = u \times v$
253	236 252	eleqtrrd	$⊢ (((φ \land r \in [0, 1]) \land (u \in II \land v \in II)) \land (r \in u \land 0 \in v)) \to ⟨r, 0⟩ \in int (II \times_{t} II) (u \times v)$
254	38 1	cnprest	$⊢ ((II \times_{t} II \in Top \land u \times v \subseteq [0, 1] \times [0, 1]) \land (⟨r, 0⟩ \in int (II \times_{t} II) (u \times v) \land K : [0, 1] \times [0, 1] ⟶ B)) \to (K \in ((II \times_{t} II) CnP C) (⟨r, 0⟩) \leftrightarrow {K ↾}_{(u \times v)} \in (((II \times_{t} II) ↾_{𝑡} (u \times v)) CnP C) (⟨r, 0⟩))$
255	248 240 253 185 254	syl22anc	$⊢ (((φ \land r \in [0, 1]) \land (u \in II \land v \in II)) \land (r \in u \land 0 \in v)) \to (K \in ((II \times_{t} II) CnP C) (⟨r, 0⟩) \leftrightarrow {K ↾}_{(u \times v)} \in (((II \times_{t} II) ↾_{𝑡} (u \times v)) CnP C) (⟨r, 0⟩))$
256	247 255	sylibrd	$⊢ (((φ \land r \in [0, 1]) \land (u \in II \land v \in II)) \land (r \in u \land 0 \in v)) \to ({K ↾}_{(u \times v)} \in (((II \times_{t} II) ↾_{𝑡} (u \times v)) Cn C) \to K \in ((II \times_{t} II) CnP C) (⟨r, 0⟩))$
257	234 256	embantd	$⊢ (((φ \land r \in [0, 1]) \land (u \in II \land v \in II)) \land (r \in u \land 0 \in v)) \to ((\exists w \in v {K ↾}_{(u \times \{w\})} \in (((II \times_{t} II) ↾_{𝑡} (u \times \{w\})) Cn C) \to {K ↾}_{(u \times v)} \in (((II \times_{t} II) ↾_{𝑡} (u \times v)) Cn C)) \to K \in ((II \times_{t} II) CnP C) (⟨r, 0⟩))$
258	257	expimpd	$⊢ ((φ \land r \in [0, 1]) \land (u \in II \land v \in II)) \to (((r \in u \land 0 \in v) \land (\exists w \in v {K ↾}_{(u \times \{w\})} \in (((II \times_{t} II) ↾_{𝑡} (u \times \{w\})) Cn C) \to {K ↾}_{(u \times v)} \in (((II \times_{t} II) ↾_{𝑡} (u \times v)) Cn C))) \to K \in ((II \times_{t} II) CnP C) (⟨r, 0⟩))$
259	183 258	biimtrid	$⊢ ((φ \land r \in [0, 1]) \land (u \in II \land v \in II)) \to ((r \in u \land 0 \in v \land (\exists w \in v {K ↾}_{(u \times \{w\})} \in (((II \times_{t} II) ↾_{𝑡} (u \times \{w\})) Cn C) \to {K ↾}_{(u \times v)} \in (((II \times_{t} II) ↾_{𝑡} (u \times v)) Cn C))) \to K \in ((II \times_{t} II) CnP C) (⟨r, 0⟩))$
260	259	rexlimdvva	$⊢ (φ \land r \in [0, 1]) \to (\exists u \in II \exists v \in II (r \in u \land 0 \in v \land (\exists w \in v {K ↾}_{(u \times \{w\})} \in (((II \times_{t} II) ↾_{𝑡} (u \times \{w\})) Cn C) \to {K ↾}_{(u \times v)} \in (((II \times_{t} II) ↾_{𝑡} (u \times v)) Cn C))) \to K \in ((II \times_{t} II) CnP C) (⟨r, 0⟩))$
261	182 260	mpd	$⊢ (φ \land r \in [0, 1]) \to K \in ((II \times_{t} II) CnP C) (⟨r, 0⟩)$
262		fveq2	$⊢ z = ⟨r, 0⟩ \to ((II \times_{t} II) CnP C) (z) = ((II \times_{t} II) CnP C) (⟨r, 0⟩)$
263	262	eleq2d	$⊢ z = ⟨r, 0⟩ \to (K \in ((II \times_{t} II) CnP C) (z) \leftrightarrow K \in ((II \times_{t} II) CnP C) (⟨r, 0⟩))$
264	263 8	elrab2	$⊢ ⟨r, 0⟩ \in M \leftrightarrow (⟨r, 0⟩ \in ([0, 1] \times [0, 1]) \land K \in ((II \times_{t} II) CnP C) (⟨r, 0⟩))$
265	175 261 264	sylanbrc	$⊢ (φ \land r \in [0, 1]) \to ⟨r, 0⟩ \in M$
266		elsni	$⊢ a \in \{0\} \to a = 0$
267	266	opeq2d	$⊢ a \in \{0\} \to ⟨r, a⟩ = ⟨r, 0⟩$
268	267	eleq1d	$⊢ a \in \{0\} \to (⟨r, a⟩ \in M \leftrightarrow ⟨r, 0⟩ \in M)$
269	265 268	syl5ibrcom	$⊢ (φ \land r \in [0, 1]) \to (a \in \{0\} \to ⟨r, a⟩ \in M)$
270	269	expimpd	$⊢ φ \to ((r \in [0, 1] \land a \in \{0\}) \to ⟨r, a⟩ \in M)$
271	172 270	biimtrid	$⊢ φ \to (⟨r, a⟩ \in ([0, 1] \times \{0\}) \to ⟨r, a⟩ \in M)$
272	171 271	relssdv	$⊢ φ \to [0, 1] \times \{0\} \subseteq M$
273		sneq	$⊢ a = 0 \to \{a\} = \{0\}$
274	273	xpeq2d	$⊢ a = 0 \to [0, 1] \times \{a\} = [0, 1] \times \{0\}$
275	274	sseq1d	$⊢ a = 0 \to ([0, 1] \times \{a\} \subseteq M \leftrightarrow [0, 1] \times \{0\} \subseteq M)$
276	275 9	elrab2	$⊢ 0 \in A \leftrightarrow (0 \in [0, 1] \land [0, 1] \times \{0\} \subseteq M)$
277	169 272 276	sylanbrc	$⊢ φ \to 0 \in A$
278	277	ne0d	$⊢ φ \to A \neq \emptyset$
279		inss2	$⊢ II \cap Clsd (II) \subseteq Clsd (II)$
280	279 166	sselid	$⊢ φ \to A \in Clsd (II)$
281	16 18 167 278 280	connclo	$⊢ φ \to A = [0, 1]$
282	281 9	eqtr3di	$⊢ φ \to [0, 1] = \{a \in [0, 1] \| [0, 1] \times \{a\} \subseteq M\}$
283		rabid2	$⊢ [0, 1] = \{a \in [0, 1] \| [0, 1] \times \{a\} \subseteq M\} \leftrightarrow \forall a \in [0, 1] [0, 1] \times \{a\} \subseteq M$
284	282 283	sylib	$⊢ φ \to \forall a \in [0, 1] [0, 1] \times \{a\} \subseteq M$
285		iunss	$⊢ ⋃_{a \in [0, 1]} ([0, 1] \times \{a\}) \subseteq M \leftrightarrow \forall a \in [0, 1] [0, 1] \times \{a\} \subseteq M$
286	284 285	sylibr	$⊢ φ \to ⋃_{a \in [0, 1]} ([0, 1] \times \{a\}) \subseteq M$
287	15 286	eqsstrid	$⊢ φ \to [0, 1] \times [0, 1] \subseteq M$
288	287 8	sseqtrdi	$⊢ φ \to [0, 1] \times [0, 1] \subseteq \{z \in ([0, 1] \times [0, 1]) \| K \in ((II \times_{t} II) CnP C) (z)\}$
289		ssrab	$⊢ [0, 1] \times [0, 1] \subseteq \{z \in ([0, 1] \times [0, 1]) \| K \in ((II \times_{t} II) CnP C) (z)\} \leftrightarrow ([0, 1] \times [0, 1] \subseteq [0, 1] \times [0, 1] \land \forall z \in ([0, 1] \times [0, 1]) K \in ((II \times_{t} II) CnP C) (z))$
290	289	simprbi	$⊢ [0, 1] \times [0, 1] \subseteq \{z \in ([0, 1] \times [0, 1]) \| K \in ((II \times_{t} II) CnP C) (z)\} \to \forall z \in ([0, 1] \times [0, 1]) K \in ((II \times_{t} II) CnP C) (z)$
291	288 290	syl	$⊢ φ \to \forall z \in ([0, 1] \times [0, 1]) K \in ((II \times_{t} II) CnP C) (z)$
292		txtopon	$⊢ (II \in TopOn ([0, 1]) \land II \in TopOn ([0, 1])) \to II \times_{t} II \in TopOn ([0, 1] \times [0, 1])$
293	211 211 292	mp2an	$⊢ II \times_{t} II \in TopOn ([0, 1] \times [0, 1])$
294		cvmtop1	$⊢ F \in (C CovMap J) \to C \in Top$
295	2 294	syl	$⊢ φ \to C \in Top$
296	1	toptopon	$⊢ C \in Top \leftrightarrow C \in TopOn (B)$
297	295 296	sylib	$⊢ φ \to C \in TopOn (B)$
298		cncnp	$⊢ (II \times_{t} II \in TopOn ([0, 1] \times [0, 1]) \land C \in TopOn (B)) \to (K \in ((II \times_{t} II) Cn C) \leftrightarrow (K : [0, 1] \times [0, 1] ⟶ B \land \forall z \in ([0, 1] \times [0, 1]) K \in ((II \times_{t} II) CnP C) (z)))$
299	293 297 298	sylancr	$⊢ φ \to (K \in ((II \times_{t} II) Cn C) \leftrightarrow (K : [0, 1] \times [0, 1] ⟶ B \land \forall z \in ([0, 1] \times [0, 1]) K \in ((II \times_{t} II) CnP C) (z)))$
300	11 291 299	mpbir2and	$⊢ φ \to K \in ((II \times_{t} II) Cn C)$

Metamath Proof Explorer

Theorem cvmlift2lem12

Proof