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 
|- { (/) , A } e. PConn

Proof

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