let R be non empty symmetric irreflexive RelStr ; :: thesis: ( not R is path-connected implies ex G1, G2 being non empty strict symmetric irreflexive RelStr st
( the carrier of G1 misses the carrier of G2 & RelStr(# the carrier of R,the InternalRel of R #) = union_of G1,G2 ) )
set cR = the carrier of R;
set IR = the InternalRel of R;
assume
not R is path-connected
; :: thesis: ex G1, G2 being non empty strict symmetric irreflexive RelStr st
( the carrier of G1 misses the carrier of G2 & RelStr(# the carrier of R,the InternalRel of R #) = union_of G1,G2 )
then consider x, y being set such that
A1:
( x in the carrier of R & y in the carrier of R & x <> y & not the InternalRel of R reduces x,y )
by Def2;
reconsider x = x, y = y as Element of R by A1;
set A1 = component x;
set A2 = the carrier of R \ (component x);
reconsider A2 = the carrier of R \ (component x) as Subset of R ;
set G1 = subrelstr (component x);
set G2 = subrelstr A2;
A2:
( the carrier of (subrelstr (component x)) = component x & the carrier of (subrelstr A2) = A2 )
by YELLOW_0:def 15;
then A3:
the carrier of (subrelstr (component x)) misses the carrier of (subrelstr A2)
by XBOOLE_1:79;
the InternalRel of R = the InternalRel of R ~
by RELAT_2:30;
then
not the InternalRel of R \/ (the InternalRel of R ~ ) reduces x,y
by A1;
then
not x,y are_convertible_wrt the InternalRel of R
by REWRITE1:def 4;
then
not [x,y] in EqCl the InternalRel of R
by MSUALG_6:41;
then
( y in the carrier of R & not y in component x )
by Th30;
then
not the carrier of (subrelstr A2) is empty
by A2, XBOOLE_0:def 5;
then A4:
( subrelstr (component x) is non empty strict RelStr & subrelstr A2 is non empty strict RelStr )
by A2;
A5:
the carrier of R = (component x) \/ A2
then A7:
the carrier of R = the carrier of (union_of (subrelstr (component x)),(subrelstr A2))
by A2, NECKLA_2:def 2;
A8:
the InternalRel of (subrelstr (component x)) misses the InternalRel of (subrelstr A2)
proof
set IG1 = the
InternalRel of
(subrelstr (component x));
set IG2 = the
InternalRel of
(subrelstr A2);
assume
not the
InternalRel of
(subrelstr (component x)) misses the
InternalRel of
(subrelstr A2)
;
:: thesis: contradiction
then
the
InternalRel of
(subrelstr (component x)) /\ the
InternalRel of
(subrelstr A2) <> {}
by XBOOLE_0:def 7;
then consider a being
set such that A9:
a in the
InternalRel of
(subrelstr (component x)) /\ the
InternalRel of
(subrelstr A2)
by XBOOLE_0:def 1;
A10:
(
a in the
InternalRel of
(subrelstr (component x)) &
a in the
InternalRel of
(subrelstr A2) )
by A9, XBOOLE_0:def 4;
then consider c1,
c2 being
set such that A11:
(
a = [c1,c2] &
c1 in component x &
c2 in component x )
by A2, RELSET_1:6;
consider g1,
g2 being
set such that A12:
(
a = [g1,g2] &
g1 in A2 &
g2 in A2 )
by A2, A10, RELSET_1:6;
(
c1 in component x &
c1 in A2 )
by A11, A12, ZFMISC_1:33;
then
c1 in (component x) /\ A2
by XBOOLE_0:def 4;
hence
contradiction
by A2, A3, XBOOLE_0:def 7;
:: thesis: verum
end;
A13:
the InternalRel of (subrelstr A2) = the InternalRel of R \ the InternalRel of (subrelstr (component x))
proof
set IG1 = the
InternalRel of
(subrelstr (component x));
set IG2 = the
InternalRel of
(subrelstr A2);
thus
the
InternalRel of
(subrelstr A2) c= the
InternalRel of
R \ the
InternalRel of
(subrelstr (component x))
:: according to XBOOLE_0:def 10 :: thesis: the InternalRel of R \ the InternalRel of (subrelstr (component x)) c= the InternalRel of (subrelstr A2)proof
let a be
set ;
:: according to TARSKI:def 3 :: thesis: ( not a in the InternalRel of (subrelstr A2) or a in the InternalRel of R \ the InternalRel of (subrelstr (component x)) )
assume A14:
a in the
InternalRel of
(subrelstr A2)
;
:: thesis: a in the InternalRel of R \ the InternalRel of (subrelstr (component x))
then consider g1,
g2 being
set such that A15:
(
a = [g1,g2] &
g1 in A2 &
g2 in A2 )
by A2, RELSET_1:6;
reconsider g1 =
g1,
g2 =
g2 as
Element of
(subrelstr A2) by A15, YELLOW_0:def 15;
A16:
g1 <= g2
by A14, A15, ORDERS_2:def 9;
reconsider u1 =
g1,
u2 =
g2 as
Element of
R by A15;
u1 <= u2
by A16, YELLOW_0:60;
then A17:
a in the
InternalRel of
R
by A15, ORDERS_2:def 9;
not
a in the
InternalRel of
(subrelstr (component x))
hence
a in the
InternalRel of
R \ the
InternalRel of
(subrelstr (component x))
by A17, XBOOLE_0:def 5;
:: thesis: verum
end;
let a be
set ;
:: according to TARSKI:def 3 :: thesis: ( not a in the InternalRel of R \ the InternalRel of (subrelstr (component x)) or a in the InternalRel of (subrelstr A2) )
assume
a in the
InternalRel of
R \ the
InternalRel of
(subrelstr (component x))
;
:: thesis: a in the InternalRel of (subrelstr A2)
then A18:
(
a in the
InternalRel of
R & not
a in the
InternalRel of
(subrelstr (component x)) )
by XBOOLE_0:def 5;
then consider c1,
c2 being
set such that A19:
(
a = [c1,c2] &
c1 in the
carrier of
R &
c2 in the
carrier of
R )
by RELSET_1:6;
reconsider c1 =
c1,
c2 =
c2 as
Element of
R by A19;
A20:
c1 <= c2
by A18, A19, ORDERS_2:def 9;
per cases
( ( c1 in component x & c2 in component x ) or ( c1 in component x & c2 in A2 ) or ( c1 in A2 & c2 in component x ) or ( c1 in A2 & c2 in A2 ) )
by A5, XBOOLE_0:def 3;
suppose
(
c1 in component x &
c2 in A2 )
;
:: thesis: a in the InternalRel of (subrelstr A2)then
a in [:(component x),A2:]
by A19, ZFMISC_1:def 2;
then A22:
a in [:(component x),A2:] /\ the
InternalRel of
R
by A18, XBOOLE_0:def 4;
[:(component x),A2:] misses the
InternalRel of
R
proof
assume
not
[:(component x),A2:] misses the
InternalRel of
R
;
:: thesis: contradiction
then
[:(component x),A2:] /\ the
InternalRel of
R <> {}
by XBOOLE_0:def 7;
then consider b being
set such that A23:
b in [:(component x),A2:] /\ the
InternalRel of
R
by XBOOLE_0:def 1;
A24:
(
b in [:(component x),A2:] &
b in the
InternalRel of
R )
by A23, XBOOLE_0:def 4;
then consider b1,
b2 being
set such that A25:
(
b1 in component x &
b2 in A2 &
b = [b1,b2] )
by ZFMISC_1:def 2;
reconsider b1 =
b1 as
Element of
R by A25;
reconsider b2 =
b2 as
Element of
R by A25;
A26:
(
b1 in the
carrier of
R &
b2 in the
carrier of
R & the
InternalRel of
R c= EqCl the
InternalRel of
R )
by MSUALG_5:def 1;
[x,b1] in EqCl the
InternalRel of
R
by A25, Th30;
then
[x,b2] in EqCl the
InternalRel of
R
by A24, A25, A26, EQREL_1:13;
then
b2 in component x
by Th30;
then
b2 in (component x) /\ A2
by A25, XBOOLE_0:def 4;
hence
contradiction
by A2, A3, XBOOLE_0:def 7;
:: thesis: verum
end; hence
a in the
InternalRel of
(subrelstr A2)
by A22, XBOOLE_0:def 7;
:: thesis: verum end; suppose
(
c1 in A2 &
c2 in component x )
;
:: thesis: a in the InternalRel of (subrelstr A2)then
a in [:A2,(component x):]
by A19, ZFMISC_1:def 2;
then A27:
a in [:A2,(component x):] /\ the
InternalRel of
R
by A18, XBOOLE_0:def 4;
[:A2,(component x):] misses the
InternalRel of
R
proof
assume
not
[:A2,(component x):] misses the
InternalRel of
R
;
:: thesis: contradiction
then
[:A2,(component x):] /\ the
InternalRel of
R <> {}
by XBOOLE_0:def 7;
then consider b being
set such that A28:
b in [:A2,(component x):] /\ the
InternalRel of
R
by XBOOLE_0:def 1;
A29:
(
b in [:A2,(component x):] &
b in the
InternalRel of
R )
by A28, XBOOLE_0:def 4;
then consider b1,
b2 being
set such that A30:
(
b1 in A2 &
b2 in component x &
b = [b1,b2] )
by ZFMISC_1:def 2;
reconsider b1 =
b1 as
Element of
R by A30;
reconsider b2 =
b2 as
Element of
R by A30;
(
b1 in the
carrier of
R &
b2 in the
carrier of
R & the
InternalRel of
R c= EqCl the
InternalRel of
R )
by MSUALG_5:def 1;
then A31:
[b2,b1] in EqCl the
InternalRel of
R
by A29, A30, EQREL_1:12;
[x,b2] in EqCl the
InternalRel of
R
by A30, Th30;
then
[x,b1] in EqCl the
InternalRel of
R
by A31, EQREL_1:13;
then
b1 in component x
by Th30;
then
b1 in (component x) /\ A2
by A30, XBOOLE_0:def 4;
hence
contradiction
by A2, A3, XBOOLE_0:def 7;
:: thesis: verum
end; hence
a in the
InternalRel of
(subrelstr A2)
by A27, XBOOLE_0:def 7;
:: thesis: verum end;
end;
the InternalRel of R = the InternalRel of (subrelstr (component x)) \/ the InternalRel of (subrelstr A2)
proof
set IG1 = the
InternalRel of
(subrelstr (component x));
set IG2 = the
InternalRel of
(subrelstr A2);
thus
the
InternalRel of
R c= the
InternalRel of
(subrelstr (component x)) \/ the
InternalRel of
(subrelstr A2)
:: according to XBOOLE_0:def 10 :: thesis: the InternalRel of (subrelstr (component x)) \/ the InternalRel of (subrelstr A2) c= the InternalRel of R
let a be
set ;
:: according to TARSKI:def 3 :: thesis: ( not a in the InternalRel of (subrelstr (component x)) \/ the InternalRel of (subrelstr A2) or a in the InternalRel of R )
assume A34:
a in the
InternalRel of
(subrelstr (component x)) \/ the
InternalRel of
(subrelstr A2)
;
:: thesis: a in the InternalRel of R
per cases
( a in the InternalRel of (subrelstr (component x)) or a in the InternalRel of (subrelstr A2) )
by A34, XBOOLE_0:def 3;
suppose A35:
a in the
InternalRel of
(subrelstr (component x))
;
:: thesis: a in the InternalRel of Rthen consider v,
w being
set such that A36:
(
a = [v,w] &
v in component x &
w in component x )
by A2, RELSET_1:6;
reconsider v =
v,
w =
w as
Element of
(subrelstr (component x)) by A36, YELLOW_0:def 15;
A37:
v <= w
by A35, A36, ORDERS_2:def 9;
reconsider u1 =
v,
u2 =
w as
Element of
R by A36;
u1 <= u2
by A37, YELLOW_0:60;
hence
a in the
InternalRel of
R
by A36, ORDERS_2:def 9;
:: thesis: verum end; suppose A38:
a in the
InternalRel of
(subrelstr A2)
;
:: thesis: a in the InternalRel of Rthen consider v,
w being
set such that A39:
(
a = [v,w] &
v in A2 &
w in A2 )
by A2, RELSET_1:6;
reconsider v =
v,
w =
w as
Element of
(subrelstr A2) by A39, YELLOW_0:def 15;
A40:
v <= w
by A38, A39, ORDERS_2:def 9;
reconsider u1 =
v,
u2 =
w as
Element of
R by A39;
u1 <= u2
by A40, YELLOW_0:60;
hence
a in the
InternalRel of
R
by A39, ORDERS_2:def 9;
:: thesis: verum end;
end;
then
the InternalRel of R = the InternalRel of (union_of (subrelstr (component x)),(subrelstr A2))
by NECKLA_2:def 2;
hence
ex G1, G2 being non empty strict symmetric irreflexive RelStr st
( the carrier of G1 misses the carrier of G2 & RelStr(# the carrier of R,the InternalRel of R #) = union_of G1,G2 )
by A3, A4, A7; :: thesis: verum