thus ( not IT is countable or IT is empty or ex F being sequence of D st IT = rng F ) :: thesis: ( ( IT is empty or ex F being sequence of D st IT = rng F ) implies IT is countable )
proof
assume that
A1: IT is countable and
A2: not IT is empty ; :: thesis: ex F being sequence of D st IT = rng F
consider f being Function such that
A3: dom f = NAT and
A4: IT c= rng f by A1, CARD_3:93;
consider x being Element of D such that
A5: x in IT by A2;
set F = (f | (f " IT)) +* ((NAT \ (f " IT)) --> x);
A6: ( rng ((f | (f " IT)) +* ((NAT \ (f " IT)) --> x)) = IT & dom ((f | (f " IT)) +* ((NAT \ (f " IT)) --> x)) = NAT )
proof
A7: f " IT c= NAT by A3, RELAT_1:132;
A8: dom (f | (f " IT)) = NAT /\ (f " IT) by A3, RELAT_1:61;
per cases ( NAT = f " IT or NAT <> f " IT ) ;
suppose A9: NAT = f " IT ; :: thesis: ( rng ((f | (f " IT)) +* ((NAT \ (f " IT)) --> x)) = IT & dom ((f | (f " IT)) +* ((NAT \ (f " IT)) --> x)) = NAT )
then A10: NAT \ (f " IT) = {} by XBOOLE_1:37;
then dom ((NAT \ (f " IT)) --> x) = {} ;
then dom (f | (f " IT)) misses dom ((NAT \ (f " IT)) --> x) ;
then (f | (f " IT)) +* ((NAT \ (f " IT)) --> x) = (f | (f " IT)) \/ ((NAT \ (f " IT)) --> x) by FUNCT_4:31;
hence rng ((f | (f " IT)) +* ((NAT \ (f " IT)) --> x)) = (rng (f | (f " IT))) \/ (rng ((NAT \ (f " IT)) --> x)) by RELAT_1:12
.= (rng (f | (f " IT))) \/ {} by A10
.= f .: (f " IT) by RELAT_1:115
.= IT by A4, FUNCT_1:77 ;
:: thesis: dom ((f | (f " IT)) +* ((NAT \ (f " IT)) --> x)) = NAT
thus dom ((f | (f " IT)) +* ((NAT \ (f " IT)) --> x)) = (dom (f | (f " IT))) \/ (dom ((NAT \ (f " IT)) --> x)) by FUNCT_4:def 1
.= (dom (f | (f " IT))) \/ {} by A10
.= NAT by A3, A9 ; :: thesis: verum
end;
suppose NAT <> f " IT ; :: thesis: ( rng ((f | (f " IT)) +* ((NAT \ (f " IT)) --> x)) = IT & dom ((f | (f " IT)) +* ((NAT \ (f " IT)) --> x)) = NAT )
then A11: not NAT \ (f " IT) is empty by A7, XBOOLE_1:37;
dom ((NAT \ (f " IT)) --> x) = NAT \ (f " IT) by FUNCOP_1:13;
then (f | (f " IT)) +* ((NAT \ (f " IT)) --> x) = (f | (f " IT)) \/ ((NAT \ (f " IT)) --> x) by A8, FUNCT_4:31, XBOOLE_1:89;
hence rng ((f | (f " IT)) +* ((NAT \ (f " IT)) --> x)) = (rng (f | (f " IT))) \/ (rng ((NAT \ (f " IT)) --> x)) by RELAT_1:12
.= (rng (f | (f " IT))) \/ {x} by A11, FUNCOP_1:8
.= (f .: (f " IT)) \/ {x} by RELAT_1:115
.= IT \/ {x} by A4, FUNCT_1:77
.= IT by A5, ZFMISC_1:40 ;
:: thesis: dom ((f | (f " IT)) +* ((NAT \ (f " IT)) --> x)) = NAT
thus dom ((f | (f " IT)) +* ((NAT \ (f " IT)) --> x)) = (dom (f | (f " IT))) \/ (dom ((NAT \ (f " IT)) --> x)) by FUNCT_4:def 1
.= (NAT /\ (f " IT)) \/ (NAT \ (f " IT)) by A8, FUNCOP_1:13
.= NAT by XBOOLE_1:51 ; :: thesis: verum
end;
end;
end;
then reconsider F = (f | (f " IT)) +* ((NAT \ (f " IT)) --> x) as sequence of D by FUNCT_2:def 1, RELSET_1:4;
take F ; :: thesis: IT = rng F
thus IT = rng F by A6; :: thesis: verum
end;
assume A12: ( IT is empty or ex F being sequence of D st IT = rng F ) ; :: thesis: IT is countable
per cases ( IT is empty or not IT is empty ) ;
suppose IT is empty ; :: thesis: IT is countable
hence IT is countable by CARD_4:1; :: thesis: verum
end;
suppose not IT is empty ; :: thesis: IT is countable
then consider F being sequence of D such that
A13: IT = rng F by A12;
dom F = NAT by FUNCT_2:def 1;
hence IT is countable by A13, CARD_3:93; :: thesis: verum
end;
end;