cvmliftiota

Description: Write out a function H that is the unique lift of F . (Contributed by Mario Carneiro, 16-Feb-2015)

	Ref	Expression
Hypotheses	cvmliftiota.b	$⊢ B = ⋃ C$
	cvmliftiota.h	$⊢ H = (ι f \in (II Cn C) \| (F \circ f = G \land f (0) = P))$
	cvmliftiota.f	$⊢ φ \to F \in (C CovMap J)$
	cvmliftiota.g	$⊢ φ \to G \in (II Cn J)$
	cvmliftiota.p	$⊢ φ \to P \in B$
	cvmliftiota.e	$⊢ φ \to F (P) = G (0)$
Assertion	cvmliftiota	$⊢ φ \to (H \in (II Cn C) \land F \circ H = G \land H (0) = P)$

Proof

Step	Hyp	Ref	Expression
1		cvmliftiota.b	$⊢ B = ⋃ C$
2		cvmliftiota.h	$⊢ H = (ι f \in (II Cn C) \| (F \circ f = G \land f (0) = P))$
3		cvmliftiota.f	$⊢ φ \to F \in (C CovMap J)$
4		cvmliftiota.g	$⊢ φ \to G \in (II Cn J)$
5		cvmliftiota.p	$⊢ φ \to P \in B$
6		cvmliftiota.e	$⊢ φ \to F (P) = G (0)$
7		coeq2	$⊢ f = g \to F \circ f = F \circ g$
8	7	eqeq1d	$⊢ f = g \to (F \circ f = G \leftrightarrow F \circ g = G)$
9		fveq1	$⊢ f = g \to f (0) = g (0)$
10	9	eqeq1d	$⊢ f = g \to (f (0) = P \leftrightarrow g (0) = P)$
11	8 10	anbi12d	$⊢ f = g \to ((F \circ f = G \land f (0) = P) \leftrightarrow (F \circ g = G \land g (0) = P))$
12	11	cbvriotavw	$⊢ (ι f \in (II Cn C) \| (F \circ f = G \land f (0) = P)) = (ι g \in (II Cn C) \| (F \circ g = G \land g (0) = P))$
13	2 12	eqtri	$⊢ H = (ι g \in (II Cn C) \| (F \circ g = G \land g (0) = P))$
14	1	cvmlift	$⊢ ((F \in (C CovMap J) \land G \in (II Cn J)) \land (P \in B \land F (P) = G (0))) \to \exists! g \in (II Cn C) (F \circ g = G \land g (0) = P)$
15	3 4 5 6 14	syl22anc	$⊢ φ \to \exists! g \in (II Cn C) (F \circ g = G \land g (0) = P)$
16		riotacl2	$⊢ \exists! g \in (II Cn C) (F \circ g = G \land g (0) = P) \to (ι g \in (II Cn C) \| (F \circ g = G \land g (0) = P)) \in \{g \in (II Cn C) \| (F \circ g = G \land g (0) = P)\}$
17	15 16	syl	$⊢ φ \to (ι g \in (II Cn C) \| (F \circ g = G \land g (0) = P)) \in \{g \in (II Cn C) \| (F \circ g = G \land g (0) = P)\}$
18	13 17	eqeltrid	$⊢ φ \to H \in \{g \in (II Cn C) \| (F \circ g = G \land g (0) = P)\}$
19		coeq2	$⊢ g = H \to F \circ g = F \circ H$
20	19	eqeq1d	$⊢ g = H \to (F \circ g = G \leftrightarrow F \circ H = G)$
21		fveq1	$⊢ g = H \to g (0) = H (0)$
22	21	eqeq1d	$⊢ g = H \to (g (0) = P \leftrightarrow H (0) = P)$
23	20 22	anbi12d	$⊢ g = H \to ((F \circ g = G \land g (0) = P) \leftrightarrow (F \circ H = G \land H (0) = P))$
24	23	elrab	$⊢ H \in \{g \in (II Cn C) \| (F \circ g = G \land g (0) = P)\} \leftrightarrow (H \in (II Cn C) \land (F \circ H = G \land H (0) = P))$
25		3anass	$⊢ (H \in (II Cn C) \land F \circ H = G \land H (0) = P) \leftrightarrow (H \in (II Cn C) \land (F \circ H = G \land H (0) = P))$
26	24 25	bitr4i	$⊢ H \in \{g \in (II Cn C) \| (F \circ g = G \land g (0) = P)\} \leftrightarrow (H \in (II Cn C) \land F \circ H = G \land H (0) = P)$
27	18 26	sylib	$⊢ φ \to (H \in (II Cn C) \land F \circ H = G \land H (0) = P)$

Metamath Proof Explorer

Theorem cvmliftiota

Proof