Metamath Proof Explorer


Theorem 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 APConn

Proof

Step Hyp Ref Expression
1 indistop ATop
2 simpl xAyAxA
3 0ex V
4 n0i xA¬A=
5 prprc2 ¬AVA=
6 5 unieqd ¬AVA=
7 3 unisn =
8 6 7 eqtrdi ¬AVA=
9 4 8 nsyl2 xAAV
10 9 adantr xAyAAV
11 uniprg VAVA=A
12 3 10 11 sylancr xAyAA=A
13 uncom A=A
14 un0 A=A
15 13 14 eqtri A=A
16 12 15 eqtrdi xAyAA=A
17 2 16 eleqtrd xAyAxA
18 simpr xAyAyA
19 18 16 eleqtrd xAyAyA
20 17 19 ifcld xAyAifz=0xyA
21 20 adantr xAyAz01ifz=0xyA
22 21 fmpttd xAyAz01ifz=0xy:01A
23 ovex 01V
24 elmapg AV01Vz01ifz=0xyA01z01ifz=0xy:01A
25 10 23 24 sylancl xAyAz01ifz=0xyA01z01ifz=0xy:01A
26 22 25 mpbird xAyAz01ifz=0xyA01
27 iitopon IITopOn01
28 cnindis IITopOn01AVIICnA=A01
29 27 10 28 sylancr xAyAIICnA=A01
30 26 29 eleqtrrd xAyAz01ifz=0xyIICnA
31 0elunit 001
32 iftrue z=0ifz=0xy=x
33 eqid z01ifz=0xy=z01ifz=0xy
34 vex xV
35 32 33 34 fvmpt 001z01ifz=0xy0=x
36 31 35 mp1i xAyAz01ifz=0xy0=x
37 1elunit 101
38 ax-1ne0 10
39 neeq1 z=1z010
40 38 39 mpbiri z=1z0
41 ifnefalse z0ifz=0xy=y
42 40 41 syl z=1ifz=0xy=y
43 vex yV
44 42 33 43 fvmpt 101z01ifz=0xy1=y
45 37 44 mp1i xAyAz01ifz=0xy1=y
46 fveq1 f=z01ifz=0xyf0=z01ifz=0xy0
47 46 eqeq1d f=z01ifz=0xyf0=xz01ifz=0xy0=x
48 fveq1 f=z01ifz=0xyf1=z01ifz=0xy1
49 48 eqeq1d f=z01ifz=0xyf1=yz01ifz=0xy1=y
50 47 49 anbi12d f=z01ifz=0xyf0=xf1=yz01ifz=0xy0=xz01ifz=0xy1=y
51 50 rspcev z01ifz=0xyIICnAz01ifz=0xy0=xz01ifz=0xy1=yfIICnAf0=xf1=y
52 30 36 45 51 syl12anc xAyAfIICnAf0=xf1=y
53 52 rgen2 xAyAfIICnAf0=xf1=y
54 eqid A=A
55 54 ispconn APConnATopxAyAfIICnAf0=xf1=y
56 1 53 55 mpbir2an APConn