cvmlift2lem11

	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)\}$
	cvmlift2lem11.1	$⊢ φ \to U \in II$
	cvmlift2lem11.2	$⊢ φ \to V \in II$
	cvmlift2lem11.3	$⊢ φ \to Y \in V$
	cvmlift2lem11.4	$⊢ φ \to Z \in V$
	cvmlift2lem11.5	$⊢ φ \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))$
Assertion	cvmlift2lem11	$⊢ φ \to (U \times \{Y\} \subseteq M \to U \times \{Z\} \subseteq M)$

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		cvmlift2lem11.1	$⊢ φ \to U \in II$
10		cvmlift2lem11.2	$⊢ φ \to V \in II$
11		cvmlift2lem11.3	$⊢ φ \to Y \in V$
12		cvmlift2lem11.4	$⊢ φ \to Z \in V$
13		cvmlift2lem11.5	$⊢ φ \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))$
14	9	adantr	$⊢ (φ \land U \times \{Y\} \subseteq M) \to U \in II$
15		elssuni	$⊢ U \in II \to U \subseteq ⋃ II$
16		iiuni	$⊢ [0, 1] = ⋃ II$
17	15 16	sseqtrrdi	$⊢ U \in II \to U \subseteq [0, 1]$
18	14 17	syl	$⊢ (φ \land U \times \{Y\} \subseteq M) \to U \subseteq [0, 1]$
19		elunii	$⊢ (Z \in V \land V \in II) \to Z \in ⋃ II$
20	19 16	eleqtrrdi	$⊢ (Z \in V \land V \in II) \to Z \in [0, 1]$
21	12 10 20	syl2anc	$⊢ φ \to Z \in [0, 1]$
22	21	adantr	$⊢ (φ \land U \times \{Y\} \subseteq M) \to Z \in [0, 1]$
23	22	snssd	$⊢ (φ \land U \times \{Y\} \subseteq M) \to \{Z\} \subseteq [0, 1]$
24		xpss12	$⊢ (U \subseteq [0, 1] \land \{Z\} \subseteq [0, 1]) \to U \times \{Z\} \subseteq [0, 1] \times [0, 1]$
25	18 23 24	syl2anc	$⊢ (φ \land U \times \{Y\} \subseteq M) \to U \times \{Z\} \subseteq [0, 1] \times [0, 1]$
26	11	adantr	$⊢ (φ \land U \times \{Y\} \subseteq M) \to Y \in V$
27	1 2 3 4 5 6 7	cvmlift2lem5	$⊢ φ \to K : [0, 1] \times [0, 1] ⟶ B$
28	27	adantr	$⊢ (φ \land U \times \{Y\} \subseteq M) \to K : [0, 1] \times [0, 1] ⟶ B$
29	10	adantr	$⊢ (φ \land U \times \{Y\} \subseteq M) \to V \in II$
30		elssuni	$⊢ V \in II \to V \subseteq ⋃ II$
31	30 16	sseqtrrdi	$⊢ V \in II \to V \subseteq [0, 1]$
32	29 31	syl	$⊢ (φ \land U \times \{Y\} \subseteq M) \to V \subseteq [0, 1]$
33	32 26	sseldd	$⊢ (φ \land U \times \{Y\} \subseteq M) \to Y \in [0, 1]$
34	33	snssd	$⊢ (φ \land U \times \{Y\} \subseteq M) \to \{Y\} \subseteq [0, 1]$
35		xpss12	$⊢ (U \subseteq [0, 1] \land \{Y\} \subseteq [0, 1]) \to U \times \{Y\} \subseteq [0, 1] \times [0, 1]$
36	18 34 35	syl2anc	$⊢ (φ \land U \times \{Y\} \subseteq M) \to U \times \{Y\} \subseteq [0, 1] \times [0, 1]$
37	28 36	fssresd	$⊢ (φ \land U \times \{Y\} \subseteq M) \to ({K ↾}_{(U \times \{Y\})}) : U \times \{Y\} ⟶ B$
38	36	adantr	$⊢ ((φ \land U \times \{Y\} \subseteq M) \land z \in (U \times \{Y\})) \to U \times \{Y\} \subseteq [0, 1] \times [0, 1]$
39		simpr	$⊢ ((φ \land U \times \{Y\} \subseteq M) \land z \in (U \times \{Y\})) \to z \in (U \times \{Y\})$
40		simpr	$⊢ (φ \land U \times \{Y\} \subseteq M) \to U \times \{Y\} \subseteq M$
41	40 8	sseqtrdi	$⊢ (φ \land U \times \{Y\} \subseteq M) \to U \times \{Y\} \subseteq \{z \in ([0, 1] \times [0, 1]) \| K \in ((II \times_{t} II) CnP C) (z)\}$
42		ssrab	$⊢ U \times \{Y\} \subseteq \{z \in ([0, 1] \times [0, 1]) \| K \in ((II \times_{t} II) CnP C) (z)\} \leftrightarrow (U \times \{Y\} \subseteq [0, 1] \times [0, 1] \land \forall z \in (U \times \{Y\}) K \in ((II \times_{t} II) CnP C) (z))$
43	42	simprbi	$⊢ U \times \{Y\} \subseteq \{z \in ([0, 1] \times [0, 1]) \| K \in ((II \times_{t} II) CnP C) (z)\} \to \forall z \in (U \times \{Y\}) K \in ((II \times_{t} II) CnP C) (z)$
44	41 43	syl	$⊢ (φ \land U \times \{Y\} \subseteq M) \to \forall z \in (U \times \{Y\}) K \in ((II \times_{t} II) CnP C) (z)$
45	44	r19.21bi	$⊢ ((φ \land U \times \{Y\} \subseteq M) \land z \in (U \times \{Y\})) \to K \in ((II \times_{t} II) CnP C) (z)$
46		iitopon	$⊢ II \in TopOn ([0, 1])$
47		txtopon	$⊢ (II \in TopOn ([0, 1]) \land II \in TopOn ([0, 1])) \to II \times_{t} II \in TopOn ([0, 1] \times [0, 1])$
48	46 46 47	mp2an	$⊢ II \times_{t} II \in TopOn ([0, 1] \times [0, 1])$
49	48	toponunii	$⊢ [0, 1] \times [0, 1] = ⋃ (II \times_{t} II)$
50	49	cnpresti	$⊢ (U \times \{Y\} \subseteq [0, 1] \times [0, 1] \land z \in (U \times \{Y\}) \land K \in ((II \times_{t} II) CnP C) (z)) \to {K ↾}_{(U \times \{Y\})} \in (((II \times_{t} II) ↾_{𝑡} (U \times \{Y\})) CnP C) (z)$
51	38 39 45 50	syl3anc	$⊢ ((φ \land U \times \{Y\} \subseteq M) \land z \in (U \times \{Y\})) \to {K ↾}_{(U \times \{Y\})} \in (((II \times_{t} II) ↾_{𝑡} (U \times \{Y\})) CnP C) (z)$
52	51	ralrimiva	$⊢ (φ \land U \times \{Y\} \subseteq M) \to \forall z \in (U \times \{Y\}) {K ↾}_{(U \times \{Y\})} \in (((II \times_{t} II) ↾_{𝑡} (U \times \{Y\})) CnP C) (z)$
53		resttopon	$⊢ (II \times_{t} II \in TopOn ([0, 1] \times [0, 1]) \land U \times \{Y\} \subseteq [0, 1] \times [0, 1]) \to (II \times_{t} II) ↾_{𝑡} (U \times \{Y\}) \in TopOn (U \times \{Y\})$
54	48 36 53	sylancr	$⊢ (φ \land U \times \{Y\} \subseteq M) \to (II \times_{t} II) ↾_{𝑡} (U \times \{Y\}) \in TopOn (U \times \{Y\})$
55		cvmtop1	$⊢ F \in (C CovMap J) \to C \in Top$
56	2 55	syl	$⊢ φ \to C \in Top$
57	56	adantr	$⊢ (φ \land U \times \{Y\} \subseteq M) \to C \in Top$
58	1	toptopon	$⊢ C \in Top \leftrightarrow C \in TopOn (B)$
59	57 58	sylib	$⊢ (φ \land U \times \{Y\} \subseteq M) \to C \in TopOn (B)$
60		cncnp	$⊢ ((II \times_{t} II) ↾_{𝑡} (U \times \{Y\}) \in TopOn (U \times \{Y\}) \land C \in TopOn (B)) \to ({K ↾}_{(U \times \{Y\})} \in (((II \times_{t} II) ↾_{𝑡} (U \times \{Y\})) Cn C) \leftrightarrow (({K ↾}_{(U \times \{Y\})}) : U \times \{Y\} ⟶ B \land \forall z \in (U \times \{Y\}) {K ↾}_{(U \times \{Y\})} \in (((II \times_{t} II) ↾_{𝑡} (U \times \{Y\})) CnP C) (z)))$
61	54 59 60	syl2anc	$⊢ (φ \land U \times \{Y\} \subseteq M) \to ({K ↾}_{(U \times \{Y\})} \in (((II \times_{t} II) ↾_{𝑡} (U \times \{Y\})) Cn C) \leftrightarrow (({K ↾}_{(U \times \{Y\})}) : U \times \{Y\} ⟶ B \land \forall z \in (U \times \{Y\}) {K ↾}_{(U \times \{Y\})} \in (((II \times_{t} II) ↾_{𝑡} (U \times \{Y\})) CnP C) (z)))$
62	37 52 61	mpbir2and	$⊢ (φ \land U \times \{Y\} \subseteq M) \to {K ↾}_{(U \times \{Y\})} \in (((II \times_{t} II) ↾_{𝑡} (U \times \{Y\})) Cn C)$
63		sneq	$⊢ w = Y \to \{w\} = \{Y\}$
64	63	xpeq2d	$⊢ w = Y \to U \times \{w\} = U \times \{Y\}$
65	64	reseq2d	$⊢ w = Y \to {K ↾}_{(U \times \{w\})} = {K ↾}_{(U \times \{Y\})}$
66	64	oveq2d	$⊢ w = Y \to (II \times_{t} II) ↾_{𝑡} (U \times \{w\}) = (II \times_{t} II) ↾_{𝑡} (U \times \{Y\})$
67	66	oveq1d	$⊢ w = Y \to ((II \times_{t} II) ↾_{𝑡} (U \times \{w\})) Cn C = ((II \times_{t} II) ↾_{𝑡} (U \times \{Y\})) Cn C$
68	65 67	eleq12d	$⊢ w = Y \to ({K ↾}_{(U \times \{w\})} \in (((II \times_{t} II) ↾_{𝑡} (U \times \{w\})) Cn C) \leftrightarrow {K ↾}_{(U \times \{Y\})} \in (((II \times_{t} II) ↾_{𝑡} (U \times \{Y\})) Cn C))$
69	68	rspcev	$⊢ (Y \in V \land {K ↾}_{(U \times \{Y\})} \in (((II \times_{t} II) ↾_{𝑡} (U \times \{Y\})) Cn C)) \to \exists w \in V {K ↾}_{(U \times \{w\})} \in (((II \times_{t} II) ↾_{𝑡} (U \times \{w\})) Cn C)$
70	26 62 69	syl2anc	$⊢ (φ \land U \times \{Y\} \subseteq M) \to \exists w \in V {K ↾}_{(U \times \{w\})} \in (((II \times_{t} II) ↾_{𝑡} (U \times \{w\})) Cn C)$
71	13	imp	$⊢ (φ \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)$
72	70 71	syldan	$⊢ (φ \land U \times \{Y\} \subseteq M) \to {K ↾}_{(U \times V)} \in (((II \times_{t} II) ↾_{𝑡} (U \times V)) Cn C)$
73	72	adantr	$⊢ ((φ \land U \times \{Y\} \subseteq M) \land z \in (U \times \{Z\})) \to {K ↾}_{(U \times V)} \in (((II \times_{t} II) ↾_{𝑡} (U \times V)) Cn C)$
74	12	adantr	$⊢ (φ \land U \times \{Y\} \subseteq M) \to Z \in V$
75	74	snssd	$⊢ (φ \land U \times \{Y\} \subseteq M) \to \{Z\} \subseteq V$
76		xpss2	$⊢ \{Z\} \subseteq V \to U \times \{Z\} \subseteq U \times V$
77	75 76	syl	$⊢ (φ \land U \times \{Y\} \subseteq M) \to U \times \{Z\} \subseteq U \times V$
78		iitop	$⊢ II \in Top$
79	78 78	txtopi	$⊢ II \times_{t} II \in Top$
80		xpss12	$⊢ (U \subseteq [0, 1] \land V \subseteq [0, 1]) \to U \times V \subseteq [0, 1] \times [0, 1]$
81	18 32 80	syl2anc	$⊢ (φ \land U \times \{Y\} \subseteq M) \to U \times V \subseteq [0, 1] \times [0, 1]$
82	49	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))$
83	79 81 82	sylancr	$⊢ (φ \land U \times \{Y\} \subseteq M) \to U \times V = ⋃ ((II \times_{t} II) ↾_{𝑡} (U \times V))$
84	77 83	sseqtrd	$⊢ (φ \land U \times \{Y\} \subseteq M) \to U \times \{Z\} \subseteq ⋃ ((II \times_{t} II) ↾_{𝑡} (U \times V))$
85	84	sselda	$⊢ ((φ \land U \times \{Y\} \subseteq M) \land z \in (U \times \{Z\})) \to z \in ⋃ ((II \times_{t} II) ↾_{𝑡} (U \times V))$
86		eqid	$⊢ ⋃ ((II \times_{t} II) ↾_{𝑡} (U \times V)) = ⋃ ((II \times_{t} II) ↾_{𝑡} (U \times V))$
87	86	cncnpi	$⊢ ({K ↾}_{(U \times V)} \in (((II \times_{t} II) ↾_{𝑡} (U \times V)) Cn C) \land z \in ⋃ ((II \times_{t} II) ↾_{𝑡} (U \times V))) \to {K ↾}_{(U \times V)} \in (((II \times_{t} II) ↾_{𝑡} (U \times V)) CnP C) (z)$
88	73 85 87	syl2anc	$⊢ ((φ \land U \times \{Y\} \subseteq M) \land z \in (U \times \{Z\})) \to {K ↾}_{(U \times V)} \in (((II \times_{t} II) ↾_{𝑡} (U \times V)) CnP C) (z)$
89	79	a1i	$⊢ ((φ \land U \times \{Y\} \subseteq M) \land z \in (U \times \{Z\})) \to II \times_{t} II \in Top$
90	81	adantr	$⊢ ((φ \land U \times \{Y\} \subseteq M) \land z \in (U \times \{Z\})) \to U \times V \subseteq [0, 1] \times [0, 1]$
91	78	a1i	$⊢ (φ \land U \times \{Y\} \subseteq M) \to II \in Top$
92		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)$
93	91 91 14 29 92	syl22anc	$⊢ (φ \land U \times \{Y\} \subseteq M) \to U \times V \in (II \times_{t} II)$
94		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$
95	79 93 94	sylancr	$⊢ (φ \land U \times \{Y\} \subseteq M) \to int (II \times_{t} II) (U \times V) = U \times V$
96	77 95	sseqtrrd	$⊢ (φ \land U \times \{Y\} \subseteq M) \to U \times \{Z\} \subseteq int (II \times_{t} II) (U \times V)$
97	96	sselda	$⊢ ((φ \land U \times \{Y\} \subseteq M) \land z \in (U \times \{Z\})) \to z \in int (II \times_{t} II) (U \times V)$
98	27	ad2antrr	$⊢ ((φ \land U \times \{Y\} \subseteq M) \land z \in (U \times \{Z\})) \to K : [0, 1] \times [0, 1] ⟶ B$
99	49 1	cnprest	$⊢ ((II \times_{t} II \in Top \land U \times V \subseteq [0, 1] \times [0, 1]) \land (z \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) (z) \leftrightarrow {K ↾}_{(U \times V)} \in (((II \times_{t} II) ↾_{𝑡} (U \times V)) CnP C) (z))$
100	89 90 97 98 99	syl22anc	$⊢ ((φ \land U \times \{Y\} \subseteq M) \land z \in (U \times \{Z\})) \to (K \in ((II \times_{t} II) CnP C) (z) \leftrightarrow {K ↾}_{(U \times V)} \in (((II \times_{t} II) ↾_{𝑡} (U \times V)) CnP C) (z))$
101	88 100	mpbird	$⊢ ((φ \land U \times \{Y\} \subseteq M) \land z \in (U \times \{Z\})) \to K \in ((II \times_{t} II) CnP C) (z)$
102	25 101	ssrabdv	$⊢ (φ \land U \times \{Y\} \subseteq M) \to U \times \{Z\} \subseteq \{z \in ([0, 1] \times [0, 1]) \| K \in ((II \times_{t} II) CnP C) (z)\}$
103	102 8	sseqtrrdi	$⊢ (φ \land U \times \{Y\} \subseteq M) \to U \times \{Z\} \subseteq M$
104	103	ex	$⊢ φ \to (U \times \{Y\} \subseteq M \to U \times \{Z\} \subseteq M)$

Metamath Proof Explorer

Theorem cvmlift2lem11

Proof