pi1val

Description: The definition of the fundamental group. (Contributed by Mario Carneiro, 11-Feb-2015) (Revised by Mario Carneiro, 10-Jul-2015)

Step	Hyp	Ref	Expression
1		pi1val.g	$⊢ G = J π_{1} Y$
2		pi1val.1	$⊢ φ \to J \in TopOn (X)$
3		pi1val.2	$⊢ φ \to Y \in X$
4		pi1val.o	$⊢ O = J Ω_{1} Y$
5		df-pi1	$⊢ π_{1} = (j \in Top, y \in ⋃ j ⟼ (j Ω_{1} y) /_{𝑠} ≃_{ph} (j))$
6	5	a1i	$⊢ φ \to π_{1} = (j \in Top, y \in ⋃ j ⟼ (j Ω_{1} y) /_{𝑠} ≃_{ph} (j))$
7		simprl	$⊢ (φ \land (j = J \land y = Y)) \to j = J$
8		simprr	$⊢ (φ \land (j = J \land y = Y)) \to y = Y$
9	7 8	oveq12d	$⊢ (φ \land (j = J \land y = Y)) \to j Ω_{1} y = J Ω_{1} Y$
10	9 4	eqtr4di	$⊢ (φ \land (j = J \land y = Y)) \to j Ω_{1} y = O$
11	7	fveq2d	$⊢ (φ \land (j = J \land y = Y)) \to ≃_{ph} (j) = ≃_{ph} (J)$
12	10 11	oveq12d	$⊢ (φ \land (j = J \land y = Y)) \to (j Ω_{1} y) /_{𝑠} ≃_{ph} (j) = O /_{𝑠} ≃_{ph} (J)$
13		unieq	$⊢ j = J \to ⋃ j = ⋃ J$
14	13	adantl	$⊢ (φ \land j = J) \to ⋃ j = ⋃ J$
15		toponuni	$⊢ J \in TopOn (X) \to X = ⋃ J$
16	2 15	syl	$⊢ φ \to X = ⋃ J$
17	16	adantr	$⊢ (φ \land j = J) \to X = ⋃ J$
18	14 17	eqtr4d	$⊢ (φ \land j = J) \to ⋃ j = X$
19		topontop	$⊢ J \in TopOn (X) \to J \in Top$
20	2 19	syl	$⊢ φ \to J \in Top$
21		ovexd	$⊢ φ \to O /_{𝑠} ≃_{ph} (J) \in V$
22	6 12 18 20 3 21	ovmpodx	$⊢ φ \to J π_{1} Y = O /_{𝑠} ≃_{ph} (J)$
23	1 22	eqtrid	$⊢ φ \to G = O /_{𝑠} ≃_{ph} (J)$

Metamath Proof Explorer