let Z be set ; :: thesis: for S being countable Language
for phi being wff string of S st Z c= AllFormulasOf S & xnot phi is Z -implied holds
xnot phi is Z,S -rules -provable
let S be countable Language; :: thesis: for phi being wff string of S st Z c= AllFormulasOf S & xnot phi is Z -implied holds
xnot phi is Z,S -rules -provable
set D = S -rules ;
set FF = AllFormulasOf S;
let phi be wff string of S; :: thesis: ( Z c= AllFormulasOf S & xnot phi is Z -implied implies xnot phi is Z,S -rules -provable )
assume Z c= AllFormulasOf S ; :: thesis: ( not xnot phi is Z -implied or xnot phi is Z,S -rules -provable )
then reconsider X = Z as Subset of (AllFormulasOf S) ;
set psi = xnot phi;
phi in AllFormulasOf S by FOMODEL2:16;
then reconsider Phi = {phi} as non empty Subset of (AllFormulasOf S) by ZFMISC_1:31;
reconsider Y = X \/ Phi as non empty Subset of (AllFormulasOf S) ;
reconsider XX = X null Phi as Subset of Y ;
reconsider Phii = Phi null X as non empty Subset of Y ;
assume B2: xnot phi is Z -implied ; :: thesis: xnot phi is Z,S -rules -provable
assume not xnot phi is Z,S -rules -provable ; :: thesis: contradiction
then ( S -rules is isotone & R1 S in S -rules & R8 S in S -rules & not xnot phi is Z,S -rules -provable ) by DefRank;
then consider U being non empty set , I being Element of U -InterpretersOf S such that
B0: Y is I -satisfied by Th21, Lm2b;
(I -TruthEval (xnot phi)) \+\ ('not' (I -TruthEval phi)) = {} ;
then B3: I -TruthEval (xnot phi) = 'not' (I -TruthEval phi) by FOMODEL0:29;
BB1: Y /\ XX is I -satisfied by B0;
phi in Phii by TARSKI:def 1;
then 1 = 'not' (I -TruthEval (xnot phi)) by B3, B0, FOMODEL2:def 42;
hence contradiction by BB1, B2, FOMODEL2:def 45; :: thesis: verum