let Y be non empty set ; :: thesis: 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; :: thesis: 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; :: thesis: EqClass z,(PA '/\' PB) = (EqClass z,PA) /\ (EqClass z,PB)
A1:
EqClass z,(PA '/\' PB) c= (EqClass z,PA) /\ (EqClass z,PB)
proof
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x in EqClass z,(PA '/\' PB) or x in (EqClass z,PA) /\ (EqClass z,PB) )
assume A2:
x in EqClass z,
(PA '/\' PB)
;
:: thesis: x in (EqClass z,PA) /\ (EqClass z,PB)
A3:
EqClass z,
(PA '/\' PB) c= EqClass z,
PA
by BVFUNC11:3;
EqClass z,
(PA '/\' PB) c= EqClass z,
PB
by BVFUNC11:3;
hence
x in (EqClass z,PA) /\ (EqClass z,PB)
by A2, A3, XBOOLE_0:def 4;
:: thesis: verum
end;
(EqClass z,PA) /\ (EqClass z,PB) c= EqClass z,(PA '/\' PB)
proof
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x in (EqClass z,PA) /\ (EqClass z,PB) or x in EqClass z,(PA '/\' PB) )
assume A4:
x in (EqClass z,PA) /\ (EqClass z,PB)
;
:: thesis: x in EqClass z,(PA '/\' PB)
then reconsider x =
x as
Element of
Y ;
A5:
(
x in EqClass z,
PA &
x in EqClass z,
PB )
by A4, XBOOLE_0:def 4;
A6:
(
x in EqClass x,
PA &
EqClass x,
PA in PA )
by EQREL_1:def 8;
A7:
(
x in EqClass x,
PB &
EqClass x,
PB in PB )
by EQREL_1:def 8;
A8:
EqClass x,
PA meets EqClass z,
PA
by A5, A6, XBOOLE_0:3;
A9:
EqClass x,
PB meets EqClass z,
PB
by A5, A7, XBOOLE_0:3;
A10:
(
z in EqClass z,
PA &
EqClass z,
PA in PA )
by EQREL_1:def 8;
A11:
(
z in EqClass z,
PB &
EqClass z,
PB in PB )
by EQREL_1:def 8;
A12:
PA '/\' PB = (INTERSECTION PA,PB) \ {{} }
by PARTIT1:def 4;
set Z =
EqClass z,
(PA '/\' PB);
(
EqClass z,
(PA '/\' PB) in INTERSECTION PA,
PB & not
EqClass z,
(PA '/\' PB) in {{} } )
by A12, XBOOLE_0:def 5;
then consider X,
Y being
set such that A13:
(
X in PA &
Y in PB &
EqClass z,
(PA '/\' PB) = X /\ Y )
by SETFAM_1:def 5;
z in X /\ Y
by A13, EQREL_1:def 8;
then A14:
(
z in X &
z in Y )
by XBOOLE_0:def 4;
then
X meets EqClass z,
PA
by A10, XBOOLE_0:3;
then A15:
X = EqClass z,
PA
by A13, EQREL_1:def 6;
Y meets EqClass z,
PB
by A11, A14, XBOOLE_0:3;
then A16:
Y = EqClass z,
PB
by A13, EQREL_1:def 6;
A17:
X = EqClass x,
PA
by A8, A15, EQREL_1:50;
x in (EqClass x,PA) /\ (EqClass x,PB)
by A6, A7, XBOOLE_0:def 4;
hence
x in EqClass z,
(PA '/\' PB)
by A9, A13, A16, A17, EQREL_1:50;
:: thesis: verum
end;
hence
EqClass z,(PA '/\' PB) = (EqClass z,PA) /\ (EqClass z,PB)
by A1, XBOOLE_0:def 10; :: thesis: verum