df-sconn

Description: Define the class of simply connected topologies. A topology is simply connected if it is path-connected and every loop (continuous path with identical start and endpoint) is contractible to a point (path-homotopic to a constant function). (Contributed by Mario Carneiro, 11-Feb-2015)

		Ref	Expression
	Assertion	df-sconn	$⊢ SConn = \{j \in PConn \| \forall f \in (II Cn j) (f (0) = f (1) \to f ≃_{ph} (j) ([0, 1] \times \{f (0)\}))\}$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		csconn	$class SConn$
1		vj	$setvar j$
2		cpconn	$class PConn$
3		vf	$setvar f$
4		cii	$class II$
5		ccn	$class Cn$
6	1	cv	$setvar j$
7	4 6 5	co	$class (II Cn j)$
8	3	cv	$setvar f$
9		cc0	$class 0$
10	9 8	cfv	$class f (0)$
11		c1	$class 1$
12	11 8	cfv	$class f (1)$
13	10 12	wceq	$wff f (0) = f (1)$
14		cphtpc	$class ≃_{ph}$
15	6 14	cfv	$class ≃_{ph} (j)$
16		cicc	$class [.]$
17	9 11 16	co	$class [0, 1]$
18	10	csn	$class \{f (0)\}$
19	17 18	cxp	$class ([0, 1] \times \{f (0)\})$
20	8 19 15	wbr	$wff f ≃_{ph} (j) ([0, 1] \times \{f (0)\})$
21	13 20	wi	$wff (f (0) = f (1) \to f ≃_{ph} (j) ([0, 1] \times \{f (0)\}))$
22	21 3 7	wral	$wff \forall f \in (II Cn j) (f (0) = f (1) \to f ≃_{ph} (j) ([0, 1] \times \{f (0)\}))$
23	22 1 2	crab	$class \{j \in PConn \| \forall f \in (II Cn j) (f (0) = f (1) \to f ≃_{ph} (j) ([0, 1] \times \{f (0)\}))\}$
24	0 23	wceq	$wff SConn = \{j \in PConn \| \forall f \in (II Cn j) (f (0) = f (1) \to f ≃_{ph} (j) ([0, 1] \times \{f (0)\}))\}$

Metamath Proof Explorer

Definition df-sconn

Detailed syntax breakdown