let S be Language; R5 S is Correct
now set f =
R5 S;
set R =
P5 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 (R5 S) . X is S -correct )assume B0:
X is
S -correct
;
(R5 S) . X is S -correct now let 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 (R5 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 (R5 S) . X holds
1 = I -TruthEval psilet x be
I -satisfied set ;
for psi being wff string of S st [x,psi] in (R5 S) . X holds
1 = I -TruthEval psilet psi be
wff string of
S;
( [x,psi] in (R5 S) . X implies 1 = I -TruthEval psi )set s =
[x,psi];
CC0:
(
([x,psi] `1) \+\ x = {} &
([x,psi] `2) \+\ psi = {} )
;
then C0:
(
dom (P5 S) c= bool (S -sequents) &
[x,psi] `1 = x &
[x,psi] `2 = psi )
by FOMODEL0:29;
assume DD1:
[x,psi] in (R5 S) . X
;
1 = I -TruthEval psithen D1:
(
[x,psi] in S -sequents &
[X,[x,psi]] in P5 S )
by Lm1e;
then
X in dom (P5 S)
by RELAT_1:def 4;
then reconsider Seqts =
X as
S -correct Subset of
(S -sequents) by B0;
reconsider seqt =
[x,psi] as
Element of
S -sequents by DD1, Lm1e;
seqt Rule5 Seqts
by D1, DefP5;
then consider v1,
v2 being
literal Element of
S,
y being
set ,
p being
FinSequence such that D2:
(
seqt `1 = y \/ {(<*v1*> ^ p)} & not
v2 is
(y \/ {p}) \/ {(seqt `2)} -occurring &
[(y \/ {((v1 SubstWith v2) . p)}),(seqt `2)] in Seqts )
by Def5;
{(<*v1*> ^ p)} null y c= AllFormulasOf S
by D2, DefPremLike;
then
<*v1*> ^ p in AllFormulasOf S
by ZFMISC_1:31;
then reconsider phi1 =
<*v1*> ^ p as
wff string of
S ;
v1 \+\ (phi1 . 1) = {}
;
then D3:
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}) ;
D5:
phi1 =
(<*v1*> ^ phi) ^ (tail phi1)
by D3, FOMODEL2:23
.=
<*v1*> ^ phi
;
then D4:
phi = p
by FOMODEL0:41;
then D10:
( not
v2 is
Psi null ((y \/ {phi}) \/ {psi}) -occurring & not
v2 is
Phi null ((y \/ {phi}) \/ {psi}) -occurring & not
v2 is
yyy null ((y \/ {phi}) \/ {psi}) -occurring )
by D2, C0;
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 D2, CC0, FOMODEL0:29;
z = {phi1}
;
then
I -TruthEval phi1 = 1
by FOMODEL2:27;
then consider u being
Element of
U such that D6:
1
= ((v1,u) ReassignIn I) -TruthEval phi
by D5, FOMODEL2:19;
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 D10, FOMODEL2:28;
then
I2 -TruthEval phi2 = 1
by D6, FOMODEL3:9;
then reconsider z2 =
{phi2} as
I2 -satisfied set by FOMODEL2:27;
not
v2 in rng psi
by D10, FOMODEL2:28;
then
{v2} misses rng psi
by ZFMISC_1:50;
then D8:
dom (v2 .--> ({} .--> u)) misses rng psi
by FUNCOP_1:13;
I2 | (rng psi) =
(I | (rng psi)) +* ((v2 .--> ({} .--> u)) | (rng psi))
by FUNCT_4:71
.=
(I | (rng psi)) null {}
by D8, RELAT_1:66
;
then D9:
I | ((rng psi) /\ (OwnSymbolsOf S)) =
(I2 | (rng psi)) | (OwnSymbolsOf S)
by RELAT_1:71
.=
I2 | ((rng psi) /\ (OwnSymbolsOf S))
by RELAT_1:71
;
( not
v2 is
yyy -occurring &
yy is
I -satisfied )
by D4, D2, C0;
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 D2, D4, C0, FOMODEL0:def 23;
hence 1 =
I2 -TruthEval psi
by FOMODEL2:def 44
.=
I -TruthEval psi
by D9, FOMODEL3:13
;
verum end; hence
(R5 S) . X is
S -correct
by FOMODEL2:def 44;
verum end;
hence
R5 S is Correct
by RuleCorr; verum