let x be object ; for FSG being Friendship_Graph holds 2 divides card (Im (FSG,x))
let FSG be Friendship_Graph; 2 divides card (Im (FSG,x))
set I = Im (FSG,x);
defpred S1[ object , object ] means ex y being object st
( [$1,y] in FSG & y in Im (FSG,x) & $2 = {$1,y} );
A1:
for x being object st x in Im (FSG,x) holds
ex y being object st S1[x,y]
proof
let y be
object ;
( y in Im (FSG,x) implies ex y being object st S1[y,y] )
assume
y in Im (
FSG,
x)
;
ex y being object st S1[y,y]
then A2:
[x,y] in FSG
by RELAT_1:169;
then A3:
(
x <> y &
x in field FSG )
by Lm2, RELAT_1:15;
y in field FSG
by A2, RELAT_1:15;
then consider z being
object such that A4:
(Im (FSG,x)) /\ (Coim (FSG,y)) = {z}
by A3, Def3;
take
{y,z}
;
S1[y,{y,z}]
A5:
z in {z}
by TARSKI:def 1;
Coim (
FSG,
y)
= Im (
FSG,
y)
by Th2;
then
z in Im (
FSG,
y)
by A5, A4, XBOOLE_0:def 4;
then A6:
[y,z] in FSG
by RELAT_1:169;
z in Im (
FSG,
x)
by A5, A4, XBOOLE_0:def 4;
hence
S1[
y,
{y,z}]
by A6;
verum
end;
consider h being Function such that
A7:
( dom h = Im (FSG,x) & ( for x being object st x in Im (FSG,x) holds
S1[x,h . x] ) )
from CLASSES1:sch 1(A1);
reconsider R = rng h as finite set by A7, FINSET_1:8;
set H = h ~ ;
for x being object st x in R holds
card (Im ((h ~),x)) = 2
proof
let y be
object ;
( y in R implies card (Im ((h ~),y)) = 2 )
assume
y in R
;
card (Im ((h ~),y)) = 2
then consider z being
object such that A8:
z in dom h
and A9:
h . z = y
by FUNCT_1:def 3;
consider w being
object such that A10:
[z,w] in FSG
and A11:
w in Im (
FSG,
x)
and A12:
y = {z,w}
by A7, A8, A9;
consider t being
object such that A13:
[w,t] in FSG
and A14:
t in Im (
FSG,
x)
and A15:
h . w = {w,t}
by A11, A7;
t = z
proof
A16:
[x,w] in FSG
by A11, RELAT_1:169;
then A17:
(
x <> w &
x in field FSG )
by Lm2, RELAT_1:15;
w in field FSG
by A16, RELAT_1:15;
then consider r being
object such that A18:
(Im (FSG,x)) /\ (Coim (FSG,w)) = {r}
by A17, Def3;
A19:
Coim (
FSG,
w)
= Im (
FSG,
w)
by Th2;
then
t in Coim (
FSG,
w)
by RELAT_1:169, A13;
then
t in {r}
by A14, A18, XBOOLE_0:def 4;
then A20:
t = r
by TARSKI:def 1;
[w,z] in FSG
by A10, Lm3;
then
z in Coim (
FSG,
w)
by A19, RELAT_1:169;
then
z in {r}
by A7, A8, A18, XBOOLE_0:def 4;
hence
t = z
by A20, TARSKI:def 1;
verum
end;
then
[w,y] in h
by A12, A15, A11, A7, FUNCT_1:def 2;
then
[y,w] in h ~
by RELAT_1:def 7;
then A21:
w in Im (
(h ~),
y)
by RELAT_1:169;
reconsider y =
y as
set by TARSKI:1;
A22:
Im (
(h ~),
y)
c= y
[z,y] in h
by A8, A9, FUNCT_1:def 2;
then
[y,z] in h ~
by RELAT_1:def 7;
then
z in Im (
(h ~),
y)
by RELAT_1:169;
then
y c= Im (
(h ~),
y)
by A12, A21, ZFMISC_1:32;
then A25:
y = Im (
(h ~),
y)
by A22;
z <> w
by A10, Lm2;
hence
card (Im ((h ~),y)) = 2
by A25, A12, CARD_2:57;
verum
end;
then A26:
card (h ~) = (card ((h ~) | ((dom (h ~)) \ R))) +` (2 *` (card R))
by SIMPLEX1:1;
dom (h ~) = R
by RELAT_1:20;
then
(dom (h ~)) \ R = {}
by XBOOLE_1:37;
then
card ((h ~) | ((dom (h ~)) \ R)) = 0
;
then
card (h ~) = 2 *` (card R)
by A26, CARD_2:18;
then 2 * (card R) =
card (h ~)
by Lm1
.=
card h
by Th1
.=
card (Im (FSG,x))
by A7, CARD_1:62
;
hence
2 divides card (Im (FSG,x))
by INT_1:def 3; verum