:: EQREL_1 semantic presentation
begin
definition
let X be set ;
func nabla X -> Relation of X equals :: EQREL_1:def 1
[:X,X:];
coherence
[:X,X:] is Relation of X
proof
[:X,X:] c= [:X,X:] ;
hence [:X,X:] is Relation of X ; ::_thesis: verum
end;
end;
:: deftheorem defines nabla EQREL_1:def_1_:_
for X being set holds nabla X = [:X,X:];
registration
let X be set ;
cluster nabla X -> reflexive total ;
coherence
( nabla X is total & nabla X is reflexive )
proof
thus dom (nabla X) c= X ; :: according to XBOOLE_0:def_10,PARTFUN1:def_2 ::_thesis: ( X c= dom (nabla X) & nabla X is reflexive )
thus X c= dom (nabla X) ::_thesis: nabla X is reflexive
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in dom (nabla X) )
assume x in X ; ::_thesis: x in dom (nabla X)
then [x,x] in [:X,X:] by ZFMISC_1:87;
hence x in dom (nabla X) by XTUPLE_0:def_12; ::_thesis: verum
end;
let x be set ; :: according to RELAT_2:def_1,RELAT_2:def_9 ::_thesis: ( not x in field (nabla X) or [x,x] in nabla X )
assume x in field (nabla X) ; ::_thesis: [x,x] in nabla X
then x in (dom (nabla X)) \/ (rng (nabla X)) ;
hence [x,x] in nabla X by ZFMISC_1:87; ::_thesis: verum
end;
end;
definition
let X be set ;
let R1, R2 be Relation of X;
:: original: /\
redefine funcR1 /\ R2 -> Relation of X;
coherence
R1 /\ R2 is Relation of X
proof
R1 /\ R2 c= [:X,X:] ;
hence R1 /\ R2 is Relation of X ; ::_thesis: verum
end;
:: original: \/
redefine funcR1 \/ R2 -> Relation of X;
coherence
R1 \/ R2 is Relation of X
proof
R1 \/ R2 c= [:X,X:] ;
hence R1 \/ R2 is Relation of X ; ::_thesis: verum
end;
end;
theorem :: EQREL_1:1
for X being set
for R1 being Relation of X holds (nabla X) \/ R1 = nabla X by XBOOLE_1:12;
theorem :: EQREL_1:2
for X being set holds
( id X is_reflexive_in X & id X is_symmetric_in X & id X is_transitive_in X )
proof
let X be set ; ::_thesis: ( id X is_reflexive_in X & id X is_symmetric_in X & id X is_transitive_in X )
thus for x being set st x in X holds
[x,x] in id X by RELAT_1:def_10; :: according to RELAT_2:def_1 ::_thesis: ( id X is_symmetric_in X & id X is_transitive_in X )
thus for x, y being set st x in X & y in X & [x,y] in id X holds
[y,x] in id X by RELAT_1:def_10; :: according to RELAT_2:def_3 ::_thesis: id X is_transitive_in X
thus for x, y, z being set st x in X & y in X & z in X & [x,y] in id X & [y,z] in id X holds
[x,z] in id X by RELAT_1:def_10; :: according to RELAT_2:def_8 ::_thesis: verum
end;
definition
let X be set ;
mode Tolerance of X is reflexive symmetric total Relation of X;
mode Equivalence_Relation of X is symmetric transitive total Relation of X;
end;
theorem :: EQREL_1:3
for X being set holds id X is Equivalence_Relation of X ;
theorem Th4: :: EQREL_1:4
for X being set holds nabla X is Equivalence_Relation of X
proof
let X be set ; ::_thesis: nabla X is Equivalence_Relation of X
for x, y being set st x in X & y in X & [x,y] in nabla X holds
[y,x] in nabla X by ZFMISC_1:88;
then A1: nabla X is_symmetric_in X by RELAT_2:def_3;
for x, y, z being set st x in X & y in X & z in X & [x,y] in nabla X & [y,z] in nabla X holds
[x,z] in nabla X by ZFMISC_1:87;
then A2: nabla X is_transitive_in X by RELAT_2:def_8;
field (nabla X) = X by ORDERS_1:12;
hence nabla X is Equivalence_Relation of X by A1, A2, RELAT_2:def_11, RELAT_2:def_16; ::_thesis: verum
end;
registration
let X be set ;
cluster nabla X -> symmetric transitive total ;
coherence
( nabla X is total & nabla X is symmetric & nabla X is transitive ) by Th4;
end;
Lm1: for x, y, X being set
for R being Relation of X st [x,y] in R holds
( x in X & y in X )
proof
let x, y, X be set ; ::_thesis: for R being Relation of X st [x,y] in R holds
( x in X & y in X )
let R be Relation of X; ::_thesis: ( [x,y] in R implies ( x in X & y in X ) )
assume [x,y] in R ; ::_thesis: ( x in X & y in X )
then ( x in dom R & y in rng R ) by XTUPLE_0:def_12, XTUPLE_0:def_13;
hence ( x in X & y in X ) ; ::_thesis: verum
end;
theorem Th5: :: EQREL_1:5
for X, x being set
for R being reflexive total Relation of X st x in X holds
[x,x] in R
proof
let X, x be set ; ::_thesis: for R being reflexive total Relation of X st x in X holds
[x,x] in R
let R be reflexive total Relation of X; ::_thesis: ( x in X implies [x,x] in R )
field R = X by ORDERS_1:12;
then R is_reflexive_in X by RELAT_2:def_9;
hence ( x in X implies [x,x] in R ) by RELAT_2:def_1; ::_thesis: verum
end;
theorem Th6: :: EQREL_1:6
for X, x, y being set
for R being symmetric total Relation of X st [x,y] in R holds
[y,x] in R
proof
let X, x, y be set ; ::_thesis: for R being symmetric total Relation of X st [x,y] in R holds
[y,x] in R
let R be symmetric total Relation of X; ::_thesis: ( [x,y] in R implies [y,x] in R )
field R = X by ORDERS_1:12;
then A1: R is_symmetric_in X by RELAT_2:def_11;
assume A2: [x,y] in R ; ::_thesis: [y,x] in R
then ( x in X & y in X ) by Lm1;
hence [y,x] in R by A2, A1, RELAT_2:def_3; ::_thesis: verum
end;
theorem Th7: :: EQREL_1:7
for X, x, y, z being set
for R being transitive total Relation of X st [x,y] in R & [y,z] in R holds
[x,z] in R
proof
let X, x, y, z be set ; ::_thesis: for R being transitive total Relation of X st [x,y] in R & [y,z] in R holds
[x,z] in R
let R be transitive total Relation of X; ::_thesis: ( [x,y] in R & [y,z] in R implies [x,z] in R )
assume that
A1: [x,y] in R and
A2: [y,z] in R ; ::_thesis: [x,z] in R
A3: z in X by A2, Lm1;
field R = X by ORDERS_1:12;
then A4: R is_transitive_in X by RELAT_2:def_16;
( x in X & y in X ) by A1, Lm1;
hence [x,z] in R by A1, A2, A3, A4, RELAT_2:def_8; ::_thesis: verum
end;
theorem :: EQREL_1:8
for X being set
for R being reflexive total Relation of X st ex x being set st x in X holds
R <> {} ;
theorem Th9: :: EQREL_1:9
for X being set
for R being Relation of X holds
( R is Equivalence_Relation of X iff ( R is reflexive & R is symmetric & R is transitive & field R = X ) )
proof
let X be set ; ::_thesis: for R being Relation of X holds
( R is Equivalence_Relation of X iff ( R is reflexive & R is symmetric & R is transitive & field R = X ) )
let R be Relation of X; ::_thesis: ( R is Equivalence_Relation of X iff ( R is reflexive & R is symmetric & R is transitive & field R = X ) )
thus ( R is Equivalence_Relation of X implies ( R is reflexive & R is symmetric & R is transitive & field R = X ) ) by ORDERS_1:12; ::_thesis: ( R is reflexive & R is symmetric & R is transitive & field R = X implies R is Equivalence_Relation of X )
assume that
A1: R is reflexive and
A2: ( R is symmetric & R is transitive ) and
A3: field R = X ; ::_thesis: R is Equivalence_Relation of X
R is_reflexive_in X by A1, A3, RELAT_2:def_9;
then dom R = X by ORDERS_1:13;
hence R is Equivalence_Relation of X by A2, PARTFUN1:def_2; ::_thesis: verum
end;
definition
let X be set ;
let EqR1, EqR2 be Equivalence_Relation of X;
:: original: /\
redefine funcEqR1 /\ EqR2 -> Equivalence_Relation of X;
coherence
EqR1 /\ EqR2 is Equivalence_Relation of X
proof
for x being set st x in X holds
[x,x] in EqR2 by Th5;
then A1: id X c= EqR2 by RELAT_1:47;
for x being set st x in X holds
[x,x] in EqR1 by Th5;
then id X c= EqR1 by RELAT_1:47;
then id X c= EqR1 /\ EqR2 by A1, XBOOLE_1:19;
then ( dom (EqR1 /\ EqR2) = X & rng (EqR1 /\ EqR2) = X ) by RELSET_1:16, RELSET_1:17;
then field (EqR1 /\ EqR2) = X ;
hence EqR1 /\ EqR2 is Equivalence_Relation of X by Th9; ::_thesis: verum
end;
end;
theorem :: EQREL_1:10
for X being set
for EqR being Equivalence_Relation of X holds (id X) /\ EqR = id X
proof
let X be set ; ::_thesis: for EqR being Equivalence_Relation of X holds (id X) /\ EqR = id X
let EqR be Equivalence_Relation of X; ::_thesis: (id X) /\ EqR = id X
now__::_thesis:_for_x,_y_being_set_st_[x,y]_in_id_X_holds_
[x,y]_in_EqR
let x, y be set ; ::_thesis: ( [x,y] in id X implies [x,y] in EqR )
assume [x,y] in id X ; ::_thesis: [x,y] in EqR
then ( x in X & x = y ) by RELAT_1:def_10;
hence [x,y] in EqR by Th5; ::_thesis: verum
end;
then id X c= EqR by RELAT_1:def_3;
hence (id X) /\ EqR = id X by XBOOLE_1:28; ::_thesis: verum
end;
theorem Th11: :: EQREL_1:11
for X being set
for SFXX being Subset-Family of [:X,X:] st SFXX <> {} & ( for Y being set st Y in SFXX holds
Y is Equivalence_Relation of X ) holds
meet SFXX is Equivalence_Relation of X
proof
let X be set ; ::_thesis: for SFXX being Subset-Family of [:X,X:] st SFXX <> {} & ( for Y being set st Y in SFXX holds
Y is Equivalence_Relation of X ) holds
meet SFXX is Equivalence_Relation of X
let SFXX be Subset-Family of [:X,X:]; ::_thesis: ( SFXX <> {} & ( for Y being set st Y in SFXX holds
Y is Equivalence_Relation of X ) implies meet SFXX is Equivalence_Relation of X )
assume that
A1: SFXX <> {} and
A2: for Y being set st Y in SFXX holds
Y is Equivalence_Relation of X ; ::_thesis: meet SFXX is Equivalence_Relation of X
reconsider XX = meet SFXX as Relation of X ;
A3: XX is_symmetric_in X
proof
let x be set ; :: according to RELAT_2:def_3 ::_thesis: for b1 being set holds
( not x in X or not b1 in X or not [x,b1] in XX or [b1,x] in XX )
let y be set ; ::_thesis: ( not x in X or not y in X or not [x,y] in XX or [y,x] in XX )
assume that
x in X and
y in X and
A4: [x,y] in XX ; ::_thesis: [y,x] in XX
now__::_thesis:_for_Y_being_set_st_Y_in_SFXX_holds_
[y,x]_in_Y
let Y be set ; ::_thesis: ( Y in SFXX implies [y,x] in Y )
assume Y in SFXX ; ::_thesis: [y,x] in Y
then ( Y is Equivalence_Relation of X & [x,y] in Y ) by A2, A4, SETFAM_1:def_1;
hence [y,x] in Y by Th6; ::_thesis: verum
end;
hence [y,x] in XX by A1, SETFAM_1:def_1; ::_thesis: verum
end;
A5: XX is_transitive_in X
proof
let x be set ; :: according to RELAT_2:def_8 ::_thesis: for b1, b2 being set holds
( not x in X or not b1 in X or not b2 in X or not [x,b1] in XX or not [b1,b2] in XX or [x,b2] in XX )
let y, z be set ; ::_thesis: ( not x in X or not y in X or not z in X or not [x,y] in XX or not [y,z] in XX or [x,z] in XX )
assume that
x in X and
y in X and
z in X and
A6: [x,y] in XX and
A7: [y,z] in XX ; ::_thesis: [x,z] in XX
now__::_thesis:_for_Y_being_set_st_Y_in_SFXX_holds_
[x,z]_in_Y
let Y be set ; ::_thesis: ( Y in SFXX implies [x,z] in Y )
assume A8: Y in SFXX ; ::_thesis: [x,z] in Y
then A9: [y,z] in Y by A7, SETFAM_1:def_1;
( Y is Equivalence_Relation of X & [x,y] in Y ) by A2, A6, A8, SETFAM_1:def_1;
hence [x,z] in Y by A9, Th7; ::_thesis: verum
end;
hence [x,z] in XX by A1, SETFAM_1:def_1; ::_thesis: verum
end;
XX is_reflexive_in X
proof
let x be set ; :: according to RELAT_2:def_1 ::_thesis: ( not x in X or [x,x] in XX )
assume A10: x in X ; ::_thesis: [x,x] in XX
for Y being set st Y in SFXX holds
[x,x] in Y
proof
let Y be set ; ::_thesis: ( Y in SFXX implies [x,x] in Y )
assume Y in SFXX ; ::_thesis: [x,x] in Y
then Y is Equivalence_Relation of X by A2;
hence [x,x] in Y by A10, Th5; ::_thesis: verum
end;
hence [x,x] in XX by A1, SETFAM_1:def_1; ::_thesis: verum
end;
then ( field XX = X & dom XX = X ) by ORDERS_1:13;
hence meet SFXX is Equivalence_Relation of X by A3, A5, PARTFUN1:def_2, RELAT_2:def_11, RELAT_2:def_16; ::_thesis: verum
end;
theorem Th12: :: EQREL_1:12
for X being set
for R being Relation of X ex EqR being Equivalence_Relation of X st
( R c= EqR & ( for EqR2 being Equivalence_Relation of X st R c= EqR2 holds
EqR c= EqR2 ) )
proof
let X be set ; ::_thesis: for R being Relation of X ex EqR being Equivalence_Relation of X st
( R c= EqR & ( for EqR2 being Equivalence_Relation of X st R c= EqR2 holds
EqR c= EqR2 ) )
let R be Relation of X; ::_thesis: ex EqR being Equivalence_Relation of X st
( R c= EqR & ( for EqR2 being Equivalence_Relation of X st R c= EqR2 holds
EqR c= EqR2 ) )
defpred S1[ set ] means ( $1 is Equivalence_Relation of X & R c= $1 );
consider F being Subset-Family of [:X,X:] such that
A1: for AX being Subset of [:X,X:] holds
( AX in F iff S1[AX] ) from SUBSET_1:sch_3();
R c= nabla X ;
then A2: F <> {} by A1;
for Y being set st Y in F holds
Y is Equivalence_Relation of X by A1;
then reconsider EqR = meet F as Equivalence_Relation of X by A2, Th11;
A3: now__::_thesis:_for_EqR2_being_Equivalence_Relation_of_X_st_R_c=_EqR2_holds_
EqR_c=_EqR2
let EqR2 be Equivalence_Relation of X; ::_thesis: ( R c= EqR2 implies EqR c= EqR2 )
assume R c= EqR2 ; ::_thesis: EqR c= EqR2
then EqR2 in F by A1;
hence EqR c= EqR2 by SETFAM_1:3; ::_thesis: verum
end;
take EqR ; ::_thesis: ( R c= EqR & ( for EqR2 being Equivalence_Relation of X st R c= EqR2 holds
EqR c= EqR2 ) )
for Y being set st Y in F holds
R c= Y by A1;
hence ( R c= EqR & ( for EqR2 being Equivalence_Relation of X st R c= EqR2 holds
EqR c= EqR2 ) ) by A2, A3, SETFAM_1:5; ::_thesis: verum
end;
definition
let X be set ;
let EqR1, EqR2 be Equivalence_Relation of X;
funcEqR1 "\/" EqR2 -> Equivalence_Relation of X means :Def2: :: EQREL_1:def 2
( EqR1 \/ EqR2 c= it & ( for EqR being Equivalence_Relation of X st EqR1 \/ EqR2 c= EqR holds
it c= EqR ) );
existence
ex b1 being Equivalence_Relation of X st
( EqR1 \/ EqR2 c= b1 & ( for EqR being Equivalence_Relation of X st EqR1 \/ EqR2 c= EqR holds
b1 c= EqR ) ) by Th12;
uniqueness
for b1, b2 being Equivalence_Relation of X st EqR1 \/ EqR2 c= b1 & ( for EqR being Equivalence_Relation of X st EqR1 \/ EqR2 c= EqR holds
b1 c= EqR ) & EqR1 \/ EqR2 c= b2 & ( for EqR being Equivalence_Relation of X st EqR1 \/ EqR2 c= EqR holds
b2 c= EqR ) holds
b1 = b2
proof
let R1, R2 be Equivalence_Relation of X; ::_thesis: ( EqR1 \/ EqR2 c= R1 & ( for EqR being Equivalence_Relation of X st EqR1 \/ EqR2 c= EqR holds
R1 c= EqR ) & EqR1 \/ EqR2 c= R2 & ( for EqR being Equivalence_Relation of X st EqR1 \/ EqR2 c= EqR holds
R2 c= EqR ) implies R1 = R2 )
assume ( EqR1 \/ EqR2 c= R1 & ( for EqR being Equivalence_Relation of X st EqR1 \/ EqR2 c= EqR holds
R1 c= EqR ) & EqR1 \/ EqR2 c= R2 & ( for EqR being Equivalence_Relation of X st EqR1 \/ EqR2 c= EqR holds
R2 c= EqR ) ) ; ::_thesis: R1 = R2
then ( R1 c= R2 & R2 c= R1 ) ;
hence R1 = R2 by XBOOLE_0:def_10; ::_thesis: verum
end;
commutativity
for b1, EqR1, EqR2 being Equivalence_Relation of X st EqR1 \/ EqR2 c= b1 & ( for EqR being Equivalence_Relation of X st EqR1 \/ EqR2 c= EqR holds
b1 c= EqR ) holds
( EqR2 \/ EqR1 c= b1 & ( for EqR being Equivalence_Relation of X st EqR2 \/ EqR1 c= EqR holds
b1 c= EqR ) ) ;
idempotence
for EqR1 being Equivalence_Relation of X holds
( EqR1 \/ EqR1 c= EqR1 & ( for EqR being Equivalence_Relation of X st EqR1 \/ EqR1 c= EqR holds
EqR1 c= EqR ) ) ;
end;
:: deftheorem Def2 defines "\/" EQREL_1:def_2_:_
for X being set
for EqR1, EqR2, b4 being Equivalence_Relation of X holds
( b4 = EqR1 "\/" EqR2 iff ( EqR1 \/ EqR2 c= b4 & ( for EqR being Equivalence_Relation of X st EqR1 \/ EqR2 c= EqR holds
b4 c= EqR ) ) );
theorem :: EQREL_1:13
for X being set
for EqR1, EqR2, EqR3 being Equivalence_Relation of X holds (EqR1 "\/" EqR2) "\/" EqR3 = EqR1 "\/" (EqR2 "\/" EqR3)
proof
let X be set ; ::_thesis: for EqR1, EqR2, EqR3 being Equivalence_Relation of X holds (EqR1 "\/" EqR2) "\/" EqR3 = EqR1 "\/" (EqR2 "\/" EqR3)
let EqR1, EqR2, EqR3 be Equivalence_Relation of X; ::_thesis: (EqR1 "\/" EqR2) "\/" EqR3 = EqR1 "\/" (EqR2 "\/" EqR3)
for EqR4 being Equivalence_Relation of X st EqR4 = EqR1 "\/" (EqR2 "\/" EqR3) holds
(EqR1 "\/" EqR2) "\/" EqR3 c= EqR4
proof
let EqR4 be Equivalence_Relation of X; ::_thesis: ( EqR4 = EqR1 "\/" (EqR2 "\/" EqR3) implies (EqR1 "\/" EqR2) "\/" EqR3 c= EqR4 )
A1: EqR2 \/ EqR3 c= EqR2 "\/" EqR3 by Def2;
assume EqR4 = EqR1 "\/" (EqR2 "\/" EqR3) ; ::_thesis: (EqR1 "\/" EqR2) "\/" EqR3 c= EqR4
then A2: EqR1 \/ (EqR2 "\/" EqR3) c= EqR4 by Def2;
EqR2 "\/" EqR3 c= EqR1 \/ (EqR2 "\/" EqR3) by XBOOLE_1:7;
then EqR2 "\/" EqR3 c= EqR4 by A2, XBOOLE_1:1;
then A3: EqR2 \/ EqR3 c= EqR4 by A1, XBOOLE_1:1;
EqR2 c= EqR2 \/ EqR3 by XBOOLE_1:7;
then A4: EqR2 c= EqR4 by A3, XBOOLE_1:1;
EqR1 c= EqR1 \/ (EqR2 "\/" EqR3) by XBOOLE_1:7;
then EqR1 c= EqR4 by A2, XBOOLE_1:1;
then EqR1 \/ EqR2 c= EqR4 by A4, XBOOLE_1:8;
then A5: EqR1 "\/" EqR2 c= EqR4 by Def2;
EqR3 c= EqR2 \/ EqR3 by XBOOLE_1:7;
then EqR3 c= EqR4 by A3, XBOOLE_1:1;
then (EqR1 "\/" EqR2) \/ EqR3 c= EqR4 by A5, XBOOLE_1:8;
hence (EqR1 "\/" EqR2) "\/" EqR3 c= EqR4 by Def2; ::_thesis: verum
end;
then A6: (EqR1 "\/" EqR2) "\/" EqR3 c= EqR1 "\/" (EqR2 "\/" EqR3) ;
for EqR4 being Equivalence_Relation of X st EqR4 = (EqR1 "\/" EqR2) "\/" EqR3 holds
EqR1 "\/" (EqR2 "\/" EqR3) c= EqR4
proof
let EqR4 be Equivalence_Relation of X; ::_thesis: ( EqR4 = (EqR1 "\/" EqR2) "\/" EqR3 implies EqR1 "\/" (EqR2 "\/" EqR3) c= EqR4 )
A7: EqR1 \/ EqR2 c= EqR1 "\/" EqR2 by Def2;
assume EqR4 = (EqR1 "\/" EqR2) "\/" EqR3 ; ::_thesis: EqR1 "\/" (EqR2 "\/" EqR3) c= EqR4
then A8: (EqR1 "\/" EqR2) \/ EqR3 c= EqR4 by Def2;
EqR1 "\/" EqR2 c= (EqR1 "\/" EqR2) \/ EqR3 by XBOOLE_1:7;
then EqR1 "\/" EqR2 c= EqR4 by A8, XBOOLE_1:1;
then A9: EqR1 \/ EqR2 c= EqR4 by A7, XBOOLE_1:1;
EqR3 c= (EqR1 "\/" EqR2) \/ EqR3 by XBOOLE_1:7;
then A10: EqR3 c= EqR4 by A8, XBOOLE_1:1;
EqR2 c= EqR1 \/ EqR2 by XBOOLE_1:7;
then EqR2 c= EqR4 by A9, XBOOLE_1:1;
then EqR2 \/ EqR3 c= EqR4 by A10, XBOOLE_1:8;
then A11: EqR2 "\/" EqR3 c= EqR4 by Def2;
EqR1 c= EqR1 \/ EqR2 by XBOOLE_1:7;
then EqR1 c= EqR4 by A9, XBOOLE_1:1;
then EqR1 \/ (EqR2 "\/" EqR3) c= EqR4 by A11, XBOOLE_1:8;
hence EqR1 "\/" (EqR2 "\/" EqR3) c= EqR4 by Def2; ::_thesis: verum
end;
then EqR1 "\/" (EqR2 "\/" EqR3) c= (EqR1 "\/" EqR2) "\/" EqR3 ;
hence (EqR1 "\/" EqR2) "\/" EqR3 = EqR1 "\/" (EqR2 "\/" EqR3) by A6, XBOOLE_0:def_10; ::_thesis: verum
end;
theorem :: EQREL_1:14
for X being set
for EqR being Equivalence_Relation of X holds EqR "\/" EqR = EqR ;
theorem :: EQREL_1:15
for X being set
for EqR1, EqR2 being Equivalence_Relation of X holds EqR1 "\/" EqR2 = EqR2 "\/" EqR1 ;
theorem :: EQREL_1:16
for X being set
for EqR1, EqR2 being Equivalence_Relation of X holds EqR1 /\ (EqR1 "\/" EqR2) = EqR1
proof
let X be set ; ::_thesis: for EqR1, EqR2 being Equivalence_Relation of X holds EqR1 /\ (EqR1 "\/" EqR2) = EqR1
let EqR1, EqR2 be Equivalence_Relation of X; ::_thesis: EqR1 /\ (EqR1 "\/" EqR2) = EqR1
thus EqR1 /\ (EqR1 "\/" EqR2) c= EqR1 by XBOOLE_1:17; :: according to XBOOLE_0:def_10 ::_thesis: EqR1 c= EqR1 /\ (EqR1 "\/" EqR2)
( EqR1 c= EqR1 \/ EqR2 & EqR1 \/ EqR2 c= EqR1 "\/" EqR2 ) by Def2, XBOOLE_1:7;
then EqR1 c= EqR1 "\/" EqR2 by XBOOLE_1:1;
hence EqR1 c= EqR1 /\ (EqR1 "\/" EqR2) by XBOOLE_1:19; ::_thesis: verum
end;
theorem :: EQREL_1:17
for X being set
for EqR1, EqR2 being Equivalence_Relation of X holds EqR1 "\/" (EqR1 /\ EqR2) = EqR1
proof
let X be set ; ::_thesis: for EqR1, EqR2 being Equivalence_Relation of X holds EqR1 "\/" (EqR1 /\ EqR2) = EqR1
let EqR1, EqR2 be Equivalence_Relation of X; ::_thesis: EqR1 "\/" (EqR1 /\ EqR2) = EqR1
( EqR1 = EqR1 \/ (EqR1 /\ EqR2) & ( for EqR being Equivalence_Relation of X st EqR1 \/ (EqR1 /\ EqR2) c= EqR holds
EqR1 c= EqR ) ) by XBOOLE_1:22;
hence EqR1 "\/" (EqR1 /\ EqR2) = EqR1 by Def2; ::_thesis: verum
end;
scheme :: EQREL_1:sch 1
ExEqRel{ F1() -> set , P1[ set , set ] } :
ex EqR being Equivalence_Relation of F1() st
for x, y being set holds
( [x,y] in EqR iff ( x in F1() & y in F1() & P1[x,y] ) )
provided
A1: for x being set st x in F1() holds
P1[x,x] and
A2: for x, y being set st P1[x,y] holds
P1[y,x] and
A3: for x, y, z being set st P1[x,y] & P1[y,z] holds
P1[x,z]
proof
consider Y being Relation of F1(),F1() such that
A4: for x, y being set holds
( [x,y] in Y iff ( x in F1() & y in F1() & P1[x,y] ) ) from RELSET_1:sch_1();
A5: Y is_transitive_in F1()
proof
let x be set ; :: according to RELAT_2:def_8 ::_thesis: for b1, b2 being set holds
( not x in F1() or not b1 in F1() or not b2 in F1() or not [x,b1] in Y or not [b1,b2] in Y or [x,b2] in Y )
let y, z be set ; ::_thesis: ( not x in F1() or not y in F1() or not z in F1() or not [x,y] in Y or not [y,z] in Y or [x,z] in Y )
assume that
A6: x in F1() and
y in F1() and
A7: z in F1() and
A8: ( [x,y] in Y & [y,z] in Y ) ; ::_thesis: [x,z] in Y
( P1[x,y] & P1[y,z] ) by A4, A8;
then P1[x,z] by A3;
hence [x,z] in Y by A4, A6, A7; ::_thesis: verum
end;
A9: Y is_symmetric_in F1()
proof
let x be set ; :: according to RELAT_2:def_3 ::_thesis: for b1 being set holds
( not x in F1() or not b1 in F1() or not [x,b1] in Y or [b1,x] in Y )
let y be set ; ::_thesis: ( not x in F1() or not y in F1() or not [x,y] in Y or [y,x] in Y )
assume that
A10: ( x in F1() & y in F1() ) and
A11: [x,y] in Y ; ::_thesis: [y,x] in Y
P1[x,y] by A4, A11;
then P1[y,x] by A2;
hence [y,x] in Y by A4, A10; ::_thesis: verum
end;
Y is_reflexive_in F1()
proof
let x be set ; :: according to RELAT_2:def_1 ::_thesis: ( not x in F1() or [x,x] in Y )
assume A12: x in F1() ; ::_thesis: [x,x] in Y
then P1[x,x] by A1;
hence [x,x] in Y by A4, A12; ::_thesis: verum
end;
then ( field Y = F1() & dom Y = F1() ) by ORDERS_1:13;
then reconsider R1 = Y as Equivalence_Relation of F1() by A9, A5, PARTFUN1:def_2, RELAT_2:def_11, RELAT_2:def_16;
take R1 ; ::_thesis: for x, y being set holds
( [x,y] in R1 iff ( x in F1() & y in F1() & P1[x,y] ) )
thus for x, y being set holds
( [x,y] in R1 iff ( x in F1() & y in F1() & P1[x,y] ) ) by A4; ::_thesis: verum
end;
notation
let R be Relation;
let x be set ;
synonym Class (R,x) for Im (R,x);
end;
definition
let X, Y be set ;
let R be Relation of X,Y;
let x be set ;
:: original: Class
redefine func Class (R,x) -> Subset of Y;
coherence
Class (R,x) is Subset of Y
proof
R .: {x} c= Y ;
hence Class (R,x) is Subset of Y ; ::_thesis: verum
end;
end;
theorem :: EQREL_1:18
for y, x being set
for R being Relation holds
( y in Class (R,x) iff [x,y] in R )
proof
let y, x be set ; ::_thesis: for R being Relation holds
( y in Class (R,x) iff [x,y] in R )
let R be Relation; ::_thesis: ( y in Class (R,x) iff [x,y] in R )
thus ( y in Class (R,x) implies [x,y] in R ) ::_thesis: ( [x,y] in R implies y in Class (R,x) )
proof
assume y in Class (R,x) ; ::_thesis: [x,y] in R
then ex z being set st
( [z,y] in R & z in {x} ) by RELAT_1:def_13;
hence [x,y] in R by TARSKI:def_1; ::_thesis: verum
end;
A1: x in {x} by TARSKI:def_1;
assume [x,y] in R ; ::_thesis: y in Class (R,x)
hence y in Class (R,x) by A1, RELAT_1:def_13; ::_thesis: verum
end;
theorem Th19: :: EQREL_1:19
for X, y, x being set
for R being symmetric total Relation of X holds
( y in Class (R,x) iff [y,x] in R )
proof
let X, y, x be set ; ::_thesis: for R being symmetric total Relation of X holds
( y in Class (R,x) iff [y,x] in R )
let R be symmetric total Relation of X; ::_thesis: ( y in Class (R,x) iff [y,x] in R )
thus ( y in Class (R,x) implies [y,x] in R ) ::_thesis: ( [y,x] in R implies y in Class (R,x) )
proof
assume y in Class (R,x) ; ::_thesis: [y,x] in R
then ex z being set st
( [z,y] in R & z in {x} ) by RELAT_1:def_13;
then [x,y] in R by TARSKI:def_1;
hence [y,x] in R by Th6; ::_thesis: verum
end;
assume [y,x] in R ; ::_thesis: y in Class (R,x)
then A1: [x,y] in R by Th6;
x in {x} by TARSKI:def_1;
hence y in Class (R,x) by A1, RELAT_1:def_13; ::_thesis: verum
end;
theorem Th20: :: EQREL_1:20
for X being set
for R being Tolerance of X
for x being set st x in X holds
x in Class (R,x)
proof
let X be set ; ::_thesis: for R being Tolerance of X
for x being set st x in X holds
x in Class (R,x)
let R be Tolerance of X; ::_thesis: for x being set st x in X holds
x in Class (R,x)
let x be set ; ::_thesis: ( x in X implies x in Class (R,x) )
assume x in X ; ::_thesis: x in Class (R,x)
then [x,x] in R by Th5;
hence x in Class (R,x) by Th19; ::_thesis: verum
end;
theorem :: EQREL_1:21
for X being set
for R being Tolerance of X
for x being set st x in X holds
ex y being set st x in Class (R,y)
proof
let X be set ; ::_thesis: for R being Tolerance of X
for x being set st x in X holds
ex y being set st x in Class (R,y)
let R be Tolerance of X; ::_thesis: for x being set st x in X holds
ex y being set st x in Class (R,y)
let x be set ; ::_thesis: ( x in X implies ex y being set st x in Class (R,y) )
assume x in X ; ::_thesis: ex y being set st x in Class (R,y)
then x in Class (R,x) by Th20;
hence ex y being set st x in Class (R,y) ; ::_thesis: verum
end;
theorem :: EQREL_1:22
for X, y, x, z being set
for R being transitive Tolerance of X st y in Class (R,x) & z in Class (R,x) holds
[y,z] in R
proof
let X, y, x, z be set ; ::_thesis: for R being transitive Tolerance of X st y in Class (R,x) & z in Class (R,x) holds
[y,z] in R
let R be transitive Tolerance of X; ::_thesis: ( y in Class (R,x) & z in Class (R,x) implies [y,z] in R )
assume that
A1: y in Class (R,x) and
A2: z in Class (R,x) ; ::_thesis: [y,z] in R
[z,x] in R by A2, Th19;
then A3: [x,z] in R by Th6;
[y,x] in R by A1, Th19;
hence [y,z] in R by A3, Th7; ::_thesis: verum
end;
Lm2: for X, y being set
for EqR being Equivalence_Relation of X
for x being set st x in X holds
( [x,y] in EqR iff Class (EqR,x) = Class (EqR,y) )
proof
let X, y be set ; ::_thesis: for EqR being Equivalence_Relation of X
for x being set st x in X holds
( [x,y] in EqR iff Class (EqR,x) = Class (EqR,y) )
let EqR be Equivalence_Relation of X; ::_thesis: for x being set st x in X holds
( [x,y] in EqR iff Class (EqR,x) = Class (EqR,y) )
let x be set ; ::_thesis: ( x in X implies ( [x,y] in EqR iff Class (EqR,x) = Class (EqR,y) ) )
assume A1: x in X ; ::_thesis: ( [x,y] in EqR iff Class (EqR,x) = Class (EqR,y) )
thus ( [x,y] in EqR implies Class (EqR,x) = Class (EqR,y) ) ::_thesis: ( Class (EqR,x) = Class (EqR,y) implies [x,y] in EqR )
proof
assume A2: [x,y] in EqR ; ::_thesis: Class (EqR,x) = Class (EqR,y)
now__::_thesis:_for_z_being_set_st_z_in_Class_(EqR,y)_holds_
z_in_Class_(EqR,x)
let z be set ; ::_thesis: ( z in Class (EqR,y) implies z in Class (EqR,x) )
assume z in Class (EqR,y) ; ::_thesis: z in Class (EqR,x)
then A3: [z,y] in EqR by Th19;
[y,x] in EqR by A2, Th6;
then [z,x] in EqR by A3, Th7;
hence z in Class (EqR,x) by Th19; ::_thesis: verum
end;
then A4: Class (EqR,y) c= Class (EqR,x) by TARSKI:def_3;
now__::_thesis:_for_z_being_set_st_z_in_Class_(EqR,x)_holds_
z_in_Class_(EqR,y)
let z be set ; ::_thesis: ( z in Class (EqR,x) implies z in Class (EqR,y) )
assume z in Class (EqR,x) ; ::_thesis: z in Class (EqR,y)
then [z,x] in EqR by Th19;
then [z,y] in EqR by A2, Th7;
hence z in Class (EqR,y) by Th19; ::_thesis: verum
end;
then Class (EqR,x) c= Class (EqR,y) by TARSKI:def_3;
hence Class (EqR,x) = Class (EqR,y) by A4, XBOOLE_0:def_10; ::_thesis: verum
end;
assume Class (EqR,x) = Class (EqR,y) ; ::_thesis: [x,y] in EqR
then x in Class (EqR,y) by A1, Th20;
hence [x,y] in EqR by Th19; ::_thesis: verum
end;
theorem Th23: :: EQREL_1:23
for X, y being set
for EqR being Equivalence_Relation of X
for x being set st x in X holds
( y in Class (EqR,x) iff Class (EqR,x) = Class (EqR,y) )
proof
let X, y be set ; ::_thesis: for EqR being Equivalence_Relation of X
for x being set st x in X holds
( y in Class (EqR,x) iff Class (EqR,x) = Class (EqR,y) )
let EqR be Equivalence_Relation of X; ::_thesis: for x being set st x in X holds
( y in Class (EqR,x) iff Class (EqR,x) = Class (EqR,y) )
let x be set ; ::_thesis: ( x in X implies ( y in Class (EqR,x) iff Class (EqR,x) = Class (EqR,y) ) )
assume A1: x in X ; ::_thesis: ( y in Class (EqR,x) iff Class (EqR,x) = Class (EqR,y) )
thus ( y in Class (EqR,x) implies Class (EqR,x) = Class (EqR,y) ) ::_thesis: ( Class (EqR,x) = Class (EqR,y) implies y in Class (EqR,x) )
proof
assume y in Class (EqR,x) ; ::_thesis: Class (EqR,x) = Class (EqR,y)
then [y,x] in EqR by Th19;
then [x,y] in EqR by Th6;
hence Class (EqR,x) = Class (EqR,y) by A1, Lm2; ::_thesis: verum
end;
assume Class (EqR,x) = Class (EqR,y) ; ::_thesis: y in Class (EqR,x)
then [x,y] in EqR by A1, Lm2;
then [y,x] in EqR by Th6;
hence y in Class (EqR,x) by Th19; ::_thesis: verum
end;
theorem Th24: :: EQREL_1:24
for X being set
for EqR being Equivalence_Relation of X
for x, y being set holds
( not y in X or Class (EqR,x) = Class (EqR,y) or Class (EqR,x) misses Class (EqR,y) )
proof
let X be set ; ::_thesis: for EqR being Equivalence_Relation of X
for x, y being set holds
( not y in X or Class (EqR,x) = Class (EqR,y) or Class (EqR,x) misses Class (EqR,y) )
let EqR be Equivalence_Relation of X; ::_thesis: for x, y being set holds
( not y in X or Class (EqR,x) = Class (EqR,y) or Class (EqR,x) misses Class (EqR,y) )
let x, y be set ; ::_thesis: ( not y in X or Class (EqR,x) = Class (EqR,y) or Class (EqR,x) misses Class (EqR,y) )
A1: ( not [x,y] in EqR implies Class (EqR,x) misses Class (EqR,y) )
proof
assume A2: not [x,y] in EqR ; ::_thesis: Class (EqR,x) misses Class (EqR,y)
assume Class (EqR,x) meets Class (EqR,y) ; ::_thesis: contradiction
then consider z being set such that
A3: z in Class (EqR,x) and
A4: z in Class (EqR,y) by XBOOLE_0:3;
[z,x] in EqR by A3, Th19;
then A5: [x,z] in EqR by Th6;
[z,y] in EqR by A4, Th19;
hence contradiction by A2, A5, Th7; ::_thesis: verum
end;
assume A6: y in X ; ::_thesis: ( Class (EqR,x) = Class (EqR,y) or Class (EqR,x) misses Class (EqR,y) )
( [x,y] in EqR implies Class (EqR,x) = Class (EqR,y) )
proof
assume [x,y] in EqR ; ::_thesis: Class (EqR,x) = Class (EqR,y)
then x in Class (EqR,y) by Th19;
hence Class (EqR,x) = Class (EqR,y) by A6, Th23; ::_thesis: verum
end;
hence ( Class (EqR,x) = Class (EqR,y) or Class (EqR,x) misses Class (EqR,y) ) by A1; ::_thesis: verum
end;
theorem Th25: :: EQREL_1:25
for X, x being set st x in X holds
Class ((id X),x) = {x}
proof
let X, x be set ; ::_thesis: ( x in X implies Class ((id X),x) = {x} )
A1: now__::_thesis:_for_y_being_set_st_y_in_Class_((id_X),x)_holds_
y_=_x
let y be set ; ::_thesis: ( y in Class ((id X),x) implies y = x )
assume y in Class ((id X),x) ; ::_thesis: y = x
then [y,x] in id X by Th19;
hence y = x by RELAT_1:def_10; ::_thesis: verum
end;
assume x in X ; ::_thesis: Class ((id X),x) = {x}
then for y being set holds
( y in Class ((id X),x) iff y = x ) by A1, Th20;
hence Class ((id X),x) = {x} by TARSKI:def_1; ::_thesis: verum
end;
theorem Th26: :: EQREL_1:26
for X, x being set st x in X holds
Class ((nabla X),x) = X
proof
let X, x be set ; ::_thesis: ( x in X implies Class ((nabla X),x) = X )
assume A1: x in X ; ::_thesis: Class ((nabla X),x) = X
now__::_thesis:_for_y_being_set_st_y_in_X_holds_
y_in_Class_((nabla_X),x)
let y be set ; ::_thesis: ( y in X implies y in Class ((nabla X),x) )
assume y in X ; ::_thesis: y in Class ((nabla X),x)
then [y,x] in nabla X by A1, ZFMISC_1:87;
hence y in Class ((nabla X),x) by Th19; ::_thesis: verum
end;
then for y being set holds
( y in X iff y in Class ((nabla X),x) ) ;
hence Class ((nabla X),x) = X by TARSKI:1; ::_thesis: verum
end;
theorem Th27: :: EQREL_1:27
for X being set
for EqR being Equivalence_Relation of X st ex x being set st Class (EqR,x) = X holds
EqR = nabla X
proof
let X be set ; ::_thesis: for EqR being Equivalence_Relation of X st ex x being set st Class (EqR,x) = X holds
EqR = nabla X
let EqR be Equivalence_Relation of X; ::_thesis: ( ex x being set st Class (EqR,x) = X implies EqR = nabla X )
given x being set such that A1: Class (EqR,x) = X ; ::_thesis: EqR = nabla X
[:X,X:] c= EqR
proof
let y be set ; :: according to RELAT_1:def_3 ::_thesis: for b1 being set holds
( not [y,b1] in [:X,X:] or [y,b1] in EqR )
let z be set ; ::_thesis: ( not [y,z] in [:X,X:] or [y,z] in EqR )
assume A2: [y,z] in [:X,X:] ; ::_thesis: [y,z] in EqR
then z in Class (EqR,x) by A1, ZFMISC_1:87;
then [z,x] in EqR by Th19;
then A3: [x,z] in EqR by Th6;
y in Class (EqR,x) by A1, A2, ZFMISC_1:87;
then [y,x] in EqR by Th19;
hence [y,z] in EqR by A3, Th7; ::_thesis: verum
end;
hence EqR = nabla X by XBOOLE_0:def_10; ::_thesis: verum
end;
theorem :: EQREL_1:28
for x, X, y being set
for EqR1, EqR2 being Equivalence_Relation of X st x in X holds
( [x,y] in EqR1 "\/" EqR2 iff ex f being FinSequence st
( 1 <= len f & x = f . 1 & y = f . (len f) & ( for i being Element of NAT st 1 <= i & i < len f holds
[(f . i),(f . (i + 1))] in EqR1 \/ EqR2 ) ) )
proof
let x, X, y be set ; ::_thesis: for EqR1, EqR2 being Equivalence_Relation of X st x in X holds
( [x,y] in EqR1 "\/" EqR2 iff ex f being FinSequence st
( 1 <= len f & x = f . 1 & y = f . (len f) & ( for i being Element of NAT st 1 <= i & i < len f holds
[(f . i),(f . (i + 1))] in EqR1 \/ EqR2 ) ) )
let EqR1, EqR2 be Equivalence_Relation of X; ::_thesis: ( x in X implies ( [x,y] in EqR1 "\/" EqR2 iff ex f being FinSequence st
( 1 <= len f & x = f . 1 & y = f . (len f) & ( for i being Element of NAT st 1 <= i & i < len f holds
[(f . i),(f . (i + 1))] in EqR1 \/ EqR2 ) ) ) )
assume A1: x in X ; ::_thesis: ( [x,y] in EqR1 "\/" EqR2 iff ex f being FinSequence st
( 1 <= len f & x = f . 1 & y = f . (len f) & ( for i being Element of NAT st 1 <= i & i < len f holds
[(f . i),(f . (i + 1))] in EqR1 \/ EqR2 ) ) )
thus ( [x,y] in EqR1 "\/" EqR2 implies ex f being FinSequence st
( 1 <= len f & x = f . 1 & y = f . (len f) & ( for i being Element of NAT st 1 <= i & i < len f holds
[(f . i),(f . (i + 1))] in EqR1 \/ EqR2 ) ) ) ::_thesis: ( ex f being FinSequence st
( 1 <= len f & x = f . 1 & y = f . (len f) & ( for i being Element of NAT st 1 <= i & i < len f holds
[(f . i),(f . (i + 1))] in EqR1 \/ EqR2 ) ) implies [x,y] in EqR1 "\/" EqR2 )
proof
defpred S1[ set , set ] means ex f being FinSequence st
( 1 <= len f & $1 = f . 1 & $2 = f . (len f) & ( for i being Element of NAT st 1 <= i & i < len f holds
[(f . i),(f . (i + 1))] in EqR1 \/ EqR2 ) );
consider Y being Relation of X,X such that
A2: for x, y being set holds
( [x,y] in Y iff ( x in X & y in X & S1[x,y] ) ) from RELSET_1:sch_1();
A3: Y is_transitive_in X
proof
let x be set ; :: according to RELAT_2:def_8 ::_thesis: for b1, b2 being set holds
( not x in X or not b1 in X or not b2 in X or not [x,b1] in Y or not [b1,b2] in Y or [x,b2] in Y )
let y, z be set ; ::_thesis: ( not x in X or not y in X or not z in X or not [x,y] in Y or not [y,z] in Y or [x,z] in Y )
assume that
A4: x in X and
A5: y in X and
A6: z in X and
A7: [x,y] in Y and
A8: [y,z] in Y ; ::_thesis: [x,z] in Y
consider g being FinSequence such that
A9: 1 <= len g and
A10: y = g . 1 and
A11: z = g . (len g) and
A12: for i being Element of NAT st 1 <= i & i < len g holds
[(g . i),(g . (i + 1))] in EqR1 \/ EqR2 by A2, A8;
consider f being FinSequence such that
A13: 1 <= len f and
A14: x = f . 1 and
A15: y = f . (len f) and
A16: for i being Element of NAT st 1 <= i & i < len f holds
[(f . i),(f . (i + 1))] in EqR1 \/ EqR2 by A2, A7;
set h = f ^ g;
A17: len (f ^ g) = (len f) + (len g) by FINSEQ_1:22;
A18: (len f) + 1 <= (len f) + (len g) by A9, XREAL_1:7;
then A19: (f ^ g) . (len (f ^ g)) = g . (((len g) + (len f)) - (len f)) by A17, FINSEQ_1:23
.= g . (len g) ;
A20: for i being Element of NAT st 1 <= i & i < len (f ^ g) holds
[((f ^ g) . i),((f ^ g) . (i + 1))] in EqR1 \/ EqR2
proof
let i be Element of NAT ; ::_thesis: ( 1 <= i & i < len (f ^ g) implies [((f ^ g) . i),((f ^ g) . (i + 1))] in EqR1 \/ EqR2 )
assume that
A21: 1 <= i and
A22: i < len (f ^ g) ; ::_thesis: [((f ^ g) . i),((f ^ g) . (i + 1))] in EqR1 \/ EqR2
A23: ( ( 1 <= i & i < len f ) or i = len f or len f < i ) by A21, XXREAL_0:1;
now__::_thesis:_[((f_^_g)_._i),((f_^_g)_._(i_+_1))]_in_EqR1_\/_EqR2
percases ( ( 1 <= i & i < len f ) or i = len f or ( (len f) + 1 <= i & i < len (f ^ g) ) ) by A22, A23, NAT_1:13;
supposeA24: ( 1 <= i & i < len f ) ; ::_thesis: [((f ^ g) . i),((f ^ g) . (i + 1))] in EqR1 \/ EqR2
then ( 1 <= i + 1 & i + 1 <= len f ) by NAT_1:13;
then i + 1 in Seg (len f) by FINSEQ_1:1;
then i + 1 in dom f by FINSEQ_1:def_3;
then A25: (f ^ g) . (i + 1) = f . (i + 1) by FINSEQ_1:def_7;
i in Seg (len f) by A24, FINSEQ_1:1;
then i in dom f by FINSEQ_1:def_3;
then (f ^ g) . i = f . i by FINSEQ_1:def_7;
hence [((f ^ g) . i),((f ^ g) . (i + 1))] in EqR1 \/ EqR2 by A16, A24, A25; ::_thesis: verum
end;
supposeA26: i = len f ; ::_thesis: [((f ^ g) . i),((f ^ g) . (i + 1))] in EqR1 \/ EqR2
len f in Seg (len f) by A13, FINSEQ_1:1;
then len f in dom f by FINSEQ_1:def_3;
then A27: (f ^ g) . i = y by A15, A26, FINSEQ_1:def_7;
A28: [y,y] in EqR1 by A5, Th5;
(f ^ g) . (i + 1) = g . ((1 + (len f)) - (len f)) by A18, A26, FINSEQ_1:23
.= y by A10 ;
hence [((f ^ g) . i),((f ^ g) . (i + 1))] in EqR1 \/ EqR2 by A27, A28, XBOOLE_0:def_3; ::_thesis: verum
end;
supposeA29: ( (len f) + 1 <= i & i < len (f ^ g) ) ; ::_thesis: [((f ^ g) . i),((f ^ g) . (i + 1))] in EqR1 \/ EqR2
then len f < i by NAT_1:13;
then reconsider k = i - (len f) as Element of NAT by NAT_1:21;
i < (len f) + (len g) by A29, FINSEQ_1:22;
then A30: i - (len f) < len g by XREAL_1:19;
( (len f) + 1 <= i + 1 & i + 1 <= (len f) + (len g) ) by A17, A29, NAT_1:13;
then A31: (f ^ g) . (i + 1) = g . ((1 + i) - (len f)) by FINSEQ_1:23
.= g . ((i - (len f)) + 1) ;
(1 + (len f)) - (len f) <= i - (len f) by A29, XREAL_1:9;
then [(g . k),(g . (k + 1))] in EqR1 \/ EqR2 by A12, A30;
hence [((f ^ g) . i),((f ^ g) . (i + 1))] in EqR1 \/ EqR2 by A17, A29, A31, FINSEQ_1:23; ::_thesis: verum
end;
end;
end;
hence [((f ^ g) . i),((f ^ g) . (i + 1))] in EqR1 \/ EqR2 ; ::_thesis: verum
end;
1 in Seg (len f) by A13, FINSEQ_1:1;
then 1 in dom f by FINSEQ_1:def_3;
then A32: x = (f ^ g) . 1 by A14, FINSEQ_1:def_7;
1 <= len (f ^ g) by A13, A17, NAT_1:12;
hence [x,z] in Y by A2, A4, A6, A11, A32, A19, A20; ::_thesis: verum
end;
A33: Y is_symmetric_in X
proof
let x be set ; :: according to RELAT_2:def_3 ::_thesis: for b1 being set holds
( not x in X or not b1 in X or not [x,b1] in Y or [b1,x] in Y )
let y be set ; ::_thesis: ( not x in X or not y in X or not [x,y] in Y or [y,x] in Y )
assume that
A34: ( x in X & y in X ) and
A35: [x,y] in Y ; ::_thesis: [y,x] in Y
consider f being FinSequence such that
A36: 1 <= len f and
A37: x = f . 1 and
A38: y = f . (len f) and
A39: for i being Element of NAT st 1 <= i & i < len f holds
[(f . i),(f . (i + 1))] in EqR1 \/ EqR2 by A2, A35;
defpred S2[ Nat, set ] means $2 = f . ((1 + (len f)) - $1);
A40: for k being Nat st k in Seg (len f) holds
ex z being set st S2[k,z] ;
consider g being FinSequence such that
A41: ( dom g = Seg (len f) & ( for k being Nat st k in Seg (len f) holds
S2[k,g . k] ) ) from FINSEQ_1:sch_1(A40);
A42: len f = len g by A41, FINSEQ_1:def_3;
A43: for j being Element of NAT st 1 <= j & j < len g holds
[(g . j),(g . (j + 1))] in EqR1 \/ EqR2
proof
let j be Element of NAT ; ::_thesis: ( 1 <= j & j < len g implies [(g . j),(g . (j + 1))] in EqR1 \/ EqR2 )
assume that
A44: 1 <= j and
A45: j < len g ; ::_thesis: [(g . j),(g . (j + 1))] in EqR1 \/ EqR2
reconsider k = (len f) - j as Element of NAT by A42, A45, NAT_1:21;
j - (len f) < (len f) - (len f) by A42, A45, XREAL_1:9;
then - ((len f) - j) < - 0 ;
then 0 < k ;
then A46: 0 + 1 <= k by NAT_1:13;
- j < - 0 by A44, XREAL_1:24;
then (len f) + (- j) < 0 + (len f) by XREAL_1:6;
then A47: [(f . k),(f . (k + 1))] in EqR1 \/ EqR2 by A39, A46;
A48: now__::_thesis:_[(f_._(k_+_1)),(f_._k)]_in_EqR1_\/_EqR2
percases ( [(f . k),(f . (k + 1))] in EqR1 or [(f . k),(f . (k + 1))] in EqR2 ) by A47, XBOOLE_0:def_3;
suppose [(f . k),(f . (k + 1))] in EqR1 ; ::_thesis: [(f . (k + 1)),(f . k)] in EqR1 \/ EqR2
then [(f . (k + 1)),(f . k)] in EqR1 by Th6;
hence [(f . (k + 1)),(f . k)] in EqR1 \/ EqR2 by XBOOLE_0:def_3; ::_thesis: verum
end;
suppose [(f . k),(f . (k + 1))] in EqR2 ; ::_thesis: [(f . (k + 1)),(f . k)] in EqR1 \/ EqR2
then [(f . (k + 1)),(f . k)] in EqR2 by Th6;
hence [(f . (k + 1)),(f . k)] in EqR1 \/ EqR2 by XBOOLE_0:def_3; ::_thesis: verum
end;
end;
end;
( 1 <= j + 1 & j + 1 <= len f ) by A42, A45, NAT_1:12, NAT_1:13;
then j + 1 in Seg (len f) by FINSEQ_1:1;
then A49: g . (j + 1) = f . (((len f) + 1) - (1 + j)) by A41
.= f . ((len f) - j) ;
j in Seg (len f) by A42, A44, A45, FINSEQ_1:1;
then g . j = f . ((1 + (len f)) - j) by A41
.= f . (((len f) - j) + 1) ;
hence [(g . j),(g . (j + 1))] in EqR1 \/ EqR2 by A49, A48; ::_thesis: verum
end;
len f in Seg (len f) by A36, FINSEQ_1:1;
then g . (len f) = f . ((1 + (len f)) - (len f)) by A41
.= f . (1 + 0) ;
then A50: x = g . (len g) by A37, A41, FINSEQ_1:def_3;
1 in Seg (len f) by A36, FINSEQ_1:1;
then A51: g . 1 = f . (((len f) + 1) - 1) by A41
.= f . (len f) ;
1 <= len g by A36, A41, FINSEQ_1:def_3;
hence [y,x] in Y by A2, A34, A38, A51, A50, A43; ::_thesis: verum
end;
Y is_reflexive_in X
proof
let x be set ; :: according to RELAT_2:def_1 ::_thesis: ( not x in X or [x,x] in Y )
assume A52: x in X ; ::_thesis: [x,x] in Y
set g = <*x*>;
A53: for i being Element of NAT st 1 <= i & i < len <*x*> holds
[(<*x*> . i),(<*x*> . (i + 1))] in EqR1 \/ EqR2 by FINSEQ_1:40;
( len <*x*> = 1 & <*x*> . 1 = x ) by FINSEQ_1:40;
hence [x,x] in Y by A2, A52, A53; ::_thesis: verum
end;
then ( field Y = X & dom Y = X ) by ORDERS_1:13;
then reconsider R1 = Y as Equivalence_Relation of X by A33, A3, PARTFUN1:def_2, RELAT_2:def_11, RELAT_2:def_16;
for x, y being set st [x,y] in EqR1 \/ EqR2 holds
[x,y] in R1
proof
let x, y be set ; ::_thesis: ( [x,y] in EqR1 \/ EqR2 implies [x,y] in R1 )
assume A54: [x,y] in EqR1 \/ EqR2 ; ::_thesis: [x,y] in R1
set g = <*x,y*>;
A55: len <*x,y*> = 1 + 1 by FINSEQ_1:44;
A56: <*x,y*> . 1 = x by FINSEQ_1:44;
A57: for i being Element of NAT st 1 <= i & i < len <*x,y*> holds
[(<*x,y*> . i),(<*x,y*> . (i + 1))] in EqR1 \/ EqR2
proof
let i be Element of NAT ; ::_thesis: ( 1 <= i & i < len <*x,y*> implies [(<*x,y*> . i),(<*x,y*> . (i + 1))] in EqR1 \/ EqR2 )
assume that
A58: 1 <= i and
A59: i < len <*x,y*> ; ::_thesis: [(<*x,y*> . i),(<*x,y*> . (i + 1))] in EqR1 \/ EqR2
i <= 1 by A55, A59, NAT_1:13;
then 1 = i by A58, XXREAL_0:1;
hence [(<*x,y*> . i),(<*x,y*> . (i + 1))] in EqR1 \/ EqR2 by A54, A56, FINSEQ_1:44; ::_thesis: verum
end;
len <*x,y*> = 2 by FINSEQ_1:44;
then A60: ( <*x,y*> . 1 = x & <*x,y*> . (len <*x,y*>) = y ) by FINSEQ_1:44;
( x in X & y in X ) by A54, Lm1;
hence [x,y] in R1 by A2, A55, A60, A57; ::_thesis: verum
end;
then EqR1 \/ EqR2 c= R1 by RELAT_1:def_3;
then A61: EqR1 "\/" EqR2 c= R1 by Def2;
assume [x,y] in EqR1 "\/" EqR2 ; ::_thesis: ex f being FinSequence st
( 1 <= len f & x = f . 1 & y = f . (len f) & ( for i being Element of NAT st 1 <= i & i < len f holds
[(f . i),(f . (i + 1))] in EqR1 \/ EqR2 ) )
then consider f being FinSequence such that
A62: ( 1 <= len f & x = f . 1 & y = f . (len f) & ( for i being Element of NAT st 1 <= i & i < len f holds
[(f . i),(f . (i + 1))] in EqR1 \/ EqR2 ) ) by A2, A61;
take f ; ::_thesis: ( 1 <= len f & x = f . 1 & y = f . (len f) & ( for i being Element of NAT st 1 <= i & i < len f holds
[(f . i),(f . (i + 1))] in EqR1 \/ EqR2 ) )
thus ( 1 <= len f & x = f . 1 & y = f . (len f) & ( for i being Element of NAT st 1 <= i & i < len f holds
[(f . i),(f . (i + 1))] in EqR1 \/ EqR2 ) ) by A62; ::_thesis: verum
end;
given f being FinSequence such that A63: 1 <= len f and
A64: x = f . 1 and
A65: y = f . (len f) and
A66: for i being Element of NAT st 1 <= i & i < len f holds
[(f . i),(f . (i + 1))] in EqR1 \/ EqR2 ; ::_thesis: [x,y] in EqR1 "\/" EqR2
defpred S1[ Element of NAT ] means ( 1 <= $1 & $1 <= len f implies [(f . 1),(f . $1)] in EqR1 "\/" EqR2 );
A67: now__::_thesis:_for_i_being_Element_of_NAT_st_S1[i]_holds_
S1[i_+_1]
let i be Element of NAT ; ::_thesis: ( S1[i] implies S1[i + 1] )
assume A68: S1[i] ; ::_thesis: S1[i + 1]
thus S1[i + 1] ::_thesis: verum
proof
assume that
A69: 1 <= i + 1 and
A70: i + 1 <= len f ; ::_thesis: [(f . 1),(f . (i + 1))] in EqR1 "\/" EqR2
A71: ( 1 <= i or 1 = i + 1 ) by A69, NAT_1:8;
A72: EqR1 \/ EqR2 c= EqR1 "\/" EqR2 by Def2;
A73: i < len f by A70, NAT_1:13;
now__::_thesis:_[(f_._1),(f_._(i_+_1))]_in_EqR1_"\/"_EqR2
percases ( 1 <= i or 0 = i ) by A71;
supposeA74: 1 <= i ; ::_thesis: [(f . 1),(f . (i + 1))] in EqR1 "\/" EqR2
then [(f . i),(f . (i + 1))] in EqR1 \/ EqR2 by A66, A73;
hence [(f . 1),(f . (i + 1))] in EqR1 "\/" EqR2 by A68, A70, A72, A74, Th7, NAT_1:13; ::_thesis: verum
end;
supposeA75: 0 = i ; ::_thesis: [(f . 1),(f . (i + 1))] in EqR1 "\/" EqR2
[(f . 1),(f . 1)] in EqR1 by A1, A64, Th5;
then [(f . 1),(f . 1)] in EqR1 \/ EqR2 by XBOOLE_0:def_3;
hence [(f . 1),(f . (i + 1))] in EqR1 "\/" EqR2 by A72, A75; ::_thesis: verum
end;
end;
end;
hence [(f . 1),(f . (i + 1))] in EqR1 "\/" EqR2 ; ::_thesis: verum
end;
end;
A76: S1[ 0 ] ;
for i being Element of NAT holds S1[i] from NAT_1:sch_1(A76, A67);
hence [x,y] in EqR1 "\/" EqR2 by A63, A64, A65; ::_thesis: verum
end;
theorem Th29: :: EQREL_1:29
for X being set
for EqR1, EqR2, E being Equivalence_Relation of X st E = EqR1 \/ EqR2 holds
for x being set holds
( not x in X or Class (E,x) = Class (EqR1,x) or Class (E,x) = Class (EqR2,x) )
proof
let X be set ; ::_thesis: for EqR1, EqR2, E being Equivalence_Relation of X st E = EqR1 \/ EqR2 holds
for x being set holds
( not x in X or Class (E,x) = Class (EqR1,x) or Class (E,x) = Class (EqR2,x) )
let EqR1, EqR2, E be Equivalence_Relation of X; ::_thesis: ( E = EqR1 \/ EqR2 implies for x being set holds
( not x in X or Class (E,x) = Class (EqR1,x) or Class (E,x) = Class (EqR2,x) ) )
assume A1: E = EqR1 \/ EqR2 ; ::_thesis: for x being set holds
( not x in X or Class (E,x) = Class (EqR1,x) or Class (E,x) = Class (EqR2,x) )
for x being set holds
( not x in X or Class (E,x) = Class (EqR1,x) or Class (E,x) = Class (EqR2,x) )
proof
let x be set ; ::_thesis: ( not x in X or Class (E,x) = Class (EqR1,x) or Class (E,x) = Class (EqR2,x) )
assume x in X ; ::_thesis: ( Class (E,x) = Class (EqR1,x) or Class (E,x) = Class (EqR2,x) )
assume that
A2: not Class (E,x) = Class (EqR1,x) and
A3: not Class (E,x) = Class (EqR2,x) ; ::_thesis: contradiction
consider y being set such that
A4: ( ( y in Class (E,x) & not y in Class (EqR1,x) ) or ( y in Class (EqR1,x) & not y in Class (E,x) ) ) by A2, TARSKI:1;
A5: now__::_thesis:_(_y_in_Class_(EqR1,x)_implies_y_in_Class_(E,x)_)
assume that
A6: y in Class (EqR1,x) and
A7: not y in Class (E,x) ; ::_thesis: contradiction
[y,x] in EqR1 by A6, Th19;
then [y,x] in E by A1, XBOOLE_0:def_3;
hence contradiction by A7, Th19; ::_thesis: verum
end;
then A8: [y,x] in E by A4, Th19;
consider z being set such that
A9: ( ( z in Class (E,x) & not z in Class (EqR2,x) ) or ( z in Class (EqR2,x) & not z in Class (E,x) ) ) by A3, TARSKI:1;
A10: now__::_thesis:_(_z_in_Class_(EqR2,x)_implies_z_in_Class_(E,x)_)
assume that
A11: z in Class (EqR2,x) and
A12: not z in Class (E,x) ; ::_thesis: contradiction
[z,x] in EqR2 by A11, Th19;
then [z,x] in E by A1, XBOOLE_0:def_3;
hence contradiction by A12, Th19; ::_thesis: verum
end;
then A13: [z,x] in E by A9, Th19;
not [z,x] in EqR2 by A9, A10, Th19;
then A14: [z,x] in EqR1 by A1, A13, XBOOLE_0:def_3;
A15: now__::_thesis:_not_[y,z]_in_EqR1
assume [y,z] in EqR1 ; ::_thesis: contradiction
then A16: [z,y] in EqR1 by Th6;
[x,z] in EqR1 by A14, Th6;
then [x,y] in EqR1 by A16, Th7;
then [y,x] in EqR1 by Th6;
hence contradiction by A4, A5, Th19; ::_thesis: verum
end;
not [y,x] in EqR1 by A4, A5, Th19;
then A17: [y,x] in EqR2 by A1, A8, XBOOLE_0:def_3;
A18: now__::_thesis:_not_[y,z]_in_EqR2
assume A19: [y,z] in EqR2 ; ::_thesis: contradiction
[x,y] in EqR2 by A17, Th6;
then [x,z] in EqR2 by A19, Th7;
then [z,x] in EqR2 by Th6;
hence contradiction by A9, A10, Th19; ::_thesis: verum
end;
[x,z] in E by A13, Th6;
then [y,z] in E by A8, Th7;
hence contradiction by A1, A18, A15, XBOOLE_0:def_3; ::_thesis: verum
end;
hence for x being set holds
( not x in X or Class (E,x) = Class (EqR1,x) or Class (E,x) = Class (EqR2,x) ) ; ::_thesis: verum
end;
theorem :: EQREL_1:30
for X being set
for EqR1, EqR2 being Equivalence_Relation of X holds
( not EqR1 \/ EqR2 = nabla X or EqR1 = nabla X or EqR2 = nabla X )
proof
let X be set ; ::_thesis: for EqR1, EqR2 being Equivalence_Relation of X holds
( not EqR1 \/ EqR2 = nabla X or EqR1 = nabla X or EqR2 = nabla X )
let EqR1, EqR2 be Equivalence_Relation of X; ::_thesis: ( not EqR1 \/ EqR2 = nabla X or EqR1 = nabla X or EqR2 = nabla X )
assume A1: EqR1 \/ EqR2 = nabla X ; ::_thesis: ( EqR1 = nabla X or EqR2 = nabla X )
( X = {} or EqR1 = nabla X or EqR2 = nabla X )
proof
set y = the Element of X;
A2: now__::_thesis:_for_x_being_set_holds_
(_not_x_in_X_or_Class_(EqR1,x)_=_X_or_Class_(EqR2,x)_=_X_)
let x be set ; ::_thesis: ( not x in X or Class (EqR1,x) = X or Class (EqR2,x) = X )
assume A3: x in X ; ::_thesis: ( Class (EqR1,x) = X or Class (EqR2,x) = X )
then ( Class ((nabla X),x) = Class (EqR1,x) or Class ((nabla X),x) = Class (EqR2,x) ) by A1, Th29;
hence ( Class (EqR1,x) = X or Class (EqR2,x) = X ) by A3, Th26; ::_thesis: verum
end;
assume X <> {} ; ::_thesis: ( EqR1 = nabla X or EqR2 = nabla X )
then ( Class (EqR1, the Element of X) = X or Class (EqR2, the Element of X) = X ) by A2;
hence ( EqR1 = nabla X or EqR2 = nabla X ) by Th27; ::_thesis: verum
end;
hence ( EqR1 = nabla X or EqR2 = nabla X ) ; ::_thesis: verum
end;
definition
let X be set ;
let EqR be Equivalence_Relation of X;
func Class EqR -> Subset-Family of X means :Def3: :: EQREL_1:def 3
for A being Subset of X holds
( A in it iff ex x being set st
( x in X & A = Class (EqR,x) ) );
existence
ex b1 being Subset-Family of X st
for A being Subset of X holds
( A in b1 iff ex x being set st
( x in X & A = Class (EqR,x) ) )
proof
defpred S1[ set ] means ex x being set st
( x in X & $1 = Class (EqR,x) );
consider F being Subset-Family of X such that
A1: for A being Subset of X holds
( A in F iff S1[A] ) from SUBSET_1:sch_3();
take F ; ::_thesis: for A being Subset of X holds
( A in F iff ex x being set st
( x in X & A = Class (EqR,x) ) )
thus for A being Subset of X holds
( A in F iff ex x being set st
( x in X & A = Class (EqR,x) ) ) by A1; ::_thesis: verum
end;
uniqueness
for b1, b2 being Subset-Family of X st ( for A being Subset of X holds
( A in b1 iff ex x being set st
( x in X & A = Class (EqR,x) ) ) ) & ( for A being Subset of X holds
( A in b2 iff ex x being set st
( x in X & A = Class (EqR,x) ) ) ) holds
b1 = b2
proof
let F1, F2 be Subset-Family of X; ::_thesis: ( ( for A being Subset of X holds
( A in F1 iff ex x being set st
( x in X & A = Class (EqR,x) ) ) ) & ( for A being Subset of X holds
( A in F2 iff ex x being set st
( x in X & A = Class (EqR,x) ) ) ) implies F1 = F2 )
assume that
A2: for A being Subset of X holds
( A in F1 iff ex x being set st
( x in X & A = Class (EqR,x) ) ) and
A3: for A being Subset of X holds
( A in F2 iff ex x being set st
( x in X & A = Class (EqR,x) ) ) ; ::_thesis: F1 = F2
now__::_thesis:_for_A_being_Subset_of_X_holds_
(_A_in_F1_iff_A_in_F2_)
let A be Subset of X; ::_thesis: ( A in F1 iff A in F2 )
( A in F1 iff ex x being set st
( x in X & A = Class (EqR,x) ) ) by A2;
hence ( A in F1 iff A in F2 ) by A3; ::_thesis: verum
end;
hence F1 = F2 by SETFAM_1:31; ::_thesis: verum
end;
end;
:: deftheorem Def3 defines Class EQREL_1:def_3_:_
for X being set
for EqR being Equivalence_Relation of X
for b3 being Subset-Family of X holds
( b3 = Class EqR iff for A being Subset of X holds
( A in b3 iff ex x being set st
( x in X & A = Class (EqR,x) ) ) );
theorem Th31: :: EQREL_1:31
for X being set
for EqR being Equivalence_Relation of X st X = {} holds
Class EqR = {}
proof
let X be set ; ::_thesis: for EqR being Equivalence_Relation of X st X = {} holds
Class EqR = {}
let EqR be Equivalence_Relation of X; ::_thesis: ( X = {} implies Class EqR = {} )
assume that
A1: X = {} and
A2: Class EqR <> {} ; ::_thesis: contradiction
set z = the Element of Class EqR;
the Element of Class EqR is Subset of X by A2, TARSKI:def_3;
then ex x being set st
( x in X & the Element of Class EqR = Class (EqR,x) ) by A2, Def3;
hence contradiction by A1; ::_thesis: verum
end;
definition
let X be set ;
mode a_partition of X -> Subset-Family of X means :Def4: :: EQREL_1:def 4
( union it = X & ( for A being Subset of X st A in it holds
( A <> {} & ( for B being Subset of X holds
( not B in it or A = B or A misses B ) ) ) ) );
existence
ex b1 being Subset-Family of X st
( union b1 = X & ( for A being Subset of X st A in b1 holds
( A <> {} & ( for B being Subset of X holds
( not B in b1 or A = B or A misses B ) ) ) ) )
proof
defpred S1[ set ] means ex x being set st
( x in X & $1 = {x} );
consider F being Subset-Family of X such that
A1: for A being Subset of X holds
( A in F iff S1[A] ) from SUBSET_1:sch_3();
A2: for A being Subset of X st A in F holds
( A <> {} & ( for B being Subset of X holds
( not B in F or A = B or A misses B ) ) )
proof
let A be Subset of X; ::_thesis: ( A in F implies ( A <> {} & ( for B being Subset of X holds
( not B in F or A = B or A misses B ) ) ) )
assume A in F ; ::_thesis: ( A <> {} & ( for B being Subset of X holds
( not B in F or A = B or A misses B ) ) )
then consider x being set such that
x in X and
A3: A = {x} by A1;
thus A <> {} by A3; ::_thesis: for B being Subset of X holds
( not B in F or A = B or A misses B )
let B be Subset of X; ::_thesis: ( not B in F or A = B or A misses B )
assume B in F ; ::_thesis: ( A = B or A misses B )
then consider y being set such that
y in X and
A4: B = {y} by A1;
now__::_thesis:_(_not_x_=_y_implies_A_misses_B_)
assume A5: not x = y ; ::_thesis: A misses B
for z being set st z in A holds
not z in B
proof
let z be set ; ::_thesis: ( z in A implies not z in B )
assume z in A ; ::_thesis: not z in B
then not z = y by A3, A5, TARSKI:def_1;
hence not z in B by A4, TARSKI:def_1; ::_thesis: verum
end;
hence A misses B by XBOOLE_0:3; ::_thesis: verum
end;
hence ( A = B or A misses B ) by A3, A4; ::_thesis: verum
end;
take F ; ::_thesis: ( union F = X & ( for A being Subset of X st A in F holds
( A <> {} & ( for B being Subset of X holds
( not B in F or A = B or A misses B ) ) ) ) )
now__::_thesis:_for_y_being_set_holds_
(_y_in_X_iff_ex_Z_being_set_st_
(_y_in_Z_&_Z_in_F_)_)
let y be set ; ::_thesis: ( y in X iff ex Z being set st
( y in Z & Z in F ) )
now__::_thesis:_(_y_in_X_implies_ex_Z_being_set_st_
(_y_in_Z_&_Z_in_F_)_)
set Z = {y};
assume A6: y in X ; ::_thesis: ex Z being set st
( y in Z & Z in F )
then {y} is Subset of X by ZFMISC_1:31;
then ( y in {y} & {y} in F ) by A1, A6, TARSKI:def_1;
hence ex Z being set st
( y in Z & Z in F ) ; ::_thesis: verum
end;
hence ( y in X iff ex Z being set st
( y in Z & Z in F ) ) ; ::_thesis: verum
end;
hence ( union F = X & ( for A being Subset of X st A in F holds
( A <> {} & ( for B being Subset of X holds
( not B in F or A = B or A misses B ) ) ) ) ) by A2, TARSKI:def_4; ::_thesis: verum
end;
end;
:: deftheorem Def4 defines a_partition EQREL_1:def_4_:_
for X being set
for b2 being Subset-Family of X holds
( b2 is a_partition of X iff ( union b2 = X & ( for A being Subset of X st A in b2 holds
( A <> {} & ( for B being Subset of X holds
( not B in b2 or A = B or A misses B ) ) ) ) ) );
theorem Th32: :: EQREL_1:32
for P being a_partition of {} holds P = {}
proof
let P be a_partition of {} ; ::_thesis: P = {}
assume not P = {} ; ::_thesis: contradiction
then consider Z being set such that
A1: Z in P by XBOOLE_0:def_1;
Z <> {} by A1, Def4;
hence contradiction by A1; ::_thesis: verum
end;
theorem Th33: :: EQREL_1:33
for X being set
for EqR being Equivalence_Relation of X holds Class EqR is a_partition of X
proof
let X be set ; ::_thesis: for EqR being Equivalence_Relation of X holds Class EqR is a_partition of X
let EqR be Equivalence_Relation of X; ::_thesis: Class EqR is a_partition of X
now__::_thesis:_for_x_being_set_holds_
(_x_in_X_iff_ex_Z_being_set_st_
(_x_in_Z_&_Z_in_Class_EqR_)_)
let x be set ; ::_thesis: ( x in X iff ex Z being set st
( x in Z & Z in Class EqR ) )
now__::_thesis:_(_x_in_X_implies_ex_Z_being_set_st_
(_x_in_Z_&_Z_in_Class_EqR_)_)
consider Z being set such that
A1: Z = Class (EqR,x) ;
assume A2: x in X ; ::_thesis: ex Z being set st
( x in Z & Z in Class EqR )
then Z in Class EqR by A1, Def3;
hence ex Z being set st
( x in Z & Z in Class EqR ) by A2, A1, Th20; ::_thesis: verum
end;
hence ( x in X iff ex Z being set st
( x in Z & Z in Class EqR ) ) ; ::_thesis: verum
end;
hence union (Class EqR) = X by TARSKI:def_4; :: according to EQREL_1:def_4 ::_thesis: for A being Subset of X st A in Class EqR holds
( A <> {} & ( for B being Subset of X holds
( not B in Class EqR or A = B or A misses B ) ) )
let A be Subset of X; ::_thesis: ( A in Class EqR implies ( A <> {} & ( for B being Subset of X holds
( not B in Class EqR or A = B or A misses B ) ) ) )
assume A in Class EqR ; ::_thesis: ( A <> {} & ( for B being Subset of X holds
( not B in Class EqR or A = B or A misses B ) ) )
then A3: ex x being set st
( x in X & A = Class (EqR,x) ) by Def3;
hence A <> {} by Th20; ::_thesis: for B being Subset of X holds
( not B in Class EqR or A = B or A misses B )
let B be Subset of X; ::_thesis: ( not B in Class EqR or A = B or A misses B )
assume B in Class EqR ; ::_thesis: ( A = B or A misses B )
then ex y being set st
( y in X & B = Class (EqR,y) ) by Def3;
hence ( A = B or A misses B ) by A3, Th24; ::_thesis: verum
end;
theorem Th34: :: EQREL_1:34
for X being set
for P being a_partition of X ex EqR being Equivalence_Relation of X st P = Class EqR
proof
let X be set ; ::_thesis: for P being a_partition of X ex EqR being Equivalence_Relation of X st P = Class EqR
let P be a_partition of X; ::_thesis: ex EqR being Equivalence_Relation of X st P = Class EqR
A1: ( X <> {} implies ex EqR being Equivalence_Relation of X st P = Class EqR )
proof
defpred S1[ set , set ] means ex A being Subset of X st
( A in P & $1 in A & $2 in A );
assume X <> {} ; ::_thesis: ex EqR being Equivalence_Relation of X st P = Class EqR
A2: for x, y, z being set st S1[x,y] & S1[y,z] holds
S1[x,z]
proof
let x, y, z be set ; ::_thesis: ( S1[x,y] & S1[y,z] implies S1[x,z] )
given A being Subset of X such that A3: A in P and
A4: ( x in A & y in A ) ; ::_thesis: ( not S1[y,z] or S1[x,z] )
given B being Subset of X such that A5: B in P and
A6: ( y in B & z in B ) ; ::_thesis: S1[x,z]
( A = B or A misses B ) by A3, A5, Def4;
hence S1[x,z] by A3, A4, A6, XBOOLE_0:3; ::_thesis: verum
end;
A7: union P = X by Def4;
A8: for x being set st x in X holds
S1[x,x]
proof
let x be set ; ::_thesis: ( x in X implies S1[x,x] )
assume x in X ; ::_thesis: S1[x,x]
then consider Z being set such that
A9: x in Z and
A10: Z in P by A7, TARSKI:def_4;
reconsider A = Z as Subset of X by A10;
take A ; ::_thesis: ( A in P & x in A & x in A )
thus ( A in P & x in A & x in A ) by A9, A10; ::_thesis: verum
end;
A11: for x, y being set st S1[x,y] holds
S1[y,x] ;
consider R being Equivalence_Relation of X such that
A12: for x, y being set holds
( [x,y] in R iff ( x in X & y in X & S1[x,y] ) ) from EQREL_1:sch_1(A8, A11, A2);
take R ; ::_thesis: P = Class R
now__::_thesis:_for_A_being_Subset_of_X_holds_
(_A_in_P_iff_A_in_Class_R_)
let A be Subset of X; ::_thesis: ( A in P iff A in Class R )
A13: now__::_thesis:_(_A_in_P_implies_A_in_Class_R_)
set x = the Element of A;
assume A14: A in P ; ::_thesis: A in Class R
then A15: A <> {} by Def4;
then A16: the Element of A in X by TARSKI:def_3;
now__::_thesis:_for_y_being_set_holds_
(_y_in_A_iff_y_in_Class_(R,_the_Element_of_A)_)
let y be set ; ::_thesis: ( y in A iff y in Class (R, the Element of A) )
A17: now__::_thesis:_(_y_in_Class_(R,_the_Element_of_A)_implies_y_in_A_)
assume y in Class (R, the Element of A) ; ::_thesis: y in A
then [y, the Element of A] in R by Th19;
then consider B being Subset of X such that
A18: ( B in P & y in B ) and
A19: the Element of A in B by A12;
A meets B by A15, A19, XBOOLE_0:3;
hence y in A by A14, A18, Def4; ::_thesis: verum
end;
now__::_thesis:_(_y_in_A_implies_y_in_Class_(R,_the_Element_of_A)_)
assume y in A ; ::_thesis: y in Class (R, the Element of A)
then [y, the Element of A] in R by A12, A14, A16;
hence y in Class (R, the Element of A) by Th19; ::_thesis: verum
end;
hence ( y in A iff y in Class (R, the Element of A) ) by A17; ::_thesis: verum
end;
then A = Class (R, the Element of A) by TARSKI:1;
hence A in Class R by A16, Def3; ::_thesis: verum
end;
now__::_thesis:_(_A_in_Class_R_implies_A_in_P_)
assume A in Class R ; ::_thesis: A in P
then consider x being set such that
A20: x in X and
A21: A = Class (R,x) by Def3;
x in Class (R,x) by A20, Th20;
then [x,x] in R by Th19;
then consider B being Subset of X such that
A22: B in P and
A23: x in B and
x in B by A12;
now__::_thesis:_for_y_being_set_holds_
(_y_in_A_iff_y_in_B_)
let y be set ; ::_thesis: ( y in A iff y in B )
A24: now__::_thesis:_(_y_in_A_implies_y_in_B_)
assume y in A ; ::_thesis: y in B
then [y,x] in R by A21, Th19;
then consider C being Subset of X such that
A25: ( C in P & y in C ) and
A26: x in C by A12;
B meets C by A23, A26, XBOOLE_0:3;
hence y in B by A22, A25, Def4; ::_thesis: verum
end;
now__::_thesis:_(_y_in_B_implies_y_in_A_)
assume y in B ; ::_thesis: y in A
then [y,x] in R by A12, A22, A23;
hence y in A by A21, Th19; ::_thesis: verum
end;
hence ( y in A iff y in B ) by A24; ::_thesis: verum
end;
hence A in P by A22, TARSKI:1; ::_thesis: verum
end;
hence ( A in P iff A in Class R ) by A13; ::_thesis: verum
end;
hence P = Class R by SETFAM_1:31; ::_thesis: verum
end;
( X = {} implies ex EqR being Equivalence_Relation of X st P = Class EqR )
proof
set EqR1 = the Equivalence_Relation of X;
assume A27: X = {} ; ::_thesis: ex EqR being Equivalence_Relation of X st P = Class EqR
take the Equivalence_Relation of X ; ::_thesis: P = Class the Equivalence_Relation of X
P = {} by A27, Th32;
hence P = Class the Equivalence_Relation of X by A27, Th31; ::_thesis: verum
end;
hence ex EqR being Equivalence_Relation of X st P = Class EqR by A1; ::_thesis: verum
end;
theorem :: EQREL_1:35
for X, y being set
for EqR being Equivalence_Relation of X
for x being set st x in X holds
( [x,y] in EqR iff Class (EqR,x) = Class (EqR,y) ) by Lm2;
theorem :: EQREL_1:36
for x, X being set
for EqR being Equivalence_Relation of X st x in Class EqR holds
ex y being Element of X st x = Class (EqR,y)
proof
let x, X be set ; ::_thesis: for EqR being Equivalence_Relation of X st x in Class EqR holds
ex y being Element of X st x = Class (EqR,y)
let EqR be Equivalence_Relation of X; ::_thesis: ( x in Class EqR implies ex y being Element of X st x = Class (EqR,y) )
assume A1: x in Class EqR ; ::_thesis: ex y being Element of X st x = Class (EqR,y)
then reconsider x = x as Subset of X ;
consider y being set such that
A2: y in X and
A3: x = Class (EqR,y) by A1, Def3;
reconsider y = y as Element of X by A2;
take y ; ::_thesis: x = Class (EqR,y)
thus x = Class (EqR,y) by A3; ::_thesis: verum
end;
begin
registration
let X be non empty set ;
cluster -> non empty for a_partition of X;
coherence
for b1 being a_partition of X holds not b1 is empty
proof
set x = the Element of X;
let P be a_partition of X; ::_thesis: not P is empty
union P = X by Def4;
then ex A being set st
( the Element of X in A & A in P ) by TARSKI:def_4;
hence not P is empty ; ::_thesis: verum
end;
end;
registration
let X be set ;
cluster -> with_non-empty_elements for a_partition of X;
coherence
for b1 being a_partition of X holds b1 is with_non-empty_elements
proof
let P be a_partition of X; ::_thesis: P is with_non-empty_elements
assume {} in P ; :: according to SETFAM_1:def_8 ::_thesis: contradiction
hence contradiction by Def4; ::_thesis: verum
end;
end;
definition
let X be set ;
let R be Equivalence_Relation of X;
:: original: Class
redefine func Class R -> a_partition of X;
coherence
Class R is a_partition of X by Th33;
end;
registration
let I be non empty set ;
let R be Equivalence_Relation of I;
cluster Class R -> non empty ;
coherence
not Class R is empty ;
end;
registration
let I be non empty set ;
let R be Equivalence_Relation of I;
cluster Class R -> with_non-empty_elements ;
coherence
Class R is with_non-empty_elements ;
end;
notation
let I be non empty set ;
let R be Equivalence_Relation of I;
let x be Element of I;
synonym EqClass (R,x) for Class (I,R);
end;
definition
let I be non empty set ;
let R be Equivalence_Relation of I;
let x be Element of I;
:: original: Class
redefine func EqClass (R,x) -> Element of Class R;
coherence
Class (R,x) is Element of Class R
proof
thus Class (R,x) is Element of Class R by Def3; ::_thesis: verum
end;
end;
definition
let X be set ;
func SmallestPartition X -> a_partition of X equals :: EQREL_1:def 5
Class (id X);
coherence
Class (id X) is a_partition of X ;
end;
:: deftheorem defines SmallestPartition EQREL_1:def_5_:_
for X being set holds SmallestPartition X = Class (id X);
theorem :: EQREL_1:37
for X being non empty set holds SmallestPartition X = { {x} where x is Element of X : verum }
proof
let X be non empty set ; ::_thesis: SmallestPartition X = { {x} where x is Element of X : verum }
set Y = { {x} where x is Element of X : verum } ;
hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: { {x} where x is Element of X : verum } c= SmallestPartition X
let x be set ; ::_thesis: ( x in SmallestPartition X implies x in { {x} where x is Element of X : verum } )
assume x in SmallestPartition X ; ::_thesis: x in { {x} where x is Element of X : verum }
then consider y being set such that
A1: y in X and
A2: x = Class ((id X),y) by Def3;
x = {y} by A1, A2, Th25;
hence x in { {x} where x is Element of X : verum } by A1; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { {x} where x is Element of X : verum } or x in SmallestPartition X )
assume x in { {x} where x is Element of X : verum } ; ::_thesis: x in SmallestPartition X
then consider y being Element of X such that
A3: x = {y} ;
Class ((id X),y) = x by A3, Th25;
hence x in SmallestPartition X by Def3; ::_thesis: verum
end;
definition
let X be non empty set ;
let x be Element of X;
let S1 be a_partition of X;
func EqClass (x,S1) -> Subset of X means :Def6: :: EQREL_1:def 6
( x in it & it in S1 );
existence
ex b1 being Subset of X st
( x in b1 & b1 in S1 )
proof
consider EQR being Equivalence_Relation of X such that
A1: S1 = Class EQR by Th34;
take Class (EQR,x) ; ::_thesis: ( x in Class (EQR,x) & Class (EQR,x) in S1 )
thus x in Class (EQR,x) by Th20; ::_thesis: Class (EQR,x) in S1
thus Class (EQR,x) in S1 by A1, Def3; ::_thesis: verum
end;
uniqueness
for b1, b2 being Subset of X st x in b1 & b1 in S1 & x in b2 & b2 in S1 holds
b1 = b2
proof
let A, B be Subset of X; ::_thesis: ( x in A & A in S1 & x in B & B in S1 implies A = B )
assume that
A2: x in A and
A3: A in S1 and
A4: x in B and
A5: B in S1 ; ::_thesis: A = B
A meets B by A2, A4, XBOOLE_0:3;
hence A = B by A3, A5, Def4; ::_thesis: verum
end;
end;
:: deftheorem Def6 defines EqClass EQREL_1:def_6_:_
for X being non empty set
for x being Element of X
for S1 being a_partition of X
for b4 being Subset of X holds
( b4 = EqClass (x,S1) iff ( x in b4 & b4 in S1 ) );
theorem Th38: :: EQREL_1:38
for X being non empty set
for S1, S2 being a_partition of X st ( for x being Element of X holds EqClass (x,S1) = EqClass (x,S2) ) holds
S1 = S2
proof
let X be non empty set ; ::_thesis: for S1, S2 being a_partition of X st ( for x being Element of X holds EqClass (x,S1) = EqClass (x,S2) ) holds
S1 = S2
let S1, S2 be a_partition of X; ::_thesis: ( ( for x being Element of X holds EqClass (x,S1) = EqClass (x,S2) ) implies S1 = S2 )
assume A1: for x being Element of X holds EqClass (x,S1) = EqClass (x,S2) ; ::_thesis: S1 = S2
now__::_thesis:_for_P_being_Subset_of_X_holds_
(_(_P_in_S1_implies_P_in_S2_)_&_(_P_in_S2_implies_P_in_S1_)_)
let P be Subset of X; ::_thesis: ( ( P in S1 implies P in S2 ) & ( P in S2 implies P in S1 ) )
thus ( P in S1 implies P in S2 ) ::_thesis: ( P in S2 implies P in S1 )
proof
set x = the Element of P;
assume A2: P in S1 ; ::_thesis: P in S2
then A3: not P is empty by Def4;
then the Element of P in P ;
then reconsider x = the Element of P as Element of X ;
P = EqClass (x,S1) by A2, A3, Def6;
then P = EqClass (x,S2) by A1;
hence P in S2 by Def6; ::_thesis: verum
end;
thus ( P in S2 implies P in S1 ) ::_thesis: verum
proof
set x = the Element of P;
assume A4: P in S2 ; ::_thesis: P in S1
then A5: P <> {} by Def4;
then the Element of P in P ;
then reconsider x = the Element of P as Element of X ;
P = EqClass (x,S2) by A4, A5, Def6;
then P = EqClass (x,S1) by A1;
hence P in S1 by Def6; ::_thesis: verum
end;
end;
hence S1 = S2 by SETFAM_1:31; ::_thesis: verum
end;
theorem Th39: :: EQREL_1:39
for X being non empty set holds {X} is a_partition of X
proof
let X be non empty set ; ::_thesis: {X} is a_partition of X
reconsider A1 = {X} as Subset-Family of X by ZFMISC_1:68;
A1: for A being Subset of X st A in A1 holds
( A <> {} & ( for B being Subset of X holds
( not B in A1 or A = B or A misses B ) ) )
proof
let A be Subset of X; ::_thesis: ( A in A1 implies ( A <> {} & ( for B being Subset of X holds
( not B in A1 or A = B or A misses B ) ) ) )
assume A2: A in A1 ; ::_thesis: ( A <> {} & ( for B being Subset of X holds
( not B in A1 or A = B or A misses B ) ) )
hence A <> {} by TARSKI:def_1; ::_thesis: for B being Subset of X holds
( not B in A1 or A = B or A misses B )
let B be Subset of X; ::_thesis: ( not B in A1 or A = B or A misses B )
assume B in A1 ; ::_thesis: ( A = B or A misses B )
then B = X by TARSKI:def_1;
hence ( A = B or A misses B ) by A2, TARSKI:def_1; ::_thesis: verum
end;
union A1 = X by ZFMISC_1:25;
hence {X} is a_partition of X by A1, Def4; ::_thesis: verum
end;
definition
let X be set ;
mode Family-Class of X is Subset-Family of (bool X);
end;
definition
let X be set ;
let F be Family-Class of X;
attrF is partition-membered means :Def7: :: EQREL_1:def 7
for S being set st S in F holds
S is a_partition of X;
end;
:: deftheorem Def7 defines partition-membered EQREL_1:def_7_:_
for X being set
for F being Family-Class of X holds
( F is partition-membered iff for S being set st S in F holds
S is a_partition of X );
registration
let X be set ;
cluster partition-membered for Element of bool (bool (bool X));
existence
ex b1 being Family-Class of X st b1 is partition-membered
proof
reconsider E = {} as Family-Class of X by XBOOLE_1:2;
take E ; ::_thesis: E is partition-membered
let S be set ; :: according to EQREL_1:def_7 ::_thesis: ( S in E implies S is a_partition of X )
assume S in E ; ::_thesis: S is a_partition of X
hence S is a_partition of X ; ::_thesis: verum
end;
end;
definition
let X be set ;
mode Part-Family of X is partition-membered Family-Class of X;
end;
registration
let X be non empty set ;
cluster non empty with_non-empty_elements for a_partition of X;
existence
not for b1 being a_partition of X holds b1 is empty
proof
take {X} ; ::_thesis: ( {X} is Subset-Family of X & {X} is a_partition of X & not {X} is empty )
thus ( {X} is Subset-Family of X & {X} is a_partition of X & not {X} is empty ) by Th39; ::_thesis: verum
end;
end;
theorem Th40: :: EQREL_1:40
for X being set
for p being a_partition of X holds {p} is Part-Family of X
proof
let X be set ; ::_thesis: for p being a_partition of X holds {p} is Part-Family of X
let p be a_partition of X; ::_thesis: {p} is Part-Family of X
for x being set st x in {p} holds
x is a_partition of X by TARSKI:def_1;
hence {p} is Part-Family of X by Def7; ::_thesis: verum
end;
registration
let X be set ;
cluster non empty partition-membered for Element of bool (bool (bool X));
existence
not for b1 being Part-Family of X holds b1 is empty
proof
set p = the a_partition of X;
reconsider P = { the a_partition of X} as Part-Family of X by Th40;
take P ; ::_thesis: not P is empty
thus not P is empty ; ::_thesis: verum
end;
end;
theorem Th41: :: EQREL_1:41
for X being non empty set
for S1 being a_partition of X
for x, y being Element of X st EqClass (x,S1) meets EqClass (y,S1) holds
EqClass (x,S1) = EqClass (y,S1)
proof
let X be non empty set ; ::_thesis: for S1 being a_partition of X
for x, y being Element of X st EqClass (x,S1) meets EqClass (y,S1) holds
EqClass (x,S1) = EqClass (y,S1)
let S1 be a_partition of X; ::_thesis: for x, y being Element of X st EqClass (x,S1) meets EqClass (y,S1) holds
EqClass (x,S1) = EqClass (y,S1)
let x, y be Element of X; ::_thesis: ( EqClass (x,S1) meets EqClass (y,S1) implies EqClass (x,S1) = EqClass (y,S1) )
consider EQR being Equivalence_Relation of X such that
A1: S1 = Class EQR by Th34;
A2: y in Class (EQR,y) by Th20;
Class (EQR,y) in S1 by A1, Def3;
then A3: Class (EQR,y) = EqClass (y,S1) by A2, Def6;
A4: x in Class (EQR,x) by Th20;
Class (EQR,x) in S1 by A1, Def3;
then A5: Class (EQR,x) = EqClass (x,S1) by A4, Def6;
assume EqClass (x,S1) meets EqClass (y,S1) ; ::_thesis: EqClass (x,S1) = EqClass (y,S1)
hence EqClass (x,S1) = EqClass (y,S1) by A5, A3, Th24; ::_thesis: verum
end;
Lm3: for X being non empty set
for x being Element of X
for F being Part-Family of X
for A being set st A in { (EqClass (x,S)) where S is a_partition of X : S in F } holds
ex T being a_partition of X st
( T in F & A = EqClass (x,T) )
proof
let X be non empty set ; ::_thesis: for x being Element of X
for F being Part-Family of X
for A being set st A in { (EqClass (x,S)) where S is a_partition of X : S in F } holds
ex T being a_partition of X st
( T in F & A = EqClass (x,T) )
let x be Element of X; ::_thesis: for F being Part-Family of X
for A being set st A in { (EqClass (x,S)) where S is a_partition of X : S in F } holds
ex T being a_partition of X st
( T in F & A = EqClass (x,T) )
let F be Part-Family of X; ::_thesis: for A being set st A in { (EqClass (x,S)) where S is a_partition of X : S in F } holds
ex T being a_partition of X st
( T in F & A = EqClass (x,T) )
let A be set ; ::_thesis: ( A in { (EqClass (x,S)) where S is a_partition of X : S in F } implies ex T being a_partition of X st
( T in F & A = EqClass (x,T) ) )
assume A in { (EqClass (x,S)) where S is a_partition of X : S in F } ; ::_thesis: ex T being a_partition of X st
( T in F & A = EqClass (x,T) )
then consider S being a_partition of X such that
A1: ( A = EqClass (x,S) & S in F ) ;
take S ; ::_thesis: ( S in F & A = EqClass (x,S) )
thus ( S in F & A = EqClass (x,S) ) by A1; ::_thesis: verum
end;
theorem :: EQREL_1:42
for A being set
for X being non empty set
for S being a_partition of X st A in S holds
ex x being Element of X st A = EqClass (x,S)
proof
let A be set ; ::_thesis: for X being non empty set
for S being a_partition of X st A in S holds
ex x being Element of X st A = EqClass (x,S)
let X be non empty set ; ::_thesis: for S being a_partition of X st A in S holds
ex x being Element of X st A = EqClass (x,S)
let S be a_partition of X; ::_thesis: ( A in S implies ex x being Element of X st A = EqClass (x,S) )
assume A1: A in S ; ::_thesis: ex x being Element of X st A = EqClass (x,S)
then not A is empty by Def4;
then consider x being set such that
A2: x in A by XBOOLE_0:def_1;
take x ; ::_thesis: ( x is Element of X & A = EqClass (x,S) )
thus ( x is Element of X & A = EqClass (x,S) ) by A1, A2, Def6; ::_thesis: verum
end;
definition
let X be non empty set ;
let F be non empty Part-Family of X;
func Intersection F -> non empty a_partition of X means :: EQREL_1:def 8
for x being Element of X holds EqClass (x,it) = meet { (EqClass (x,S)) where S is a_partition of X : S in F } ;
uniqueness
for b1, b2 being non empty a_partition of X st ( for x being Element of X holds EqClass (x,b1) = meet { (EqClass (x,S)) where S is a_partition of X : S in F } ) & ( for x being Element of X holds EqClass (x,b2) = meet { (EqClass (x,S)) where S is a_partition of X : S in F } ) holds
b1 = b2
proof
given S1, S2 being a_partition of X such that A1: for x being Element of X holds EqClass (x,S1) = meet { (EqClass (x,S)) where S is a_partition of X : S in F } and
A2: for x being Element of X holds EqClass (x,S2) = meet { (EqClass (x,S)) where S is a_partition of X : S in F } and
A3: not S1 = S2 ; ::_thesis: contradiction
now__::_thesis:_for_x_being_Element_of_X_holds_EqClass_(x,S1)_=_EqClass_(x,S2)
let x be Element of X; ::_thesis: EqClass (x,S1) = EqClass (x,S2)
EqClass (x,S1) = meet { (EqClass (x,S)) where S is a_partition of X : S in F } by A1;
hence EqClass (x,S1) = EqClass (x,S2) by A2; ::_thesis: verum
end;
hence contradiction by A3, Th38; ::_thesis: verum
end;
existence
ex b1 being non empty a_partition of X st
for x being Element of X holds EqClass (x,b1) = meet { (EqClass (x,S)) where S is a_partition of X : S in F }
proof
thus ex G being non empty a_partition of X st
for x being Element of X holds EqClass (x,G) = meet { (EqClass (x,S)) where S is a_partition of X : S in F } ::_thesis: verum
proof
set G = { (meet { (EqClass (x,S)) where S is a_partition of X : S in F } ) where x is Element of X : verum } ;
{ (meet { (EqClass (x,S)) where S is a_partition of X : S in F } ) where x is Element of X : verum } c= bool X
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in { (meet { (EqClass (x,S)) where S is a_partition of X : S in F } ) where x is Element of X : verum } or y in bool X )
assume y in { (meet { (EqClass (x,S)) where S is a_partition of X : S in F } ) where x is Element of X : verum } ; ::_thesis: y in bool X
then consider x being Element of X such that
A4: y = meet { (EqClass (x,S)) where S is a_partition of X : S in F } ;
y c= X
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in y or e in X )
consider T being set such that
A5: T in F by XBOOLE_0:def_1;
reconsider T = T as a_partition of X by A5, Def7;
EqClass (x,T) in { (EqClass (x,S)) where S is a_partition of X : S in F } by A5;
then consider f being set such that
A6: f in { (EqClass (x,S)) where S is a_partition of X : S in F } ;
consider S being a_partition of X such that
A7: f = EqClass (x,S) and
S in F by A6;
assume e in y ; ::_thesis: e in X
then e in EqClass (x,S) by A4, A6, A7, SETFAM_1:def_1;
hence e in X ; ::_thesis: verum
end;
hence y in bool X ; ::_thesis: verum
end;
then reconsider G = { (meet { (EqClass (x,S)) where S is a_partition of X : S in F } ) where x is Element of X : verum } as Subset-Family of X ;
G is a_partition of X
proof
X c= union G
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in X or a in union G )
consider T being set such that
A8: T in F by XBOOLE_0:def_1;
assume a in X ; ::_thesis: a in union G
then reconsider a1 = a as Element of X ;
reconsider T = T as a_partition of X by A8, Def7;
A9: meet { (EqClass (a1,S)) where S is a_partition of X : S in F } in G ;
A10: for T being set st T in { (EqClass (a1,S)) where S is a_partition of X : S in F } holds
a1 in T
proof
let T be set ; ::_thesis: ( T in { (EqClass (a1,S)) where S is a_partition of X : S in F } implies a1 in T )
assume T in { (EqClass (a1,S)) where S is a_partition of X : S in F } ; ::_thesis: a1 in T
then ex A being a_partition of X st
( T = EqClass (a1,A) & A in F ) ;
hence a1 in T by Def6; ::_thesis: verum
end;
EqClass (a1,T) in { (EqClass (a1,S)) where S is a_partition of X : S in F } by A8;
then a in meet { (EqClass (a1,S)) where S is a_partition of X : S in F } by A10, SETFAM_1:def_1;
hence a in union G by A9, TARSKI:def_4; ::_thesis: verum
end;
hence union G = X by XBOOLE_0:def_10; :: according to EQREL_1:def_4 ::_thesis: for A being Subset of X st A in G holds
( A <> {} & ( for B being Subset of X holds
( not B in G or A = B or A misses B ) ) )
let A be Subset of X; ::_thesis: ( A in G implies ( A <> {} & ( for B being Subset of X holds
( not B in G or A = B or A misses B ) ) ) )
consider T being set such that
A11: T in F by XBOOLE_0:def_1;
reconsider T = T as a_partition of X by A11, Def7;
assume A12: A in G ; ::_thesis: ( A <> {} & ( for B being Subset of X holds
( not B in G or A = B or A misses B ) ) )
then consider x being Element of X such that
A13: A = meet { (EqClass (x,S)) where S is a_partition of X : S in F } ;
A14: for Y being set st Y in { (EqClass (x,S)) where S is a_partition of X : S in F } holds
x in Y
proof
let Y be set ; ::_thesis: ( Y in { (EqClass (x,S)) where S is a_partition of X : S in F } implies x in Y )
assume Y in { (EqClass (x,S)) where S is a_partition of X : S in F } ; ::_thesis: x in Y
then ex T being a_partition of X st
( Y = EqClass (x,T) & T in F ) ;
hence x in Y by Def6; ::_thesis: verum
end;
EqClass (x,T) in { (EqClass (x,S)) where S is a_partition of X : S in F } by A11;
hence A <> {} by A13, A14, SETFAM_1:def_1; ::_thesis: for B being Subset of X holds
( not B in G or A = B or A misses B )
consider x being Element of X such that
A15: A = meet { (EqClass (x,S)) where S is a_partition of X : S in F } by A12;
let B be Subset of X; ::_thesis: ( not B in G or A = B or A misses B )
assume B in G ; ::_thesis: ( A = B or A misses B )
then consider y being Element of X such that
A16: B = meet { (EqClass (y,S)) where S is a_partition of X : S in F } ;
thus ( A = B or A misses B ) ::_thesis: verum
proof
A17: not { (EqClass (y,S)) where S is a_partition of X : S in F } is empty
proof
consider T being set such that
A18: T in F by XBOOLE_0:def_1;
reconsider T = T as a_partition of X by A18, Def7;
EqClass (y,T) in { (EqClass (y,S)) where S is a_partition of X : S in F } by A18;
hence not { (EqClass (y,S)) where S is a_partition of X : S in F } is empty ; ::_thesis: verum
end;
A19: not { (EqClass (x,S)) where S is a_partition of X : S in F } is empty
proof
consider T being set such that
A20: T in F by XBOOLE_0:def_1;
reconsider T = T as a_partition of X by A20, Def7;
EqClass (x,T) in { (EqClass (x,S)) where S is a_partition of X : S in F } by A20;
hence not { (EqClass (x,S)) where S is a_partition of X : S in F } is empty ; ::_thesis: verum
end;
now__::_thesis:_(_not_A_meets_B_or_A_=_B_or_A_misses_B_)
assume A meets B ; ::_thesis: ( A = B or A misses B )
then consider c being set such that
A21: ( c in A & c in B ) by XBOOLE_0:3;
c in (meet { (EqClass (x,S)) where S is a_partition of X : S in F } ) /\ (meet { (EqClass (y,S)) where S is a_partition of X : S in F } ) by A15, A16, A21, XBOOLE_0:def_4;
then A22: c in meet ( { (EqClass (x,S)) where S is a_partition of X : S in F } \/ { (EqClass (y,S)) where S is a_partition of X : S in F } ) by A19, A17, SETFAM_1:9;
A23: now__::_thesis:_for_T_being_a_partition_of_X_st_T_in_F_holds_
c_in_EqClass_(y,T)
let T be a_partition of X; ::_thesis: ( T in F implies c in EqClass (y,T) )
assume T in F ; ::_thesis: c in EqClass (y,T)
then EqClass (y,T) in { (EqClass (y,S)) where S is a_partition of X : S in F } ;
then EqClass (y,T) in { (EqClass (x,S)) where S is a_partition of X : S in F } \/ { (EqClass (y,S)) where S is a_partition of X : S in F } by XBOOLE_0:def_3;
hence c in EqClass (y,T) by A22, SETFAM_1:def_1; ::_thesis: verum
end;
A24: now__::_thesis:_for_T_being_a_partition_of_X_st_T_in_F_holds_
c_in_EqClass_(x,T)
let T be a_partition of X; ::_thesis: ( T in F implies c in EqClass (x,T) )
assume T in F ; ::_thesis: c in EqClass (x,T)
then EqClass (x,T) in { (EqClass (x,S)) where S is a_partition of X : S in F } ;
then EqClass (x,T) in { (EqClass (x,S)) where S is a_partition of X : S in F } \/ { (EqClass (y,S)) where S is a_partition of X : S in F } by XBOOLE_0:def_3;
hence c in EqClass (x,T) by A22, SETFAM_1:def_1; ::_thesis: verum
end;
A25: for T being a_partition of X st T in F holds
ex A being set st
( A in EqClass (x,T) & A in EqClass (y,T) )
proof
let T be a_partition of X; ::_thesis: ( T in F implies ex A being set st
( A in EqClass (x,T) & A in EqClass (y,T) ) )
assume A26: T in F ; ::_thesis: ex A being set st
( A in EqClass (x,T) & A in EqClass (y,T) )
take c ; ::_thesis: ( c in EqClass (x,T) & c in EqClass (y,T) )
thus ( c in EqClass (x,T) & c in EqClass (y,T) ) by A24, A23, A26; ::_thesis: verum
end;
A27: for T being a_partition of X st T in F holds
EqClass (x,T) meets EqClass (y,T)
proof
let T be a_partition of X; ::_thesis: ( T in F implies EqClass (x,T) meets EqClass (y,T) )
assume T in F ; ::_thesis: EqClass (x,T) meets EqClass (y,T)
then ex A being set st
( A in EqClass (x,T) & A in EqClass (y,T) ) by A25;
hence EqClass (x,T) meets EqClass (y,T) by XBOOLE_0:3; ::_thesis: verum
end;
A28: { (EqClass (y,S)) where S is a_partition of X : S in F } c= { (EqClass (x,S)) where S is a_partition of X : S in F }
proof
let A be set ; :: according to TARSKI:def_3 ::_thesis: ( not A in { (EqClass (y,S)) where S is a_partition of X : S in F } or A in { (EqClass (x,S)) where S is a_partition of X : S in F } )
assume A in { (EqClass (y,S)) where S is a_partition of X : S in F } ; ::_thesis: A in { (EqClass (x,S)) where S is a_partition of X : S in F }
then consider T being a_partition of X such that
A29: T in F and
A30: A = EqClass (y,T) by Lm3;
A = EqClass (x,T) by A27, A29, A30, Th41;
hence A in { (EqClass (x,S)) where S is a_partition of X : S in F } by A29; ::_thesis: verum
end;
{ (EqClass (x,S)) where S is a_partition of X : S in F } c= { (EqClass (y,S)) where S is a_partition of X : S in F }
proof
let A be set ; :: according to TARSKI:def_3 ::_thesis: ( not A in { (EqClass (x,S)) where S is a_partition of X : S in F } or A in { (EqClass (y,S)) where S is a_partition of X : S in F } )
assume A in { (EqClass (x,S)) where S is a_partition of X : S in F } ; ::_thesis: A in { (EqClass (y,S)) where S is a_partition of X : S in F }
then consider T being a_partition of X such that
A31: T in F and
A32: A = EqClass (x,T) by Lm3;
A = EqClass (y,T) by A27, A31, A32, Th41;
hence A in { (EqClass (y,S)) where S is a_partition of X : S in F } by A31; ::_thesis: verum
end;
hence ( A = B or A misses B ) by A15, A16, A28, XBOOLE_0:def_10; ::_thesis: verum
end;
hence ( A = B or A misses B ) ; ::_thesis: verum
end;
end;
then reconsider G = G as non empty a_partition of X ;
take G ; ::_thesis: for x being Element of X holds EqClass (x,G) = meet { (EqClass (x,S)) where S is a_partition of X : S in F }
for x being Element of X holds EqClass (x,G) = meet { (EqClass (x,S)) where S is a_partition of X : S in F }
proof
let x be Element of X; ::_thesis: EqClass (x,G) = meet { (EqClass (x,S)) where S is a_partition of X : S in F }
A33: now__::_thesis:_for_Y_being_set_st_Y_in__{__(EqClass_(x,S))_where_S_is_a_partition_of_X_:_S_in_F__}__holds_
x_in_Y
let Y be set ; ::_thesis: ( Y in { (EqClass (x,S)) where S is a_partition of X : S in F } implies x in Y )
assume Y in { (EqClass (x,S)) where S is a_partition of X : S in F } ; ::_thesis: x in Y
then ex T being a_partition of X st
( Y = EqClass (x,T) & T in F ) ;
hence x in Y by Def6; ::_thesis: verum
end;
not { (EqClass (x,S)) where S is a_partition of X : S in F } is empty
proof
consider T being set such that
A34: T in F by XBOOLE_0:def_1;
reconsider T = T as a_partition of X by A34, Def7;
EqClass (x,T) in { (EqClass (x,S)) where S is a_partition of X : S in F } by A34;
hence not { (EqClass (x,S)) where S is a_partition of X : S in F } is empty ; ::_thesis: verum
end;
then ( meet { (EqClass (x,S)) where S is a_partition of X : S in F } in G & x in meet { (EqClass (x,S)) where S is a_partition of X : S in F } ) by A33, SETFAM_1:def_1;
hence EqClass (x,G) = meet { (EqClass (x,S)) where S is a_partition of X : S in F } by Def6; ::_thesis: verum
end;
hence for x being Element of X holds EqClass (x,G) = meet { (EqClass (x,S)) where S is a_partition of X : S in F } ; ::_thesis: verum
end;
end;
end;
:: deftheorem defines Intersection EQREL_1:def_8_:_
for X being non empty set
for F being non empty Part-Family of X
for b3 being non empty a_partition of X holds
( b3 = Intersection F iff for x being Element of X holds EqClass (x,b3) = meet { (EqClass (x,S)) where S is a_partition of X : S in F } );
theorem Th43: :: EQREL_1:43
for X being non empty set
for S being a_partition of X
for A being Subset of S holds (union S) \ (union A) = union (S \ A)
proof
let X be non empty set ; ::_thesis: for S being a_partition of X
for A being Subset of S holds (union S) \ (union A) = union (S \ A)
let S be a_partition of X; ::_thesis: for A being Subset of S holds (union S) \ (union A) = union (S \ A)
let A be Subset of S; ::_thesis: (union S) \ (union A) = union (S \ A)
thus (union S) \ (union A) c= union (S \ A) :: according to XBOOLE_0:def_10 ::_thesis: union (S \ A) c= (union S) \ (union A)
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in (union S) \ (union A) or y in union (S \ A) )
assume A1: y in (union S) \ (union A) ; ::_thesis: y in union (S \ A)
then y in union S by XBOOLE_0:def_5;
then consider z being set such that
A2: y in z and
A3: z in S by TARSKI:def_4;
not y in union A by A1, XBOOLE_0:def_5;
then not z in A by A2, TARSKI:def_4;
then z in S \ A by A3, XBOOLE_0:def_5;
hence y in union (S \ A) by A2, TARSKI:def_4; ::_thesis: verum
end;
thus union (S \ A) c= (union S) \ (union A) ::_thesis: verum
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in union (S \ A) or y in (union S) \ (union A) )
assume y in union (S \ A) ; ::_thesis: y in (union S) \ (union A)
then consider z being set such that
A4: y in z and
A5: z in S \ A by TARSKI:def_4;
A6: z in S by A5, XBOOLE_0:def_5;
A7: not z in A by A5, XBOOLE_0:def_5;
A8: now__::_thesis:_for_w_being_set_st_w_in_A_holds_
not_y_in_w
let w be set ; ::_thesis: ( w in A implies not y in w )
assume A9: w in A ; ::_thesis: not y in w
then w in S ;
then z misses w by A6, A7, A9, Def4;
hence not y in w by A4, XBOOLE_0:3; ::_thesis: verum
end;
A10: now__::_thesis:_not_y_in_union_A
assume y in union A ; ::_thesis: contradiction
then ex v being set st
( y in v & v in A ) by TARSKI:def_4;
hence contradiction by A8; ::_thesis: verum
end;
y in union S by A4, A6, TARSKI:def_4;
hence y in (union S) \ (union A) by A10, XBOOLE_0:def_5; ::_thesis: verum
end;
end;
theorem :: EQREL_1:44
for X being non empty set
for A being Subset of X
for S being a_partition of X st A in S holds
union (S \ {A}) = X \ A
proof
let X be non empty set ; ::_thesis: for A being Subset of X
for S being a_partition of X st A in S holds
union (S \ {A}) = X \ A
let A be Subset of X; ::_thesis: for S being a_partition of X st A in S holds
union (S \ {A}) = X \ A
let S be a_partition of X; ::_thesis: ( A in S implies union (S \ {A}) = X \ A )
assume A1: A in S ; ::_thesis: union (S \ {A}) = X \ A
{A} c= S
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in {A} or y in S )
assume y in {A} ; ::_thesis: y in S
hence y in S by A1, TARSKI:def_1; ::_thesis: verum
end;
then reconsider AA = {A} as Subset of S ;
thus union (S \ {A}) = (union S) \ (union AA) by Th43
.= X \ (union {A}) by Def4
.= X \ A by ZFMISC_1:25 ; ::_thesis: verum
end;
theorem :: EQREL_1:45
{} is a_partition of {}
proof
reconsider A = {} as Subset-Family of {} by XBOOLE_1:2;
( union A = {} & ( for a being Subset of {} st a in A holds
( a <> {} & ( for b being Subset of {} holds
( not b in A or a = b or a misses b ) ) ) ) ) ;
hence {} is a_partition of {} by Def4; ::_thesis: verum
end;
begin
theorem :: EQREL_1:46
for X, X1 being set
for F being Function st X c= F " X1 holds
F .: X c= X1
proof
let X, X1 be set ; ::_thesis: for F being Function st X c= F " X1 holds
F .: X c= X1
let F be Function; ::_thesis: ( X c= F " X1 implies F .: X c= X1 )
assume X c= F " X1 ; ::_thesis: F .: X c= X1
then A1: F .: X c= F .: (F " X1) by RELAT_1:123;
F .: (F " X1) c= X1 by FUNCT_1:75;
hence F .: X c= X1 by A1, XBOOLE_1:1; ::_thesis: verum
end;
theorem Th47: :: EQREL_1:47
for e, X, Y being set st e c= [:X,Y:] holds
(.: (pr1 (X,Y))) . e = (pr1 (X,Y)) .: e
proof
let e, X, Y be set ; ::_thesis: ( e c= [:X,Y:] implies (.: (pr1 (X,Y))) . e = (pr1 (X,Y)) .: e )
assume e c= [:X,Y:] ; ::_thesis: (.: (pr1 (X,Y))) . e = (pr1 (X,Y)) .: e
then e c= dom (pr1 (X,Y)) by FUNCT_3:def_4;
hence (.: (pr1 (X,Y))) . e = (pr1 (X,Y)) .: e by FUNCT_3:def_1; ::_thesis: verum
end;
theorem Th48: :: EQREL_1:48
for e, X, Y being set st e c= [:X,Y:] holds
(.: (pr2 (X,Y))) . e = (pr2 (X,Y)) .: e
proof
let e, X, Y be set ; ::_thesis: ( e c= [:X,Y:] implies (.: (pr2 (X,Y))) . e = (pr2 (X,Y)) .: e )
assume e c= [:X,Y:] ; ::_thesis: (.: (pr2 (X,Y))) . e = (pr2 (X,Y)) .: e
then e c= dom (pr2 (X,Y)) by FUNCT_3:def_5;
hence (.: (pr2 (X,Y))) . e = (pr2 (X,Y)) .: e by FUNCT_3:def_1; ::_thesis: verum
end;
theorem Th49: :: EQREL_1:49
for X, Y being set
for X1 being Subset of X
for Y1 being Subset of Y st [:X1,Y1:] <> {} holds
( (pr1 (X,Y)) .: [:X1,Y1:] = X1 & (pr2 (X,Y)) .: [:X1,Y1:] = Y1 )
proof
let X, Y be set ; ::_thesis: for X1 being Subset of X
for Y1 being Subset of Y st [:X1,Y1:] <> {} holds
( (pr1 (X,Y)) .: [:X1,Y1:] = X1 & (pr2 (X,Y)) .: [:X1,Y1:] = Y1 )
let X1 be Subset of X; ::_thesis: for Y1 being Subset of Y st [:X1,Y1:] <> {} holds
( (pr1 (X,Y)) .: [:X1,Y1:] = X1 & (pr2 (X,Y)) .: [:X1,Y1:] = Y1 )
let Y1 be Subset of Y; ::_thesis: ( [:X1,Y1:] <> {} implies ( (pr1 (X,Y)) .: [:X1,Y1:] = X1 & (pr2 (X,Y)) .: [:X1,Y1:] = Y1 ) )
assume A1: [:X1,Y1:] <> {} ; ::_thesis: ( (pr1 (X,Y)) .: [:X1,Y1:] = X1 & (pr2 (X,Y)) .: [:X1,Y1:] = Y1 )
then A2: X1 <> {} ;
A3: Y1 <> {} by A1;
A4: X <> {} by A2;
now__::_thesis:_for_x_being_set_holds_
(_(_x_in_(pr1_(X,Y))_.:_[:X1,Y1:]_implies_x_in_X1_)_&_(_x_in_X1_implies_x_in_(pr1_(X,Y))_.:_[:X1,Y1:]_)_)
set y = the Element of Y1;
let x be set ; ::_thesis: ( ( x in (pr1 (X,Y)) .: [:X1,Y1:] implies x in X1 ) & ( x in X1 implies x in (pr1 (X,Y)) .: [:X1,Y1:] ) )
thus ( x in (pr1 (X,Y)) .: [:X1,Y1:] implies x in X1 ) ::_thesis: ( x in X1 implies x in (pr1 (X,Y)) .: [:X1,Y1:] )
proof
assume x in (pr1 (X,Y)) .: [:X1,Y1:] ; ::_thesis: x in X1
then consider u being set such that
A5: u in [:X,Y:] and
A6: ( u in [:X1,Y1:] & x = (pr1 (X,Y)) . u ) by FUNCT_2:64;
A7: u `2 in Y by A5, MCART_1:10;
( u `1 in X1 & x = (pr1 (X,Y)) . ((u `1),(u `2)) ) by A6, MCART_1:10, MCART_1:21;
hence x in X1 by A7, FUNCT_3:def_4; ::_thesis: verum
end;
assume A8: x in X1 ; ::_thesis: x in (pr1 (X,Y)) .: [:X1,Y1:]
the Element of Y1 in Y by A3, TARSKI:def_3;
then A9: x = (pr1 (X,Y)) . (x, the Element of Y1) by A8, FUNCT_3:def_4;
[x, the Element of Y1] in [:X1,Y1:] by A3, A8, ZFMISC_1:87;
hence x in (pr1 (X,Y)) .: [:X1,Y1:] by A4, A9, FUNCT_2:35; ::_thesis: verum
end;
hence (pr1 (X,Y)) .: [:X1,Y1:] = X1 by TARSKI:1; ::_thesis: (pr2 (X,Y)) .: [:X1,Y1:] = Y1
A10: Y <> {} by A3;
now__::_thesis:_for_y_being_set_holds_
(_(_y_in_(pr2_(X,Y))_.:_[:X1,Y1:]_implies_y_in_Y1_)_&_(_y_in_Y1_implies_y_in_(pr2_(X,Y))_.:_[:X1,Y1:]_)_)
set x = the Element of X1;
let y be set ; ::_thesis: ( ( y in (pr2 (X,Y)) .: [:X1,Y1:] implies y in Y1 ) & ( y in Y1 implies y in (pr2 (X,Y)) .: [:X1,Y1:] ) )
thus ( y in (pr2 (X,Y)) .: [:X1,Y1:] implies y in Y1 ) ::_thesis: ( y in Y1 implies y in (pr2 (X,Y)) .: [:X1,Y1:] )
proof
assume y in (pr2 (X,Y)) .: [:X1,Y1:] ; ::_thesis: y in Y1
then consider u being set such that
A11: u in [:X,Y:] and
A12: ( u in [:X1,Y1:] & y = (pr2 (X,Y)) . u ) by FUNCT_2:64;
A13: u `1 in X by A11, MCART_1:10;
( u `2 in Y1 & y = (pr2 (X,Y)) . ((u `1),(u `2)) ) by A12, MCART_1:10, MCART_1:21;
hence y in Y1 by A13, FUNCT_3:def_5; ::_thesis: verum
end;
assume A14: y in Y1 ; ::_thesis: y in (pr2 (X,Y)) .: [:X1,Y1:]
the Element of X1 in X by A2, TARSKI:def_3;
then A15: y = (pr2 (X,Y)) . ( the Element of X1,y) by A14, FUNCT_3:def_5;
[ the Element of X1,y] in [:X1,Y1:] by A2, A14, ZFMISC_1:87;
hence y in (pr2 (X,Y)) .: [:X1,Y1:] by A10, A15, FUNCT_2:35; ::_thesis: verum
end;
hence (pr2 (X,Y)) .: [:X1,Y1:] = Y1 by TARSKI:1; ::_thesis: verum
end;
theorem Th50: :: EQREL_1:50
for X, Y being set
for X1 being Subset of X
for Y1 being Subset of Y st [:X1,Y1:] <> {} holds
( (.: (pr1 (X,Y))) . [:X1,Y1:] = X1 & (.: (pr2 (X,Y))) . [:X1,Y1:] = Y1 )
proof
let X, Y be set ; ::_thesis: for X1 being Subset of X
for Y1 being Subset of Y st [:X1,Y1:] <> {} holds
( (.: (pr1 (X,Y))) . [:X1,Y1:] = X1 & (.: (pr2 (X,Y))) . [:X1,Y1:] = Y1 )
let X1 be Subset of X; ::_thesis: for Y1 being Subset of Y st [:X1,Y1:] <> {} holds
( (.: (pr1 (X,Y))) . [:X1,Y1:] = X1 & (.: (pr2 (X,Y))) . [:X1,Y1:] = Y1 )
let Y1 be Subset of Y; ::_thesis: ( [:X1,Y1:] <> {} implies ( (.: (pr1 (X,Y))) . [:X1,Y1:] = X1 & (.: (pr2 (X,Y))) . [:X1,Y1:] = Y1 ) )
assume A1: [:X1,Y1:] <> {} ; ::_thesis: ( (.: (pr1 (X,Y))) . [:X1,Y1:] = X1 & (.: (pr2 (X,Y))) . [:X1,Y1:] = Y1 )
thus (.: (pr1 (X,Y))) . [:X1,Y1:] = (pr1 (X,Y)) .: [:X1,Y1:] by Th47
.= X1 by A1, Th49 ; ::_thesis: (.: (pr2 (X,Y))) . [:X1,Y1:] = Y1
thus (.: (pr2 (X,Y))) . [:X1,Y1:] = (pr2 (X,Y)) .: [:X1,Y1:] by Th48
.= Y1 by A1, Th49 ; ::_thesis: verum
end;
theorem :: EQREL_1:51
for X, Y being set
for A being Subset of [:X,Y:]
for H being Subset-Family of [:X,Y:] st ( for e being set st e in H holds
( e c= A & ex X1 being Subset of X ex Y1 being Subset of Y st e = [:X1,Y1:] ) ) holds
[:(union ((.: (pr1 (X,Y))) .: H)),(meet ((.: (pr2 (X,Y))) .: H)):] c= A
proof
let X, Y be set ; ::_thesis: for A being Subset of [:X,Y:]
for H being Subset-Family of [:X,Y:] st ( for e being set st e in H holds
( e c= A & ex X1 being Subset of X ex Y1 being Subset of Y st e = [:X1,Y1:] ) ) holds
[:(union ((.: (pr1 (X,Y))) .: H)),(meet ((.: (pr2 (X,Y))) .: H)):] c= A
let A be Subset of [:X,Y:]; ::_thesis: for H being Subset-Family of [:X,Y:] st ( for e being set st e in H holds
( e c= A & ex X1 being Subset of X ex Y1 being Subset of Y st e = [:X1,Y1:] ) ) holds
[:(union ((.: (pr1 (X,Y))) .: H)),(meet ((.: (pr2 (X,Y))) .: H)):] c= A
let H be Subset-Family of [:X,Y:]; ::_thesis: ( ( for e being set st e in H holds
( e c= A & ex X1 being Subset of X ex Y1 being Subset of Y st e = [:X1,Y1:] ) ) implies [:(union ((.: (pr1 (X,Y))) .: H)),(meet ((.: (pr2 (X,Y))) .: H)):] c= A )
assume A1: for e being set st e in H holds
( e c= A & ex X1 being Subset of X ex Y1 being Subset of Y st e = [:X1,Y1:] ) ; ::_thesis: [:(union ((.: (pr1 (X,Y))) .: H)),(meet ((.: (pr2 (X,Y))) .: H)):] c= A
let u be set ; :: according to RELAT_1:def_3 ::_thesis: for b1 being set holds
( not [u,b1] in [:(union ((.: (pr1 (X,Y))) .: H)),(meet ((.: (pr2 (X,Y))) .: H)):] or [u,b1] in A )
let v be set ; ::_thesis: ( not [u,v] in [:(union ((.: (pr1 (X,Y))) .: H)),(meet ((.: (pr2 (X,Y))) .: H)):] or [u,v] in A )
assume A2: [u,v] in [:(union ((.: (pr1 (X,Y))) .: H)),(meet ((.: (pr2 (X,Y))) .: H)):] ; ::_thesis: [u,v] in A
then A3: v in meet ((.: (pr2 (X,Y))) .: H) by ZFMISC_1:87;
u in union ((.: (pr1 (X,Y))) .: H) by A2, ZFMISC_1:87;
then consider x being set such that
A4: u in x and
A5: x in (.: (pr1 (X,Y))) .: H by TARSKI:def_4;
consider y being set such that
y in dom (.: (pr1 (X,Y))) and
A6: y in H and
A7: x = (.: (pr1 (X,Y))) . y by A5, FUNCT_1:def_6;
consider X1 being Subset of X, Y1 being Subset of Y such that
A8: y = [:X1,Y1:] by A1, A6;
A9: y <> {} by A4, A7, FUNCT_3:8;
y in bool [:X,Y:] by A6;
then y in bool (dom (pr2 (X,Y))) by FUNCT_3:def_5;
then y in dom (.: (pr2 (X,Y))) by FUNCT_3:def_1;
then (.: (pr2 (X,Y))) . y in (.: (pr2 (X,Y))) .: H by A6, FUNCT_1:def_6;
then Y1 in (.: (pr2 (X,Y))) .: H by A8, A9, Th50;
then A10: v in Y1 by A3, SETFAM_1:def_1;
u in X1 by A4, A7, A8, A9, Th50;
then A11: [u,v] in y by A8, A10, ZFMISC_1:87;
y c= A by A1, A6;
hence [u,v] in A by A11; ::_thesis: verum
end;
theorem :: EQREL_1:52
for X, Y being set
for A being Subset of [:X,Y:]
for H being Subset-Family of [:X,Y:] st ( for e being set st e in H holds
( e c= A & ex X1 being Subset of X ex Y1 being Subset of Y st e = [:X1,Y1:] ) ) holds
[:(meet ((.: (pr1 (X,Y))) .: H)),(union ((.: (pr2 (X,Y))) .: H)):] c= A
proof
let X, Y be set ; ::_thesis: for A being Subset of [:X,Y:]
for H being Subset-Family of [:X,Y:] st ( for e being set st e in H holds
( e c= A & ex X1 being Subset of X ex Y1 being Subset of Y st e = [:X1,Y1:] ) ) holds
[:(meet ((.: (pr1 (X,Y))) .: H)),(union ((.: (pr2 (X,Y))) .: H)):] c= A
let A be Subset of [:X,Y:]; ::_thesis: for H being Subset-Family of [:X,Y:] st ( for e being set st e in H holds
( e c= A & ex X1 being Subset of X ex Y1 being Subset of Y st e = [:X1,Y1:] ) ) holds
[:(meet ((.: (pr1 (X,Y))) .: H)),(union ((.: (pr2 (X,Y))) .: H)):] c= A
let H be Subset-Family of [:X,Y:]; ::_thesis: ( ( for e being set st e in H holds
( e c= A & ex X1 being Subset of X ex Y1 being Subset of Y st e = [:X1,Y1:] ) ) implies [:(meet ((.: (pr1 (X,Y))) .: H)),(union ((.: (pr2 (X,Y))) .: H)):] c= A )
assume A1: for e being set st e in H holds
( e c= A & ex X1 being Subset of X ex Y1 being Subset of Y st e = [:X1,Y1:] ) ; ::_thesis: [:(meet ((.: (pr1 (X,Y))) .: H)),(union ((.: (pr2 (X,Y))) .: H)):] c= A
let u be set ; :: according to RELAT_1:def_3 ::_thesis: for b1 being set holds
( not [u,b1] in [:(meet ((.: (pr1 (X,Y))) .: H)),(union ((.: (pr2 (X,Y))) .: H)):] or [u,b1] in A )
let v be set ; ::_thesis: ( not [u,v] in [:(meet ((.: (pr1 (X,Y))) .: H)),(union ((.: (pr2 (X,Y))) .: H)):] or [u,v] in A )
assume A2: [u,v] in [:(meet ((.: (pr1 (X,Y))) .: H)),(union ((.: (pr2 (X,Y))) .: H)):] ; ::_thesis: [u,v] in A
then A3: u in meet ((.: (pr1 (X,Y))) .: H) by ZFMISC_1:87;
v in union ((.: (pr2 (X,Y))) .: H) by A2, ZFMISC_1:87;
then consider x being set such that
A4: v in x and
A5: x in (.: (pr2 (X,Y))) .: H by TARSKI:def_4;
consider y being set such that
y in dom (.: (pr2 (X,Y))) and
A6: y in H and
A7: x = (.: (pr2 (X,Y))) . y by A5, FUNCT_1:def_6;
consider X1 being Subset of X, Y1 being Subset of Y such that
A8: y = [:X1,Y1:] by A1, A6;
A9: y <> {} by A4, A7, FUNCT_3:8;
y in bool [:X,Y:] by A6;
then y in bool (dom (pr1 (X,Y))) by FUNCT_3:def_4;
then y in dom (.: (pr1 (X,Y))) by FUNCT_3:def_1;
then (.: (pr1 (X,Y))) . y in (.: (pr1 (X,Y))) .: H by A6, FUNCT_1:def_6;
then X1 in (.: (pr1 (X,Y))) .: H by A8, A9, Th50;
then A10: u in X1 by A3, SETFAM_1:def_1;
v in Y1 by A4, A7, A8, A9, Th50;
then A11: [u,v] in y by A8, A10, ZFMISC_1:87;
y c= A by A1, A6;
hence [u,v] in A by A11; ::_thesis: verum
end;
theorem :: EQREL_1:53
for X being set
for Y being non empty set
for f being Function of X,Y
for H being Subset-Family of X holds union ((.: f) .: H) = f .: (union H)
proof
let X be set ; ::_thesis: for Y being non empty set
for f being Function of X,Y
for H being Subset-Family of X holds union ((.: f) .: H) = f .: (union H)
let Y be non empty set ; ::_thesis: for f being Function of X,Y
for H being Subset-Family of X holds union ((.: f) .: H) = f .: (union H)
let f be Function of X,Y; ::_thesis: for H being Subset-Family of X holds union ((.: f) .: H) = f .: (union H)
let H be Subset-Family of X; ::_thesis: union ((.: f) .: H) = f .: (union H)
dom f = X by FUNCT_2:def_1;
hence union ((.: f) .: H) = f .: (union H) by FUNCT_3:14; ::_thesis: verum
end;
theorem :: EQREL_1:54
for X being set
for a being Subset-Family of X holds union (union a) = union { (union A) where A is Subset of X : A in a }
proof
let X be set ; ::_thesis: for a being Subset-Family of X holds union (union a) = union { (union A) where A is Subset of X : A in a }
let a be Subset-Family of X; ::_thesis: union (union a) = union { (union A) where A is Subset of X : A in a }
thus union (union a) c= union { (union A) where A is Subset of X : A in a } :: according to XBOOLE_0:def_10 ::_thesis: union { (union A) where A is Subset of X : A in a } c= union (union a)
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in union (union a) or e in union { (union A) where A is Subset of X : A in a } )
assume e in union (union a) ; ::_thesis: e in union { (union A) where A is Subset of X : A in a }
then consider B being set such that
A1: e in B and
A2: B in union a by TARSKI:def_4;
consider C being set such that
A3: B in C and
A4: C in a by A2, TARSKI:def_4;
A5: union C in { (union A) where A is Subset of X : A in a } by A4;
e in union C by A1, A3, TARSKI:def_4;
hence e in union { (union A) where A is Subset of X : A in a } by A5, TARSKI:def_4; ::_thesis: verum
end;
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in union { (union A) where A is Subset of X : A in a } or e in union (union a) )
assume e in union { (union A) where A is Subset of X : A in a } ; ::_thesis: e in union (union a)
then consider c being set such that
A6: e in c and
A7: c in { (union A) where A is Subset of X : A in a } by TARSKI:def_4;
consider A being Subset of X such that
A8: c = union A and
A9: A in a by A7;
consider b being set such that
A10: e in b and
A11: b in A by A6, A8, TARSKI:def_4;
b in union a by A9, A11, TARSKI:def_4;
hence e in union (union a) by A10, TARSKI:def_4; ::_thesis: verum
end;
theorem Th55: :: EQREL_1:55
for X being set
for D being Subset-Family of X st union D = X holds
for A being Subset of D
for B being Subset of X st B = union A holds
B ` c= union (A `)
proof
let X be set ; ::_thesis: for D being Subset-Family of X st union D = X holds
for A being Subset of D
for B being Subset of X st B = union A holds
B ` c= union (A `)
let D be Subset-Family of X; ::_thesis: ( union D = X implies for A being Subset of D
for B being Subset of X st B = union A holds
B ` c= union (A `) )
assume A1: union D = X ; ::_thesis: for A being Subset of D
for B being Subset of X st B = union A holds
B ` c= union (A `)
let A be Subset of D; ::_thesis: for B being Subset of X st B = union A holds
B ` c= union (A `)
let B be Subset of X; ::_thesis: ( B = union A implies B ` c= union (A `) )
assume A2: B = union A ; ::_thesis: B ` c= union (A `)
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in B ` or e in union (A `) )
assume A3: e in B ` ; ::_thesis: e in union (A `)
then consider u being set such that
A4: e in u and
A5: u in D by A1, TARSKI:def_4;
not e in B by A3, XBOOLE_0:def_5;
then not u in A by A2, A4, TARSKI:def_4;
then u in A ` by A5, SUBSET_1:29;
hence e in union (A `) by A4, TARSKI:def_4; ::_thesis: verum
end;
theorem :: EQREL_1:56
for X, Y, Z being non empty set
for F being Function of X,Y
for G being Function of X,Z st ( for x, x9 being Element of X st F . x = F . x9 holds
G . x = G . x9 ) holds
ex H being Function of Y,Z st H * F = G
proof
let X, Y, Z be non empty set ; ::_thesis: for F being Function of X,Y
for G being Function of X,Z st ( for x, x9 being Element of X st F . x = F . x9 holds
G . x = G . x9 ) holds
ex H being Function of Y,Z st H * F = G
let F be Function of X,Y; ::_thesis: for G being Function of X,Z st ( for x, x9 being Element of X st F . x = F . x9 holds
G . x = G . x9 ) holds
ex H being Function of Y,Z st H * F = G
let G be Function of X,Z; ::_thesis: ( ( for x, x9 being Element of X st F . x = F . x9 holds
G . x = G . x9 ) implies ex H being Function of Y,Z st H * F = G )
defpred S1[ set , set ] means ( for x being Element of X holds not $1 = F . x or for x being Element of X st $1 = F . x holds
$2 = G . x );
assume A1: for x, x9 being Element of X st F . x = F . x9 holds
G . x = G . x9 ; ::_thesis: ex H being Function of Y,Z st H * F = G
A2: now__::_thesis:_for_e_being_set_st_e_in_Y_holds_
ex_u_being_set_st_
(_u_in_Z_&_S1[e,u]_)
let e be set ; ::_thesis: ( e in Y implies ex u being set st
( u in Z & S1[e,u] ) )
assume e in Y ; ::_thesis: ex u being set st
( u in Z & S1[e,u] )
now__::_thesis:_(_(_ex_x_being_Element_of_X_st_e_=_F_._x_&_ex_u_being_Element_of_Z_st_
(_u_in_Z_&_(_ex_x_being_Element_of_X_st_e_=_F_._x_implies_ex_x_being_Element_of_X_st_
(_e_=_F_._x_&_u_=_G_._x_)_)_)_)_or_(_(_for_x_being_Element_of_X_holds_not_e_=_F_._x_)_&_ex_u_being_set_st_
(_u_in_Z_&_(_ex_x_being_Element_of_X_st_e_=_F_._x_implies_ex_x_being_Element_of_X_st_
(_e_=_F_._x_&_u_=_G_._x_)_)_)_)_)
percases ( ex x being Element of X st e = F . x or for x being Element of X holds not e = F . x ) ;
case ex x being Element of X st e = F . x ; ::_thesis: ex u being Element of Z st
( u in Z & ( ex x being Element of X st e = F . x implies ex x being Element of X st
( e = F . x & u = G . x ) ) )
then consider x being Element of X such that
A3: e = F . x ;
take u = G . x; ::_thesis: ( u in Z & ( ex x being Element of X st e = F . x implies ex x being Element of X st
( e = F . x & u = G . x ) ) )
thus ( u in Z & ( ex x being Element of X st e = F . x implies ex x being Element of X st
( e = F . x & u = G . x ) ) ) by A3; ::_thesis: verum
end;
caseA4: for x being Element of X holds not e = F . x ; ::_thesis: ex u being set st
( u in Z & ( ex x being Element of X st e = F . x implies ex x being Element of X st
( e = F . x & u = G . x ) ) )
set u = the Element of Z;
the Element of Z in Z ;
hence ex u being set st
( u in Z & ( ex x being Element of X st e = F . x implies ex x being Element of X st
( e = F . x & u = G . x ) ) ) by A4; ::_thesis: verum
end;
end;
end;
then consider u being set such that
A5: u in Z and
A6: ( ex x being Element of X st e = F . x implies ex x being Element of X st
( e = F . x & u = G . x ) ) ;
take u = u; ::_thesis: ( u in Z & S1[e,u] )
thus u in Z by A5; ::_thesis: S1[e,u]
thus S1[e,u] by A1, A6; ::_thesis: verum
end;
consider H being Function of Y,Z such that
A7: for e being set st e in Y holds
S1[e,H . e] from FUNCT_2:sch_1(A2);
take H ; ::_thesis: H * F = G
now__::_thesis:_for_x_being_Element_of_X_holds_(H_*_F)_._x_=_G_._x
let x be Element of X; ::_thesis: (H * F) . x = G . x
thus (H * F) . x = H . (F . x) by FUNCT_2:15
.= G . x by A7 ; ::_thesis: verum
end;
hence H * F = G by FUNCT_2:63; ::_thesis: verum
end;
theorem :: EQREL_1:57
for X, Y, Z being non empty set
for y being Element of Y
for F being Function of X,Y
for G being Function of Y,Z holds F " {y} c= (G * F) " {(G . y)}
proof
let X, Y, Z be non empty set ; ::_thesis: for y being Element of Y
for F being Function of X,Y
for G being Function of Y,Z holds F " {y} c= (G * F) " {(G . y)}
let y be Element of Y; ::_thesis: for F being Function of X,Y
for G being Function of Y,Z holds F " {y} c= (G * F) " {(G . y)}
let F be Function of X,Y; ::_thesis: for G being Function of Y,Z holds F " {y} c= (G * F) " {(G . y)}
let G be Function of Y,Z; ::_thesis: F " {y} c= (G * F) " {(G . y)}
F " {y} c= (G * F) " (Im (G,y)) by FUNCT_2:44;
hence F " {y} c= (G * F) " {(G . y)} by SETWISEO:8; ::_thesis: verum
end;
theorem :: EQREL_1:58
for X, Y, Z being non empty set
for F being Function of X,Y
for x being Element of X
for z being Element of Z holds [:F,(id Z):] . (x,z) = [(F . x),z]
proof
let X, Y, Z be non empty set ; ::_thesis: for F being Function of X,Y
for x being Element of X
for z being Element of Z holds [:F,(id Z):] . (x,z) = [(F . x),z]
let F be Function of X,Y; ::_thesis: for x being Element of X
for z being Element of Z holds [:F,(id Z):] . (x,z) = [(F . x),z]
let x be Element of X; ::_thesis: for z being Element of Z holds [:F,(id Z):] . (x,z) = [(F . x),z]
let z be Element of Z; ::_thesis: [:F,(id Z):] . (x,z) = [(F . x),z]
thus [:F,(id Z):] . (x,z) = [(F . x),((id Z) . z)] by FUNCT_3:75
.= [(F . x),z] by FUNCT_1:18 ; ::_thesis: verum
end;
theorem :: EQREL_1:59
for X, Y, Z being non empty set
for F being Function of X,Y
for A being Subset of X
for B being Subset of Z holds [:F,(id Z):] .: [:A,B:] = [:(F .: A),B:]
proof
let X, Y, Z be non empty set ; ::_thesis: for F being Function of X,Y
for A being Subset of X
for B being Subset of Z holds [:F,(id Z):] .: [:A,B:] = [:(F .: A),B:]
let F be Function of X,Y; ::_thesis: for A being Subset of X
for B being Subset of Z holds [:F,(id Z):] .: [:A,B:] = [:(F .: A),B:]
let A be Subset of X; ::_thesis: for B being Subset of Z holds [:F,(id Z):] .: [:A,B:] = [:(F .: A),B:]
let B be Subset of Z; ::_thesis: [:F,(id Z):] .: [:A,B:] = [:(F .: A),B:]
thus [:F,(id Z):] .: [:A,B:] = [:(F .: A),((id Z) .: B):] by FUNCT_3:72
.= [:(F .: A),B:] by FUNCT_1:92 ; ::_thesis: verum
end;
theorem :: EQREL_1:60
for X, Y, Z being non empty set
for F being Function of X,Y
for y being Element of Y
for z being Element of Z holds [:F,(id Z):] " {[y,z]} = [:(F " {y}),{z}:]
proof
let X, Y, Z be non empty set ; ::_thesis: for F being Function of X,Y
for y being Element of Y
for z being Element of Z holds [:F,(id Z):] " {[y,z]} = [:(F " {y}),{z}:]
let F be Function of X,Y; ::_thesis: for y being Element of Y
for z being Element of Z holds [:F,(id Z):] " {[y,z]} = [:(F " {y}),{z}:]
let y be Element of Y; ::_thesis: for z being Element of Z holds [:F,(id Z):] " {[y,z]} = [:(F " {y}),{z}:]
let z be Element of Z; ::_thesis: [:F,(id Z):] " {[y,z]} = [:(F " {y}),{z}:]
thus [:F,(id Z):] " {[y,z]} = [:F,(id Z):] " [:{y},{z}:] by ZFMISC_1:29
.= [:(F " {y}),((id Z) " {z}):] by FUNCT_3:73
.= [:(F " {y}),{z}:] by FUNCT_2:94 ; ::_thesis: verum
end;
theorem :: EQREL_1:61
for X being non empty set
for D being Subset-Family of X
for A being Subset of D holds union A is Subset of X
proof
let X be non empty set ; ::_thesis: for D being Subset-Family of X
for A being Subset of D holds union A is Subset of X
let D be Subset-Family of X; ::_thesis: for A being Subset of D holds union A is Subset of X
let A be Subset of D; ::_thesis: union A is Subset of X
union A c= X
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in union A or e in X )
assume e in union A ; ::_thesis: e in X
then ex u being set st
( e in u & u in A ) by TARSKI:def_4;
then e in union D by TARSKI:def_4;
hence e in X ; ::_thesis: verum
end;
hence union A is Subset of X ; ::_thesis: verum
end;
theorem :: EQREL_1:62
for X being set
for D being a_partition of X
for A, B being Subset of D holds union (A /\ B) = (union A) /\ (union B)
proof
let X be set ; ::_thesis: for D being a_partition of X
for A, B being Subset of D holds union (A /\ B) = (union A) /\ (union B)
let D be a_partition of X; ::_thesis: for A, B being Subset of D holds union (A /\ B) = (union A) /\ (union B)
let A, B be Subset of D; ::_thesis: union (A /\ B) = (union A) /\ (union B)
thus union (A /\ B) c= (union A) /\ (union B) by ZFMISC_1:79; :: according to XBOOLE_0:def_10 ::_thesis: (union A) /\ (union B) c= union (A /\ B)
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in (union A) /\ (union B) or e in union (A /\ B) )
assume A1: e in (union A) /\ (union B) ; ::_thesis: e in union (A /\ B)
then e in union A by XBOOLE_0:def_4;
then consider a being set such that
A2: e in a and
A3: a in A by TARSKI:def_4;
A4: a in D by A3;
e in union B by A1, XBOOLE_0:def_4;
then consider b being set such that
A5: e in b and
A6: b in B by TARSKI:def_4;
A7: b in D by A6;
not a misses b by A2, A5, XBOOLE_0:3;
then a = b by A4, A7, Def4;
then a in A /\ B by A3, A6, XBOOLE_0:def_4;
hence e in union (A /\ B) by A2, TARSKI:def_4; ::_thesis: verum
end;
theorem :: EQREL_1:63
for X being non empty set
for D being a_partition of X
for A being Subset of D
for B being Subset of X st B = union A holds
B ` = union (A `)
proof
let X be non empty set ; ::_thesis: for D being a_partition of X
for A being Subset of D
for B being Subset of X st B = union A holds
B ` = union (A `)
let D be a_partition of X; ::_thesis: for A being Subset of D
for B being Subset of X st B = union A holds
B ` = union (A `)
let A be Subset of D; ::_thesis: for B being Subset of X st B = union A holds
B ` = union (A `)
let B be Subset of X; ::_thesis: ( B = union A implies B ` = union (A `) )
assume A1: B = union A ; ::_thesis: B ` = union (A `)
union D = X by Def4;
hence B ` c= union (A `) by A1, Th55; :: according to XBOOLE_0:def_10 ::_thesis: union (A `) c= B `
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in union (A `) or e in B ` )
assume e in union (A `) ; ::_thesis: e in B `
then consider u being set such that
A2: e in u and
A3: u in A ` by TARSKI:def_4;
A4: u in D by A3;
assume not e in B ` ; ::_thesis: contradiction
then e in B by A2, A4, SUBSET_1:29;
then consider v being set such that
A5: e in v and
A6: v in A by A1, TARSKI:def_4;
A7: v in D by A6;
not u misses v by A2, A5, XBOOLE_0:3;
then u = v by A4, A7, Def4;
hence contradiction by A3, A6, XBOOLE_0:def_5; ::_thesis: verum
end;
theorem :: EQREL_1:64
for X being non empty set
for E being Equivalence_Relation of X holds not Class E is empty ;
registration
let X be non empty set ;
cluster non empty with_non-empty_elements for a_partition of X;
existence
not for b1 being a_partition of X holds b1 is empty
proof
reconsider P = Class (nabla X) as a_partition of X ;
take P ; ::_thesis: not P is empty
thus not P is empty ; ::_thesis: verum
end;
end;
definition
let X be non empty set ;
let D be non empty a_partition of X;
func proj D -> Function of X,D means :Def9: :: EQREL_1:def 9
for p being Element of X holds p in it . p;
existence
ex b1 being Function of X,D st
for p being Element of X holds p in b1 . p
proof
defpred S1[ set , set ] means $1 in $2;
A1: now__::_thesis:_for_e_being_set_st_e_in_X_holds_
ex_u_being_set_st_
(_u_in_D_&_S1[e,u]_)
A2: union D = X by Def4;
let e be set ; ::_thesis: ( e in X implies ex u being set st
( u in D & S1[e,u] ) )
assume e in X ; ::_thesis: ex u being set st
( u in D & S1[e,u] )
then ex u being set st
( e in u & u in D ) by A2, TARSKI:def_4;
hence ex u being set st
( u in D & S1[e,u] ) ; ::_thesis: verum
end;
consider F being Function of X,D such that
A3: for e being set st e in X holds
S1[e,F . e] from FUNCT_2:sch_1(A1);
take F ; ::_thesis: for p being Element of X holds p in F . p
let p be Element of X; ::_thesis: p in F . p
thus p in F . p by A3; ::_thesis: verum
end;
correctness
uniqueness
for b1, b2 being Function of X,D st ( for p being Element of X holds p in b1 . p ) & ( for p being Element of X holds p in b2 . p ) holds
b1 = b2;
proof
let F, G be Function of X,D; ::_thesis: ( ( for p being Element of X holds p in F . p ) & ( for p being Element of X holds p in G . p ) implies F = G )
assume A4: ( ( for p being Element of X holds p in F . p ) & ( for p being Element of X holds p in G . p ) ) ; ::_thesis: F = G
now__::_thesis:_for_x_being_Element_of_X_holds_F_._x_=_G_._x
let x be Element of X; ::_thesis: F . x = G . x
( x in F . x & x in G . x ) by A4;
then A5: not F . x misses G . x by XBOOLE_0:3;
( F . x is Subset of X & G . x is Subset of X ) by TARSKI:def_3;
hence F . x = G . x by A5, Def4; ::_thesis: verum
end;
hence F = G by FUNCT_2:63; ::_thesis: verum
end;
end;
:: deftheorem Def9 defines proj EQREL_1:def_9_:_
for X being non empty set
for D being non empty a_partition of X
for b3 being Function of X,D holds
( b3 = proj D iff for p being Element of X holds p in b3 . p );
theorem Th65: :: EQREL_1:65
for X being non empty set
for D being non empty a_partition of X
for p being Element of X
for A being Element of D st p in A holds
A = (proj D) . p
proof
let X be non empty set ; ::_thesis: for D being non empty a_partition of X
for p being Element of X
for A being Element of D st p in A holds
A = (proj D) . p
let D be non empty a_partition of X; ::_thesis: for p being Element of X
for A being Element of D st p in A holds
A = (proj D) . p
let p be Element of X; ::_thesis: for A being Element of D st p in A holds
A = (proj D) . p
let A be Element of D; ::_thesis: ( p in A implies A = (proj D) . p )
assume A1: p in A ; ::_thesis: A = (proj D) . p
p in (proj D) . p by Def9;
then ( (proj D) . p is Subset of X & not (proj D) . p misses A ) by A1, TARSKI:def_3, XBOOLE_0:3;
hence A = (proj D) . p by Def4; ::_thesis: verum
end;
theorem :: EQREL_1:66
for X being non empty set
for D being non empty a_partition of X
for p being Element of D holds p = (proj D) " {p}
proof
let X be non empty set ; ::_thesis: for D being non empty a_partition of X
for p being Element of D holds p = (proj D) " {p}
let D be non empty a_partition of X; ::_thesis: for p being Element of D holds p = (proj D) " {p}
let p be Element of D; ::_thesis: p = (proj D) " {p}
thus p c= (proj D) " {p} :: according to XBOOLE_0:def_10 ::_thesis: (proj D) " {p} c= p
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in p or e in (proj D) " {p} )
assume A1: e in p ; ::_thesis: e in (proj D) " {p}
then (proj D) . e = p by Th65;
then (proj D) . e in {p} by TARSKI:def_1;
hence e in (proj D) " {p} by A1, FUNCT_2:38; ::_thesis: verum
end;
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in (proj D) " {p} or e in p )
assume A2: e in (proj D) " {p} ; ::_thesis: e in p
then (proj D) . e in {p} by FUNCT_1:def_7;
then (proj D) . e = p by TARSKI:def_1;
hence e in p by A2, Def9; ::_thesis: verum
end;
theorem :: EQREL_1:67
for X being non empty set
for D being non empty a_partition of X
for A being Subset of D holds (proj D) " A = union A
proof
let X be non empty set ; ::_thesis: for D being non empty a_partition of X
for A being Subset of D holds (proj D) " A = union A
let D be non empty a_partition of X; ::_thesis: for A being Subset of D holds (proj D) " A = union A
let A be Subset of D; ::_thesis: (proj D) " A = union A
thus (proj D) " A c= union A :: according to XBOOLE_0:def_10 ::_thesis: union A c= (proj D) " A
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in (proj D) " A or e in union A )
assume e in (proj D) " A ; ::_thesis: e in union A
then ( (proj D) . e in A & e in (proj D) . e ) by Def9, FUNCT_2:38;
hence e in union A by TARSKI:def_4; ::_thesis: verum
end;
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in union A or e in (proj D) " A )
assume e in union A ; ::_thesis: e in (proj D) " A
then consider u being set such that
A1: e in u and
A2: u in A by TARSKI:def_4;
A3: u in D by A2;
then (proj D) . e = u by A1, Th65;
hence e in (proj D) " A by A1, A2, A3, FUNCT_2:38; ::_thesis: verum
end;
theorem :: EQREL_1:68
for X being non empty set
for D being non empty a_partition of X
for W being Element of D ex W9 being Element of X st (proj D) . W9 = W
proof
let X be non empty set ; ::_thesis: for D being non empty a_partition of X
for W being Element of D ex W9 being Element of X st (proj D) . W9 = W
let D be non empty a_partition of X; ::_thesis: for W being Element of D ex W9 being Element of X st (proj D) . W9 = W
let W be Element of D; ::_thesis: ex W9 being Element of X st (proj D) . W9 = W
reconsider p = W as Subset of X ;
p <> {} by Def4;
then consider W9 being Element of X such that
A1: W9 in p by SUBSET_1:4;
take W9 ; ::_thesis: (proj D) . W9 = W
thus (proj D) . W9 = W by A1, Th65; ::_thesis: verum
end;
theorem :: EQREL_1:69
for X being non empty set
for D being non empty a_partition of X
for W being Subset of X st ( for B being Subset of X st B in D & B meets W holds
B c= W ) holds
W = (proj D) " ((proj D) .: W)
proof
let X be non empty set ; ::_thesis: for D being non empty a_partition of X
for W being Subset of X st ( for B being Subset of X st B in D & B meets W holds
B c= W ) holds
W = (proj D) " ((proj D) .: W)
let D be non empty a_partition of X; ::_thesis: for W being Subset of X st ( for B being Subset of X st B in D & B meets W holds
B c= W ) holds
W = (proj D) " ((proj D) .: W)
let W be Subset of X; ::_thesis: ( ( for B being Subset of X st B in D & B meets W holds
B c= W ) implies W = (proj D) " ((proj D) .: W) )
assume A1: for B being Subset of X st B in D & B meets W holds
B c= W ; ::_thesis: W = (proj D) " ((proj D) .: W)
W c= X ;
then W c= dom (proj D) by FUNCT_2:def_1;
hence W c= (proj D) " ((proj D) .: W) by FUNCT_1:76; :: according to XBOOLE_0:def_10 ::_thesis: (proj D) " ((proj D) .: W) c= W
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in (proj D) " ((proj D) .: W) or e in W )
assume A2: e in (proj D) " ((proj D) .: W) ; ::_thesis: e in W
then reconsider d = e as Element of X ;
(proj D) . e in (proj D) .: W by A2, FUNCT_1:def_7;
then consider c being Element of X such that
A3: c in W and
A4: (proj D) . d = (proj D) . c by FUNCT_2:65;
reconsider B = (proj D) . c as Subset of X by TARSKI:def_3;
c in (proj D) . c by Def9;
then B meets W by A3, XBOOLE_0:3;
then A5: B c= W by A1;
d in B by A4, Def9;
hence e in W by A5; ::_thesis: verum
end;
theorem :: EQREL_1:70
for X being set
for P being a_partition of X
for x, a, b being set st x in a & a in P & x in b & b in P holds
a = b
proof
let X be set ; ::_thesis: for P being a_partition of X
for x, a, b being set st x in a & a in P & x in b & b in P holds
a = b
let P be a_partition of X; ::_thesis: for x, a, b being set st x in a & a in P & x in b & b in P holds
a = b
let x, a, b be set ; ::_thesis: ( x in a & a in P & x in b & b in P implies a = b )
assume that
A1: x in a and
A2: a in P and
A3: x in b and
A4: b in P ; ::_thesis: a = b
a meets b by A1, A3, XBOOLE_0:3;
hence a = b by A2, A4, Def4; ::_thesis: verum
end;