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 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | indistop | |
|
2 | simpl | |
|
3 | 0ex | |
|
4 | n0i | |
|
5 | prprc2 | |
|
6 | 5 | unieqd | |
7 | 3 | unisn | |
8 | 6 7 | eqtrdi | |
9 | 4 8 | nsyl2 | |
10 | 9 | adantr | |
11 | uniprg | |
|
12 | 3 10 11 | sylancr | |
13 | uncom | |
|
14 | un0 | |
|
15 | 13 14 | eqtri | |
16 | 12 15 | eqtrdi | |
17 | 2 16 | eleqtrd | |
18 | simpr | |
|
19 | 18 16 | eleqtrd | |
20 | 17 19 | ifcld | |
21 | 20 | adantr | |
22 | 21 | fmpttd | |
23 | ovex | |
|
24 | elmapg | |
|
25 | 10 23 24 | sylancl | |
26 | 22 25 | mpbird | |
27 | iitopon | |
|
28 | cnindis | |
|
29 | 27 10 28 | sylancr | |
30 | 26 29 | eleqtrrd | |
31 | 0elunit | |
|
32 | iftrue | |
|
33 | eqid | |
|
34 | vex | |
|
35 | 32 33 34 | fvmpt | |
36 | 31 35 | mp1i | |
37 | 1elunit | |
|
38 | ax-1ne0 | |
|
39 | neeq1 | |
|
40 | 38 39 | mpbiri | |
41 | ifnefalse | |
|
42 | 40 41 | syl | |
43 | vex | |
|
44 | 42 33 43 | fvmpt | |
45 | 37 44 | mp1i | |
46 | fveq1 | |
|
47 | 46 | eqeq1d | |
48 | fveq1 | |
|
49 | 48 | eqeq1d | |
50 | 47 49 | anbi12d | |
51 | 50 | rspcev | |
52 | 30 36 45 51 | syl12anc | |
53 | 52 | rgen2 | |
54 | eqid | |
|
55 | 54 | ispconn | |
56 | 1 53 55 | mpbir2an | |