cvmlift3lem2

	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)$
Assertion	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)$

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	4	adantr	$⊢ (φ \land X \in Y) \to K \in SConn$
11		sconnpconn	$⊢ K \in SConn \to K \in PConn$
12	10 11	syl	$⊢ (φ \land X \in Y) \to K \in PConn$
13	6	adantr	$⊢ (φ \land X \in Y) \to O \in Y$
14		simpr	$⊢ (φ \land X \in Y) \to X \in Y$
15	2	pconncn	$⊢ (K \in PConn \land O \in Y \land X \in Y) \to \exists a \in (II Cn K) (a (0) = O \land a (1) = X)$
16	12 13 14 15	syl3anc	$⊢ (φ \land X \in Y) \to \exists a \in (II Cn K) (a (0) = O \land a (1) = X)$
17		eqid	$⊢ (ι g \in (II Cn C) \| (F \circ g = G \circ a \land g (0) = P)) = (ι g \in (II Cn C) \| (F \circ g = G \circ a \land g (0) = P))$
18	3	ad2antrr	$⊢ ((φ \land X \in Y) \land (a \in (II Cn K) \land (a (0) = O \land a (1) = X))) \to F \in (C CovMap J)$
19		simprl	$⊢ ((φ \land X \in Y) \land (a \in (II Cn K) \land (a (0) = O \land a (1) = X))) \to a \in (II Cn K)$
20	7	ad2antrr	$⊢ ((φ \land X \in Y) \land (a \in (II Cn K) \land (a (0) = O \land a (1) = X))) \to G \in (K Cn J)$
21		cnco	$⊢ (a \in (II Cn K) \land G \in (K Cn J)) \to G \circ a \in (II Cn J)$
22	19 20 21	syl2anc	$⊢ ((φ \land X \in Y) \land (a \in (II Cn K) \land (a (0) = O \land a (1) = X))) \to G \circ a \in (II Cn J)$
23	8	ad2antrr	$⊢ ((φ \land X \in Y) \land (a \in (II Cn K) \land (a (0) = O \land a (1) = X))) \to P \in B$
24		simprrl	$⊢ ((φ \land X \in Y) \land (a \in (II Cn K) \land (a (0) = O \land a (1) = X))) \to a (0) = O$
25	24	fveq2d	$⊢ ((φ \land X \in Y) \land (a \in (II Cn K) \land (a (0) = O \land a (1) = X))) \to G (a (0)) = G (O)$
26		iiuni	$⊢ [0, 1] = ⋃ II$
27	26 2	cnf	$⊢ a \in (II Cn K) \to a : [0, 1] ⟶ Y$
28	19 27	syl	$⊢ ((φ \land X \in Y) \land (a \in (II Cn K) \land (a (0) = O \land a (1) = X))) \to a : [0, 1] ⟶ Y$
29		0elunit	$⊢ 0 \in [0, 1]$
30		fvco3	$⊢ (a : [0, 1] ⟶ Y \land 0 \in [0, 1]) \to (G \circ a) (0) = G (a (0))$
31	28 29 30	sylancl	$⊢ ((φ \land X \in Y) \land (a \in (II Cn K) \land (a (0) = O \land a (1) = X))) \to (G \circ a) (0) = G (a (0))$
32	9	ad2antrr	$⊢ ((φ \land X \in Y) \land (a \in (II Cn K) \land (a (0) = O \land a (1) = X))) \to F (P) = G (O)$
33	25 31 32	3eqtr4rd	$⊢ ((φ \land X \in Y) \land (a \in (II Cn K) \land (a (0) = O \land a (1) = X))) \to F (P) = (G \circ a) (0)$
34	1 17 18 22 23 33	cvmliftiota	$⊢ ((φ \land X \in Y) \land (a \in (II Cn K) \land (a (0) = O \land a (1) = X))) \to ((ι g \in (II Cn C) \| (F \circ g = G \circ a \land g (0) = P)) \in (II Cn C) \land F \circ (ι g \in (II Cn C) \| (F \circ g = G \circ a \land g (0) = P)) = G \circ a \land (ι g \in (II Cn C) \| (F \circ g = G \circ a \land g (0) = P)) (0) = P)$
35	34	simp1d	$⊢ ((φ \land X \in Y) \land (a \in (II Cn K) \land (a (0) = O \land a (1) = X))) \to (ι g \in (II Cn C) \| (F \circ g = G \circ a \land g (0) = P)) \in (II Cn C)$
36	26 1	cnf	$⊢ (ι g \in (II Cn C) \| (F \circ g = G \circ a \land g (0) = P)) \in (II Cn C) \to (ι g \in (II Cn C) \| (F \circ g = G \circ a \land g (0) = P)) : [0, 1] ⟶ B$
37	35 36	syl	$⊢ ((φ \land X \in Y) \land (a \in (II Cn K) \land (a (0) = O \land a (1) = X))) \to (ι g \in (II Cn C) \| (F \circ g = G \circ a \land g (0) = P)) : [0, 1] ⟶ B$
38		1elunit	$⊢ 1 \in [0, 1]$
39		ffvelrn	$⊢ ((ι g \in (II Cn C) \| (F \circ g = G \circ a \land g (0) = P)) : [0, 1] ⟶ B \land 1 \in [0, 1]) \to (ι g \in (II Cn C) \| (F \circ g = G \circ a \land g (0) = P)) (1) \in B$
40	37 38 39	sylancl	$⊢ ((φ \land X \in Y) \land (a \in (II Cn K) \land (a (0) = O \land a (1) = X))) \to (ι g \in (II Cn C) \| (F \circ g = G \circ a \land g (0) = P)) (1) \in B$
41		simprrr	$⊢ ((φ \land X \in Y) \land (a \in (II Cn K) \land (a (0) = O \land a (1) = X))) \to a (1) = X$
42		eqidd	$⊢ ((φ \land X \in Y) \land (a \in (II Cn K) \land (a (0) = O \land a (1) = X))) \to (ι g \in (II Cn C) \| (F \circ g = G \circ a \land g (0) = P)) (1) = (ι g \in (II Cn C) \| (F \circ g = G \circ a \land g (0) = P)) (1)$
43		fveq1	$⊢ f = a \to f (0) = a (0)$
44	43	eqeq1d	$⊢ f = a \to (f (0) = O \leftrightarrow a (0) = O)$
45		fveq1	$⊢ f = a \to f (1) = a (1)$
46	45	eqeq1d	$⊢ f = a \to (f (1) = X \leftrightarrow a (1) = X)$
47		coeq2	$⊢ f = a \to G \circ f = G \circ a$
48	47	eqeq2d	$⊢ f = a \to (F \circ g = G \circ f \leftrightarrow F \circ g = G \circ a)$
49	48	anbi1d	$⊢ f = a \to ((F \circ g = G \circ f \land g (0) = P) \leftrightarrow (F \circ g = G \circ a \land g (0) = P))$
50	49	riotabidv	$⊢ f = a \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 a \land g (0) = P))$
51	50	fveq1d	$⊢ f = a \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 a \land g (0) = P)) (1)$
52	51	eqeq1d	$⊢ f = a \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 a \land g (0) = P)) (1) \leftrightarrow (ι g \in (II Cn C) \| (F \circ g = G \circ a \land g (0) = P)) (1) = (ι g \in (II Cn C) \| (F \circ g = G \circ a \land g (0) = P)) (1))$
53	44 46 52	3anbi123d	$⊢ f = 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) = (ι g \in (II Cn C) \| (F \circ g = G \circ a \land g (0) = P)) (1)) \leftrightarrow (a (0) = O \land a (1) = X \land (ι g \in (II Cn C) \| (F \circ g = G \circ a \land g (0) = P)) (1) = (ι g \in (II Cn C) \| (F \circ g = G \circ a \land g (0) = P)) (1)))$
54	53	rspcev	$⊢ (a \in (II Cn K) \land (a (0) = O \land a (1) = X \land (ι g \in (II Cn C) \| (F \circ g = G \circ a \land g (0) = P)) (1) = (ι g \in (II Cn C) \| (F \circ g = G \circ a \land g (0) = P)) (1))) \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) = (ι g \in (II Cn C) \| (F \circ g = G \circ a \land g (0) = P)) (1))$
55	19 24 41 42 54	syl13anc	$⊢ ((φ \land X \in Y) \land (a \in (II Cn K) \land (a (0) = O \land a (1) = 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) = (ι g \in (II Cn C) \| (F \circ g = G \circ a \land g (0) = P)) (1))$
56	3	ad4antr	$⊢ ((((φ \land X \in Y) \land (a \in (II Cn K) \land (a (0) = O \land a (1) = X))) \land w \in B) \land (h \in (II Cn K) \land (h (0) = O \land h (1) = X \land (ι g \in (II Cn C) \| (F \circ g = G \circ h \land g (0) = P)) (1) = w))) \to F \in (C CovMap J)$
57	4	ad4antr	$⊢ ((((φ \land X \in Y) \land (a \in (II Cn K) \land (a (0) = O \land a (1) = X))) \land w \in B) \land (h \in (II Cn K) \land (h (0) = O \land h (1) = X \land (ι g \in (II Cn C) \| (F \circ g = G \circ h \land g (0) = P)) (1) = w))) \to K \in SConn$
58	5	ad4antr	$⊢ ((((φ \land X \in Y) \land (a \in (II Cn K) \land (a (0) = O \land a (1) = X))) \land w \in B) \land (h \in (II Cn K) \land (h (0) = O \land h (1) = X \land (ι g \in (II Cn C) \| (F \circ g = G \circ h \land g (0) = P)) (1) = w))) \to K \in N-LocallyPConn$
59	6	ad4antr	$⊢ ((((φ \land X \in Y) \land (a \in (II Cn K) \land (a (0) = O \land a (1) = X))) \land w \in B) \land (h \in (II Cn K) \land (h (0) = O \land h (1) = X \land (ι g \in (II Cn C) \| (F \circ g = G \circ h \land g (0) = P)) (1) = w))) \to O \in Y$
60	7	ad4antr	$⊢ ((((φ \land X \in Y) \land (a \in (II Cn K) \land (a (0) = O \land a (1) = X))) \land w \in B) \land (h \in (II Cn K) \land (h (0) = O \land h (1) = X \land (ι g \in (II Cn C) \| (F \circ g = G \circ h \land g (0) = P)) (1) = w))) \to G \in (K Cn J)$
61	8	ad4antr	$⊢ ((((φ \land X \in Y) \land (a \in (II Cn K) \land (a (0) = O \land a (1) = X))) \land w \in B) \land (h \in (II Cn K) \land (h (0) = O \land h (1) = X \land (ι g \in (II Cn C) \| (F \circ g = G \circ h \land g (0) = P)) (1) = w))) \to P \in B$
62	9	ad4antr	$⊢ ((((φ \land X \in Y) \land (a \in (II Cn K) \land (a (0) = O \land a (1) = X))) \land w \in B) \land (h \in (II Cn K) \land (h (0) = O \land h (1) = X \land (ι g \in (II Cn C) \| (F \circ g = G \circ h \land g (0) = P)) (1) = w))) \to F (P) = G (O)$
63	19	ad2antrr	$⊢ ((((φ \land X \in Y) \land (a \in (II Cn K) \land (a (0) = O \land a (1) = X))) \land w \in B) \land (h \in (II Cn K) \land (h (0) = O \land h (1) = X \land (ι g \in (II Cn C) \| (F \circ g = G \circ h \land g (0) = P)) (1) = w))) \to a \in (II Cn K)$
64	24	ad2antrr	$⊢ ((((φ \land X \in Y) \land (a \in (II Cn K) \land (a (0) = O \land a (1) = X))) \land w \in B) \land (h \in (II Cn K) \land (h (0) = O \land h (1) = X \land (ι g \in (II Cn C) \| (F \circ g = G \circ h \land g (0) = P)) (1) = w))) \to a (0) = O$
65		simprl	$⊢ ((((φ \land X \in Y) \land (a \in (II Cn K) \land (a (0) = O \land a (1) = X))) \land w \in B) \land (h \in (II Cn K) \land (h (0) = O \land h (1) = X \land (ι g \in (II Cn C) \| (F \circ g = G \circ h \land g (0) = P)) (1) = w))) \to h \in (II Cn K)$
66		simprr1	$⊢ ((((φ \land X \in Y) \land (a \in (II Cn K) \land (a (0) = O \land a (1) = X))) \land w \in B) \land (h \in (II Cn K) \land (h (0) = O \land h (1) = X \land (ι g \in (II Cn C) \| (F \circ g = G \circ h \land g (0) = P)) (1) = w))) \to h (0) = O$
67	41	ad2antrr	$⊢ ((((φ \land X \in Y) \land (a \in (II Cn K) \land (a (0) = O \land a (1) = X))) \land w \in B) \land (h \in (II Cn K) \land (h (0) = O \land h (1) = X \land (ι g \in (II Cn C) \| (F \circ g = G \circ h \land g (0) = P)) (1) = w))) \to a (1) = X$
68		simprr2	$⊢ ((((φ \land X \in Y) \land (a \in (II Cn K) \land (a (0) = O \land a (1) = X))) \land w \in B) \land (h \in (II Cn K) \land (h (0) = O \land h (1) = X \land (ι g \in (II Cn C) \| (F \circ g = G \circ h \land g (0) = P)) (1) = w))) \to h (1) = X$
69	67 68	eqtr4d	$⊢ ((((φ \land X \in Y) \land (a \in (II Cn K) \land (a (0) = O \land a (1) = X))) \land w \in B) \land (h \in (II Cn K) \land (h (0) = O \land h (1) = X \land (ι g \in (II Cn C) \| (F \circ g = G \circ h \land g (0) = P)) (1) = w))) \to a (1) = h (1)$
70	1 2 56 57 58 59 60 61 62 63 64 65 66 69	cvmlift3lem1	$⊢ ((((φ \land X \in Y) \land (a \in (II Cn K) \land (a (0) = O \land a (1) = X))) \land w \in B) \land (h \in (II Cn K) \land (h (0) = O \land h (1) = X \land (ι g \in (II Cn C) \| (F \circ g = G \circ h \land g (0) = P)) (1) = w))) \to (ι g \in (II Cn C) \| (F \circ g = G \circ a \land g (0) = P)) (1) = (ι g \in (II Cn C) \| (F \circ g = G \circ h \land g (0) = P)) (1)$
71		simprr3	$⊢ ((((φ \land X \in Y) \land (a \in (II Cn K) \land (a (0) = O \land a (1) = X))) \land w \in B) \land (h \in (II Cn K) \land (h (0) = O \land h (1) = X \land (ι g \in (II Cn C) \| (F \circ g = G \circ h \land g (0) = P)) (1) = w))) \to (ι g \in (II Cn C) \| (F \circ g = G \circ h \land g (0) = P)) (1) = w$
72	70 71	eqtrd	$⊢ ((((φ \land X \in Y) \land (a \in (II Cn K) \land (a (0) = O \land a (1) = X))) \land w \in B) \land (h \in (II Cn K) \land (h (0) = O \land h (1) = X \land (ι g \in (II Cn C) \| (F \circ g = G \circ h \land g (0) = P)) (1) = w))) \to (ι g \in (II Cn C) \| (F \circ g = G \circ a \land g (0) = P)) (1) = w$
73	72	rexlimdvaa	$⊢ (((φ \land X \in Y) \land (a \in (II Cn K) \land (a (0) = O \land a (1) = X))) \land w \in B) \to (\exists h \in (II Cn K) (h (0) = O \land h (1) = X \land (ι g \in (II Cn C) \| (F \circ g = G \circ h \land g (0) = P)) (1) = w) \to (ι g \in (II Cn C) \| (F \circ g = G \circ a \land g (0) = P)) (1) = w)$
74	73	ralrimiva	$⊢ ((φ \land X \in Y) \land (a \in (II Cn K) \land (a (0) = O \land a (1) = X))) \to \forall w \in B (\exists h \in (II Cn K) (h (0) = O \land h (1) = X \land (ι g \in (II Cn C) \| (F \circ g = G \circ h \land g (0) = P)) (1) = w) \to (ι g \in (II Cn C) \| (F \circ g = G \circ a \land g (0) = P)) (1) = w)$
75		eqeq2	$⊢ z = (ι g \in (II Cn C) \| (F \circ g = G \circ a \land g (0) = P)) (1) \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) = (ι g \in (II Cn C) \| (F \circ g = G \circ a \land g (0) = P)) (1))$
76	75	3anbi3d	$⊢ z = (ι g \in (II Cn C) \| (F \circ g = G \circ a \land g (0) = P)) (1) \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) = (ι g \in (II Cn C) \| (F \circ g = G \circ a \land g (0) = P)) (1)))$
77	76	rexbidv	$⊢ z = (ι g \in (II Cn C) \| (F \circ g = G \circ a \land g (0) = P)) (1) \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) = (ι g \in (II Cn C) \| (F \circ g = G \circ a \land g (0) = P)) (1)))$
78		eqeq1	$⊢ z = (ι g \in (II Cn C) \| (F \circ g = G \circ a \land g (0) = P)) (1) \to (z = w \leftrightarrow (ι g \in (II Cn C) \| (F \circ g = G \circ a \land g (0) = P)) (1) = w)$
79	78	imbi2d	$⊢ z = (ι g \in (II Cn C) \| (F \circ g = G \circ a \land g (0) = P)) (1) \to ((\exists h \in (II Cn K) (h (0) = O \land h (1) = X \land (ι g \in (II Cn C) \| (F \circ g = G \circ h \land g (0) = P)) (1) = w) \to z = w) \leftrightarrow (\exists h \in (II Cn K) (h (0) = O \land h (1) = X \land (ι g \in (II Cn C) \| (F \circ g = G \circ h \land g (0) = P)) (1) = w) \to (ι g \in (II Cn C) \| (F \circ g = G \circ a \land g (0) = P)) (1) = w))$
80	79	ralbidv	$⊢ z = (ι g \in (II Cn C) \| (F \circ g = G \circ a \land g (0) = P)) (1) \to (\forall w \in B (\exists h \in (II Cn K) (h (0) = O \land h (1) = X \land (ι g \in (II Cn C) \| (F \circ g = G \circ h \land g (0) = P)) (1) = w) \to z = w) \leftrightarrow \forall w \in B (\exists h \in (II Cn K) (h (0) = O \land h (1) = X \land (ι g \in (II Cn C) \| (F \circ g = G \circ h \land g (0) = P)) (1) = w) \to (ι g \in (II Cn C) \| (F \circ g = G \circ a \land g (0) = P)) (1) = w))$
81	77 80	anbi12d	$⊢ z = (ι g \in (II Cn C) \| (F \circ g = G \circ a \land g (0) = P)) (1) \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) \land \forall w \in B (\exists h \in (II Cn K) (h (0) = O \land h (1) = X \land (ι g \in (II Cn C) \| (F \circ g = G \circ h \land g (0) = P)) (1) = w) \to z = w)) \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) = (ι g \in (II Cn C) \| (F \circ g = G \circ a \land g (0) = P)) (1)) \land \forall w \in B (\exists h \in (II Cn K) (h (0) = O \land h (1) = X \land (ι g \in (II Cn C) \| (F \circ g = G \circ h \land g (0) = P)) (1) = w) \to (ι g \in (II Cn C) \| (F \circ g = G \circ a \land g (0) = P)) (1) = w)))$
82	81	rspcev	$⊢ ((ι g \in (II Cn C) \| (F \circ g = G \circ a \land g (0) = P)) (1) \in B \land (\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) = (ι g \in (II Cn C) \| (F \circ g = G \circ a \land g (0) = P)) (1)) \land \forall w \in B (\exists h \in (II Cn K) (h (0) = O \land h (1) = X \land (ι g \in (II Cn C) \| (F \circ g = G \circ h \land g (0) = P)) (1) = w) \to (ι g \in (II Cn C) \| (F \circ g = G \circ a \land g (0) = P)) (1) = w))) \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) \land \forall w \in B (\exists h \in (II Cn K) (h (0) = O \land h (1) = X \land (ι g \in (II Cn C) \| (F \circ g = G \circ h \land g (0) = P)) (1) = w) \to z = w))$
83	40 55 74 82	syl12anc	$⊢ ((φ \land X \in Y) \land (a \in (II Cn K) \land (a (0) = O \land a (1) = X))) \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) \land \forall w \in B (\exists h \in (II Cn K) (h (0) = O \land h (1) = X \land (ι g \in (II Cn C) \| (F \circ g = G \circ h \land g (0) = P)) (1) = w) \to z = w))$
84		fveq1	$⊢ f = h \to f (0) = h (0)$
85	84	eqeq1d	$⊢ f = h \to (f (0) = O \leftrightarrow h (0) = O)$
86		fveq1	$⊢ f = h \to f (1) = h (1)$
87	86	eqeq1d	$⊢ f = h \to (f (1) = X \leftrightarrow h (1) = X)$
88		coeq2	$⊢ f = h \to G \circ f = G \circ h$
89	88	eqeq2d	$⊢ f = h \to (F \circ g = G \circ f \leftrightarrow F \circ g = G \circ h)$
90	89	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))$
91	90	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))$
92	91	fveq1d	$⊢ f = h \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 h \land g (0) = P)) (1)$
93	92	eqeq1d	$⊢ f = h \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 h \land g (0) = P)) (1) = z)$
94	85 87 93	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) = z) \leftrightarrow (h (0) = O \land h (1) = X \land (ι g \in (II Cn C) \| (F \circ g = G \circ h \land g (0) = P)) (1) = z))$
95	94	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) = z) \leftrightarrow \exists h \in (II Cn K) (h (0) = O \land h (1) = X \land (ι g \in (II Cn C) \| (F \circ g = G \circ h \land g (0) = P)) (1) = z)$
96		eqeq2	$⊢ z = w \to ((ι g \in (II Cn C) \| (F \circ g = G \circ h \land g (0) = P)) (1) = z \leftrightarrow (ι g \in (II Cn C) \| (F \circ g = G \circ h \land g (0) = P)) (1) = w)$
97	96	3anbi3d	$⊢ z = w \to ((h (0) = O \land h (1) = X \land (ι g \in (II Cn C) \| (F \circ g = G \circ h \land g (0) = P)) (1) = z) \leftrightarrow (h (0) = O \land h (1) = X \land (ι g \in (II Cn C) \| (F \circ g = G \circ h \land g (0) = P)) (1) = w))$
98	97	rexbidv	$⊢ z = w \to (\exists h \in (II Cn K) (h (0) = O \land h (1) = X \land (ι g \in (II Cn C) \| (F \circ g = G \circ h \land g (0) = P)) (1) = z) \leftrightarrow \exists h \in (II Cn K) (h (0) = O \land h (1) = X \land (ι g \in (II Cn C) \| (F \circ g = G \circ h \land g (0) = P)) (1) = w))$
99	95 98	syl5bb	$⊢ z = w \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 h \in (II Cn K) (h (0) = O \land h (1) = X \land (ι g \in (II Cn C) \| (F \circ g = G \circ h \land g (0) = P)) (1) = w))$
100	99	reu8	$⊢ \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) \leftrightarrow \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) \land \forall w \in B (\exists h \in (II Cn K) (h (0) = O \land h (1) = X \land (ι g \in (II Cn C) \| (F \circ g = G \circ h \land g (0) = P)) (1) = w) \to z = w))$
101	83 100	sylibr	$⊢ ((φ \land X \in Y) \land (a \in (II Cn K) \land (a (0) = O \land a (1) = X))) \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)$
102	101	rexlimdvaa	$⊢ (φ \land X \in Y) \to (\exists a \in (II Cn K) (a (0) = O \land a (1) = X) \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))$
103	16 102	mpd	$⊢ (φ \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)$

Metamath Proof Explorer

Theorem cvmlift3lem2

Proof