elpi1i

Description: The elements of the fundamental group. (Contributed by Jeff Madsen, 19-Jun-2010) (Revised by Mario Carneiro, 10-Jul-2015)

Step	Hyp	Ref	Expression
1		elpi1.g	$⊢ G = J π_{1} Y$
2		elpi1.b	$⊢ B = {Base}_{G}$
3		elpi1.1	$⊢ φ \to J \in TopOn (X)$
4		elpi1.2	$⊢ φ \to Y \in X$
5		elpi1i.3	$⊢ φ \to F \in (II Cn J)$
6		elpi1i.4	$⊢ φ \to F (0) = Y$
7		elpi1i.5	$⊢ φ \to F (1) = Y$
8		eceq1	$⊢ f = F \to [f] ≃_{ph} (J) = [F] ≃_{ph} (J)$
9	8	eqcomd	$⊢ f = F \to [F] ≃_{ph} (J) = [f] ≃_{ph} (J)$
10	9	biantrud	$⊢ f = F \to ((f (0) = Y \land f (1) = Y) \leftrightarrow ((f (0) = Y \land f (1) = Y) \land [F] ≃_{ph} (J) = [f] ≃_{ph} (J)))$
11		fveq1	$⊢ f = F \to f (0) = F (0)$
12	11	eqeq1d	$⊢ f = F \to (f (0) = Y \leftrightarrow F (0) = Y)$
13		fveq1	$⊢ f = F \to f (1) = F (1)$
14	13	eqeq1d	$⊢ f = F \to (f (1) = Y \leftrightarrow F (1) = Y)$
15	12 14	anbi12d	$⊢ f = F \to ((f (0) = Y \land f (1) = Y) \leftrightarrow (F (0) = Y \land F (1) = Y))$
16	10 15	bitr3d	$⊢ f = F \to (((f (0) = Y \land f (1) = Y) \land [F] ≃_{ph} (J) = [f] ≃_{ph} (J)) \leftrightarrow (F (0) = Y \land F (1) = Y))$
17	16	rspcev	$⊢ (F \in (II Cn J) \land (F (0) = Y \land F (1) = Y)) \to \exists f \in (II Cn J) ((f (0) = Y \land f (1) = Y) \land [F] ≃_{ph} (J) = [f] ≃_{ph} (J))$
18	5 6 7 17	syl12anc	$⊢ φ \to \exists f \in (II Cn J) ((f (0) = Y \land f (1) = Y) \land [F] ≃_{ph} (J) = [f] ≃_{ph} (J))$
19	1 2 3 4	elpi1	$⊢ φ \to ([F] ≃_{ph} (J) \in B \leftrightarrow \exists f \in (II Cn J) ((f (0) = Y \land f (1) = Y) \land [F] ≃_{ph} (J) = [f] ≃_{ph} (J)))$
20	18 19	mpbird	$⊢ φ \to [F] ≃_{ph} (J) \in B$

Metamath Proof Explorer