reconsider C = (y>=0-plane \ y=0-line) /\ (product <*RAT,RAT*>) as dense Subset of Niemytzki-plane by Th36;
set T = Niemytzki-plane ;
defpred S1[ object , object ] means ex D1 being set ex U, V being open Subset of Niemytzki-plane st
( D1 = $1 & $2 = U /\ C & D1 c= U & y=0-line \ D1 c= V & U misses V );
A1:
exp (2,omega) in exp (2,(exp (2,omega)))
by CARD_5:14;
card C c= card (product <*RAT,RAT*>)
by CARD_1:11, XBOOLE_1:17;
then
card C c= omega
by Th8, CARD_4:6, TOPGEN_3:17;
then A2:
exp (2,(card C)) c= exp (2,omega)
by CARD_2:93;
assume A3:
for W, V being Subset of Niemytzki-plane st W <> {} & V <> {} & W is closed & V is closed & W misses V holds
ex P, Q being Subset of Niemytzki-plane st
( P is open & Q is open & W c= P & V c= Q & P misses Q )
; COMPTS_1:def 3 contradiction
A4:
for a being object st a in bool y=0-line holds
ex b being object st S1[a,b]
consider G being Function such that
A14:
dom G = bool y=0-line
and
A15:
for a being object st a in bool y=0-line holds
S1[a,G . a]
from CLASSES1:sch 1(A4);
G is one-to-one
proof
let x,
y be
object ;
FUNCT_1:def 4 ( not x in proj1 G or not y in proj1 G or not G . x = G . y or x = y )
assume that A16:
x in dom G
and A17:
y in dom G
;
( not G . x = G . y or x = y )
reconsider A =
x,
B =
y as
Subset of
y=0-line by A16, A17, A14;
assume that A18:
G . x = G . y
and A19:
x <> y
;
contradiction
consider z being
object such that A20:
( (
z in A & not
z in B ) or (
z in B & not
z in A ) )
by A19, TARSKI:2;
A21:
(
z in A \ B or
z in B \ A )
by A20, XBOOLE_0:def 5;
consider D1 being
set ,
UB,
VB being
open Subset of
Niemytzki-plane such that A22:
D1 = B
and A23:
G . B = UB /\ C
and A24:
D1 c= UB
and A25:
y=0-line \ D1 c= VB
and A26:
UB misses VB
by A15;
consider D1 being
set ,
UA,
VA being
open Subset of
Niemytzki-plane such that A27:
D1 = A
and A28:
G . A = UA /\ C
and A29:
D1 c= UA
and A30:
y=0-line \ D1 c= VA
and A31:
UA misses VA
by A15;
B \ A = B /\ (A `)
by SUBSET_1:13;
then A32:
B \ A c= UB /\ VA
by A30, A24, XBOOLE_1:27, A22, A27;
A \ B = A /\ (B `)
by SUBSET_1:13;
then
A \ B c= UA /\ VB
by A29, A25, XBOOLE_1:27, A22, A27;
then
(
C meets UA /\ VB or
C meets UB /\ VA )
by A32, A21, TOPS_1:45;
then
( ex
z being
object st
(
z in C &
z in UA /\ VB ) or ex
z being
object st
(
z in C &
z in UB /\ VA ) )
by XBOOLE_0:3;
then consider z being
set such that A33:
z in C
and A34:
(
z in UA /\ VB or
z in UB /\ VA )
;
( (
z in UA &
z in VB ) or (
z in UB &
z in VA ) )
by A34, XBOOLE_0:def 4;
then
( (
z in UA & not
z in UB ) or (
z in UB & not
z in UA ) )
by A31, A26, XBOOLE_0:3;
then
( (
z in G . A & not
z in G . B ) or (
z in G . B & not
z in G . A ) )
by A28, A23, A33, XBOOLE_0:def 4;
hence
contradiction
by A18;
verum
end;
then A35:
card (dom G) c= card (rng G)
by CARD_1:10;
rng G c= bool C
then
card (rng G) c= card (bool C)
by CARD_1:11;
then
card (bool y=0-line) c= card (bool C)
by A35, A14;
then A38:
exp (2,continuum) c= card (bool C)
by Th16, CARD_2:31;
card (bool C) = exp (2,(card C))
by CARD_2:31;
then
exp (2,continuum) c= exp (2,omega)
by A38, A2;
then
exp (2,omega) in exp (2,omega)
by A1, TOPGEN_3:29;
hence
contradiction
; verum