cvmlift3lem9

	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))))\})$
Assertion	cvmlift3lem9	$⊢ φ \to \exists f \in (K Cn C) (F \circ f = G \land f (O) = P)$

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	1 2 3 4 5 6 7 8 9 10 11	cvmlift3lem8	$⊢ φ \to H \in (K Cn C)$
13	1 2 3 4 5 6 7 8 9 10	cvmlift3lem5	$⊢ φ \to F \circ H = G$
14		iitopon	$⊢ II \in TopOn ([0, 1])$
15	14	a1i	$⊢ φ \to II \in TopOn ([0, 1])$
16		sconntop	$⊢ K \in SConn \to K \in Top$
17	4 16	syl	$⊢ φ \to K \in Top$
18	2	toptopon	$⊢ K \in Top \leftrightarrow K \in TopOn (Y)$
19	17 18	sylib	$⊢ φ \to K \in TopOn (Y)$
20		cnconst2	$⊢ (II \in TopOn ([0, 1]) \land K \in TopOn (Y) \land O \in Y) \to [0, 1] \times \{O\} \in (II Cn K)$
21	15 19 6 20	syl3anc	$⊢ φ \to [0, 1] \times \{O\} \in (II Cn K)$
22		0elunit	$⊢ 0 \in [0, 1]$
23		fvconst2g	$⊢ (O \in Y \land 0 \in [0, 1]) \to ([0, 1] \times \{O\}) (0) = O$
24	6 22 23	sylancl	$⊢ φ \to ([0, 1] \times \{O\}) (0) = O$
25		1elunit	$⊢ 1 \in [0, 1]$
26		fvconst2g	$⊢ (O \in Y \land 1 \in [0, 1]) \to ([0, 1] \times \{O\}) (1) = O$
27	6 25 26	sylancl	$⊢ φ \to ([0, 1] \times \{O\}) (1) = O$
28	9	sneqd	$⊢ φ \to \{F (P)\} = \{G (O)\}$
29	28	xpeq2d	$⊢ φ \to [0, 1] \times \{F (P)\} = [0, 1] \times \{G (O)\}$
30		cvmcn	$⊢ F \in (C CovMap J) \to F \in (C Cn J)$
31		eqid	$⊢ ⋃ J = ⋃ J$
32	1 31	cnf	$⊢ F \in (C Cn J) \to F : B ⟶ ⋃ J$
33		ffn	$⊢ F : B ⟶ ⋃ J \to F Fn B$
34	3 30 32 33	4syl	$⊢ φ \to F Fn B$
35		fcoconst	$⊢ (F Fn B \land P \in B) \to F \circ ([0, 1] \times \{P\}) = [0, 1] \times \{F (P)\}$
36	34 8 35	syl2anc	$⊢ φ \to F \circ ([0, 1] \times \{P\}) = [0, 1] \times \{F (P)\}$
37	2 31	cnf	$⊢ G \in (K Cn J) \to G : Y ⟶ ⋃ J$
38	7 37	syl	$⊢ φ \to G : Y ⟶ ⋃ J$
39	38	ffnd	$⊢ φ \to G Fn Y$
40		fcoconst	$⊢ (G Fn Y \land O \in Y) \to G \circ ([0, 1] \times \{O\}) = [0, 1] \times \{G (O)\}$
41	39 6 40	syl2anc	$⊢ φ \to G \circ ([0, 1] \times \{O\}) = [0, 1] \times \{G (O)\}$
42	29 36 41	3eqtr4d	$⊢ φ \to F \circ ([0, 1] \times \{P\}) = G \circ ([0, 1] \times \{O\})$
43		fvconst2g	$⊢ (P \in B \land 0 \in [0, 1]) \to ([0, 1] \times \{P\}) (0) = P$
44	8 22 43	sylancl	$⊢ φ \to ([0, 1] \times \{P\}) (0) = P$
45		cvmtop1	$⊢ F \in (C CovMap J) \to C \in Top$
46	3 45	syl	$⊢ φ \to C \in Top$
47	1	toptopon	$⊢ C \in Top \leftrightarrow C \in TopOn (B)$
48	46 47	sylib	$⊢ φ \to C \in TopOn (B)$
49		cnconst2	$⊢ (II \in TopOn ([0, 1]) \land C \in TopOn (B) \land P \in B) \to [0, 1] \times \{P\} \in (II Cn C)$
50	15 48 8 49	syl3anc	$⊢ φ \to [0, 1] \times \{P\} \in (II Cn C)$
51		cvmtop2	$⊢ F \in (C CovMap J) \to J \in Top$
52	3 51	syl	$⊢ φ \to J \in Top$
53	31	toptopon	$⊢ J \in Top \leftrightarrow J \in TopOn (⋃ J)$
54	52 53	sylib	$⊢ φ \to J \in TopOn (⋃ J)$
55	38 6	ffvelcdmd	$⊢ φ \to G (O) \in ⋃ J$
56		cnconst2	$⊢ (II \in TopOn ([0, 1]) \land J \in TopOn (⋃ J) \land G (O) \in ⋃ J) \to [0, 1] \times \{G (O)\} \in (II Cn J)$
57	15 54 55 56	syl3anc	$⊢ φ \to [0, 1] \times \{G (O)\} \in (II Cn J)$
58	41 57	eqeltrd	$⊢ φ \to G \circ ([0, 1] \times \{O\}) \in (II Cn J)$
59		fvconst2g	$⊢ (G (O) \in ⋃ J \land 0 \in [0, 1]) \to ([0, 1] \times \{G (O)\}) (0) = G (O)$
60	55 22 59	sylancl	$⊢ φ \to ([0, 1] \times \{G (O)\}) (0) = G (O)$
61	41	fveq1d	$⊢ φ \to (G \circ ([0, 1] \times \{O\})) (0) = ([0, 1] \times \{G (O)\}) (0)$
62	60 61 9	3eqtr4rd	$⊢ φ \to F (P) = (G \circ ([0, 1] \times \{O\})) (0)$
63	1	cvmlift	$⊢ ((F \in (C CovMap J) \land G \circ ([0, 1] \times \{O\}) \in (II Cn J)) \land (P \in B \land F (P) = (G \circ ([0, 1] \times \{O\})) (0))) \to \exists! g \in (II Cn C) (F \circ g = G \circ ([0, 1] \times \{O\}) \land g (0) = P)$
64	3 58 8 62 63	syl22anc	$⊢ φ \to \exists! g \in (II Cn C) (F \circ g = G \circ ([0, 1] \times \{O\}) \land g (0) = P)$
65		coeq2	$⊢ g = [0, 1] \times \{P\} \to F \circ g = F \circ ([0, 1] \times \{P\})$
66	65	eqeq1d	$⊢ g = [0, 1] \times \{P\} \to (F \circ g = G \circ ([0, 1] \times \{O\}) \leftrightarrow F \circ ([0, 1] \times \{P\}) = G \circ ([0, 1] \times \{O\}))$
67		fveq1	$⊢ g = [0, 1] \times \{P\} \to g (0) = ([0, 1] \times \{P\}) (0)$
68	67	eqeq1d	$⊢ g = [0, 1] \times \{P\} \to (g (0) = P \leftrightarrow ([0, 1] \times \{P\}) (0) = P)$
69	66 68	anbi12d	$⊢ g = [0, 1] \times \{P\} \to ((F \circ g = G \circ ([0, 1] \times \{O\}) \land g (0) = P) \leftrightarrow (F \circ ([0, 1] \times \{P\}) = G \circ ([0, 1] \times \{O\}) \land ([0, 1] \times \{P\}) (0) = P))$
70	69	riota2	$⊢ ([0, 1] \times \{P\} \in (II Cn C) \land \exists! g \in (II Cn C) (F \circ g = G \circ ([0, 1] \times \{O\}) \land g (0) = P)) \to ((F \circ ([0, 1] \times \{P\}) = G \circ ([0, 1] \times \{O\}) \land ([0, 1] \times \{P\}) (0) = P) \leftrightarrow (ι g \in (II Cn C) \| (F \circ g = G \circ ([0, 1] \times \{O\}) \land g (0) = P)) = [0, 1] \times \{P\})$
71	50 64 70	syl2anc	$⊢ φ \to ((F \circ ([0, 1] \times \{P\}) = G \circ ([0, 1] \times \{O\}) \land ([0, 1] \times \{P\}) (0) = P) \leftrightarrow (ι g \in (II Cn C) \| (F \circ g = G \circ ([0, 1] \times \{O\}) \land g (0) = P)) = [0, 1] \times \{P\})$
72	42 44 71	mpbi2and	$⊢ φ \to (ι g \in (II Cn C) \| (F \circ g = G \circ ([0, 1] \times \{O\}) \land g (0) = P)) = [0, 1] \times \{P\}$
73	72	fveq1d	$⊢ φ \to (ι g \in (II Cn C) \| (F \circ g = G \circ ([0, 1] \times \{O\}) \land g (0) = P)) (1) = ([0, 1] \times \{P\}) (1)$
74		fvconst2g	$⊢ (P \in B \land 1 \in [0, 1]) \to ([0, 1] \times \{P\}) (1) = P$
75	8 25 74	sylancl	$⊢ φ \to ([0, 1] \times \{P\}) (1) = P$
76	73 75	eqtrd	$⊢ φ \to (ι g \in (II Cn C) \| (F \circ g = G \circ ([0, 1] \times \{O\}) \land g (0) = P)) (1) = P$
77		fveq1	$⊢ f = [0, 1] \times \{O\} \to f (0) = ([0, 1] \times \{O\}) (0)$
78	77	eqeq1d	$⊢ f = [0, 1] \times \{O\} \to (f (0) = O \leftrightarrow ([0, 1] \times \{O\}) (0) = O)$
79		fveq1	$⊢ f = [0, 1] \times \{O\} \to f (1) = ([0, 1] \times \{O\}) (1)$
80	79	eqeq1d	$⊢ f = [0, 1] \times \{O\} \to (f (1) = O \leftrightarrow ([0, 1] \times \{O\}) (1) = O)$
81		coeq2	$⊢ f = [0, 1] \times \{O\} \to G \circ f = G \circ ([0, 1] \times \{O\})$
82	81	eqeq2d	$⊢ f = [0, 1] \times \{O\} \to (F \circ g = G \circ f \leftrightarrow F \circ g = G \circ ([0, 1] \times \{O\}))$
83	82	anbi1d	$⊢ f = [0, 1] \times \{O\} \to ((F \circ g = G \circ f \land g (0) = P) \leftrightarrow (F \circ g = G \circ ([0, 1] \times \{O\}) \land g (0) = P))$
84	83	riotabidv	$⊢ f = [0, 1] \times \{O\} \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 ([0, 1] \times \{O\}) \land g (0) = P))$
85	84	fveq1d	$⊢ f = [0, 1] \times \{O\} \to (ι g \in (II Cn C) \| (F \circ g = G \circ f \land g (0) = P)) (1) = (ι g \in (II Cn C) \| (F \circ g = G \circ ([0, 1] \times \{O\}) \land g (0) = P)) (1)$
86	85	eqeq1d	$⊢ f = [0, 1] \times \{O\} \to ((ι g \in (II Cn C) \| (F \circ g = G \circ f \land g (0) = P)) (1) = P \leftrightarrow (ι g \in (II Cn C) \| (F \circ g = G \circ ([0, 1] \times \{O\}) \land g (0) = P)) (1) = P)$
87	78 80 86	3anbi123d	$⊢ f = [0, 1] \times \{O\} \to ((f (0) = O \land f (1) = O \land (ι g \in (II Cn C) \| (F \circ g = G \circ f \land g (0) = P)) (1) = P) \leftrightarrow (([0, 1] \times \{O\}) (0) = O \land ([0, 1] \times \{O\}) (1) = O \land (ι g \in (II Cn C) \| (F \circ g = G \circ ([0, 1] \times \{O\}) \land g (0) = P)) (1) = P))$
88	87	rspcev	$⊢ ([0, 1] \times \{O\} \in (II Cn K) \land (([0, 1] \times \{O\}) (0) = O \land ([0, 1] \times \{O\}) (1) = O \land (ι g \in (II Cn C) \| (F \circ g = G \circ ([0, 1] \times \{O\}) \land g (0) = P)) (1) = P)) \to \exists f \in (II Cn K) (f (0) = O \land f (1) = O \land (ι g \in (II Cn C) \| (F \circ g = G \circ f \land g (0) = P)) (1) = P)$
89	21 24 27 76 88	syl13anc	$⊢ φ \to \exists f \in (II Cn K) (f (0) = O \land f (1) = O \land (ι g \in (II Cn C) \| (F \circ g = G \circ f \land g (0) = P)) (1) = P)$
90	1 2 3 4 5 6 7 8 9 10	cvmlift3lem4	$⊢ (φ \land O \in Y) \to (H (O) = P \leftrightarrow \exists f \in (II Cn K) (f (0) = O \land f (1) = O \land (ι g \in (II Cn C) \| (F \circ g = G \circ f \land g (0) = P)) (1) = P))$
91	6 90	mpdan	$⊢ φ \to (H (O) = P \leftrightarrow \exists f \in (II Cn K) (f (0) = O \land f (1) = O \land (ι g \in (II Cn C) \| (F \circ g = G \circ f \land g (0) = P)) (1) = P))$
92	89 91	mpbird	$⊢ φ \to H (O) = P$
93		coeq2	$⊢ f = H \to F \circ f = F \circ H$
94	93	eqeq1d	$⊢ f = H \to (F \circ f = G \leftrightarrow F \circ H = G)$
95		fveq1	$⊢ f = H \to f (O) = H (O)$
96	95	eqeq1d	$⊢ f = H \to (f (O) = P \leftrightarrow H (O) = P)$
97	94 96	anbi12d	$⊢ f = H \to ((F \circ f = G \land f (O) = P) \leftrightarrow (F \circ H = G \land H (O) = P))$
98	97	rspcev	$⊢ (H \in (K Cn C) \land (F \circ H = G \land H (O) = P)) \to \exists f \in (K Cn C) (F \circ f = G \land f (O) = P)$
99	12 13 92 98	syl12anc	$⊢ φ \to \exists f \in (K Cn C) (F \circ f = G \land f (O) = P)$

Metamath Proof Explorer

Theorem cvmlift3lem9

Proof