let G be finite set ; card { {x,[y,(union G)]} where x, y is Element of union G : {x,y} in PairsOf G } = 2 * (card (PairsOf G))
set Y = union G;
set A = { {x,[y,(union G)]} where x, y is Element of union G : {x,y} in PairsOf G } ;
set EG = PairsOf G;
set uG = union G;
set s = canFS (PairsOf G);
A1:
len (canFS (PairsOf G)) = card (PairsOf G)
by FINSEQ_1:93;
A2:
rng (canFS (PairsOf G)) = PairsOf G
by FUNCT_2:def 3;
defpred S1[ object , object ] means for a, b being set st $1 = {a,b} holds
$2 = {{a,[b,(union G)]},{b,[a,(union G)]}};
A3:
for x, y1, y2 being object st x in PairsOf G & S1[x,y1] & S1[x,y2] holds
y1 = y2
proof
let x,
v1,
v2 be
object ;
( x in PairsOf G & S1[x,v1] & S1[x,v2] implies v1 = v2 )
assume that A4:
x in PairsOf G
and A5:
S1[
x,
v1]
and A6:
S1[
x,
v2]
;
v1 = v2
consider x1,
y1 being
set such that
x1 <> y1
and
x1 in union G
and
y1 in union G
and A7:
x = {x1,y1}
by A4, Th11;
v2 = {{x1,[y1,(union G)]},{y1,[x1,(union G)]}}
by A7, A6;
hence
v1 = v2
by A7, A5;
verum
end;
A8:
for x being object st x in PairsOf G holds
ex y being object st S1[x,y]
proof
let x be
object ;
( x in PairsOf G implies ex y being object st S1[x,y] )
assume
x in PairsOf G
;
ex y being object st S1[x,y]
then consider x1,
y1 being
set such that
x1 <> y1
and
x1 in union G
and
y1 in union G
and A9:
x = {x1,y1}
by Th11;
take y =
{{x1,[y1,(union G)]},{y1,[x1,(union G)]}};
S1[x,y]
let a,
b be
set ;
( x = {a,b} implies y = {{a,[b,(union G)]},{b,[a,(union G)]}} )
assume
x = {a,b}
;
y = {{a,[b,(union G)]},{b,[a,(union G)]}}
then
( (
a = x1 &
b = y1 ) or (
a = y1 &
b = x1 ) )
by A9, ZFMISC_1:6;
hence
y = {{a,[b,(union G)]},{b,[a,(union G)]}}
;
verum
end;
consider f being Function such that
A10:
dom f = PairsOf G
and
A11:
for x being object st x in PairsOf G holds
S1[x,f . x]
from FUNCT_1:sch 2(A3, A8);
now for y being set st y in rng (f * (canFS (PairsOf G))) holds
y is finite let y be
set ;
( y in rng (f * (canFS (PairsOf G))) implies y is finite )assume
y in rng (f * (canFS (PairsOf G)))
;
y is finite then
y in rng f
by FUNCT_1:14;
then consider x being
object such that A12:
x in dom f
and A13:
y = f . x
by FUNCT_1:def 3;
consider x1,
y1 being
set such that
x1 <> y1
and
x1 in union G
and
y1 in union G
and A14:
x = {x1,y1}
by A12, A10, Th11;
y = {{x1,[y1,(union G)]},{y1,[x1,(union G)]}}
by A14, A13, A12, A10, A11;
hence
y is
finite
;
verum end;
then reconsider S = f * (canFS (PairsOf G)) as V40() FinSequence by A2, A10, FINSEQ_1:16, FINSET_1:def 2;
A15:
dom S = dom (canFS (PairsOf G))
by A2, A10, RELAT_1:27;
deffunc H1( set ) -> Element of NAT = card (S . $1);
consider L being FinSequence of NAT such that
A16:
len L = len S
and
A17:
for j being Nat st j in dom L holds
L . j = H1(j)
from FINSEQ_2:sch 1();
A18:
dom S = dom L
by A16, FINSEQ_3:29;
A19:
for i being Nat st i in dom S holds
( S . i is finite & L . i = card (S . i) )
by A18, A17;
now for x, y being object st x <> y holds
not S . x meets S . ylet x,
y be
object ;
( x <> y implies not S . b1 meets S . b2 )assume A20:
x <> y
;
not S . b1 meets S . b2per cases
( ( x in dom S & y in dom S ) or not x in dom S or not y in dom S )
;
suppose that A21:
x in dom S
and A22:
y in dom S
;
not S . b1 meets S . b2A23:
(
x in dom (canFS (PairsOf G)) &
(canFS (PairsOf G)) . x in dom f )
by A21, FUNCT_1:11;
A24:
(
y in dom (canFS (PairsOf G)) &
(canFS (PairsOf G)) . y in dom f )
by A22, FUNCT_1:11;
consider x1,
y1 being
set such that
x1 <> y1
and A25:
(
x1 in union G &
y1 in union G )
and A26:
(canFS (PairsOf G)) . x = {x1,y1}
by A23, A10, Th11;
consider x2,
y2 being
set such that
x2 <> y2
and A27:
(
x2 in union G &
y2 in union G )
and A28:
(canFS (PairsOf G)) . y = {x2,y2}
by A24, A10, Th11;
A29:
S . x = f . ((canFS (PairsOf G)) . x)
by A21, FUNCT_1:12;
A30:
S . y = f . ((canFS (PairsOf G)) . y)
by A22, FUNCT_1:12;
A31:
S . x = {{x1,[y1,(union G)]},{y1,[x1,(union G)]}}
by A26, A29, A23, A10, A11;
A32:
S . y = {{x2,[y2,(union G)]},{y2,[x2,(union G)]}}
by A28, A30, A24, A10, A11;
assume
S . x meets S . y
;
contradictionthen consider a being
object such that A33:
a in S . x
and A34:
a in S . y
by XBOOLE_0:3;
A35:
(
a = {x1,[y1,(union G)]} or
a = {y1,[x1,(union G)]} )
by A33, A31, TARSKI:def 2;
A36:
(
a = {x2,[y2,(union G)]} or
a = {y2,[x2,(union G)]} )
by A34, A32, TARSKI:def 2;
( (
x1 = x2 &
y1 = y2 ) or (
x1 = y2 &
y1 = x2 ) or (
y1 = x2 &
x1 = y2 ) )
by A25, A27, A35, A36, Th4;
hence
contradiction
by A26, A28, A20, A23, A24, FUNCT_1:def 4;
verum end; end;
then A37:
S is disjoint_valued
by PROB_2:def 2;
Union S = union (rng S)
;
then A38:
card (union (rng S)) = Sum L
by A18, A19, A37, DIST_1:17;
A39: dom ((len L) |-> 2) =
Seg (len L)
by FUNCOP_1:13
.=
dom L
by FINSEQ_1:def 3
;
now for j being Nat st j in dom L holds
L . j = ((len L) |-> 2) . jlet j be
Nat;
( j in dom L implies L . j = ((len L) |-> 2) . j )assume A40:
j in dom L
;
L . j = ((len L) |-> 2) . jA41:
S . j = f . ((canFS (PairsOf G)) . j)
by A40, A18, FUNCT_1:12;
consider x,
y being
set such that A42:
x <> y
and
x in union G
and
y in union G
and A43:
(canFS (PairsOf G)) . j = {x,y}
by Th11, A40, A18, A15, A2, FUNCT_1:3;
A44:
f . ((canFS (PairsOf G)) . j) = {{x,[y,(union G)]},{y,[x,(union G)]}}
by A43, A11, A40, A18, A15, A2, FUNCT_1:3;
A46:
j in Seg (len L)
by A40, FINSEQ_1:def 3;
thus L . j =
card (S . j)
by A40, A17
.=
2
by A45, A44, A41, CARD_2:57
.=
((len L) |-> 2) . j
by A46, FINSEQ_2:57
;
verum end;
then A47:
L = (len L) |-> 2
by A39;
A48:
len L = card (PairsOf G)
by A16, A15, A1, FINSEQ_3:29;
union (rng S) = { {x,[y,(union G)]} where x, y is Element of union G : {x,y} in PairsOf G }
proof
thus
union (rng S) c= { {x,[y,(union G)]} where x, y is Element of union G : {x,y} in PairsOf G }
XBOOLE_0:def 10 { {x,[y,(union G)]} where x, y is Element of union G : {x,y} in PairsOf G } c= union (rng S)proof
let a be
object ;
TARSKI:def 3 ( not a in union (rng S) or a in { {x,[y,(union G)]} where x, y is Element of union G : {x,y} in PairsOf G } )
assume
a in union (rng S)
;
a in { {x,[y,(union G)]} where x, y is Element of union G : {x,y} in PairsOf G }
then consider YY being
set such that A49:
a in YY
and A50:
YY in rng S
by TARSKI:def 4;
consider b being
object such that A51:
b in dom S
and A52:
YY = S . b
by A50, FUNCT_1:def 3;
A53:
S . b = f . ((canFS (PairsOf G)) . b)
by A51, FUNCT_1:12;
A54:
(canFS (PairsOf G)) . b in PairsOf G
by A51, A15, A2, FUNCT_1:3;
consider x,
y being
set such that
x <> y
and A55:
x in union G
and A56:
y in union G
and A57:
(canFS (PairsOf G)) . b = {x,y}
by Th11, A51, A15, A2, FUNCT_1:3;
f . ((canFS (PairsOf G)) . b) = {{x,[y,(union G)]},{y,[x,(union G)]}}
by A57, A11, A51, A15, A2, FUNCT_1:3;
then
(
a = {x,[y,(union G)]} or
a = {y,[x,(union G)]} )
by A49, A52, A53, TARSKI:def 2;
hence
a in { {x,[y,(union G)]} where x, y is Element of union G : {x,y} in PairsOf G }
by A57, A54, A55, A56;
verum
end;
thus
{ {x,[y,(union G)]} where x, y is Element of union G : {x,y} in PairsOf G } c= union (rng S)
verumproof
let a be
object ;
TARSKI:def 3 ( not a in { {x,[y,(union G)]} where x, y is Element of union G : {x,y} in PairsOf G } or a in union (rng S) )
assume
a in { {x,[y,(union G)]} where x, y is Element of union G : {x,y} in PairsOf G }
;
a in union (rng S)
then consider x,
y being
Element of
union G such that A58:
a = {x,[y,(union G)]}
and A59:
{x,y} in PairsOf G
;
consider c being
object such that
c in dom (canFS (PairsOf G))
and A60:
(canFS (PairsOf G)) . c = {x,y}
by A59, A2, FUNCT_1:def 3;
rng S = rng f
by A10, A2, RELAT_1:28;
then A61:
f . ((canFS (PairsOf G)) . c) in rng S
by A10, A60, A59, FUNCT_1:3;
f . ((canFS (PairsOf G)) . c) = {{x,[y,(union G)]},{y,[x,(union G)]}}
by A60, A59, A11;
then
a in f . ((canFS (PairsOf G)) . c)
by A58, TARSKI:def 2;
hence
a in union (rng S)
by A61, TARSKI:def 4;
verum
end;
end;
hence
card { {x,[y,(union G)]} where x, y is Element of union G : {x,y} in PairsOf G } = 2 * (card (PairsOf G))
by A38, A47, A48, RVSUM_1:80; verum