let Y be non empty set ; for z being Element of Y
for PA, PB being a_partition of Y holds EqClass (z,(PA '/\' PB)) = (EqClass (z,PA)) /\ (EqClass (z,PB))
let z be Element of Y; for PA, PB being a_partition of Y holds EqClass (z,(PA '/\' PB)) = (EqClass (z,PA)) /\ (EqClass (z,PB))
let PA, PB be a_partition of Y; EqClass (z,(PA '/\' PB)) = (EqClass (z,PA)) /\ (EqClass (z,PB))
A1:
(EqClass (z,PA)) /\ (EqClass (z,PB)) c= EqClass (z,(PA '/\' PB))
proof
set Z =
EqClass (
z,
(PA '/\' PB));
let x be
object ;
TARSKI:def 3 ( not x in (EqClass (z,PA)) /\ (EqClass (z,PB)) or x in EqClass (z,(PA '/\' PB)) )
assume A2:
x in (EqClass (z,PA)) /\ (EqClass (z,PB))
;
x in EqClass (z,(PA '/\' PB))
then reconsider x =
x as
Element of
Y ;
A3:
x in EqClass (
x,
PA)
by EQREL_1:def 6;
x in EqClass (
z,
PA)
by A2, XBOOLE_0:def 4;
then A4:
EqClass (
x,
PA)
meets EqClass (
z,
PA)
by A3, XBOOLE_0:3;
A5:
x in EqClass (
x,
PB)
by EQREL_1:def 6;
PA '/\' PB = (INTERSECTION (PA,PB)) \ {{}}
by PARTIT1:def 4;
then
EqClass (
z,
(PA '/\' PB))
in INTERSECTION (
PA,
PB)
by XBOOLE_0:def 5;
then consider X,
Y being
set such that A6:
X in PA
and A7:
Y in PB
and A8:
EqClass (
z,
(PA '/\' PB))
= X /\ Y
by SETFAM_1:def 5;
A9:
z in X /\ Y
by A8, EQREL_1:def 6;
then
(
z in EqClass (
z,
PB) &
z in Y )
by EQREL_1:def 6, XBOOLE_0:def 4;
then
Y meets EqClass (
z,
PB)
by XBOOLE_0:3;
then A10:
Y = EqClass (
z,
PB)
by A7, EQREL_1:def 4;
x in EqClass (
z,
PB)
by A2, XBOOLE_0:def 4;
then A11:
EqClass (
x,
PB)
meets EqClass (
z,
PB)
by A5, XBOOLE_0:3;
(
z in EqClass (
z,
PA) &
z in X )
by A9, EQREL_1:def 6, XBOOLE_0:def 4;
then
X meets EqClass (
z,
PA)
by XBOOLE_0:3;
then
X = EqClass (
z,
PA)
by A6, EQREL_1:def 4;
then A12:
X = EqClass (
x,
PA)
by A4, EQREL_1:41;
x in (EqClass (x,PA)) /\ (EqClass (x,PB))
by A3, A5, XBOOLE_0:def 4;
hence
x in EqClass (
z,
(PA '/\' PB))
by A11, A8, A10, A12, EQREL_1:41;
verum
end;
EqClass (z,(PA '/\' PB)) c= (EqClass (z,PA)) /\ (EqClass (z,PB))
proof
let x be
object ;
TARSKI:def 3 ( not x in EqClass (z,(PA '/\' PB)) or x in (EqClass (z,PA)) /\ (EqClass (z,PB)) )
A13:
(
EqClass (
z,
(PA '/\' PB))
c= EqClass (
z,
PA) &
EqClass (
z,
(PA '/\' PB))
c= EqClass (
z,
PB) )
by BVFUNC11:3;
assume
x in EqClass (
z,
(PA '/\' PB))
;
x in (EqClass (z,PA)) /\ (EqClass (z,PB))
hence
x in (EqClass (z,PA)) /\ (EqClass (z,PB))
by A13, XBOOLE_0:def 4;
verum
end;
hence
EqClass (z,(PA '/\' PB)) = (EqClass (z,PA)) /\ (EqClass (z,PB))
by A1, XBOOLE_0:def 10; verum