indispconn

Description: The indiscrete topology (or trivial topology) on any set is path-connected. (Contributed by Mario Carneiro, 7-Jul-2015) (Revised by Mario Carneiro, 14-Aug-2015)

		Ref	Expression
	Assertion	indispconn	$⊢ \{\emptyset, A\} \in PConn$

Proof

Step	Hyp	Ref	Expression
1		indistop	$⊢ \{\emptyset, A\} \in Top$
2		simpl	$⊢ (x \in ⋃ \{\emptyset, A\} \land y \in ⋃ \{\emptyset, A\}) \to x \in ⋃ \{\emptyset, A\}$
3		0ex	$⊢ \emptyset \in V$
4		n0i	$⊢ x \in ⋃ \{\emptyset, A\} \to \neg ⋃ \{\emptyset, A\} = \emptyset$
5		prprc2	$⊢ \neg A \in V \to \{\emptyset, A\} = \{\emptyset\}$
6	5	unieqd	$⊢ \neg A \in V \to ⋃ \{\emptyset, A\} = ⋃ \{\emptyset\}$
7	3	unisn	$⊢ ⋃ \{\emptyset\} = \emptyset$
8	6 7	eqtrdi	$⊢ \neg A \in V \to ⋃ \{\emptyset, A\} = \emptyset$
9	4 8	nsyl2	$⊢ x \in ⋃ \{\emptyset, A\} \to A \in V$
10	9	adantr	$⊢ (x \in ⋃ \{\emptyset, A\} \land y \in ⋃ \{\emptyset, A\}) \to A \in V$
11		uniprg	$⊢ (\emptyset \in V \land A \in V) \to ⋃ \{\emptyset, A\} = \emptyset \cup A$
12	3 10 11	sylancr	$⊢ (x \in ⋃ \{\emptyset, A\} \land y \in ⋃ \{\emptyset, A\}) \to ⋃ \{\emptyset, A\} = \emptyset \cup A$
13		uncom	$⊢ \emptyset \cup A = A \cup \emptyset$
14		un0	$⊢ A \cup \emptyset = A$
15	13 14	eqtri	$⊢ \emptyset \cup A = A$
16	12 15	eqtrdi	$⊢ (x \in ⋃ \{\emptyset, A\} \land y \in ⋃ \{\emptyset, A\}) \to ⋃ \{\emptyset, A\} = A$
17	2 16	eleqtrd	$⊢ (x \in ⋃ \{\emptyset, A\} \land y \in ⋃ \{\emptyset, A\}) \to x \in A$
18		simpr	$⊢ (x \in ⋃ \{\emptyset, A\} \land y \in ⋃ \{\emptyset, A\}) \to y \in ⋃ \{\emptyset, A\}$
19	18 16	eleqtrd	$⊢ (x \in ⋃ \{\emptyset, A\} \land y \in ⋃ \{\emptyset, A\}) \to y \in A$
20	17 19	ifcld	$⊢ (x \in ⋃ \{\emptyset, A\} \land y \in ⋃ \{\emptyset, A\}) \to if (z = 0, x, y) \in A$
21	20	adantr	$⊢ ((x \in ⋃ \{\emptyset, A\} \land y \in ⋃ \{\emptyset, A\}) \land z \in [0, 1]) \to if (z = 0, x, y) \in A$
22	21	fmpttd	$⊢ (x \in ⋃ \{\emptyset, A\} \land y \in ⋃ \{\emptyset, A\}) \to (z \in [0, 1] ⟼ if (z = 0, x, y)) : [0, 1] ⟶ A$
23		ovex	$⊢ [0, 1] \in V$
24		elmapg	$⊢ (A \in V \land [0, 1] \in V) \to ((z \in [0, 1] ⟼ if (z = 0, x, y)) \in (A^{[0, 1]}) \leftrightarrow (z \in [0, 1] ⟼ if (z = 0, x, y)) : [0, 1] ⟶ A)$
25	10 23 24	sylancl	$⊢ (x \in ⋃ \{\emptyset, A\} \land y \in ⋃ \{\emptyset, A\}) \to ((z \in [0, 1] ⟼ if (z = 0, x, y)) \in (A^{[0, 1]}) \leftrightarrow (z \in [0, 1] ⟼ if (z = 0, x, y)) : [0, 1] ⟶ A)$
26	22 25	mpbird	$⊢ (x \in ⋃ \{\emptyset, A\} \land y \in ⋃ \{\emptyset, A\}) \to (z \in [0, 1] ⟼ if (z = 0, x, y)) \in (A^{[0, 1]})$
27		iitopon	$⊢ II \in TopOn ([0, 1])$
28		cnindis	$⊢ (II \in TopOn ([0, 1]) \land A \in V) \to II Cn \{\emptyset, A\} = A^{[0, 1]}$
29	27 10 28	sylancr	$⊢ (x \in ⋃ \{\emptyset, A\} \land y \in ⋃ \{\emptyset, A\}) \to II Cn \{\emptyset, A\} = A^{[0, 1]}$
30	26 29	eleqtrrd	$⊢ (x \in ⋃ \{\emptyset, A\} \land y \in ⋃ \{\emptyset, A\}) \to (z \in [0, 1] ⟼ if (z = 0, x, y)) \in (II Cn \{\emptyset, A\})$
31		0elunit	$⊢ 0 \in [0, 1]$
32		iftrue	$⊢ z = 0 \to if (z = 0, x, y) = x$
33		eqid	$⊢ (z \in [0, 1] ⟼ if (z = 0, x, y)) = (z \in [0, 1] ⟼ if (z = 0, x, y))$
34		vex	$⊢ x \in V$
35	32 33 34	fvmpt	$⊢ 0 \in [0, 1] \to (z \in [0, 1] ⟼ if (z = 0, x, y)) (0) = x$
36	31 35	mp1i	$⊢ (x \in ⋃ \{\emptyset, A\} \land y \in ⋃ \{\emptyset, A\}) \to (z \in [0, 1] ⟼ if (z = 0, x, y)) (0) = x$
37		1elunit	$⊢ 1 \in [0, 1]$
38		ax-1ne0	$⊢ 1 \neq 0$
39		neeq1	$⊢ z = 1 \to (z \neq 0 \leftrightarrow 1 \neq 0)$
40	38 39	mpbiri	$⊢ z = 1 \to z \neq 0$
41		ifnefalse	$⊢ z \neq 0 \to if (z = 0, x, y) = y$
42	40 41	syl	$⊢ z = 1 \to if (z = 0, x, y) = y$
43		vex	$⊢ y \in V$
44	42 33 43	fvmpt	$⊢ 1 \in [0, 1] \to (z \in [0, 1] ⟼ if (z = 0, x, y)) (1) = y$
45	37 44	mp1i	$⊢ (x \in ⋃ \{\emptyset, A\} \land y \in ⋃ \{\emptyset, A\}) \to (z \in [0, 1] ⟼ if (z = 0, x, y)) (1) = y$
46		fveq1	$⊢ f = (z \in [0, 1] ⟼ if (z = 0, x, y)) \to f (0) = (z \in [0, 1] ⟼ if (z = 0, x, y)) (0)$
47	46	eqeq1d	$⊢ f = (z \in [0, 1] ⟼ if (z = 0, x, y)) \to (f (0) = x \leftrightarrow (z \in [0, 1] ⟼ if (z = 0, x, y)) (0) = x)$
48		fveq1	$⊢ f = (z \in [0, 1] ⟼ if (z = 0, x, y)) \to f (1) = (z \in [0, 1] ⟼ if (z = 0, x, y)) (1)$
49	48	eqeq1d	$⊢ f = (z \in [0, 1] ⟼ if (z = 0, x, y)) \to (f (1) = y \leftrightarrow (z \in [0, 1] ⟼ if (z = 0, x, y)) (1) = y)$
50	47 49	anbi12d	$⊢ f = (z \in [0, 1] ⟼ if (z = 0, x, y)) \to ((f (0) = x \land f (1) = y) \leftrightarrow ((z \in [0, 1] ⟼ if (z = 0, x, y)) (0) = x \land (z \in [0, 1] ⟼ if (z = 0, x, y)) (1) = y))$
51	50	rspcev	$⊢ ((z \in [0, 1] ⟼ if (z = 0, x, y)) \in (II Cn \{\emptyset, A\}) \land ((z \in [0, 1] ⟼ if (z = 0, x, y)) (0) = x \land (z \in [0, 1] ⟼ if (z = 0, x, y)) (1) = y)) \to \exists f \in (II Cn \{\emptyset, A\}) (f (0) = x \land f (1) = y)$
52	30 36 45 51	syl12anc	$⊢ (x \in ⋃ \{\emptyset, A\} \land y \in ⋃ \{\emptyset, A\}) \to \exists f \in (II Cn \{\emptyset, A\}) (f (0) = x \land f (1) = y)$
53	52	rgen2	$⊢ \forall x \in ⋃ \{\emptyset, A\} \forall y \in ⋃ \{\emptyset, A\} \exists f \in (II Cn \{\emptyset, A\}) (f (0) = x \land f (1) = y)$
54		eqid	$⊢ ⋃ \{\emptyset, A\} = ⋃ \{\emptyset, A\}$
55	54	ispconn	$⊢ \{\emptyset, A\} \in PConn \leftrightarrow (\{\emptyset, A\} \in Top \land \forall x \in ⋃ \{\emptyset, A\} \forall y \in ⋃ \{\emptyset, A\} \exists f \in (II Cn \{\emptyset, A\}) (f (0) = x \land f (1) = y))$
56	1 53 55	mpbir2an	$⊢ \{\emptyset, A\} \in PConn$

Metamath Proof Explorer

Theorem indispconn

Proof