let Z be set ; for S being Language
for D being RuleSet of S
for X being functional set
for num being Function of NAT,(ExFormulasOf S) st D is isotone & R1 S in D & R8 S in D & R2 S in D & R5 S in D & not (LettersOf S) \ (SymbolsOf (X /\ (((AllSymbolsOf S) *) \ {{}}))) is finite & X addw (D,num) c= Z & not Z is D -inconsistent & 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 Function of NAT,(ExFormulasOf S) st D is isotone & R1 S in D & R8 S in D & R2 S in D & R5 S in D & not (LettersOf S) \ (SymbolsOf (X /\ (((AllSymbolsOf S) *) \ {{}}))) is finite & X addw (D,num) c= Z & not Z is D -inconsistent & rng num = ExFormulasOf S holds
Z is S -witnessed
let D be RuleSet of S; for X being functional set
for num being Function of NAT,(ExFormulasOf S) st D is isotone & R1 S in D & R8 S in D & R2 S in D & R5 S in D & not (LettersOf S) \ (SymbolsOf (X /\ (((AllSymbolsOf S) *) \ {{}}))) is finite & X addw (D,num) c= Z & not Z is D -inconsistent & rng num = ExFormulasOf S holds
Z is S -witnessed
let X be functional set ; for num being Function of NAT,(ExFormulasOf S) st D is isotone & R1 S in D & R8 S in D & R2 S in D & R5 S in D & not (LettersOf S) \ (SymbolsOf (X /\ (((AllSymbolsOf S) *) \ {{}}))) is finite & X addw (D,num) c= Z & not Z is D -inconsistent & rng num = ExFormulasOf S holds
Z is S -witnessed
set L = LettersOf S;
set F = S -firstChar ;
set EF = ExFormulasOf S;
let num be Function of NAT,(ExFormulasOf S); ( D is isotone & R1 S in D & R8 S in D & R2 S in D & R5 S in D & not (LettersOf S) \ (SymbolsOf (X /\ (((AllSymbolsOf S) *) \ {{}}))) is finite & X addw (D,num) c= Z & not Z is D -inconsistent & 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 B9:
X c= X addw (D,num)
by XBOOLE_1:37;
assume B8:
( D is isotone & R1 S in D & R8 S in D & R2 S in D & R5 S in D & not (LettersOf S) \ (SymbolsOf (X /\ (((AllSymbolsOf S) *) \ {{}}))) is finite )
; ( not X addw (D,num) c= Z or Z is D -inconsistent or not rng num = ExFormulasOf S or Z is S -witnessed )
assume B0:
( X addw (D,num) c= Z & not Z is D -inconsistent )
; ( not rng num = ExFormulasOf S or Z is S -witnessed )
then
( X c= Z & not Z is D -inconsistent )
by B9, XBOOLE_1:1;
then B20:
not X is D -inconsistent
by Th16;
assume B1:
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 B3:
(
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
set such that C0:
(
x in dom num &
num . x = phii )
by B1, FUNCT_1:def 3;
reconsider mm =
x as
Element of
NAT by C0;
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 Th18, B8, B20;
B6:
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 B4:
(
((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 B5:
((D,num) addw X) . mm c= Z
by B0, 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 B5, XBOOLE_1:8;
then
not
(((D,num) addw X) . mm) \/ {(<*l1*> ^ phi1)} is
D -inconsistent
by B0, Th16;
then (((D,num) addw X) . mm) \/ {((l1,l2) -SymbolSubstIn phi1)} =
(
D,
phii)
AddAsWitnessTo (((D,num) addw X) . mm)
by DefWit2, B3
.=
((D,num) addw X) . (mm + 1)
by DefWit3, C0
;
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 B7:
(
l1,
l2)
-SymbolSubstIn phi1 in X addw (
D,
num)
by B4, TARSKI:def 4;
take
l2
;
( (l1,l2) -SymbolSubstIn phi1 in Z & not l2 in rng phi1 )
thus
(
l1,
l2)
-SymbolSubstIn phi1 in Z
by B0, B7;
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 B6, XBOOLE_0:def 3;
hence
not
l2 in rng phi1
by FOMODEL0:45;
verum
end;
hence
Z is S -witnessed
by DefWit1; verum