let V be set ; :: thesis: for C being finite set
for u being Element of (SubstLatt (V,C))
for a being Element of PFuncs (V,C)
for K being Element of Fin (PFuncs (V,C)) st K = {a} holds
ex v being Element of SubstitutionSet (V,C) st
( v in SUB u & v ^ K = {} & ( for b being Element of PFuncs (V,C) st b in (diff u) . v holds
b tolerates a ) )
let C be finite set ; :: thesis: for u being Element of (SubstLatt (V,C))
for a being Element of PFuncs (V,C)
for K being Element of Fin (PFuncs (V,C)) st K = {a} holds
ex v being Element of SubstitutionSet (V,C) st
( v in SUB u & v ^ K = {} & ( for b being Element of PFuncs (V,C) st b in (diff u) . v holds
b tolerates a ) )
let u be Element of (SubstLatt (V,C)); :: thesis: for a being Element of PFuncs (V,C)
for K being Element of Fin (PFuncs (V,C)) st K = {a} holds
ex v being Element of SubstitutionSet (V,C) st
( v in SUB u & v ^ K = {} & ( for b being Element of PFuncs (V,C) st b in (diff u) . v holds
b tolerates a ) )
let a be Element of PFuncs (V,C); :: thesis: for K being Element of Fin (PFuncs (V,C)) st K = {a} holds
ex v being Element of SubstitutionSet (V,C) st
( v in SUB u & v ^ K = {} & ( for b being Element of PFuncs (V,C) st b in (diff u) . v holds
b tolerates a ) )
deffunc H1( set ) -> set = $1;
let K be Element of Fin (PFuncs (V,C)); :: thesis: ( K = {a} implies ex v being Element of SubstitutionSet (V,C) st
( v in SUB u & v ^ K = {} & ( for b being Element of PFuncs (V,C) st b in (diff u) . v holds
b tolerates a ) ) )
assume A1: K = {a} ; :: thesis: ex v being Element of SubstitutionSet (V,C) st
( v in SUB u & v ^ K = {} & ( for b being Element of PFuncs (V,C) st b in (diff u) . v holds
b tolerates a ) )
deffunc H2( Element of PFuncs (V,C), Element of PFuncs (V,C)) -> set = $1 \/ $2;
defpred S1[ Element of PFuncs (V,C)] means ( not $1 tolerates a & $1 in u & $1 tolerates a );
deffunc H3( Element of PFuncs (V,C), Element of PFuncs (V,C)) -> set = $1 \/ $2;
defpred S2[ Element of PFuncs (V,C)] means ( $1 is finite & not $1 tolerates a );
set M = { H1(s) where s is Element of PFuncs (V,C) : ( H1(s) in u & S2[s] ) } ;
defpred S3[ Element of PFuncs (V,C), Element of PFuncs (V,C)] means ( $1 in { H1(s) where s is Element of PFuncs (V,C) : ( H1(s) in u & S2[s] ) } & $2 in {a} & $1 tolerates $2 );
defpred S4[ Element of PFuncs (V,C), Element of PFuncs (V,C)] means ( $2 = a & $1 in { H1(s) where s is Element of PFuncs (V,C) : ( H1(s) in u & S2[s] ) } & $1 tolerates $2 );
defpred S5[ Element of PFuncs (V,C)] means ( $1 in { H1(s) where s is Element of PFuncs (V,C) : ( H1(s) in u & S2[s] ) } & $1 tolerates a );
defpred S6[ Element of PFuncs (V,C), Element of PFuncs (V,C)] means ( $1 in { H1(s) where s is Element of PFuncs (V,C) : ( H1(s) in u & S2[s] ) } & $1 tolerates $2 );
deffunc H4( Element of PFuncs (V,C)) -> set = $1 \/ a;
A2: { H1(s) where s is Element of PFuncs (V,C) : ( H1(s) in u & S2[s] ) } c= u from FRAENKEL:sch 17();
 then reconsider v = { H1(s) where s is Element of PFuncs (V,C) : ( H1(s) in u & S2[s] ) } as Element of (SubstLatt (V,C)) by Th17;
reconsider v = v as Element of SubstitutionSet (V,C) by SUBSTLAT:def 4;
take v ; :: thesis: ( v in SUB u & v ^ K = {} & ( for b being Element of PFuncs (V,C) st b in (diff u) . v holds
b tolerates a ) )
thus v in SUB u by A2; :: thesis: ( v ^ K = {} & ( for b being Element of PFuncs (V,C) st b in (diff u) . v holds
b tolerates a ) )
A3: for s, t being Element of PFuncs (V,C) holds
( S3[s,t] iff S4[s,t] ) by TARSKI:def 1;
A4: { H3(s,t) where s, t is Element of PFuncs (V,C) : S3[s,t] } = { H3(s9,t9) where s9, t9 is Element of PFuncs (V,C) : S4[s9,t9] } from FRAENKEL:sch 4(A3);
 for s being Element of PFuncs (V,C) holds
( s in { H1(s) where s is Element of PFuncs (V,C) : ( H1(s) in u & S2[s] ) } iff ( s is finite & not s tolerates a & s in u ) )
proof
let s be Element of PFuncs (V,C); :: thesis: ( s in { H1(s) where s is Element of PFuncs (V,C) : ( H1(s) in u & S2[s] ) } iff ( s is finite & not s tolerates a & s in u ) )
thus ( s in { H1(s) where s is Element of PFuncs (V,C) : ( H1(s) in u & S2[s] ) } implies ( s is finite & not s tolerates a & s in u ) ) :: thesis: ( s is finite & not s tolerates a & s in u implies s in { H1(s) where s is Element of PFuncs (V,C) : ( H1(s) in u & S2[s] ) } )
proof
assume s in { H1(s) where s is Element of PFuncs (V,C) : ( H1(s) in u & S2[s] ) } ; :: thesis: ( s is finite & not s tolerates a & s in u )
then ex s2 being Element of PFuncs (V,C) st
( s2 = s & s2 in u & s2 is finite & not s2 tolerates a ) ;
hence ( s is finite & not s tolerates a & s in u ) ; :: thesis: verum
end;
thus ( s is finite & not s tolerates a & s in u implies s in { H1(s) where s is Element of PFuncs (V,C) : ( H1(s) in u & S2[s] ) } ) ; :: thesis: verum
end;
then A5: for s being Element of PFuncs (V,C) holds
( S5[s] iff S1[s] ) ;
A6: { H4(s9) where s9 is Element of PFuncs (V,C) : S5[s9] } = { H4(s) where s is Element of PFuncs (V,C) : S1[s] } from FRAENKEL:sch 3(A5);
 { H2(s,t) where s, t is Element of PFuncs (V,C) : ( t = a & S6[s,t] ) } = { H2(s9,a) where s9 is Element of PFuncs (V,C) : S6[s9,a] } from FRAENKEL:sch 20();
 then A7: v ^ K = { (s \/ a) where s is Element of PFuncs (V,C) : ( not s tolerates a & s in u & s tolerates a ) } by A1, A4, A6, SUBSTLAT:def 3;
thus v ^ K = {} :: thesis: for b being Element of PFuncs (V,C) st b in (diff u) . v holds
b tolerates a
proof
assume v ^ K <> {} ; :: thesis: contradiction
then consider x being object such that
A8: x in v ^ K by XBOOLE_0:def 1;
ex s1 being Element of PFuncs (V,C) st
( x = s1 \/ a & not s1 tolerates a & s1 in u & s1 tolerates a ) by A7, A8;
hence contradiction ; :: thesis: verum
end;
let b be Element of PFuncs (V,C); :: thesis: ( b in (diff u) . v implies b tolerates a )
assume b in (diff u) . v ; :: thesis: b tolerates a
then A9: b in u \ v by Def7;
then A10: not b in { H1(s) where s is Element of PFuncs (V,C) : ( H1(s) in u & S2[s] ) } by XBOOLE_0:def 5;
u in the carrier of (SubstLatt (V,C)) ;
then u in SubstitutionSet (V,C) by SUBSTLAT:def 4;
then b is finite by A9, Th1;
hence b tolerates a by A9, A10; :: thesis: verum