cvmlift3lem8

	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	cvmlift3lem8	$⊢ φ \to H \in (K Cn C)$

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	cvmlift3lem3	$⊢ φ \to H : Y ⟶ B$
13	3	adantr	$⊢ (φ \land y \in Y) \to F \in (C CovMap J)$
14		eqid	$⊢ ⋃ J = ⋃ J$
15	2 14	cnf	$⊢ G \in (K Cn J) \to G : Y ⟶ ⋃ J$
16	7 15	syl	$⊢ φ \to G : Y ⟶ ⋃ J$
17	16	ffvelcdmda	$⊢ (φ \land y \in Y) \to G (y) \in ⋃ J$
18	11 14	cvmcov	$⊢ (F \in (C CovMap J) \land G (y) \in ⋃ J) \to \exists a \in J (G (y) \in a \land S (a) \neq \emptyset)$
19	13 17 18	syl2anc	$⊢ (φ \land y \in Y) \to \exists a \in J (G (y) \in a \land S (a) \neq \emptyset)$
20		n0	$⊢ S (a) \neq \emptyset \leftrightarrow \exists t t \in S (a)$
21	5	ad2antrr	$⊢ ((φ \land y \in Y) \land (G (y) \in a \land t \in S (a))) \to K \in N-LocallyPConn$
22	7	ad2antrr	$⊢ ((φ \land y \in Y) \land (G (y) \in a \land t \in S (a))) \to G \in (K Cn J)$
23		simprr	$⊢ ((φ \land y \in Y) \land (G (y) \in a \land t \in S (a))) \to t \in S (a)$
24	11	cvmsrcl	$⊢ t \in S (a) \to a \in J$
25	23 24	syl	$⊢ ((φ \land y \in Y) \land (G (y) \in a \land t \in S (a))) \to a \in J$
26		cnima	$⊢ (G \in (K Cn J) \land a \in J) \to G^{-1} [a] \in K$
27	22 25 26	syl2anc	$⊢ ((φ \land y \in Y) \land (G (y) \in a \land t \in S (a))) \to G^{-1} [a] \in K$
28		simplr	$⊢ ((φ \land y \in Y) \land (G (y) \in a \land t \in S (a))) \to y \in Y$
29		simprl	$⊢ ((φ \land y \in Y) \land (G (y) \in a \land t \in S (a))) \to G (y) \in a$
30		ffn	$⊢ G : Y ⟶ ⋃ J \to G Fn Y$
31		elpreima	$⊢ G Fn Y \to (y \in G^{-1} [a] \leftrightarrow (y \in Y \land G (y) \in a))$
32	22 15 30 31	4syl	$⊢ ((φ \land y \in Y) \land (G (y) \in a \land t \in S (a))) \to (y \in G^{-1} [a] \leftrightarrow (y \in Y \land G (y) \in a))$
33	28 29 32	mpbir2and	$⊢ ((φ \land y \in Y) \land (G (y) \in a \land t \in S (a))) \to y \in G^{-1} [a]$
34		nlly2i	$⊢ (K \in N-LocallyPConn\landG^{-1} [a] \in K\landy \in G^{-1} [a]\to\exists m \in 𝒫 G^{-1} [a] \exists v \in K (y \in v \land v \subseteq m \land K ↾_{𝑡} m \in PConn))$
35	21 27 33 34	syl3anc	$⊢ ((φ \land y \in Y) \land (G (y) \in a \land t \in S (a))) \to \exists m \in 𝒫 G^{-1} [a] \exists v \in K (y \in v \land v \subseteq m \land K ↾_{𝑡} m \in PConn)$
36	3	ad3antrrr	$⊢ (((φ \land y \in Y) \land (G (y) \in a \land t \in S (a))) \land ((m \in 𝒫 G^{-1} [a] \land v \in K) \land (y \in v \land v \subseteq m \land K ↾_{𝑡} m \in PConn))) \to F \in (C CovMap J)$
37	4	ad3antrrr	$⊢ (((φ \land y \in Y) \land (G (y) \in a \land t \in S (a))) \land ((m \in 𝒫 G^{-1} [a] \land v \in K) \land (y \in v \land v \subseteq m \land K ↾_{𝑡} m \in PConn))) \to K \in SConn$
38	5	ad3antrrr	$⊢ (((φ \land y \in Y) \land (G (y) \in a \land t \in S (a))) \land ((m \in 𝒫 G^{-1} [a] \land v \in K) \land (y \in v \land v \subseteq m \land K ↾_{𝑡} m \in PConn))) \to K \in N-LocallyPConn$
39	6	ad3antrrr	$⊢ (((φ \land y \in Y) \land (G (y) \in a \land t \in S (a))) \land ((m \in 𝒫 G^{-1} [a] \land v \in K) \land (y \in v \land v \subseteq m \land K ↾_{𝑡} m \in PConn))) \to O \in Y$
40	7	ad3antrrr	$⊢ (((φ \land y \in Y) \land (G (y) \in a \land t \in S (a))) \land ((m \in 𝒫 G^{-1} [a] \land v \in K) \land (y \in v \land v \subseteq m \land K ↾_{𝑡} m \in PConn))) \to G \in (K Cn J)$
41	8	ad3antrrr	$⊢ (((φ \land y \in Y) \land (G (y) \in a \land t \in S (a))) \land ((m \in 𝒫 G^{-1} [a] \land v \in K) \land (y \in v \land v \subseteq m \land K ↾_{𝑡} m \in PConn))) \to P \in B$
42	9	ad3antrrr	$⊢ (((φ \land y \in Y) \land (G (y) \in a \land t \in S (a))) \land ((m \in 𝒫 G^{-1} [a] \land v \in K) \land (y \in v \land v \subseteq m \land K ↾_{𝑡} m \in PConn))) \to F (P) = G (O)$
43	29	adantr	$⊢ (((φ \land y \in Y) \land (G (y) \in a \land t \in S (a))) \land ((m \in 𝒫 G^{-1} [a] \land v \in K) \land (y \in v \land v \subseteq m \land K ↾_{𝑡} m \in PConn))) \to G (y) \in a$
44	23	adantr	$⊢ (((φ \land y \in Y) \land (G (y) \in a \land t \in S (a))) \land ((m \in 𝒫 G^{-1} [a] \land v \in K) \land (y \in v \land v \subseteq m \land K ↾_{𝑡} m \in PConn))) \to t \in S (a)$
45		simprll	$⊢ (((φ \land y \in Y) \land (G (y) \in a \land t \in S (a))) \land ((m \in 𝒫 G^{-1} [a] \land v \in K) \land (y \in v \land v \subseteq m \land K ↾_{𝑡} m \in PConn))) \to m \in 𝒫 G^{-1} [a]$
46	45	elpwid	$⊢ (((φ \land y \in Y) \land (G (y) \in a \land t \in S (a))) \land ((m \in 𝒫 G^{-1} [a] \land v \in K) \land (y \in v \land v \subseteq m \land K ↾_{𝑡} m \in PConn))) \to m \subseteq G^{-1} [a]$
47		eqid	$⊢ (ι b \in t \| H (y) \in b) = (ι b \in t \| H (y) \in b)$
48		simprr3	$⊢ (((φ \land y \in Y) \land (G (y) \in a \land t \in S (a))) \land ((m \in 𝒫 G^{-1} [a] \land v \in K) \land (y \in v \land v \subseteq m \land K ↾_{𝑡} m \in PConn))) \to K ↾_{𝑡} m \in PConn$
49		simprlr	$⊢ (((φ \land y \in Y) \land (G (y) \in a \land t \in S (a))) \land ((m \in 𝒫 G^{-1} [a] \land v \in K) \land (y \in v \land v \subseteq m \land K ↾_{𝑡} m \in PConn))) \to v \in K$
50		simprr2	$⊢ (((φ \land y \in Y) \land (G (y) \in a \land t \in S (a))) \land ((m \in 𝒫 G^{-1} [a] \land v \in K) \land (y \in v \land v \subseteq m \land K ↾_{𝑡} m \in PConn))) \to v \subseteq m$
51		simprr1	$⊢ (((φ \land y \in Y) \land (G (y) \in a \land t \in S (a))) \land ((m \in 𝒫 G^{-1} [a] \land v \in K) \land (y \in v \land v \subseteq m \land K ↾_{𝑡} m \in PConn))) \to y \in v$
52	1 2 36 37 38 39 40 41 42 10 11 43 44 46 47 48 49 50 51	cvmlift3lem7	$⊢ (((φ \land y \in Y) \land (G (y) \in a \land t \in S (a))) \land ((m \in 𝒫 G^{-1} [a] \land v \in K) \land (y \in v \land v \subseteq m \land K ↾_{𝑡} m \in PConn))) \to H \in (K CnP C) (y)$
53	52	expr	$⊢ (((φ \land y \in Y) \land (G (y) \in a \land t \in S (a))) \land (m \in 𝒫 G^{-1} [a] \land v \in K)) \to ((y \in v \land v \subseteq m \land K ↾_{𝑡} m \in PConn) \to H \in (K CnP C) (y))$
54	53	rexlimdvva	$⊢ ((φ \land y \in Y) \land (G (y) \in a \land t \in S (a))) \to (\exists m \in 𝒫 G^{-1} [a] \exists v \in K (y \in v \land v \subseteq m \land K ↾_{𝑡} m \in PConn) \to H \in (K CnP C) (y))$
55	35 54	mpd	$⊢ ((φ \land y \in Y) \land (G (y) \in a \land t \in S (a))) \to H \in (K CnP C) (y)$
56	55	expr	$⊢ ((φ \land y \in Y) \land G (y) \in a) \to (t \in S (a) \to H \in (K CnP C) (y))$
57	56	exlimdv	$⊢ ((φ \land y \in Y) \land G (y) \in a) \to (\exists t t \in S (a) \to H \in (K CnP C) (y))$
58	20 57	biimtrid	$⊢ ((φ \land y \in Y) \land G (y) \in a) \to (S (a) \neq \emptyset \to H \in (K CnP C) (y))$
59	58	expimpd	$⊢ (φ \land y \in Y) \to ((G (y) \in a \land S (a) \neq \emptyset) \to H \in (K CnP C) (y))$
60	59	rexlimdvw	$⊢ (φ \land y \in Y) \to (\exists a \in J (G (y) \in a \land S (a) \neq \emptyset) \to H \in (K CnP C) (y))$
61	19 60	mpd	$⊢ (φ \land y \in Y) \to H \in (K CnP C) (y)$
62	61	ralrimiva	$⊢ φ \to \forall y \in Y H \in (K CnP C) (y)$
63		sconntop	$⊢ K \in SConn \to K \in Top$
64	4 63	syl	$⊢ φ \to K \in Top$
65	2	toptopon	$⊢ K \in Top \leftrightarrow K \in TopOn (Y)$
66	64 65	sylib	$⊢ φ \to K \in TopOn (Y)$
67		cvmtop1	$⊢ F \in (C CovMap J) \to C \in Top$
68	3 67	syl	$⊢ φ \to C \in Top$
69	1	toptopon	$⊢ C \in Top \leftrightarrow C \in TopOn (B)$
70	68 69	sylib	$⊢ φ \to C \in TopOn (B)$
71		cncnp	$⊢ (K \in TopOn (Y) \land C \in TopOn (B)) \to (H \in (K Cn C) \leftrightarrow (H : Y ⟶ B \land \forall y \in Y H \in (K CnP C) (y)))$
72	66 70 71	syl2anc	$⊢ φ \to (H \in (K Cn C) \leftrightarrow (H : Y ⟶ B \land \forall y \in Y H \in (K CnP C) (y)))$
73	12 62 72	mpbir2and	$⊢ φ \to H \in (K Cn C)$

Metamath Proof Explorer

Theorem cvmlift3lem8

Proof