let P be non empty PreferenceSpace; ( P is total iff CharRel P is connected Order of the carrier of P )
Z1:
( P is total implies CharRel P is connected Order of the carrier of P )
proof
assume A1:
P is
total
;
CharRel P is connected Order of the carrier of P
set R = the
PrefRel of
P;
set T = the
ToleranceRel of
P;
set X = the
carrier of
P;
set I = the
InternalRel of
P;
set C =
CharRel P;
k2:
(( the PrefRel of P \/ ( the PrefRel of P ~)) \/ the ToleranceRel of P) \/ the
InternalRel of
P = nabla the
carrier of
P
by PrefDef;
the
ToleranceRel of
P is
total
by PrefDef;
then A5:
field the
ToleranceRel of
P = the
carrier of
P
by ORDERS_1:12;
the
ToleranceRel of
P is
symmetric
by PrefDef;
then Y5:
the
ToleranceRel of
P = the
ToleranceRel of
P ~
by RELAT_2:13;
the
PrefRel of
P is
asymmetric
by PrefDef;
then Y6:
the
PrefRel of
P /\ ( the PrefRel of P ~) = {}
by Lemma17, XBOOLE_0:def 7;
a4:
field ( the PrefRel of P \/ the ToleranceRel of P) =
(field the PrefRel of P) \/ (field the ToleranceRel of P)
by RELAT_1:18
.=
the
carrier of
P
by A5, XBOOLE_1:12
;
(CharRel P) \/ ((CharRel P) ~) =
( the PrefRel of P \/ the ToleranceRel of P) \/ (( the PrefRel of P ~) \/ ( the ToleranceRel of P ~))
by RELAT_1:23
.=
[: the carrier of P, the carrier of P:]
by A1, k2, XBOOLE_1:5
;
then ss:
CharRel P is
strongly_connected
by RELAT_2:30, a4;
CharRel P is_reflexive_in the
carrier of
P
by a4, ss, RELAT_2:def 9;
then A3:
dom (CharRel P) = the
carrier of
P
by ORDERS_1:13;
y1:
(CharRel P) /\ ((CharRel P) ~) =
( the PrefRel of P \/ the ToleranceRel of P) /\ (( the PrefRel of P ~) \/ ( the ToleranceRel of P ~))
by RELAT_1:23
.=
the
ToleranceRel of
P \/ ( the PrefRel of P /\ ( the PrefRel of P ~))
by XBOOLE_1:24, Y5
.=
id the
carrier of
P
by Y6, A1
;
Y9:
( the PrefRel of P * the PrefRel of P) \/ ( the PrefRel of P \/ (id the carrier of P)) c= the
PrefRel of
P \/ ( the PrefRel of P \/ (id the carrier of P))
by XBOOLE_1:9, A1, RELAT_2:27;
y7:
the
PrefRel of
P \/ ( the PrefRel of P \/ (id the carrier of P)) c= ( the PrefRel of P \/ (id the carrier of P)) \/ ( the PrefRel of P \/ (id the carrier of P))
by XBOOLE_1:7, XBOOLE_1:9;
B9:
dom the
PrefRel of
P c= the
carrier of
P
;
B10:
rng the
PrefRel of
P c= the
carrier of
P
;
B11:
dom (id the carrier of P) c= the
carrier of
P
;
B13:
( the PrefRel of P \/ (id the carrier of P)) * (id the carrier of P) = ( the PrefRel of P * (id the carrier of P)) \/ ((id the carrier of P) * (id the carrier of P))
by SYSREL:6;
W2:
(id the carrier of P) * the
PrefRel of
P = the
PrefRel of
P
by RELAT_1:51, B9;
W3:
the
PrefRel of
P * (id the carrier of P) = the
PrefRel of
P
by RELAT_1:53, B10;
W4:
(id the carrier of P) * (id the carrier of P) = id the
carrier of
P
by RELAT_1:51, B11;
(CharRel P) * (CharRel P) =
(( the PrefRel of P \/ (id the carrier of P)) * the PrefRel of P) \/ (( the PrefRel of P \/ (id the carrier of P)) * (id the carrier of P))
by RELAT_1:32, A1
.=
(( the PrefRel of P * the PrefRel of P) \/ ((id the carrier of P) * the PrefRel of P)) \/ (( the PrefRel of P * (id the carrier of P)) \/ ((id the carrier of P) * (id the carrier of P)))
by SYSREL:6, B13
.=
( the PrefRel of P * the PrefRel of P) \/ ( the PrefRel of P \/ ( the PrefRel of P \/ (id the carrier of P)))
by XBOOLE_1:4, W2, W3, W4
.=
( the PrefRel of P * the PrefRel of P) \/ ( the PrefRel of P \/ (id the carrier of P))
by XBOOLE_1:6
;
hence
CharRel P is
connected Order of the
carrier of
P
by y1, ss, A3, RELAT_2:27, XBOOLE_1:1, Y9, A1, y7, PARTFUN1:def 2, RELAT_2:22;
verum
end;
( CharRel P is connected Order of the carrier of P implies P is total )
proof
assume B1:
CharRel P is
connected Order of the
carrier of
P
;
P is total
set R = the
PrefRel of
P;
set T = the
ToleranceRel of
P;
set I = the
InternalRel of
P;
set X = the
carrier of
P;
S1:
field ( the PrefRel of P \/ the ToleranceRel of P) = the
carrier of
P
by B1, ORDERS_1:12;
B5:
dom ( the PrefRel of P \/ the ToleranceRel of P) = the
carrier of
P
by PARTFUN1:def 2, B1;
the
ToleranceRel of
P is
symmetric
by PrefDef;
then S0:
the
ToleranceRel of
P = the
ToleranceRel of
P ~
by RELAT_2:13;
B7:
the
PrefRel of
P is
asymmetric
by PrefDef;
then B6:
the
PrefRel of
P /\ ( the PrefRel of P ~) = {}
by Lemma17, XBOOLE_0:def 7;
B9:
dom the
PrefRel of
P c= the
carrier of
P
;
B10:
rng the
PrefRel of
P c= the
carrier of
P
;
S6:
id the
carrier of
P misses the
PrefRel of
P
by Lemma21, B7;
X1:
the
ToleranceRel of
P = id the
carrier of
P
x2:
the
PrefRel of
P * the
PrefRel of
P c= the
PrefRel of
P
proof
B11:
dom (id the carrier of P) c= the
carrier of
P
;
W2:
(id the carrier of P) * the
PrefRel of
P = the
PrefRel of
P
by RELAT_1:51, B9;
W3:
the
PrefRel of
P * (id the carrier of P) = the
PrefRel of
P
by RELAT_1:53, B10;
W4:
(id the carrier of P) * (id the carrier of P) = id the
carrier of
P
by RELAT_1:51, B11;
B14:
( the PrefRel of P \/ (id the carrier of P)) * the
PrefRel of
P = ( the PrefRel of P * the PrefRel of P) \/ ((id the carrier of P) * the PrefRel of P)
by SYSREL:6;
B13:
( the PrefRel of P \/ (id the carrier of P)) * (id the carrier of P) = ( the PrefRel of P * (id the carrier of P)) \/ ((id the carrier of P) * (id the carrier of P))
by SYSREL:6;
( the PrefRel of P \/ (id the carrier of P)) * ( the PrefRel of P \/ (id the carrier of P)) =
(( the PrefRel of P \/ (id the carrier of P)) * the PrefRel of P) \/ (( the PrefRel of P \/ (id the carrier of P)) * (id the carrier of P))
by RELAT_1:32
.=
( the PrefRel of P * the PrefRel of P) \/ ( the PrefRel of P \/ ( the PrefRel of P \/ (id the carrier of P)))
by XBOOLE_1:4, W2, W3, W4, B14, B13
.=
( the PrefRel of P * the PrefRel of P) \/ ( the PrefRel of P \/ (id the carrier of P))
by XBOOLE_1:6
;
then
the
PrefRel of
P * the
PrefRel of
P c= the
PrefRel of
P \/ (id the carrier of P)
by RELAT_2:27, B1, X1, XBOOLE_1:11;
hence
the
PrefRel of
P * the
PrefRel of
P c= the
PrefRel of
P
by Lemma22, B7, XBOOLE_1:73;
verum
end;
the
InternalRel of
P = {}
proof
set Z =
( the PrefRel of P \/ ( the PrefRel of P ~)) \/ the
ToleranceRel of
P;
( the
PrefRel of
P \/ the
ToleranceRel of
P is_connected_in the
carrier of
P & the
PrefRel of
P \/ the
ToleranceRel of
P is_reflexive_in the
carrier of
P )
by S1, B1, RELAT_2:def 14, RELAT_2:def 9;
then
the
PrefRel of
P \/ the
ToleranceRel of
P is
strongly_connected
by RELAT_2:def 15, S1, ORDERS_1:7;
then
[: the carrier of P, the carrier of P:] c= ( the PrefRel of P \/ the ToleranceRel of P) \/ (( the PrefRel of P \/ the ToleranceRel of P) ~)
by RELAT_2:30, S1;
then
[: the carrier of P, the carrier of P:] c= ( the PrefRel of P \/ the ToleranceRel of P) \/ (( the PrefRel of P ~) \/ ( the ToleranceRel of P ~))
by RELAT_1:23;
then S2:
[: the carrier of P, the carrier of P:] c= ( the PrefRel of P \/ ( the PrefRel of P ~)) \/ the
ToleranceRel of
P
by XBOOLE_1:5, S0;
s3:
(( the PrefRel of P \/ ( the PrefRel of P ~)) \/ the ToleranceRel of P) \/ the
InternalRel of
P = nabla the
carrier of
P
by PrefDef;
s4:
the
PrefRel of
P, the
ToleranceRel of
P, the
InternalRel of
P are_mutually_disjoint
by PrefDef;
the
InternalRel of
P is
symmetric
by PrefDef;
then
the
PrefRel of
P ~ misses the
InternalRel of
P
by s4, Lemma20;
then
the
InternalRel of
P misses ( the PrefRel of P \/ ( the PrefRel of P ~)) \/ the
ToleranceRel of
P
by s4, XBOOLE_1:114;
hence
the
InternalRel of
P = {}
by XBOOLE_1:11, S2, Lemma19, s3;
verum
end;
hence
P is
total
by X1, x2, RELAT_2:27;
verum
end;
hence
( P is total iff CharRel P is connected Order of the carrier of P )
by Z1; verum