let V, C be set ; for A, B being Element of SubstitutionSet (V,C) st ( for a being set st a in A holds
ex b being set st
( b in B & b c= a ) ) holds
mi (A ^ B) = A
let A, B be Element of SubstitutionSet (V,C); ( ( for a being set st a in A holds
ex b being set st
( b in B & b c= a ) ) implies mi (A ^ B) = A )
assume A1:
for a being set st a in A holds
ex b being set st
( b in B & b c= a )
; mi (A ^ B) = A
A2:
mi (A ^ B) c= A ^ B
by SUBSTLAT:8;
thus
mi (A ^ B) c= A
XBOOLE_0:def 10 A c= mi (A ^ B)proof
let a be
object ;
TARSKI:def 3 ( not a in mi (A ^ B) or a in A )
reconsider aa =
a as
set by TARSKI:1;
A3:
A c= PFuncs (
V,
C)
by FINSUB_1:def 5;
assume A4:
a in mi (A ^ B)
;
a in A
then consider b,
c being
set such that A5:
b in A
and
c in B
and A6:
a = b \/ c
by A2, SUBSTLAT:15;
A7:
b c= aa
by A6, XBOOLE_1:7;
consider b1 being
set such that A8:
b1 in B
and A9:
b1 c= b
by A1, A5;
B c= PFuncs (
V,
C)
by FINSUB_1:def 5;
then reconsider b9 =
b,
b19 =
b1 as
Element of
PFuncs (
V,
C)
by A5, A8, A3;
A10:
b = b1 \/ b
by A9, XBOOLE_1:12;
b19 tolerates b9
by A9, PARTFUN1:54;
then
b in A ^ B
by A5, A8, A10, SUBSTLAT:16;
hence
a in A
by A4, A5, A7, SUBSTLAT:6;
verum
end;
thus
A c= mi (A ^ B)
verumproof
let a be
object ;
TARSKI:def 3 ( not a in A or a in mi (A ^ B) )
reconsider aa =
a as
set by TARSKI:1;
A11:
A c= PFuncs (
V,
C)
by FINSUB_1:def 5;
assume A12:
a in A
;
a in mi (A ^ B)
then consider b being
set such that A13:
b in B
and A14:
b c= aa
by A1;
B c= PFuncs (
V,
C)
by FINSUB_1:def 5;
then reconsider a9 =
a,
b9 =
b as
Element of
PFuncs (
V,
C)
by A12, A13, A11;
A15:
a9 tolerates b9
by A14, PARTFUN1:54;
A16:
a in mi A
by A12, SUBSTLAT:11;
A17:
for
b being
finite set st
b in A ^ B &
b c= aa holds
b = a
a9 = a9 \/ b9
by A14, XBOOLE_1:12;
then A22:
a9 in A ^ B
by A12, A13, A15, SUBSTLAT:16;
aa is
finite
by A12, Th1;
hence
a in mi (A ^ B)
by A22, A17, SUBSTLAT:7;
verum
end;