set X = {0};

set Y = {1};

set J = 1TopSp {0,1};

let T be non empty TopSpace; :: thesis: ( T is connected iff for f being Function of T,(1TopSp {0,1}) holds

( not f is continuous or not f is onto ) )

A1: the carrier of (1TopSp {0,1}) = {0,1} by PCOMPS_1:5;

then reconsider X = {0}, Y = {1} as non empty open Subset of (1TopSp {0,1}) by TDLAT_3:15, ZFMISC_1:7;

thus ( T is connected implies for f being Function of T,(1TopSp {0,1}) holds

( not f is continuous or not f is onto ) ) :: thesis: ( ( for f being Function of T,(1TopSp {0,1}) holds

( not f is continuous or not f is onto ) ) implies T is connected )

assume A7: for f being Function of T,(1TopSp {0,1}) holds

( not f is continuous or not f is onto ) ; :: thesis: T is connected

deffunc H_{1}( object ) -> Element of (1TopSp {0,1}) = j1;

deffunc H_{2}( object ) -> Element of (1TopSp {0,1}) = j0;

assume not T is connected ; :: thesis: contradiction

then consider A, B being Subset of T such that

A8: [#] T = A \/ B and

A9: A <> {} T and

A10: B <> {} T and

A11: ( A is open & B is open ) and

A12: A misses B by CONNSP_1:11;

defpred S_{1}[ object ] means $1 in A;

A13: for x being object st x in the carrier of T holds

( ( S_{1}[x] implies H_{2}(x) in the carrier of (1TopSp {0,1}) ) & ( not S_{1}[x] implies H_{1}(x) in the carrier of (1TopSp {0,1}) ) )
;

consider f being Function of the carrier of T, the carrier of (1TopSp {0,1}) such that

A14: for x being object st x in the carrier of T holds

( ( S_{1}[x] implies f . x = H_{2}(x) ) & ( not S_{1}[x] implies f . x = H_{1}(x) ) )
from FUNCT_2:sch 5(A13);

reconsider f = f as Function of T,(1TopSp {0,1}) ;

A15: dom f = the carrier of T by FUNCT_2:def 1;

A16: f " Y = B

then ( [#] (1TopSp {0,1}) <> {} & ( for P being Subset of (1TopSp {0,1}) st P is open holds

f " P is open ) ) by A1, A11, A19, A16, ZFMISC_1:36;

then A30: f is continuous by TOPS_2:43;

f is onto by A22;

hence contradiction by A7, A30; :: thesis: verum

set Y = {1};

set J = 1TopSp {0,1};

let T be non empty TopSpace; :: thesis: ( T is connected iff for f being Function of T,(1TopSp {0,1}) holds

( not f is continuous or not f is onto ) )

A1: the carrier of (1TopSp {0,1}) = {0,1} by PCOMPS_1:5;

then reconsider X = {0}, Y = {1} as non empty open Subset of (1TopSp {0,1}) by TDLAT_3:15, ZFMISC_1:7;

thus ( T is connected implies for f being Function of T,(1TopSp {0,1}) holds

( not f is continuous or not f is onto ) ) :: thesis: ( ( for f being Function of T,(1TopSp {0,1}) holds

( not f is continuous or not f is onto ) ) implies T is connected )

proof

reconsider j0 = 0 , j1 = 1 as Element of (1TopSp {0,1}) by A1, TARSKI:def 2;
assume A2:
T is connected
; :: thesis: for f being Function of T,(1TopSp {0,1}) holds

( not f is continuous or not f is onto )

given f being Function of T,(1TopSp {0,1}) such that A3: f is continuous and

A4: f is onto ; :: thesis: contradiction

set A = f " X;

set B = f " Y;

rng f = the carrier of (1TopSp {0,1}) by A4;

then A5: ( f " X <> {} T & f " Y <> {} T ) by RELAT_1:139;

A6: ( the carrier of T = (f " X) \/ (f " Y) & f " X misses f " Y ) by A1, Th3, FUNCT_1:71, ZFMISC_1:11;

[#] (1TopSp {0,1}) <> {} ;

then ( f " X is open & f " Y is open ) by A3, TOPS_2:43;

hence contradiction by A2, A5, A6, CONNSP_1:11; :: thesis: verum

end;( not f is continuous or not f is onto )

given f being Function of T,(1TopSp {0,1}) such that A3: f is continuous and

A4: f is onto ; :: thesis: contradiction

set A = f " X;

set B = f " Y;

rng f = the carrier of (1TopSp {0,1}) by A4;

then A5: ( f " X <> {} T & f " Y <> {} T ) by RELAT_1:139;

A6: ( the carrier of T = (f " X) \/ (f " Y) & f " X misses f " Y ) by A1, Th3, FUNCT_1:71, ZFMISC_1:11;

[#] (1TopSp {0,1}) <> {} ;

then ( f " X is open & f " Y is open ) by A3, TOPS_2:43;

hence contradiction by A2, A5, A6, CONNSP_1:11; :: thesis: verum

assume A7: for f being Function of T,(1TopSp {0,1}) holds

( not f is continuous or not f is onto ) ; :: thesis: T is connected

deffunc H

deffunc H

assume not T is connected ; :: thesis: contradiction

then consider A, B being Subset of T such that

A8: [#] T = A \/ B and

A9: A <> {} T and

A10: B <> {} T and

A11: ( A is open & B is open ) and

A12: A misses B by CONNSP_1:11;

defpred S

A13: for x being object st x in the carrier of T holds

( ( S

consider f being Function of the carrier of T, the carrier of (1TopSp {0,1}) such that

A14: for x being object st x in the carrier of T holds

( ( S

reconsider f = f as Function of T,(1TopSp {0,1}) ;

A15: dom f = the carrier of T by FUNCT_2:def 1;

A16: f " Y = B

proof

assume A18: x in B ; :: thesis: x in f " Y

then not x in A by A12, XBOOLE_0:3;

then f . x = 1 by A14, A18;

then f . x in Y by TARSKI:def 1;

hence x in f " Y by A15, A18, FUNCT_1:def 7; :: thesis: verum

end;

A19:
f " X = A
hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: B c= f " Y

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in B or x in f " Y )let x be object ; :: thesis: ( x in f " Y implies x in B )

assume A17: x in f " Y ; :: thesis: x in B

then f . x in Y by FUNCT_1:def 7;

then f . x = 1 by TARSKI:def 1;

then not S_{1}[x]
by A14;

hence x in B by A8, A17, XBOOLE_0:def 3; :: thesis: verum

end;assume A17: x in f " Y ; :: thesis: x in B

then f . x in Y by FUNCT_1:def 7;

then f . x = 1 by TARSKI:def 1;

then not S

hence x in B by A8, A17, XBOOLE_0:def 3; :: thesis: verum

assume A18: x in B ; :: thesis: x in f " Y

then not x in A by A12, XBOOLE_0:3;

then f . x = 1 by A14, A18;

then f . x in Y by TARSKI:def 1;

hence x in f " Y by A15, A18, FUNCT_1:def 7; :: thesis: verum

proof

assume A21: x in A ; :: thesis: x in f " X

then f . x = 0 by A14;

then f . x in X by TARSKI:def 1;

hence x in f " X by A15, A21, FUNCT_1:def 7; :: thesis: verum

end;

A22:
rng f = the carrier of (1TopSp {0,1})
hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: A c= f " X

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A or x in f " X )let x be object ; :: thesis: ( x in f " X implies x in A )

assume A20: x in f " X ; :: thesis: x in A

then f . x in X by FUNCT_1:def 7;

then f . x = 0 by TARSKI:def 1;

hence x in A by A14, A20; :: thesis: verum

end;assume A20: x in f " X ; :: thesis: x in A

then f . x in X by FUNCT_1:def 7;

then f . x = 0 by TARSKI:def 1;

hence x in A by A14, A20; :: thesis: verum

assume A21: x in A ; :: thesis: x in f " X

then f . x = 0 by A14;

then f . x in X by TARSKI:def 1;

hence x in f " X by A15, A21, FUNCT_1:def 7; :: thesis: verum

proof

then
( f " ({} (1TopSp {0,1})) = {} T & f " ([#] (1TopSp {0,1})) = [#] T )
by A15, RELAT_1:134;
thus
rng f c= the carrier of (1TopSp {0,1})
; :: according to XBOOLE_0:def 10 :: thesis: the carrier of (1TopSp {0,1}) c= rng f

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in the carrier of (1TopSp {0,1}) or y in rng f )

assume A23: y in the carrier of (1TopSp {0,1}) ; :: thesis: y in rng f

end;let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in the carrier of (1TopSp {0,1}) or y in rng f )

assume A23: y in the carrier of (1TopSp {0,1}) ; :: thesis: y in rng f

per cases
( y = 0 or y = 1 )
by A1, A23, TARSKI:def 2;

end;

suppose A24:
y = 0
; :: thesis: y in rng f

consider x being object such that

A25: x in f " X by A9, A19, XBOOLE_0:def 1;

f . x in X by A25, FUNCT_1:def 7;

then A26: f . x = 0 by TARSKI:def 1;

x in dom f by A25, FUNCT_1:def 7;

hence y in rng f by A24, A26, FUNCT_1:def 3; :: thesis: verum

end;A25: x in f " X by A9, A19, XBOOLE_0:def 1;

f . x in X by A25, FUNCT_1:def 7;

then A26: f . x = 0 by TARSKI:def 1;

x in dom f by A25, FUNCT_1:def 7;

hence y in rng f by A24, A26, FUNCT_1:def 3; :: thesis: verum

suppose A27:
y = 1
; :: thesis: y in rng f

consider x being object such that

A28: x in f " Y by A10, A16, XBOOLE_0:def 1;

f . x in Y by A28, FUNCT_1:def 7;

then A29: f . x = 1 by TARSKI:def 1;

x in dom f by A28, FUNCT_1:def 7;

hence y in rng f by A27, A29, FUNCT_1:def 3; :: thesis: verum

end;A28: x in f " Y by A10, A16, XBOOLE_0:def 1;

f . x in Y by A28, FUNCT_1:def 7;

then A29: f . x = 1 by TARSKI:def 1;

x in dom f by A28, FUNCT_1:def 7;

hence y in rng f by A27, A29, FUNCT_1:def 3; :: thesis: verum

then ( [#] (1TopSp {0,1}) <> {} & ( for P being Subset of (1TopSp {0,1}) st P is open holds

f " P is open ) ) by A1, A11, A19, A16, ZFMISC_1:36;

then A30: f is continuous by TOPS_2:43;

f is onto by A22;

hence contradiction by A7, A30; :: thesis: verum