let S be Language; R#5 S is Correct
now for X being set st X is S -correct holds
(R#5 S) . X is S -correct set f =
R#5 S;
set R =
P#5 S;
set Q =
S -sequents ;
set E =
TheEqSymbOf S;
set N =
TheNorSymbOf S;
set FF =
AllFormulasOf S;
set TT =
AllTermsOf S;
set SS =
AllSymbolsOf S;
set F =
S -firstChar ;
set O =
OwnSymbolsOf S;
let X be
set ;
( X is S -correct implies (R#5 S) . X is S -correct )assume A1:
X is
S -correct
;
(R#5 S) . X is S -correct now for U being non empty set
for I being Element of U -InterpretersOf S
for x being b2 -satisfied set
for psi being wff string of S st [x,psi] in (R#5 S) . X holds
1 = I -TruthEval psilet U be non
empty set ;
for I being Element of U -InterpretersOf S
for x being b1 -satisfied set
for psi being wff string of S st [x,psi] in (R#5 S) . X holds
1 = I -TruthEval psiset II =
U -InterpretersOf S;
let I be
Element of
U -InterpretersOf S;
for x being I -satisfied set
for psi being wff string of S st [x,psi] in (R#5 S) . X holds
1 = I -TruthEval psilet x be
I -satisfied set ;
for psi being wff string of S st [x,psi] in (R#5 S) . X holds
1 = I -TruthEval psilet psi be
wff string of
S;
( [x,psi] in (R#5 S) . X implies 1 = I -TruthEval psi )set s =
[x,psi];
assume A4:
[x,psi] in (R#5 S) . X
;
1 = I -TruthEval psithen A5:
(
[x,psi] in S -sequents &
[X,[x,psi]] in P#5 S )
by Lm30;
then
X in dom (P#5 S)
by XTUPLE_0:def 12;
then reconsider Seqts =
X as
S -correct Subset of
(S -sequents) by A1;
reconsider seqt =
[x,psi] as
Element of
S -sequents by A4, Lm30;
seqt Rule5 Seqts
by A5, Def42;
then consider v1,
v2 being
literal Element of
S,
y being
set ,
p being
FinSequence such that A6:
(
seqt `1 = y \/ {(<*v1*> ^ p)} &
v2 is
(y \/ {p}) \/ {(seqt `2)} -absent &
[(y \/ {((v1 SubstWith v2) . p)}),(seqt `2)] in Seqts )
;
{(<*v1*> ^ p)} null y c= AllFormulasOf S
by A6, Def4;
then
<*v1*> ^ p in AllFormulasOf S
by ZFMISC_1:31;
then reconsider phi1 =
<*v1*> ^ p as
wff string of
S ;
v1 \+\ (phi1 . 1) = {}
;
then A7:
v1 =
phi1 . 1
by FOMODEL0:29
.=
(S -firstChar) . phi1
by FOMODEL0:6
;
then reconsider phi1 =
phi1 as non
0wff wff exal string of
S by FOMODEL2:def 32;
reconsider phi =
head phi1 as
wff string of
S ;
{psi} null (y \/ {phi}) = {psi}
;
then reconsider Psi =
{psi} as non
empty Subset of
((y \/ {phi}) \/ {psi}) ;
{phi} null (y \/ {psi}) is
Subset of
((y \/ {phi}) \/ {psi})
by XBOOLE_1:4;
then reconsider Phi =
{phi} as non
empty Subset of
((y \/ {phi}) \/ {psi}) ;
y \/ ({phi} \/ {psi}) = (y \/ {phi}) \/ {psi}
by XBOOLE_1:4;
then
y null ({phi} \/ {psi}) c= (y \/ {phi}) \/ {psi}
;
then reconsider yyy =
y as
Subset of
((y \/ {phi}) \/ {psi}) ;
A8:
phi1 =
(<*v1*> ^ phi) ^ (tail phi1)
by A7, FOMODEL2:23
.=
<*v1*> ^ phi
;
then A9:
phi = p
by FOMODEL0:41;
then A10:
(
v2 is
Psi null ((y \/ {phi}) \/ {psi}) -absent &
v2 is
Phi null ((y \/ {phi}) \/ {psi}) -absent &
v2 is
yyy null ((y \/ {phi}) \/ {psi}) -absent )
by A6;
reconsider phi2 = (
v1,
v2)
-SymbolSubstIn phi as
wff string of
S ;
reconsider yy =
y null {phi1},
z =
{phi1} null y as
I -satisfied Subset of
x by A6;
z = {phi1}
;
then
I -TruthEval phi1 = 1
by FOMODEL2:27;
then consider u being
Element of
U such that A11:
1
= ((v1,u) ReassignIn I) -TruthEval phi
by FOMODEL2:19, A8;
set f2 =
v2 .--> ({} .--> u);
reconsider I1 = (
v1,
u)
ReassignIn I,
I2 = (
v2,
u)
ReassignIn I as
Element of
U -InterpretersOf S ;
not
v2 in rng phi
by A10, FOMODEL2:28;
then
I2 -TruthEval phi2 = 1
by A11, FOMODEL3:9;
then reconsider z2 =
{phi2} as
I2 -satisfied set by FOMODEL2:27;
{v2} misses rng psi
by ZFMISC_1:50, A10, FOMODEL2:28;
then A12:
dom (v2 .--> ({} .--> u)) misses rng psi
;
I2 | (rng psi) =
(I | (rng psi)) +* ((v2 .--> ({} .--> u)) | (rng psi))
by FUNCT_4:71
.=
(I | (rng psi)) null {}
by A12, RELAT_1:66
;
then A13:
I | ((rng psi) /\ (OwnSymbolsOf S)) =
(I2 | (rng psi)) | (OwnSymbolsOf S)
by RELAT_1:71
.=
I2 | ((rng psi) /\ (OwnSymbolsOf S))
by RELAT_1:71
;
(
v2 is
yyy -absent &
yy is
I -satisfied )
by A9, A6;
then reconsider yyyy =
yyy as
I2 -satisfied Subset of
x by FOMODEL3:14;
reconsider zz =
yyyy \/ z2 as
I2 -satisfied set ;
[zz,psi] in Seqts
by A6, A9, FOMODEL0:def 22;
hence 1 =
I2 -TruthEval psi
by FOMODEL2:def 44
.=
I -TruthEval psi
by A13, FOMODEL3:13
;
verum end; hence
(R#5 S) . X is
S -correct
;
verum end;
hence
R#5 S is Correct
; verum