let A be non empty Subset of GRZ-formula-set; :: thesis: for t, u being GRZ-formula holds
( A, GRZ-rules |- t '&' u iff ( A, GRZ-rules |- t & A, GRZ-rules |- u ) )
let t, u be GRZ-formula; :: thesis: ( A, GRZ-rules |- t '&' u iff ( A, GRZ-rules |- t & A, GRZ-rules |- u ) )
thus ( A, GRZ-rules |- t '&' u implies ( A, GRZ-rules |- t & A, GRZ-rules |- u ) ) :: thesis: ( A, GRZ-rules |- t & A, GRZ-rules |- u implies A, GRZ-rules |- t '&' u )
proof
assume A1: A, GRZ-rules |- t '&' u ; :: thesis: ( A, GRZ-rules |- t & A, GRZ-rules |- u )
set S = {(t '&' u)};
for a being object st a in {(t '&' u)} holds
a in GRZ-formula-set
proof
let a be object ; :: thesis: ( a in {(t '&' u)} implies a in GRZ-formula-set )
assume a in {(t '&' u)} ; :: thesis: a in GRZ-formula-set
then a = t '&' u by TARSKI:def 1;
hence a in GRZ-formula-set ; :: thesis: verum
end;
then {(t '&' u)} c= GRZ-formula-set ;
then reconsider S = {(t '&' u)} as GRZ-formula-finset ;
A2: A, GRZ-rules |- S by A1, TARSKI:def 1;
[S,t] in GRZ-ConjElimL ;
then [S,t] in GRZ-rules by Def35;
hence A, GRZ-rules |- t by A2, Th48; :: thesis: A, GRZ-rules |- u
[S,u] in GRZ-ConjElimR ;
then [S,u] in GRZ-rules by Def35;
hence A, GRZ-rules |- u by A2, Th48; :: thesis: verum
end;
assume that
A10: A, GRZ-rules |- t and
A11: A, GRZ-rules |- u ; :: thesis: A, GRZ-rules |- t '&' u
set S1 = {t,u};
for a being object st a in {t,u} holds
a in GRZ-formula-set
proof
let a be object ; :: thesis: ( a in {t,u} implies a in GRZ-formula-set )
assume a in {t,u} ; :: thesis: a in GRZ-formula-set
then ( a = t or a = u ) by TARSKI:def 2;
hence a in GRZ-formula-set ; :: thesis: verum
end;
then {t,u} c= GRZ-formula-set ;
then reconsider S1 = {t,u} as GRZ-formula-finset ;
A12: A, GRZ-rules |- S1 by A10, A11, TARSKI:def 2;
[S1,(t '&' u)] in GRZ-ConjIntro ;
then [S1,(t '&' u)] in GRZ-rules by Def35;
hence A, GRZ-rules |- t '&' u by A12, Th48; :: thesis: verum