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 )
proof
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;
reconsider j0 = 0 , j1 = 1 as Element of (1TopSp {0,1}) by A1, TARSKI:def 2;
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 H1( object ) -> Element of (1TopSp {0,1}) = j1;
deffunc H2( 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 S1[ object ] means $1 in A;
A13: for x being object st x in the carrier of T holds
( ( S1[x] implies H2(x) in the carrier of (1TopSp {0,1}) ) & ( not S1[x] implies H1(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
( ( S1[x] implies f . x = H2(x) ) & ( not S1[x] implies f . x = H1(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
proof
hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: B c= 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 S1[x] by A14;
hence x in B by A8, A17, XBOOLE_0:def 3; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in B or x in f " Y )
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
proof
hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: A c= 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;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A or x in f " X )
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})
proof
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
per cases ( y = 0 or y = 1 ) by A1, A23, TARSKI:def 2;
end;
end;
then ( f " ({} (1TopSp {0,1})) = {} T & f " ([#] (1TopSp {0,1})) = [#] T ) by A15, RELAT_1:134;
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