cvmlift3lem7

	Ref	Expression
Hypotheses	cvmlift3.b	$⊢ B = ⋃ C$
	cvmlift3.y	$⊢ Y = ⋃ K$
	cvmlift3.f	$⊢ φ \to F \in (C CovMap J)$
	cvmlift3.k	$⊢ φ \to K \in SConn$
	cvmlift3.l	$⊢ φ \to K \in N-LocallyPConn$
	cvmlift3.o	$⊢ φ \to O \in Y$
	cvmlift3.g	$⊢ φ \to G \in (K Cn J)$
	cvmlift3.p	$⊢ φ \to P \in B$
	cvmlift3.e	$⊢ φ \to F (P) = G (O)$
	cvmlift3.h	$⊢ H = (x \in Y ⟼ (ι z \in B \| \exists f \in (II Cn K) (f (0) = O \land f (1) = x \land (ι g \in (II Cn C) \| (F \circ g = G \circ f \land g (0) = P)) (1) = z)))$
	cvmlift3lem7.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))))\})$
	cvmlift3lem7.1	$⊢ φ \to G (X) \in A$
	cvmlift3lem7.2	$⊢ φ \to T \in S (A)$
	cvmlift3lem7.3	$⊢ φ \to M \subseteq G^{-1} [A]$
	cvmlift3lem7.w	$⊢ W = (ι b \in T \| H (X) \in b)$
	cvmlift3lem7.7	$⊢ φ \to K ↾_{𝑡} M \in PConn$
	cvmlift3lem7.4	$⊢ φ \to V \in K$
	cvmlift3lem7.5	$⊢ φ \to V \subseteq M$
	cvmlift3lem7.6	$⊢ φ \to X \in V$
Assertion	cvmlift3lem7	$⊢ φ \to H \in (K CnP C) (X)$

Proof

Step	Hyp	Ref	Expression
1		cvmlift3.b	$⊢ B = ⋃ C$
2		cvmlift3.y	$⊢ Y = ⋃ K$
3		cvmlift3.f	$⊢ φ \to F \in (C CovMap J)$
4		cvmlift3.k	$⊢ φ \to K \in SConn$
5		cvmlift3.l	$⊢ φ \to K \in N-LocallyPConn$
6		cvmlift3.o	$⊢ φ \to O \in Y$
7		cvmlift3.g	$⊢ φ \to G \in (K Cn J)$
8		cvmlift3.p	$⊢ φ \to P \in B$
9		cvmlift3.e	$⊢ φ \to F (P) = G (O)$
10		cvmlift3.h	$⊢ H = (x \in Y ⟼ (ι z \in B \| \exists f \in (II Cn K) (f (0) = O \land f (1) = x \land (ι g \in (II Cn C) \| (F \circ g = G \circ f \land g (0) = P)) (1) = z)))$
11		cvmlift3lem7.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))))\})$
12		cvmlift3lem7.1	$⊢ φ \to G (X) \in A$
13		cvmlift3lem7.2	$⊢ φ \to T \in S (A)$
14		cvmlift3lem7.3	$⊢ φ \to M \subseteq G^{-1} [A]$
15		cvmlift3lem7.w	$⊢ W = (ι b \in T \| H (X) \in b)$
16		cvmlift3lem7.7	$⊢ φ \to K ↾_{𝑡} M \in PConn$
17		cvmlift3lem7.4	$⊢ φ \to V \in K$
18		cvmlift3lem7.5	$⊢ φ \to V \subseteq M$
19		cvmlift3lem7.6	$⊢ φ \to X \in V$
20	1 2 3 4 5 6 7 8 9 10	cvmlift3lem3	$⊢ φ \to H : Y ⟶ B$
21	1 2 3 4 5 6 7 8 9 10	cvmlift3lem5	$⊢ φ \to F \circ H = G$
22	21 7	eqeltrd	$⊢ φ \to F \circ H \in (K Cn J)$
23		sconntop	$⊢ K \in SConn \to K \in Top$
24	4 23	syl	$⊢ φ \to K \in Top$
25		cnvimass	$⊢ G^{-1} [A] \subseteq dom G$
26		eqid	$⊢ ⋃ J = ⋃ J$
27	2 26	cnf	$⊢ G \in (K Cn J) \to G : Y ⟶ ⋃ J$
28		fdm	$⊢ G : Y ⟶ ⋃ J \to dom G = Y$
29	7 27 28	3syl	$⊢ φ \to dom G = Y$
30	25 29	sseqtrid	$⊢ φ \to G^{-1} [A] \subseteq Y$
31	14 30	sstrd	$⊢ φ \to M \subseteq Y$
32	18 19	sseldd	$⊢ φ \to X \in M$
33	31 32	sseldd	$⊢ φ \to X \in Y$
34	20 33	ffvelrnd	$⊢ φ \to H (X) \in B$
35		fvco3	$⊢ (H : Y ⟶ B \land X \in Y) \to (F \circ H) (X) = F (H (X))$
36	20 33 35	syl2anc	$⊢ φ \to (F \circ H) (X) = F (H (X))$
37	21	fveq1d	$⊢ φ \to (F \circ H) (X) = G (X)$
38	36 37	eqtr3d	$⊢ φ \to F (H (X)) = G (X)$
39	38 12	eqeltrd	$⊢ φ \to F (H (X)) \in A$
40	11 1 15	cvmsiota	$⊢ (F \in (C CovMap J) \land (T \in S (A) \land H (X) \in B \land F (H (X)) \in A)) \to (W \in T \land H (X) \in W)$
41	3 13 34 39 40	syl13anc	$⊢ φ \to (W \in T \land H (X) \in W)$
42		eqid	$⊢ H (X) = H (X)$
43	1 2 3 4 5 6 7 8 9 10	cvmlift3lem4	$⊢ (φ \land X \in Y) \to (H (X) = H (X) \leftrightarrow \exists f \in (II Cn K) (f (0) = O \land f (1) = X \land (ι g \in (II Cn C) \| (F \circ g = G \circ f \land g (0) = P)) (1) = H (X)))$
44	42 43	mpbii	$⊢ (φ \land X \in Y) \to \exists f \in (II Cn K) (f (0) = O \land f (1) = X \land (ι g \in (II Cn C) \| (F \circ g = G \circ f \land g (0) = P)) (1) = H (X))$
45	33 44	mpdan	$⊢ φ \to \exists f \in (II Cn K) (f (0) = O \land f (1) = X \land (ι g \in (II Cn C) \| (F \circ g = G \circ f \land g (0) = P)) (1) = H (X))$
46	45	adantr	$⊢ (φ \land y \in M) \to \exists f \in (II Cn K) (f (0) = O \land f (1) = X \land (ι g \in (II Cn C) \| (F \circ g = G \circ f \land g (0) = P)) (1) = H (X))$
47		fveq1	$⊢ f = h \to f (0) = h (0)$
48	47	eqeq1d	$⊢ f = h \to (f (0) = O \leftrightarrow h (0) = O)$
49		fveq1	$⊢ f = h \to f (1) = h (1)$
50	49	eqeq1d	$⊢ f = h \to (f (1) = X \leftrightarrow h (1) = X)$
51		coeq2	$⊢ f = h \to G \circ f = G \circ h$
52	51	eqeq2d	$⊢ f = h \to (F \circ g = G \circ f \leftrightarrow F \circ g = G \circ h)$
53	52	anbi1d	$⊢ f = h \to ((F \circ g = G \circ f \land g (0) = P) \leftrightarrow (F \circ g = G \circ h \land g (0) = P))$
54	53	riotabidv	$⊢ f = h \to (ι g \in (II Cn C) \| (F \circ g = G \circ f \land g (0) = P)) = (ι g \in (II Cn C) \| (F \circ g = G \circ h \land g (0) = P))$
55		coeq2	$⊢ a = g \to F \circ a = F \circ g$
56	55	eqeq1d	$⊢ a = g \to (F \circ a = G \circ h \leftrightarrow F \circ g = G \circ h)$
57		fveq1	$⊢ a = g \to a (0) = g (0)$
58	57	eqeq1d	$⊢ a = g \to (a (0) = P \leftrightarrow g (0) = P)$
59	56 58	anbi12d	$⊢ a = g \to ((F \circ a = G \circ h \land a (0) = P) \leftrightarrow (F \circ g = G \circ h \land g (0) = P))$
60	59	cbvriotavw	$⊢ (ι a \in (II Cn C) \| (F \circ a = G \circ h \land a (0) = P)) = (ι g \in (II Cn C) \| (F \circ g = G \circ h \land g (0) = P))$
61	54 60	eqtr4di	$⊢ f = h \to (ι g \in (II Cn C) \| (F \circ g = G \circ f \land g (0) = P)) = (ι a \in (II Cn C) \| (F \circ a = G \circ h \land a (0) = P))$
62	61	fveq1d	$⊢ f = h \to (ι g \in (II Cn C) \| (F \circ g = G \circ f \land g (0) = P)) (1) = (ι a \in (II Cn C) \| (F \circ a = G \circ h \land a (0) = P)) (1)$
63	62	eqeq1d	$⊢ f = h \to ((ι g \in (II Cn C) \| (F \circ g = G \circ f \land g (0) = P)) (1) = H (X) \leftrightarrow (ι a \in (II Cn C) \| (F \circ a = G \circ h \land a (0) = P)) (1) = H (X))$
64	48 50 63	3anbi123d	$⊢ f = h \to ((f (0) = O \land f (1) = X \land (ι g \in (II Cn C) \| (F \circ g = G \circ f \land g (0) = P)) (1) = H (X)) \leftrightarrow (h (0) = O \land h (1) = X \land (ι a \in (II Cn C) \| (F \circ a = G \circ h \land a (0) = P)) (1) = H (X)))$
65	64	cbvrexvw	$⊢ \exists f \in (II Cn K) (f (0) = O \land f (1) = X \land (ι g \in (II Cn C) \| (F \circ g = G \circ f \land g (0) = P)) (1) = H (X)) \leftrightarrow \exists h \in (II Cn K) (h (0) = O \land h (1) = X \land (ι a \in (II Cn C) \| (F \circ a = G \circ h \land a (0) = P)) (1) = H (X))$
66	46 65	sylib	$⊢ (φ \land y \in M) \to \exists h \in (II Cn K) (h (0) = O \land h (1) = X \land (ι a \in (II Cn C) \| (F \circ a = G \circ h \land a (0) = P)) (1) = H (X))$
67	16	adantr	$⊢ (φ \land y \in M) \to K ↾_{𝑡} M \in PConn$
68	2	restuni	$⊢ (K \in Top \land M \subseteq Y) \to M = ⋃ (K ↾_{𝑡} M)$
69	24 31 68	syl2anc	$⊢ φ \to M = ⋃ (K ↾_{𝑡} M)$
70	32 69	eleqtrd	$⊢ φ \to X \in ⋃ (K ↾_{𝑡} M)$
71	70	adantr	$⊢ (φ \land y \in M) \to X \in ⋃ (K ↾_{𝑡} M)$
72	69	eleq2d	$⊢ φ \to (y \in M \leftrightarrow y \in ⋃ (K ↾_{𝑡} M))$
73	72	biimpa	$⊢ (φ \land y \in M) \to y \in ⋃ (K ↾_{𝑡} M)$
74		eqid	$⊢ ⋃ (K ↾_{𝑡} M) = ⋃ (K ↾_{𝑡} M)$
75	74	pconncn	$⊢ (K ↾_{𝑡} M \in PConn \land X \in ⋃ (K ↾_{𝑡} M) \land y \in ⋃ (K ↾_{𝑡} M)) \to \exists n \in (II Cn (K ↾_{𝑡} M)) (n (0) = X \land n (1) = y)$
76	67 71 73 75	syl3anc	$⊢ (φ \land y \in M) \to \exists n \in (II Cn (K ↾_{𝑡} M)) (n (0) = X \land n (1) = y)$
77		reeanv	$⊢ \exists h \in (II Cn K) \exists n \in (II Cn (K ↾_{𝑡} M)) ((h (0) = O \land h (1) = X \land (ι a \in (II Cn C) \| (F \circ a = G \circ h \land a (0) = P)) (1) = H (X)) \land (n (0) = X \land n (1) = y)) \leftrightarrow (\exists h \in (II Cn K) (h (0) = O \land h (1) = X \land (ι a \in (II Cn C) \| (F \circ a = G \circ h \land a (0) = P)) (1) = H (X)) \land \exists n \in (II Cn (K ↾_{𝑡} M)) (n (0) = X \land n (1) = y))$
78	3	ad3antrrr	$⊢ (((φ \land y \in M) \land (h \in (II Cn K) \land n \in (II Cn (K ↾_{𝑡} M)))) \land ((h (0) = O \land h (1) = X \land (ι a \in (II Cn C) \| (F \circ a = G \circ h \land a (0) = P)) (1) = H (X)) \land (n (0) = X \land n (1) = y))) \to F \in (C CovMap J)$
79	4	ad3antrrr	$⊢ (((φ \land y \in M) \land (h \in (II Cn K) \land n \in (II Cn (K ↾_{𝑡} M)))) \land ((h (0) = O \land h (1) = X \land (ι a \in (II Cn C) \| (F \circ a = G \circ h \land a (0) = P)) (1) = H (X)) \land (n (0) = X \land n (1) = y))) \to K \in SConn$
80	5	ad3antrrr	$⊢ (((φ \land y \in M) \land (h \in (II Cn K) \land n \in (II Cn (K ↾_{𝑡} M)))) \land ((h (0) = O \land h (1) = X \land (ι a \in (II Cn C) \| (F \circ a = G \circ h \land a (0) = P)) (1) = H (X)) \land (n (0) = X \land n (1) = y))) \to K \in N-LocallyPConn$
81	6	ad3antrrr	$⊢ (((φ \land y \in M) \land (h \in (II Cn K) \land n \in (II Cn (K ↾_{𝑡} M)))) \land ((h (0) = O \land h (1) = X \land (ι a \in (II Cn C) \| (F \circ a = G \circ h \land a (0) = P)) (1) = H (X)) \land (n (0) = X \land n (1) = y))) \to O \in Y$
82	7	ad3antrrr	$⊢ (((φ \land y \in M) \land (h \in (II Cn K) \land n \in (II Cn (K ↾_{𝑡} M)))) \land ((h (0) = O \land h (1) = X \land (ι a \in (II Cn C) \| (F \circ a = G \circ h \land a (0) = P)) (1) = H (X)) \land (n (0) = X \land n (1) = y))) \to G \in (K Cn J)$
83	8	ad3antrrr	$⊢ (((φ \land y \in M) \land (h \in (II Cn K) \land n \in (II Cn (K ↾_{𝑡} M)))) \land ((h (0) = O \land h (1) = X \land (ι a \in (II Cn C) \| (F \circ a = G \circ h \land a (0) = P)) (1) = H (X)) \land (n (0) = X \land n (1) = y))) \to P \in B$
84	9	ad3antrrr	$⊢ (((φ \land y \in M) \land (h \in (II Cn K) \land n \in (II Cn (K ↾_{𝑡} M)))) \land ((h (0) = O \land h (1) = X \land (ι a \in (II Cn C) \| (F \circ a = G \circ h \land a (0) = P)) (1) = H (X)) \land (n (0) = X \land n (1) = y))) \to F (P) = G (O)$
85	12	ad3antrrr	$⊢ (((φ \land y \in M) \land (h \in (II Cn K) \land n \in (II Cn (K ↾_{𝑡} M)))) \land ((h (0) = O \land h (1) = X \land (ι a \in (II Cn C) \| (F \circ a = G \circ h \land a (0) = P)) (1) = H (X)) \land (n (0) = X \land n (1) = y))) \to G (X) \in A$
86	13	ad3antrrr	$⊢ (((φ \land y \in M) \land (h \in (II Cn K) \land n \in (II Cn (K ↾_{𝑡} M)))) \land ((h (0) = O \land h (1) = X \land (ι a \in (II Cn C) \| (F \circ a = G \circ h \land a (0) = P)) (1) = H (X)) \land (n (0) = X \land n (1) = y))) \to T \in S (A)$
87	14	ad3antrrr	$⊢ (((φ \land y \in M) \land (h \in (II Cn K) \land n \in (II Cn (K ↾_{𝑡} M)))) \land ((h (0) = O \land h (1) = X \land (ι a \in (II Cn C) \| (F \circ a = G \circ h \land a (0) = P)) (1) = H (X)) \land (n (0) = X \land n (1) = y))) \to M \subseteq G^{-1} [A]$
88	32	ad3antrrr	$⊢ (((φ \land y \in M) \land (h \in (II Cn K) \land n \in (II Cn (K ↾_{𝑡} M)))) \land ((h (0) = O \land h (1) = X \land (ι a \in (II Cn C) \| (F \circ a = G \circ h \land a (0) = P)) (1) = H (X)) \land (n (0) = X \land n (1) = y))) \to X \in M$
89		simpllr	$⊢ (((φ \land y \in M) \land (h \in (II Cn K) \land n \in (II Cn (K ↾_{𝑡} M)))) \land ((h (0) = O \land h (1) = X \land (ι a \in (II Cn C) \| (F \circ a = G \circ h \land a (0) = P)) (1) = H (X)) \land (n (0) = X \land n (1) = y))) \to y \in M$
90		simplrl	$⊢ (((φ \land y \in M) \land (h \in (II Cn K) \land n \in (II Cn (K ↾_{𝑡} M)))) \land ((h (0) = O \land h (1) = X \land (ι a \in (II Cn C) \| (F \circ a = G \circ h \land a (0) = P)) (1) = H (X)) \land (n (0) = X \land n (1) = y))) \to h \in (II Cn K)$
91		simprl	$⊢ (((φ \land y \in M) \land (h \in (II Cn K) \land n \in (II Cn (K ↾_{𝑡} M)))) \land ((h (0) = O \land h (1) = X \land (ι a \in (II Cn C) \| (F \circ a = G \circ h \land a (0) = P)) (1) = H (X)) \land (n (0) = X \land n (1) = y))) \to (h (0) = O \land h (1) = X \land (ι a \in (II Cn C) \| (F \circ a = G \circ h \land a (0) = P)) (1) = H (X))$
92		simplrr	$⊢ (((φ \land y \in M) \land (h \in (II Cn K) \land n \in (II Cn (K ↾_{𝑡} M)))) \land ((h (0) = O \land h (1) = X \land (ι a \in (II Cn C) \| (F \circ a = G \circ h \land a (0) = P)) (1) = H (X)) \land (n (0) = X \land n (1) = y))) \to n \in (II Cn (K ↾_{𝑡} M))$
93		simprr	$⊢ (((φ \land y \in M) \land (h \in (II Cn K) \land n \in (II Cn (K ↾_{𝑡} M)))) \land ((h (0) = O \land h (1) = X \land (ι a \in (II Cn C) \| (F \circ a = G \circ h \land a (0) = P)) (1) = H (X)) \land (n (0) = X \land n (1) = y))) \to (n (0) = X \land n (1) = y)$
94	55	eqeq1d	$⊢ a = g \to (F \circ a = G \circ n \leftrightarrow F \circ g = G \circ n)$
95	57	eqeq1d	$⊢ a = g \to (a (0) = H (X) \leftrightarrow g (0) = H (X))$
96	94 95	anbi12d	$⊢ a = g \to ((F \circ a = G \circ n \land a (0) = H (X)) \leftrightarrow (F \circ g = G \circ n \land g (0) = H (X)))$
97	96	cbvriotavw	$⊢ (ι a \in (II Cn C) \| (F \circ a = G \circ n \land a (0) = H (X))) = (ι g \in (II Cn C) \| (F \circ g = G \circ n \land g (0) = H (X)))$
98	1 2 78 79 80 81 82 83 84 10 11 85 86 87 15 88 89 90 60 91 92 93 97	cvmlift3lem6	$⊢ (((φ \land y \in M) \land (h \in (II Cn K) \land n \in (II Cn (K ↾_{𝑡} M)))) \land ((h (0) = O \land h (1) = X \land (ι a \in (II Cn C) \| (F \circ a = G \circ h \land a (0) = P)) (1) = H (X)) \land (n (0) = X \land n (1) = y))) \to H (y) \in W$
99	98	ex	$⊢ ((φ \land y \in M) \land (h \in (II Cn K) \land n \in (II Cn (K ↾_{𝑡} M)))) \to (((h (0) = O \land h (1) = X \land (ι a \in (II Cn C) \| (F \circ a = G \circ h \land a (0) = P)) (1) = H (X)) \land (n (0) = X \land n (1) = y)) \to H (y) \in W)$
100	99	rexlimdvva	$⊢ (φ \land y \in M) \to (\exists h \in (II Cn K) \exists n \in (II Cn (K ↾_{𝑡} M)) ((h (0) = O \land h (1) = X \land (ι a \in (II Cn C) \| (F \circ a = G \circ h \land a (0) = P)) (1) = H (X)) \land (n (0) = X \land n (1) = y)) \to H (y) \in W)$
101	77 100	syl5bir	$⊢ (φ \land y \in M) \to ((\exists h \in (II Cn K) (h (0) = O \land h (1) = X \land (ι a \in (II Cn C) \| (F \circ a = G \circ h \land a (0) = P)) (1) = H (X)) \land \exists n \in (II Cn (K ↾_{𝑡} M)) (n (0) = X \land n (1) = y)) \to H (y) \in W)$
102	66 76 101	mp2and	$⊢ (φ \land y \in M) \to H (y) \in W$
103	102	ralrimiva	$⊢ φ \to \forall y \in M H (y) \in W$
104	20	ffund	$⊢ φ \to Fun H$
105	20	fdmd	$⊢ φ \to dom H = Y$
106	31 105	sseqtrrd	$⊢ φ \to M \subseteq dom H$
107		funimass4	$⊢ (Fun H \land M \subseteq dom H) \to (H [M] \subseteq W \leftrightarrow \forall y \in M H (y) \in W)$
108	104 106 107	syl2anc	$⊢ φ \to (H [M] \subseteq W \leftrightarrow \forall y \in M H (y) \in W)$
109	103 108	mpbird	$⊢ φ \to H [M] \subseteq W$
110	1 2 11 3 20 22 24 33 13 41 31 109	cvmlift2lem9a	$⊢ φ \to {H ↾}_{M} \in ((K ↾_{𝑡} M) Cn C)$
111	74	cncnpi	$⊢ ({H ↾}_{M} \in ((K ↾_{𝑡} M) Cn C) \land X \in ⋃ (K ↾_{𝑡} M)) \to {H ↾}_{M} \in ((K ↾_{𝑡} M) CnP C) (X)$
112	110 70 111	syl2anc	$⊢ φ \to {H ↾}_{M} \in ((K ↾_{𝑡} M) CnP C) (X)$
113	2	ssntr	$⊢ ((K \in Top \land M \subseteq Y) \land (V \in K \land V \subseteq M)) \to V \subseteq int (K) (M)$
114	24 31 17 18 113	syl22anc	$⊢ φ \to V \subseteq int (K) (M)$
115	114 19	sseldd	$⊢ φ \to X \in int (K) (M)$
116	2 1	cnprest	$⊢ ((K \in Top \land M \subseteq Y) \land (X \in int (K) (M) \land H : Y ⟶ B)) \to (H \in (K CnP C) (X) \leftrightarrow {H ↾}_{M} \in ((K ↾_{𝑡} M) CnP C) (X))$
117	24 31 115 20 116	syl22anc	$⊢ φ \to (H \in (K CnP C) (X) \leftrightarrow {H ↾}_{M} \in ((K ↾_{𝑡} M) CnP C) (X))$
118	112 117	mpbird	$⊢ φ \to H \in (K CnP C) (X)$

Metamath Proof Explorer

Theorem cvmlift3lem7

Proof