let Z be set ; for S being Language
for D being RuleSet of S
for X being functional set
for num being sequence of (ExFormulasOf S) st D is isotone & R#1 S in D & R#8 S in D & R#2 S in D & R#5 S in D & (LettersOf S) \ (SymbolsOf (X /\ (((AllSymbolsOf S) *) \ {{}}))) is infinite & X addw (D,num) c= Z & Z is D -consistent & rng num = ExFormulasOf S holds
Z is S -witnessed
let S be Language; for D being RuleSet of S
for X being functional set
for num being sequence of (ExFormulasOf S) st D is isotone & R#1 S in D & R#8 S in D & R#2 S in D & R#5 S in D & (LettersOf S) \ (SymbolsOf (X /\ (((AllSymbolsOf S) *) \ {{}}))) is infinite & X addw (D,num) c= Z & Z is D -consistent & rng num = ExFormulasOf S holds
Z is S -witnessed
let D be RuleSet of S; for X being functional set
for num being sequence of (ExFormulasOf S) st D is isotone & R#1 S in D & R#8 S in D & R#2 S in D & R#5 S in D & (LettersOf S) \ (SymbolsOf (X /\ (((AllSymbolsOf S) *) \ {{}}))) is infinite & X addw (D,num) c= Z & Z is D -consistent & rng num = ExFormulasOf S holds
Z is S -witnessed
let X be functional set ; for num being sequence of (ExFormulasOf S) st D is isotone & R#1 S in D & R#8 S in D & R#2 S in D & R#5 S in D & (LettersOf S) \ (SymbolsOf (X /\ (((AllSymbolsOf S) *) \ {{}}))) is infinite & X addw (D,num) c= Z & Z is D -consistent & rng num = ExFormulasOf S holds
Z is S -witnessed
set L = LettersOf S;
set F = S -firstChar ;
set EF = ExFormulasOf S;
let num be sequence of (ExFormulasOf S); ( D is isotone & R#1 S in D & R#8 S in D & R#2 S in D & R#5 S in D & (LettersOf S) \ (SymbolsOf (X /\ (((AllSymbolsOf S) *) \ {{}}))) is infinite & X addw (D,num) c= Z & Z is D -consistent & rng num = ExFormulasOf S implies Z is S -witnessed )
set f = (D,num) addw X;
set Y = X addw (D,num);
set SS = AllSymbolsOf S;
X \ (X addw (D,num)) = {}
;
then A1:
X c= X addw (D,num)
by XBOOLE_1:37;
assume A2:
( D is isotone & R#1 S in D & R#8 S in D & R#2 S in D & R#5 S in D & (LettersOf S) \ (SymbolsOf (X /\ (((AllSymbolsOf S) *) \ {{}}))) is infinite )
; ( not X addw (D,num) c= Z or not Z is D -consistent or not rng num = ExFormulasOf S or Z is S -witnessed )
assume A3:
( X addw (D,num) c= Z & Z is D -consistent )
; ( not rng num = ExFormulasOf S or Z is S -witnessed )
then
( X c= Z & Z is D -consistent )
by A1, XBOOLE_1:1;
then A4:
X is D -consistent
;
assume A5:
rng num = ExFormulasOf S
; Z is S -witnessed
set strings = ((AllSymbolsOf S) *) \ {{}};
for l1 being literal Element of S
for phi1 being wff string of S st <*l1*> ^ phi1 in Z holds
ex l2 being literal Element of S st
( (l1,l2) -SymbolSubstIn phi1 in Z & not l2 in rng phi1 )
proof
let l1 be
literal Element of
S;
for phi1 being wff string of S st <*l1*> ^ phi1 in Z holds
ex l2 being literal Element of S st
( (l1,l2) -SymbolSubstIn phi1 in Z & not l2 in rng phi1 )let phi1 be
wff string of
S;
( <*l1*> ^ phi1 in Z implies ex l2 being literal Element of S st
( (l1,l2) -SymbolSubstIn phi1 in Z & not l2 in rng phi1 ) )
set phi =
<*l1*> ^ phi1;
(
<*l1*> ^ phi1 = (<*l1*> ^ phi1) ^ {} & not
<*l1*> ^ phi1 is
0wff )
;
then A6:
(
l1 = (S -firstChar) . (<*l1*> ^ phi1) &
phi1 = head (<*l1*> ^ phi1) )
by FOMODEL2:23;
<*l1*> ^ phi1 in ExFormulasOf S
;
then reconsider phii =
<*l1*> ^ phi1 as
Element of
ExFormulasOf S ;
consider x being
object such that A7:
(
x in dom num &
num . x = phii )
by A5, FUNCT_1:def 3;
reconsider mm =
x as
Element of
NAT by A7;
reconsider MM =
mm + 1 as
Element of
NAT by ORDINAL1:def 12;
reconsider Xm =
((D,num) addw X) . mm as
functional set ;
set no =
SymbolsOf ((((AllSymbolsOf S) *) \ {{}}) /\ ((((D,num) addw X) . mm) \/ {phi1}));
reconsider T =
(((AllSymbolsOf S) *) \ {{}}) /\ {phi1} as
finite FinSequence-membered Subset of
{phi1} ;
reconsider t =
SymbolsOf T as
finite set ;
reconsider i =
(LettersOf S) \ (SymbolsOf ((((D,num) addw X) . mm) /\ (((AllSymbolsOf S) *) \ {{}}))) as
infinite Subset of
(LettersOf S) by Th17, A2, A4;
A8:
SymbolsOf ((((AllSymbolsOf S) *) \ {{}}) /\ ((((D,num) addw X) . mm) \/ {phi1})) =
SymbolsOf (((((AllSymbolsOf S) *) \ {{}}) /\ (((D,num) addw X) . mm)) \/ ((((AllSymbolsOf S) *) \ {{}}) /\ {phi1}))
by XBOOLE_1:23
.=
(SymbolsOf ((((AllSymbolsOf S) *) \ {{}}) /\ (((D,num) addw X) . mm))) \/ (SymbolsOf T)
by FOMODEL0:47
;
then
(LettersOf S) \ (SymbolsOf ((((AllSymbolsOf S) *) \ {{}}) /\ ((((D,num) addw X) . mm) \/ {phi1}))) = i \ t
by XBOOLE_1:41;
then reconsider yes =
(LettersOf S) \ (SymbolsOf ((((AllSymbolsOf S) *) \ {{}}) /\ ((((D,num) addw X) . mm) \/ {phi1}))) as non
empty Subset of
(LettersOf S) ;
set ll2 = the
Element of
yes;
reconsider l2 = the
Element of
yes as
literal Element of
S by TARSKI:def 3;
set psi1 = (
l1,
l2)
-SymbolSubstIn phi1;
dom ((D,num) addw X) = NAT
by FUNCT_2:def 1;
then A9:
(
((D,num) addw X) . mm in rng ((D,num) addw X) &
((D,num) addw X) . MM in rng ((D,num) addw X) )
by FUNCT_1:def 3;
then
((D,num) addw X) . mm c= X addw (
D,
num)
by ZFMISC_1:74;
then A10:
((D,num) addw X) . mm c= Z
by A3, XBOOLE_1:1;
assume
<*l1*> ^ phi1 in Z
;
ex l2 being literal Element of S st
( (l1,l2) -SymbolSubstIn phi1 in Z & not l2 in rng phi1 )
then
{(<*l1*> ^ phi1)} c= Z
by ZFMISC_1:31;
then
(((D,num) addw X) . mm) \/ {(<*l1*> ^ phi1)} c= Z
by A10, XBOOLE_1:8;
then
(((D,num) addw X) . mm) \/ {(<*l1*> ^ phi1)} is
D -consistent
by A3;
then (((D,num) addw X) . mm) \/ {((l1,l2) -SymbolSubstIn phi1)} =
(
D,
phii)
AddAsWitnessTo (((D,num) addw X) . mm)
by Def66, A6
.=
((D,num) addw X) . (mm + 1)
by Def71, A7
;
then
{((l1,l2) -SymbolSubstIn phi1)} null (((D,num) addw X) . mm) c= ((D,num) addw X) . MM
;
then
(
l1,
l2)
-SymbolSubstIn phi1 in ((D,num) addw X) . MM
by ZFMISC_1:31;
then A11:
(
l1,
l2)
-SymbolSubstIn phi1 in X addw (
D,
num)
by TARSKI:def 4, A9;
take
l2
;
( (l1,l2) -SymbolSubstIn phi1 in Z & not l2 in rng phi1 )
thus
(
l1,
l2)
-SymbolSubstIn phi1 in Z
by A3, A11;
not l2 in rng phi1
not
l2 in SymbolsOf ((((AllSymbolsOf S) *) \ {{}}) /\ ((((D,num) addw X) . mm) \/ {phi1}))
by XBOOLE_0:def 5;
then
not
l2 in SymbolsOf {phi1}
by A8, XBOOLE_0:def 3;
hence
not
l2 in rng phi1
by FOMODEL0:45;
verum
end;
hence
Z is S -witnessed
; verum