elpi1

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

	Ref	Expression
Hypotheses	elpi1.g	$⊢ G = J π_{1} Y$
	elpi1.b	$⊢ B = {Base}_{G}$
	elpi1.1	$⊢ φ \to J \in TopOn (X)$
	elpi1.2	$⊢ φ \to Y \in X$
Assertion	elpi1	$⊢ φ \to (F \in B \leftrightarrow \exists f \in (II Cn J) ((f (0) = Y \land f (1) = Y) \land F = [f] ≃_{ph} (J)))$

Proof

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	2	a1i	$⊢ φ \to B = {Base}_{G}$
6	1 3 4 5	pi1bas2	$⊢ φ \to B = ⋃ B / ≃_{ph} (J)$
7	6	eleq2d	$⊢ φ \to (F \in B \leftrightarrow F \in (⋃ B / ≃_{ph} (J)))$
8		elex	$⊢ F \in (⋃ B / ≃_{ph} (J)) \to F \in V$
9		id	$⊢ F = [f] ≃_{ph} (J) \to F = [f] ≃_{ph} (J)$
10		fvex	$⊢ ≃_{ph} (J) \in V$
11		ecexg	$⊢ ≃_{ph} (J) \in V \to [f] ≃_{ph} (J) \in V$
12	10 11	ax-mp	$⊢ [f] ≃_{ph} (J) \in V$
13	9 12	eqeltrdi	$⊢ F = [f] ≃_{ph} (J) \to F \in V$
14	13	rexlimivw	$⊢ \exists f \in ⋃ B F = [f] ≃_{ph} (J) \to F \in V$
15		elqsg	$⊢ F \in V \to (F \in (⋃ B / ≃_{ph} (J)) \leftrightarrow \exists f \in ⋃ B F = [f] ≃_{ph} (J))$
16	8 14 15	pm5.21nii	$⊢ F \in (⋃ B / ≃_{ph} (J)) \leftrightarrow \exists f \in ⋃ B F = [f] ≃_{ph} (J)$
17	1 3 4 5	pi1eluni	$⊢ φ \to (f \in ⋃ B \leftrightarrow (f \in (II Cn J) \land f (0) = Y \land f (1) = Y))$
18		3anass	$⊢ (f \in (II Cn J) \land f (0) = Y \land f (1) = Y) \leftrightarrow (f \in (II Cn J) \land (f (0) = Y \land f (1) = Y))$
19	17 18	bitrdi	$⊢ φ \to (f \in ⋃ B \leftrightarrow (f \in (II Cn J) \land (f (0) = Y \land f (1) = Y)))$
20	19	anbi1d	$⊢ φ \to ((f \in ⋃ B \land F = [f] ≃_{ph} (J)) \leftrightarrow ((f \in (II Cn J) \land (f (0) = Y \land f (1) = Y)) \land F = [f] ≃_{ph} (J)))$
21		anass	$⊢ ((f \in (II Cn J) \land (f (0) = Y \land f (1) = Y)) \land F = [f] ≃_{ph} (J)) \leftrightarrow (f \in (II Cn J) \land ((f (0) = Y \land f (1) = Y) \land F = [f] ≃_{ph} (J)))$
22	20 21	bitrdi	$⊢ φ \to ((f \in ⋃ B \land F = [f] ≃_{ph} (J)) \leftrightarrow (f \in (II Cn J) \land ((f (0) = Y \land f (1) = Y) \land F = [f] ≃_{ph} (J))))$
23	22	rexbidv2	$⊢ φ \to (\exists f \in ⋃ B F = [f] ≃_{ph} (J) \leftrightarrow \exists f \in (II Cn J) ((f (0) = Y \land f (1) = Y) \land F = [f] ≃_{ph} (J)))$
24	16 23	bitrid	$⊢ φ \to (F \in (⋃ B / ≃_{ph} (J)) \leftrightarrow \exists f \in (II Cn J) ((f (0) = Y \land f (1) = Y) \land F = [f] ≃_{ph} (J)))$
25	7 24	bitrd	$⊢ φ \to (F \in B \leftrightarrow \exists f \in (II Cn J) ((f (0) = Y \land f (1) = Y) \land F = [f] ≃_{ph} (J)))$

Metamath Proof Explorer

Theorem elpi1

Proof