sconnpi1

Description: A path-connected topological space is simply connected iff its fundamental group is trivial. (Contributed by Mario Carneiro, 12-Feb-2015)

		Ref	Expression
	Hypothesis	sconnpi1.1	$⊢ X = ⋃ J$
	Assertion	sconnpi1	$⊢ (J \in PConn \land Y \in X) \to (J \in SConn \leftrightarrow {Base}_{(J π_{1} Y)} \approx 1_{𝑜})$

Proof

Step	Hyp	Ref	Expression
1		sconnpi1.1	$⊢ X = ⋃ J$
2		sconntop	$⊢ J \in SConn \to J \in Top$
3	2	adantl	$⊢ (Y \in X \land J \in SConn) \to J \in Top$
4		simpl	$⊢ (Y \in X \land J \in SConn) \to Y \in X$
5		eqid	$⊢ J π_{1} Y = J π_{1} Y$
6		eqid	$⊢ {Base}_{(J π_{1} Y)} = {Base}_{(J π_{1} Y)}$
7		simpl	$⊢ (J \in Top \land Y \in X) \to J \in Top$
8	1	toptopon	$⊢ J \in Top \leftrightarrow J \in TopOn (X)$
9	7 8	sylib	$⊢ (J \in Top \land Y \in X) \to J \in TopOn (X)$
10		simpr	$⊢ (J \in Top \land Y \in X) \to Y \in X$
11	5 6 9 10	elpi1	$⊢ (J \in Top \land Y \in X) \to (x \in {Base}_{(J π_{1} Y)} \leftrightarrow \exists f \in (II Cn J) ((f (0) = Y \land f (1) = Y) \land x = [f] ≃_{ph} (J)))$
12	3 4 11	syl2anc	$⊢ (Y \in X \land J \in SConn) \to (x \in {Base}_{(J π_{1} Y)} \leftrightarrow \exists f \in (II Cn J) ((f (0) = Y \land f (1) = Y) \land x = [f] ≃_{ph} (J)))$
13		phtpcer	$⊢ ≃_{ph} (J) Er (II Cn J)$
14	13	a1i	$⊢ (((Y \in X \land J \in SConn) \land f \in (II Cn J)) \land (f (0) = Y \land f (1) = Y)) \to ≃_{ph} (J) Er (II Cn J)$
15		simpllr	$⊢ (((Y \in X \land J \in SConn) \land f \in (II Cn J)) \land (f (0) = Y \land f (1) = Y)) \to J \in SConn$
16		simplr	$⊢ (((Y \in X \land J \in SConn) \land f \in (II Cn J)) \land (f (0) = Y \land f (1) = Y)) \to f \in (II Cn J)$
17		simprl	$⊢ (((Y \in X \land J \in SConn) \land f \in (II Cn J)) \land (f (0) = Y \land f (1) = Y)) \to f (0) = Y$
18		simprr	$⊢ (((Y \in X \land J \in SConn) \land f \in (II Cn J)) \land (f (0) = Y \land f (1) = Y)) \to f (1) = Y$
19	17 18	eqtr4d	$⊢ (((Y \in X \land J \in SConn) \land f \in (II Cn J)) \land (f (0) = Y \land f (1) = Y)) \to f (0) = f (1)$
20		sconnpht	$⊢ (J \in SConn \land f \in (II Cn J) \land f (0) = f (1)) \to f ≃_{ph} (J) ([0, 1] \times \{f (0)\})$
21	15 16 19 20	syl3anc	$⊢ (((Y \in X \land J \in SConn) \land f \in (II Cn J)) \land (f (0) = Y \land f (1) = Y)) \to f ≃_{ph} (J) ([0, 1] \times \{f (0)\})$
22	17	sneqd	$⊢ (((Y \in X \land J \in SConn) \land f \in (II Cn J)) \land (f (0) = Y \land f (1) = Y)) \to \{f (0)\} = \{Y\}$
23	22	xpeq2d	$⊢ (((Y \in X \land J \in SConn) \land f \in (II Cn J)) \land (f (0) = Y \land f (1) = Y)) \to [0, 1] \times \{f (0)\} = [0, 1] \times \{Y\}$
24	21 23	breqtrd	$⊢ (((Y \in X \land J \in SConn) \land f \in (II Cn J)) \land (f (0) = Y \land f (1) = Y)) \to f ≃_{ph} (J) ([0, 1] \times \{Y\})$
25	14 24	erthi	$⊢ (((Y \in X \land J \in SConn) \land f \in (II Cn J)) \land (f (0) = Y \land f (1) = Y)) \to [f] ≃_{ph} (J) = [([0, 1] \times \{Y\})] ≃_{ph} (J)$
26	3 8	sylib	$⊢ (Y \in X \land J \in SConn) \to J \in TopOn (X)$
27		eqid	$⊢ [0, 1] \times \{Y\} = [0, 1] \times \{Y\}$
28	5 27	pi1id	$⊢ (J \in TopOn (X) \land Y \in X) \to [([0, 1] \times \{Y\})] ≃_{ph} (J) = 0_{(J π_{1} Y)}$
29	26 4 28	syl2anc	$⊢ (Y \in X \land J \in SConn) \to [([0, 1] \times \{Y\})] ≃_{ph} (J) = 0_{(J π_{1} Y)}$
30	29	ad2antrr	$⊢ (((Y \in X \land J \in SConn) \land f \in (II Cn J)) \land (f (0) = Y \land f (1) = Y)) \to [([0, 1] \times \{Y\})] ≃_{ph} (J) = 0_{(J π_{1} Y)}$
31	25 30	eqtrd	$⊢ (((Y \in X \land J \in SConn) \land f \in (II Cn J)) \land (f (0) = Y \land f (1) = Y)) \to [f] ≃_{ph} (J) = 0_{(J π_{1} Y)}$
32		velsn	$⊢ x \in \{0_{(J π_{1} Y)}\} \leftrightarrow x = 0_{(J π_{1} Y)}$
33		eqeq1	$⊢ x = [f] ≃_{ph} (J) \to (x = 0_{(J π_{1} Y)} \leftrightarrow [f] ≃_{ph} (J) = 0_{(J π_{1} Y)})$
34	32 33	bitrid	$⊢ x = [f] ≃_{ph} (J) \to (x \in \{0_{(J π_{1} Y)}\} \leftrightarrow [f] ≃_{ph} (J) = 0_{(J π_{1} Y)})$
35	31 34	syl5ibrcom	$⊢ (((Y \in X \land J \in SConn) \land f \in (II Cn J)) \land (f (0) = Y \land f (1) = Y)) \to (x = [f] ≃_{ph} (J) \to x \in \{0_{(J π_{1} Y)}\})$
36	35	expimpd	$⊢ ((Y \in X \land J \in SConn) \land f \in (II Cn J)) \to (((f (0) = Y \land f (1) = Y) \land x = [f] ≃_{ph} (J)) \to x \in \{0_{(J π_{1} Y)}\})$
37	36	rexlimdva	$⊢ (Y \in X \land J \in SConn) \to (\exists f \in (II Cn J) ((f (0) = Y \land f (1) = Y) \land x = [f] ≃_{ph} (J)) \to x \in \{0_{(J π_{1} Y)}\})$
38	12 37	sylbid	$⊢ (Y \in X \land J \in SConn) \to (x \in {Base}_{(J π_{1} Y)} \to x \in \{0_{(J π_{1} Y)}\})$
39	38	ssrdv	$⊢ (Y \in X \land J \in SConn) \to {Base}_{(J π_{1} Y)} \subseteq \{0_{(J π_{1} Y)}\}$
40	5	pi1grp	$⊢ (J \in TopOn (X) \land Y \in X) \to J π_{1} Y \in Grp$
41	26 4 40	syl2anc	$⊢ (Y \in X \land J \in SConn) \to J π_{1} Y \in Grp$
42		eqid	$⊢ 0_{(J π_{1} Y)} = 0_{(J π_{1} Y)}$
43	6 42	grpidcl	$⊢ J π_{1} Y \in Grp \to 0_{(J π_{1} Y)} \in {Base}_{(J π_{1} Y)}$
44	41 43	syl	$⊢ (Y \in X \land J \in SConn) \to 0_{(J π_{1} Y)} \in {Base}_{(J π_{1} Y)}$
45	44	snssd	$⊢ (Y \in X \land J \in SConn) \to \{0_{(J π_{1} Y)}\} \subseteq {Base}_{(J π_{1} Y)}$
46	39 45	eqssd	$⊢ (Y \in X \land J \in SConn) \to {Base}_{(J π_{1} Y)} = \{0_{(J π_{1} Y)}\}$
47		fvex	$⊢ 0_{(J π_{1} Y)} \in V$
48	47	ensn1	$⊢ \{0_{(J π_{1} Y)}\} \approx 1_{𝑜}$
49	46 48	eqbrtrdi	$⊢ (Y \in X \land J \in SConn) \to {Base}_{(J π_{1} Y)} \approx 1_{𝑜}$
50	49	adantll	$⊢ ((J \in PConn \land Y \in X) \land J \in SConn) \to {Base}_{(J π_{1} Y)} \approx 1_{𝑜}$
51		simpll	$⊢ ((J \in PConn \land Y \in X) \land {Base}_{(J π_{1} Y)} \approx 1_{𝑜}) \to J \in PConn$
52		eqid	$⊢ J π_{1} f (0) = J π_{1} f (0)$
53		eqid	$⊢ {Base}_{(J π_{1} f (0))} = {Base}_{(J π_{1} f (0))}$
54		simplll	$⊢ (((J \in PConn \land Y \in X) \land {Base}_{(J π_{1} Y)} \approx 1_{𝑜}) \land (f \in (II Cn J) \land f (0) = f (1))) \to J \in PConn$
55		pconntop	$⊢ J \in PConn \to J \in Top$
56	54 55	syl	$⊢ (((J \in PConn \land Y \in X) \land {Base}_{(J π_{1} Y)} \approx 1_{𝑜}) \land (f \in (II Cn J) \land f (0) = f (1))) \to J \in Top$
57	56 8	sylib	$⊢ (((J \in PConn \land Y \in X) \land {Base}_{(J π_{1} Y)} \approx 1_{𝑜}) \land (f \in (II Cn J) \land f (0) = f (1))) \to J \in TopOn (X)$
58		simprl	$⊢ (((J \in PConn \land Y \in X) \land {Base}_{(J π_{1} Y)} \approx 1_{𝑜}) \land (f \in (II Cn J) \land f (0) = f (1))) \to f \in (II Cn J)$
59		iiuni	$⊢ [0, 1] = ⋃ II$
60	59 1	cnf	$⊢ f \in (II Cn J) \to f : [0, 1] ⟶ X$
61	58 60	syl	$⊢ (((J \in PConn \land Y \in X) \land {Base}_{(J π_{1} Y)} \approx 1_{𝑜}) \land (f \in (II Cn J) \land f (0) = f (1))) \to f : [0, 1] ⟶ X$
62		0elunit	$⊢ 0 \in [0, 1]$
63		ffvelcdm	$⊢ (f : [0, 1] ⟶ X \land 0 \in [0, 1]) \to f (0) \in X$
64	61 62 63	sylancl	$⊢ (((J \in PConn \land Y \in X) \land {Base}_{(J π_{1} Y)} \approx 1_{𝑜}) \land (f \in (II Cn J) \land f (0) = f (1))) \to f (0) \in X$
65		eqidd	$⊢ (((J \in PConn \land Y \in X) \land {Base}_{(J π_{1} Y)} \approx 1_{𝑜}) \land (f \in (II Cn J) \land f (0) = f (1))) \to f (0) = f (0)$
66		simprr	$⊢ (((J \in PConn \land Y \in X) \land {Base}_{(J π_{1} Y)} \approx 1_{𝑜}) \land (f \in (II Cn J) \land f (0) = f (1))) \to f (0) = f (1)$
67	66	eqcomd	$⊢ (((J \in PConn \land Y \in X) \land {Base}_{(J π_{1} Y)} \approx 1_{𝑜}) \land (f \in (II Cn J) \land f (0) = f (1))) \to f (1) = f (0)$
68	52 53 57 64 58 65 67	elpi1i	$⊢ (((J \in PConn \land Y \in X) \land {Base}_{(J π_{1} Y)} \approx 1_{𝑜}) \land (f \in (II Cn J) \land f (0) = f (1))) \to [f] ≃_{ph} (J) \in {Base}_{(J π_{1} f (0))}$
69		eqid	$⊢ [0, 1] \times \{f (0)\} = [0, 1] \times \{f (0)\}$
70	69	pcoptcl	$⊢ (J \in TopOn (X) \land f (0) \in X) \to ([0, 1] \times \{f (0)\} \in (II Cn J) \land ([0, 1] \times \{f (0)\}) (0) = f (0) \land ([0, 1] \times \{f (0)\}) (1) = f (0))$
71	57 64 70	syl2anc	$⊢ (((J \in PConn \land Y \in X) \land {Base}_{(J π_{1} Y)} \approx 1_{𝑜}) \land (f \in (II Cn J) \land f (0) = f (1))) \to ([0, 1] \times \{f (0)\} \in (II Cn J) \land ([0, 1] \times \{f (0)\}) (0) = f (0) \land ([0, 1] \times \{f (0)\}) (1) = f (0))$
72	71	simp1d	$⊢ (((J \in PConn \land Y \in X) \land {Base}_{(J π_{1} Y)} \approx 1_{𝑜}) \land (f \in (II Cn J) \land f (0) = f (1))) \to [0, 1] \times \{f (0)\} \in (II Cn J)$
73	71	simp2d	$⊢ (((J \in PConn \land Y \in X) \land {Base}_{(J π_{1} Y)} \approx 1_{𝑜}) \land (f \in (II Cn J) \land f (0) = f (1))) \to ([0, 1] \times \{f (0)\}) (0) = f (0)$
74	71	simp3d	$⊢ (((J \in PConn \land Y \in X) \land {Base}_{(J π_{1} Y)} \approx 1_{𝑜}) \land (f \in (II Cn J) \land f (0) = f (1))) \to ([0, 1] \times \{f (0)\}) (1) = f (0)$
75	52 53 57 64 72 73 74	elpi1i	$⊢ (((J \in PConn \land Y \in X) \land {Base}_{(J π_{1} Y)} \approx 1_{𝑜}) \land (f \in (II Cn J) \land f (0) = f (1))) \to [([0, 1] \times \{f (0)\})] ≃_{ph} (J) \in {Base}_{(J π_{1} f (0))}$
76		simpllr	$⊢ (((J \in PConn \land Y \in X) \land {Base}_{(J π_{1} Y)} \approx 1_{𝑜}) \land (f \in (II Cn J) \land f (0) = f (1))) \to Y \in X$
77	1 52 5 53 6	pconnpi1	$⊢ (J \in PConn \land f (0) \in X \land Y \in X) \to (J π_{1} f (0)) ≃_{𝑔} (J π_{1} Y)$
78	54 64 76 77	syl3anc	$⊢ (((J \in PConn \land Y \in X) \land {Base}_{(J π_{1} Y)} \approx 1_{𝑜}) \land (f \in (II Cn J) \land f (0) = f (1))) \to (J π_{1} f (0)) ≃_{𝑔} (J π_{1} Y)$
79	53 6	gicen	$⊢ (J π_{1} f (0)) ≃_{𝑔} (J π_{1} Y) \to {Base}_{(J π_{1} f (0))} \approx {Base}_{(J π_{1} Y)}$
80	78 79	syl	$⊢ (((J \in PConn \land Y \in X) \land {Base}_{(J π_{1} Y)} \approx 1_{𝑜}) \land (f \in (II Cn J) \land f (0) = f (1))) \to {Base}_{(J π_{1} f (0))} \approx {Base}_{(J π_{1} Y)}$
81		simplr	$⊢ (((J \in PConn \land Y \in X) \land {Base}_{(J π_{1} Y)} \approx 1_{𝑜}) \land (f \in (II Cn J) \land f (0) = f (1))) \to {Base}_{(J π_{1} Y)} \approx 1_{𝑜}$
82		entr	$⊢ ({Base}_{(J π_{1} f (0))} \approx {Base}_{(J π_{1} Y)} \land {Base}_{(J π_{1} Y)} \approx 1_{𝑜}) \to {Base}_{(J π_{1} f (0))} \approx 1_{𝑜}$
83	80 81 82	syl2anc	$⊢ (((J \in PConn \land Y \in X) \land {Base}_{(J π_{1} Y)} \approx 1_{𝑜}) \land (f \in (II Cn J) \land f (0) = f (1))) \to {Base}_{(J π_{1} f (0))} \approx 1_{𝑜}$
84		en1eqsn	$⊢ ([([0, 1] \times \{f (0)\})] ≃_{ph} (J) \in {Base}_{(J π_{1} f (0))} \land {Base}_{(J π_{1} f (0))} \approx 1_{𝑜}) \to {Base}_{(J π_{1} f (0))} = \{[([0, 1] \times \{f (0)\})] ≃_{ph} (J)\}$
85	75 83 84	syl2anc	$⊢ (((J \in PConn \land Y \in X) \land {Base}_{(J π_{1} Y)} \approx 1_{𝑜}) \land (f \in (II Cn J) \land f (0) = f (1))) \to {Base}_{(J π_{1} f (0))} = \{[([0, 1] \times \{f (0)\})] ≃_{ph} (J)\}$
86	68 85	eleqtrd	$⊢ (((J \in PConn \land Y \in X) \land {Base}_{(J π_{1} Y)} \approx 1_{𝑜}) \land (f \in (II Cn J) \land f (0) = f (1))) \to [f] ≃_{ph} (J) \in \{[([0, 1] \times \{f (0)\})] ≃_{ph} (J)\}$
87		elsni	$⊢ [f] ≃_{ph} (J) \in \{[([0, 1] \times \{f (0)\})] ≃_{ph} (J)\} \to [f] ≃_{ph} (J) = [([0, 1] \times \{f (0)\})] ≃_{ph} (J)$
88	86 87	syl	$⊢ (((J \in PConn \land Y \in X) \land {Base}_{(J π_{1} Y)} \approx 1_{𝑜}) \land (f \in (II Cn J) \land f (0) = f (1))) \to [f] ≃_{ph} (J) = [([0, 1] \times \{f (0)\})] ≃_{ph} (J)$
89	13	a1i	$⊢ (((J \in PConn \land Y \in X) \land {Base}_{(J π_{1} Y)} \approx 1_{𝑜}) \land (f \in (II Cn J) \land f (0) = f (1))) \to ≃_{ph} (J) Er (II Cn J)$
90	89 58	erth	$⊢ (((J \in PConn \land Y \in X) \land {Base}_{(J π_{1} Y)} \approx 1_{𝑜}) \land (f \in (II Cn J) \land f (0) = f (1))) \to (f ≃_{ph} (J) ([0, 1] \times \{f (0)\}) \leftrightarrow [f] ≃_{ph} (J) = [([0, 1] \times \{f (0)\})] ≃_{ph} (J))$
91	88 90	mpbird	$⊢ (((J \in PConn \land Y \in X) \land {Base}_{(J π_{1} Y)} \approx 1_{𝑜}) \land (f \in (II Cn J) \land f (0) = f (1))) \to f ≃_{ph} (J) ([0, 1] \times \{f (0)\})$
92	91	expr	$⊢ (((J \in PConn \land Y \in X) \land {Base}_{(J π_{1} Y)} \approx 1_{𝑜}) \land f \in (II Cn J)) \to (f (0) = f (1) \to f ≃_{ph} (J) ([0, 1] \times \{f (0)\}))$
93	92	ralrimiva	$⊢ ((J \in PConn \land Y \in X) \land {Base}_{(J π_{1} Y)} \approx 1_{𝑜}) \to \forall f \in (II Cn J) (f (0) = f (1) \to f ≃_{ph} (J) ([0, 1] \times \{f (0)\}))$
94		issconn	$⊢ J \in SConn \leftrightarrow (J \in PConn \land \forall f \in (II Cn J) (f (0) = f (1) \to f ≃_{ph} (J) ([0, 1] \times \{f (0)\})))$
95	51 93 94	sylanbrc	$⊢ ((J \in PConn \land Y \in X) \land {Base}_{(J π_{1} Y)} \approx 1_{𝑜}) \to J \in SConn$
96	50 95	impbida	$⊢ (J \in PConn \land Y \in X) \to (J \in SConn \leftrightarrow {Base}_{(J π_{1} Y)} \approx 1_{𝑜})$

Metamath Proof Explorer

Theorem sconnpi1

Proof