defpred S1[ object , object ] means ex D1 being set st
( D1 = $1 & $2 in D1 );
let A be set ; ( A is mutually-disjoint & ( for a being set st a in A holds
ex x, y being Real st
( x < y & ].x,y.[ c= a ) ) implies A is countable )
assume A1:
for a, b being set st a in A & b in A & a <> b holds
a misses b
; TAXONOM2:def 5 ( ex a being set st
( a in A & ( for x, y being Real holds
( not x < y or not ].x,y.[ c= a ) ) ) or A is countable )
assume A2:
for a being set st a in A holds
ex x, y being Real st
( x < y & ].x,y.[ c= a )
; A is countable
A3:
now for a being object st a in A holds
ex q being object st
( q in RAT & S1[a,q] )let a be
object ;
( a in A implies ex q being object st
( q in RAT & S1[a,q] ) )reconsider aa =
a as
set by TARSKI:1;
assume
a in A
;
ex q being object st
( q in RAT & S1[a,q] )then consider x,
y being
Real such that A4:
x < y
and A5:
].x,y.[ c= aa
by A2;
consider q being
Rational such that A6:
x < q
and A7:
q < y
by A4, RAT_1:7;
A8:
q in RAT
by RAT_1:def 2;
q in ].x,y.[
by A6, A7, XXREAL_1:4;
hence
ex
q being
object st
(
q in RAT &
S1[
a,
q] )
by A5, A8;
verum end;
consider f being Function such that
A9:
( dom f = A & rng f c= RAT )
and
A10:
for a being object st a in A holds
S1[a,f . a]
from FUNCT_1:sch 6(A3);
f is one-to-one
proof
let a,
b be
object ;
FUNCT_1:def 4 ( not a in dom f or not b in dom f or not f . a = f . b or a = b )
assume that A11:
a in dom f
and A12:
b in dom f
and A13:
f . a = f . b
and A14:
a <> b
;
contradiction
reconsider a =
a,
b =
b as
set by TARSKI:1;
S1[
b,
f . b]
by A12, A9, A10;
then A15:
f . a in b
by A13;
S1[
a,
f . a]
by A11, A9, A10;
then A16:
f . a in a
;
a misses b
by A11, A12, A14, A1, A9;
hence
contradiction
by A16, A15, XBOOLE_0:3;
verum
end;
then
card A c= card RAT
by A9, CARD_1:10;
hence
A is countable
by Th17; verum