defpred S1[ object , object ] means for i, j being Nat st $1 = [i,j] holds
$2 = [:{i},(Im ((Nbdl1 m),j)):] \/ [:(Im ((Nbdl1 n),i)),{j}:];
A1:
for x being object st x in [:(Seg n),(Seg m):] holds
ex y being object st
( y in bool [:(Seg n),(Seg m):] & S1[x,y] )
proof
let x be
object ;
( x in [:(Seg n),(Seg m):] implies ex y being object st
( y in bool [:(Seg n),(Seg m):] & S1[x,y] ) )
assume
x in [:(Seg n),(Seg m):]
;
ex y being object st
( y in bool [:(Seg n),(Seg m):] & S1[x,y] )
then consider u,
y being
object such that A2:
u in Seg n
and A3:
y in Seg m
and A4:
x = [u,y]
by ZFMISC_1:def 2;
reconsider i =
u,
j =
y as
Nat by A2, A3;
set y3 =
[:{i},(Im ((Nbdl1 m),j)):] \/ [:(Im ((Nbdl1 n),u)),{j}:];
A5:
[:{i},(Im ((Nbdl1 m),j)):] \/ [:(Im ((Nbdl1 n),u)),{j}:] c= [:(Seg n),(Seg m):]
proof
let z be
object ;
TARSKI:def 3 ( not z in [:{i},(Im ((Nbdl1 m),j)):] \/ [:(Im ((Nbdl1 n),u)),{j}:] or z in [:(Seg n),(Seg m):] )
assume A6:
z in [:{i},(Im ((Nbdl1 m),j)):] \/ [:(Im ((Nbdl1 n),u)),{j}:]
;
z in [:(Seg n),(Seg m):]
end;
for
i4,
j4 being
Nat st
x = [i4,j4] holds
[:{i},(Im ((Nbdl1 m),j)):] \/ [:(Im ((Nbdl1 n),u)),{j}:] = [:{i4},(Im ((Nbdl1 m),j4)):] \/ [:(Im ((Nbdl1 n),i4)),{j4}:]
proof
let i4,
j4 be
Nat;
( x = [i4,j4] implies [:{i},(Im ((Nbdl1 m),j)):] \/ [:(Im ((Nbdl1 n),u)),{j}:] = [:{i4},(Im ((Nbdl1 m),j4)):] \/ [:(Im ((Nbdl1 n),i4)),{j4}:] )
assume
x = [i4,j4]
;
[:{i},(Im ((Nbdl1 m),j)):] \/ [:(Im ((Nbdl1 n),u)),{j}:] = [:{i4},(Im ((Nbdl1 m),j4)):] \/ [:(Im ((Nbdl1 n),i4)),{j4}:]
then
(
i4 = u &
j4 = y )
by A4, XTUPLE_0:1;
hence
[:{i},(Im ((Nbdl1 m),j)):] \/ [:(Im ((Nbdl1 n),u)),{j}:] = [:{i4},(Im ((Nbdl1 m),j4)):] \/ [:(Im ((Nbdl1 n),i4)),{j4}:]
;
verum
end;
hence
ex
y being
object st
(
y in bool [:(Seg n),(Seg m):] &
S1[
x,
y] )
by A5;
verum
end;
consider f being Function of [:(Seg n),(Seg m):],(bool [:(Seg n),(Seg m):]) such that
A12:
for x being object st x in [:(Seg n),(Seg m):] holds
S1[x,f . x]
from FUNCT_2:sch 1(A1);
consider R being Relation of [:(Seg n),(Seg m):] such that
A13:
for i being set st i in [:(Seg n),(Seg m):] holds
Im (R,i) = f . i
by FUNCT_2:93;
take
R
; for x being set st x in [:(Seg n),(Seg m):] holds
for i, j being Nat st x = [i,j] holds
Im (R,x) = [:{i},(Im ((Nbdl1 m),j)):] \/ [:(Im ((Nbdl1 n),i)),{j}:]
let x be set ; ( x in [:(Seg n),(Seg m):] implies for i, j being Nat st x = [i,j] holds
Im (R,x) = [:{i},(Im ((Nbdl1 m),j)):] \/ [:(Im ((Nbdl1 n),i)),{j}:] )
assume A14:
x in [:(Seg n),(Seg m):]
; for i, j being Nat st x = [i,j] holds
Im (R,x) = [:{i},(Im ((Nbdl1 m),j)):] \/ [:(Im ((Nbdl1 n),i)),{j}:]
let i, j be Nat; ( x = [i,j] implies Im (R,x) = [:{i},(Im ((Nbdl1 m),j)):] \/ [:(Im ((Nbdl1 n),i)),{j}:] )
assume A15:
x = [i,j]
; Im (R,x) = [:{i},(Im ((Nbdl1 m),j)):] \/ [:(Im ((Nbdl1 n),i)),{j}:]
thus Im (R,x) =
f . x
by A13, A14
.=
[:{i},(Im ((Nbdl1 m),j)):] \/ [:(Im ((Nbdl1 n),i)),{j}:]
by A12, A14, A15
; verum