let x be object ; :: thesis: for FSG being Friendship_Graph st FSG is without_universal_friend & x in field FSG holds
card (field FSG) = 1 + ((card (Im (FSG,x))) * ((card (Im (FSG,x))) - 1))
let FSG be Friendship_Graph; :: thesis: ( FSG is without_universal_friend & x in field FSG implies card (field FSG) = 1 + ((card (Im (FSG,x))) * ((card (Im (FSG,x))) - 1)) )
defpred S1[ object , object ] means for x, y being object st $1 = [x,y] holds
$2 = y;
assume that
A1: FSG is without_universal_friend and
A2: x in field FSG ; :: thesis: card (field FSG) = 1 + ((card (Im (FSG,x))) * ((card (Im (FSG,x))) - 1))
set I = Im (FSG,x);
set F = field FSG;
set FI = (field FSG) \ ({x} \/ (Im (FSG,x)));
defpred S2[ object , object ] means ( $1 in Im (FSG,x) & [$1,$2] in FSG & not [x,$2] in FSG );
consider RR being Relation such that
A3: for y, z being object holds
( [y,z] in RR iff ( y in Im (FSG,x) & z in (field FSG) \ ({x} \/ (Im (FSG,x))) & S2[y,z] ) ) from RELAT_1:sch 1();
 card (Im (FSG,x)) > 2 by Th10, A1, A2;
then reconsider cI = (card (Im (FSG,x))) - 2 as Element of NAT by NAT_1:21;
for y being object st y in Im (FSG,x) holds
card (Im (RR,y)) = cI
proof
let y be object ; :: thesis: ( y in Im (FSG,x) implies card (Im (RR,y)) = cI )
x in {x} by TARSKI:def 1;
then x in {x} \/ (Im (FSG,x)) by XBOOLE_0:def 3;
then not x in (field FSG) \ ({x} \/ (Im (FSG,x))) by XBOOLE_0:def 5;
then A4: not [y,x] in RR by A3;
assume A5: y in Im (FSG,x) ; :: thesis: card (Im (RR,y)) = cI
then A6: [x,y] in FSG by RELAT_1:169;
then A7: x <> y by Lm2;
y in field FSG by A6, RELAT_1:15;
then consider z being object such that
A8: (Im (FSG,x)) /\ (Coim (FSG,y)) = {z} by A7, Def3, A2;
A9: z in {z} by TARSKI:def 1;
then A10: z in Im (FSG,x) by XBOOLE_0:def 4, A8;
then A11: [x,z] in FSG by RELAT_1:169;
Coim (FSG,y) = Im (FSG,y) by Th2;
then A12: z in Im (FSG,y) by A9, XBOOLE_0:def 4, A8;
then A13: [y,z] in FSG by RELAT_1:169;
A14: (Im (FSG,y)) \ {z,x} c= Im (RR,y)
proof
let d be object ; :: according to TARSKI:def 3 :: thesis: ( not d in (Im (FSG,y)) \ {z,x} or d in Im (RR,y) )
assume A15: d in (Im (FSG,y)) \ {z,x} ; :: thesis: d in Im (RR,y)
then A16: not d in {z,x} by XBOOLE_0:def 5;
A17: [y,d] in FSG by A15, RELAT_1:169;
then A18: d in field FSG by RELAT_1:15;
A19: not d in Im (FSG,x)
proof
A20: ( [d,y] in FSG & [z,y] in FSG ) by A17, Lm3, A13;
assume d in Im (FSG,x) ; :: thesis: contradiction
then [x,d] in FSG by RELAT_1:169;
then d = z by A20, A11, Lm5, A7;
hence contradiction by A16, TARSKI:def 2; :: thesis: verum
end;
A21: not [x,d] in FSG
proof
assume A22: [x,d] in FSG ; :: thesis: contradiction
A23: ( [d,y] in FSG & [x,z] in FSG ) by A17, Lm3, A10, RELAT_1:169;
[z,y] in FSG by A13, Lm3;
then d = z by A22, A23, Lm5, A7;
hence contradiction by A16, TARSKI:def 2; :: thesis: verum
end;
d <> x by A16, TARSKI:def 2;
then not d in {x} by TARSKI:def 1;
then not d in (Im (FSG,x)) \/ {x} by A19, XBOOLE_0:def 3;
then d in (field FSG) \ ({x} \/ (Im (FSG,x))) by A18, XBOOLE_0:def 5;
then [y,d] in RR by A3, A21, A5, A15, RELAT_1:169;
hence d in Im (RR,y) by RELAT_1:169; :: thesis: verum
end;
A24: not [y,z] in RR by A11, A3;
Im (RR,y) c= (Im (FSG,y)) \ {x,z}
proof
let d be object ; :: according to TARSKI:def 3 :: thesis: ( not d in Im (RR,y) or d in (Im (FSG,y)) \ {x,z} )
assume A25: d in Im (RR,y) ; :: thesis: d in (Im (FSG,y)) \ {x,z}
then [y,d] in RR by RELAT_1:169;
then [y,d] in FSG by A3;
then A26: d in Im (FSG,y) by RELAT_1:169;
( d <> x & d <> z ) by A25, A4, RELAT_1:169, A24;
then not d in {x,z} by TARSKI:def 2;
hence d in (Im (FSG,y)) \ {x,z} by A26, XBOOLE_0:def 5; :: thesis: verum
end;
then A27: Im (RR,y) = (Im (FSG,y)) \ {x,z} by A14;
y in field FSG by A6, RELAT_1:15;
then A28: card (Im (FSG,x)) = card (Im (FSG,y)) by A1, A2, Th11;
[y,x] in FSG by A6, Lm3;
then x in Im (FSG,y) by RELAT_1:169;
then A29: card ((Im (FSG,y)) \ {x,z}) = (card (Im (FSG,y))) - (card {x,z}) by ZFMISC_1:32, A12, CARD_2:44;
x <> z by A11, Lm2;
hence card (Im (RR,y)) = cI by A28, A27, A29, CARD_2:57; :: thesis: verum
end;
then A30: card RR = (card (RR | ((dom RR) \ (Im (FSG,x))))) +` (cI *` (card (Im (FSG,x)))) by SIMPLEX1:1;
dom RR c= Im (FSG,x)
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in dom RR or y in Im (FSG,x) )
assume y in dom RR ; :: thesis: y in Im (FSG,x)
then ex z being object st [y,z] in RR by XTUPLE_0:def 12;
hence y in Im (FSG,x) by A3; :: thesis: verum
end;
then (dom RR) \ (Im (FSG,x)) = {} by XBOOLE_1:37;
then card (RR | ((dom RR) \ (Im (FSG,x)))) = 0 ;
then A31: card RR = cI *` (card (Im (FSG,x))) by A30, CARD_2:18
.= cI * (card (Im (FSG,x))) by Lm1 ;
A32: for y being object st y in RR holds
ex z being object st S1[y,z]
proof
let y be object ; :: thesis: ( y in RR implies ex z being object st S1[y,z] )
assume A33: y in RR ; :: thesis: ex z being object st S1[y,z]
consider z, t being object such that
A34: [z,t] = y by A33, RELAT_1:def 1;
take t ; :: thesis: S1[y,t]
thus S1[y,t] by XTUPLE_0:1, A34; :: thesis: verum
end;
consider pr being Function such that
A35: ( dom pr = RR & ( for x being object st x in RR holds
S1[x,pr . x] ) ) from CLASSES1:sch 1(A32);
 A36: pr is one-to-one
proof
let x1, x2 be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x1 in dom pr or not x2 in dom pr or not pr . x1 = pr . x2 or x1 = x2 )
assume that
A37: x1 in dom pr and
A38: x2 in dom pr and
A39: pr . x1 = pr . x2 ; :: thesis: x1 = x2
consider y1, t1 being object such that
A40: x1 = [y1,t1] by A37, A35, RELAT_1:def 1;
t1 in (field FSG) \ ({x} \/ (Im (FSG,x))) by A40, A35, A37, A3;
then not t1 in {x} \/ (Im (FSG,x)) by XBOOLE_0:def 5;
then not t1 in {x} by XBOOLE_0:def 3;
then A41: t1 <> x by TARSKI:def 1;
consider y2, t2 being object such that
A42: x2 = [y2,t2] by A35, RELAT_1:def 1, A38;
A43: ( t1 = pr . x1 & [y1,t1] in FSG ) by A37, A40, A35, A3;
A44: ( t2 = pr . x2 & [y2,t2] in FSG ) by A38, A42, A35, A3;
y2 in Im (FSG,x) by A42, A35, A38, A3;
then A45: [x,y2] in FSG by RELAT_1:169;
y1 in Im (FSG,x) by A40, A35, A37, A3;
then [x,y1] in FSG by RELAT_1:169;
hence x1 = x2 by A41, A39, A43, A44, A45, Lm5, A40, A42; :: thesis: verum
end;
A46: (field FSG) \ ({x} \/ (Im (FSG,x))) c= rng pr
proof
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in (field FSG) \ ({x} \/ (Im (FSG,x))) or z in rng pr )
assume A47: z in (field FSG) \ ({x} \/ (Im (FSG,x))) ; :: thesis: z in rng pr
then A48: not z in {x} \/ (Im (FSG,x)) by XBOOLE_0:def 5;
then A49: not z in Im (FSG,x) by XBOOLE_0:def 3;
not z in {x} by A48, XBOOLE_0:def 3;
then z <> x by TARSKI:def 1;
then consider t being object such that
A50: (Im (FSG,x)) /\ (Coim (FSG,z)) = {t} by A2, A47, Def3;
A51: t in {t} by TARSKI:def 1;
Coim (FSG,z) = Im (FSG,z) by Th2;
then t in Im (FSG,z) by A51, A50, XBOOLE_0:def 4;
then [z,t] in FSG by RELAT_1:169;
then S2[t,z] by A49, RELAT_1:169, Lm3, A51, A50, XBOOLE_0:def 4;
then ( [t,z] in RR & pr . [t,z] = z ) by A3, A47, A35;
hence z in rng pr by A35, FUNCT_1:def 3; :: thesis: verum
end;
rng pr c= (field FSG) \ ({x} \/ (Im (FSG,x)))
proof
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in rng pr or z in (field FSG) \ ({x} \/ (Im (FSG,x))) )
assume z in rng pr ; :: thesis: z in (field FSG) \ ({x} \/ (Im (FSG,x)))
then consider t being object such that
A52: t in dom pr and
A53: pr . t = z by FUNCT_1:def 3;
consider t1, t2 being object such that
A54: t = [t1,t2] by A52, A35, RELAT_1:def 1;
pr . t = t2 by A52, A54, A35;
hence z in (field FSG) \ ({x} \/ (Im (FSG,x))) by A52, A54, A35, A3, A53; :: thesis: verum
end;
then rng pr = (field FSG) \ ({x} \/ (Im (FSG,x))) by A46;
then A55: cI * (card (Im (FSG,x))) = card ((field FSG) \ ({x} \/ (Im (FSG,x)))) by WELLORD2:def 4, A36, A35, CARD_1:5, A31;
A56: Im (FSG,x) c= field FSG
proof
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in Im (FSG,x) or z in field FSG )
assume z in Im (FSG,x) ; :: thesis: z in field FSG
then [x,z] in FSG by RELAT_1:169;
hence z in field FSG by RELAT_1:15; :: thesis: verum
end;
not [x,x] in FSG by Lm2;
then A57: card ({x} \/ (Im (FSG,x))) = (card (Im (FSG,x))) + 1 by RELAT_1:169, CARD_2:41;
{x} c= field FSG by A2, ZFMISC_1:31;
then cI * (card (Im (FSG,x))) = (card (field FSG)) - (card ({x} \/ (Im (FSG,x)))) by A56, XBOOLE_1:8, CARD_2:44, A55;
then card (field FSG) = (cI * (card (Im (FSG,x)))) + ((card (Im (FSG,x))) + 1) by A57;
hence card (field FSG) = 1 + ((card (Im (FSG,x))) * ((card (Im (FSG,x))) - 1)) ; :: thesis: verum