cvmlift3lem4

	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)))$
Assertion	cvmlift3lem4	$⊢ (φ \land X \in Y) \to (H (X) = A \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) = A))$

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	1 2 3 4 5 6 7 8 9 10	cvmlift3lem3	$⊢ φ \to H : Y ⟶ B$
12	11	ffvelrnda	$⊢ (φ \land X \in Y) \to H (X) \in B$
13		eleq1	$⊢ H (X) = A \to (H (X) \in B \leftrightarrow A \in B)$
14	12 13	syl5ibcom	$⊢ (φ \land X \in Y) \to (H (X) = A \to A \in B)$
15		eqid	$⊢ (ι 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 f \land g (0) = P))$
16	3	ad2antrr	$⊢ ((φ \land X \in Y) \land (f \in (II Cn K) \land f (0) = O)) \to F \in (C CovMap J)$
17		simprl	$⊢ ((φ \land X \in Y) \land (f \in (II Cn K) \land f (0) = O)) \to f \in (II Cn K)$
18	7	ad2antrr	$⊢ ((φ \land X \in Y) \land (f \in (II Cn K) \land f (0) = O)) \to G \in (K Cn J)$
19		cnco	$⊢ (f \in (II Cn K) \land G \in (K Cn J)) \to G \circ f \in (II Cn J)$
20	17 18 19	syl2anc	$⊢ ((φ \land X \in Y) \land (f \in (II Cn K) \land f (0) = O)) \to G \circ f \in (II Cn J)$
21	8	ad2antrr	$⊢ ((φ \land X \in Y) \land (f \in (II Cn K) \land f (0) = O)) \to P \in B$
22		simprr	$⊢ ((φ \land X \in Y) \land (f \in (II Cn K) \land f (0) = O)) \to f (0) = O$
23	22	fveq2d	$⊢ ((φ \land X \in Y) \land (f \in (II Cn K) \land f (0) = O)) \to G (f (0)) = G (O)$
24		iiuni	$⊢ [0, 1] = ⋃ II$
25	24 2	cnf	$⊢ f \in (II Cn K) \to f : [0, 1] ⟶ Y$
26	17 25	syl	$⊢ ((φ \land X \in Y) \land (f \in (II Cn K) \land f (0) = O)) \to f : [0, 1] ⟶ Y$
27		0elunit	$⊢ 0 \in [0, 1]$
28		fvco3	$⊢ (f : [0, 1] ⟶ Y \land 0 \in [0, 1]) \to (G \circ f) (0) = G (f (0))$
29	26 27 28	sylancl	$⊢ ((φ \land X \in Y) \land (f \in (II Cn K) \land f (0) = O)) \to (G \circ f) (0) = G (f (0))$
30	9	ad2antrr	$⊢ ((φ \land X \in Y) \land (f \in (II Cn K) \land f (0) = O)) \to F (P) = G (O)$
31	23 29 30	3eqtr4rd	$⊢ ((φ \land X \in Y) \land (f \in (II Cn K) \land f (0) = O)) \to F (P) = (G \circ f) (0)$
32	1 15 16 20 21 31	cvmliftiota	$⊢ ((φ \land X \in Y) \land (f \in (II Cn K) \land f (0) = O)) \to ((ι g \in (II Cn C) \| (F \circ g = G \circ f \land g (0) = P)) \in (II Cn C) \land F \circ (ι g \in (II Cn C) \| (F \circ g = G \circ f \land g (0) = P)) = G \circ f \land (ι g \in (II Cn C) \| (F \circ g = G \circ f \land g (0) = P)) (0) = P)$
33	32	simp1d	$⊢ ((φ \land X \in Y) \land (f \in (II Cn K) \land f (0) = O)) \to (ι g \in (II Cn C) \| (F \circ g = G \circ f \land g (0) = P)) \in (II Cn C)$
34	24 1	cnf	$⊢ (ι g \in (II Cn C) \| (F \circ g = G \circ f \land g (0) = P)) \in (II Cn C) \to (ι g \in (II Cn C) \| (F \circ g = G \circ f \land g (0) = P)) : [0, 1] ⟶ B$
35	33 34	syl	$⊢ ((φ \land X \in Y) \land (f \in (II Cn K) \land f (0) = O)) \to (ι g \in (II Cn C) \| (F \circ g = G \circ f \land g (0) = P)) : [0, 1] ⟶ B$
36		1elunit	$⊢ 1 \in [0, 1]$
37		ffvelrn	$⊢ ((ι g \in (II Cn C) \| (F \circ g = G \circ f \land g (0) = P)) : [0, 1] ⟶ B \land 1 \in [0, 1]) \to (ι g \in (II Cn C) \| (F \circ g = G \circ f \land g (0) = P)) (1) \in B$
38	35 36 37	sylancl	$⊢ ((φ \land X \in Y) \land (f \in (II Cn K) \land f (0) = O)) \to (ι g \in (II Cn C) \| (F \circ g = G \circ f \land g (0) = P)) (1) \in B$
39		eleq1	$⊢ (ι g \in (II Cn C) \| (F \circ g = G \circ f \land g (0) = P)) (1) = A \to ((ι g \in (II Cn C) \| (F \circ g = G \circ f \land g (0) = P)) (1) \in B \leftrightarrow A \in B)$
40	38 39	syl5ibcom	$⊢ ((φ \land X \in Y) \land (f \in (II Cn K) \land f (0) = O)) \to ((ι g \in (II Cn C) \| (F \circ g = G \circ f \land g (0) = P)) (1) = A \to A \in B)$
41	40	expr	$⊢ ((φ \land X \in Y) \land f \in (II Cn K)) \to (f (0) = O \to ((ι g \in (II Cn C) \| (F \circ g = G \circ f \land g (0) = P)) (1) = A \to A \in B))$
42	41	a1dd	$⊢ ((φ \land X \in Y) \land f \in (II Cn K)) \to (f (0) = O \to (f (1) = X \to ((ι g \in (II Cn C) \| (F \circ g = G \circ f \land g (0) = P)) (1) = A \to A \in B)))$
43	42	3impd	$⊢ ((φ \land X \in Y) \land f \in (II Cn K)) \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) = A) \to A \in B)$
44	43	rexlimdva	$⊢ (φ \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) = A) \to A \in B)$
45		eqeq2	$⊢ x = X \to (f (1) = x \leftrightarrow f (1) = X)$
46	45	3anbi2d	$⊢ x = X \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) = z) \leftrightarrow (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))$
47	46	rexbidv	$⊢ x = X \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) = z) \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) = z))$
48	47	riotabidv	$⊢ x = X \to (ι 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)) = (ι 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))$
49		riotaex	$⊢ (ι 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)) \in V$
50	48 10 49	fvmpt	$⊢ X \in Y \to H (X) = (ι 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))$
51	50	adantl	$⊢ (φ \land X \in Y) \to H (X) = (ι 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))$
52	51	eqeq1d	$⊢ (φ \land X \in Y) \to (H (X) = A \leftrightarrow (ι 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)) = A)$
53	52	adantl	$⊢ (A \in B \land (φ \land X \in Y)) \to (H (X) = A \leftrightarrow (ι 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)) = A)$
54	1 2 3 4 5 6 7 8 9	cvmlift3lem2	$⊢ (φ \land X \in Y) \to \exists! 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)$
55		eqeq2	$⊢ z = A \to ((ι g \in (II Cn C) \| (F \circ g = G \circ f \land g (0) = P)) (1) = z \leftrightarrow (ι g \in (II Cn C) \| (F \circ g = G \circ f \land g (0) = P)) (1) = A)$
56	55	3anbi3d	$⊢ z = A \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) = z) \leftrightarrow (f (0) = O \land f (1) = X \land (ι g \in (II Cn C) \| (F \circ g = G \circ f \land g (0) = P)) (1) = A))$
57	56	rexbidv	$⊢ z = A \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) = z) \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) = A))$
58	57	riota2	$⊢ (A \in B \land \exists! 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)) \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) = A) \leftrightarrow (ι 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)) = A)$
59	54 58	sylan2	$⊢ (A \in B \land (φ \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) = A) \leftrightarrow (ι 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)) = A)$
60	53 59	bitr4d	$⊢ (A \in B \land (φ \land X \in Y)) \to (H (X) = A \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) = A))$
61	60	expcom	$⊢ (φ \land X \in Y) \to (A \in B \to (H (X) = A \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) = A)))$
62	14 44 61	pm5.21ndd	$⊢ (φ \land X \in Y) \to (H (X) = A \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) = A))$

Metamath Proof Explorer

Theorem cvmlift3lem4

Proof