let p, q be ZF-formula; :: thesis: for M being non empty set
for v being Function of VAR,M holds
( M,v |= (('not' p) '&' ('not' q)) => ('not' (p 'or' q)) & M |= (('not' p) '&' ('not' q)) => ('not' (p 'or' q)) )
let M be non empty set ; :: thesis: for v being Function of VAR,M holds
( M,v |= (('not' p) '&' ('not' q)) => ('not' (p 'or' q)) & M |= (('not' p) '&' ('not' q)) => ('not' (p 'or' q)) )
let v be Function of VAR,M; :: thesis: ( M,v |= (('not' p) '&' ('not' q)) => ('not' (p 'or' q)) & M |= (('not' p) '&' ('not' q)) => ('not' (p 'or' q)) )
now :: thesis: for v being Function of VAR,M holds M,v |= (('not' p) '&' ('not' q)) => ('not' (p 'or' q))
let v be Function of VAR,M; :: thesis: M,v |= (('not' p) '&' ('not' q)) => ('not' (p 'or' q))
now :: thesis: ( M,v |= ('not' p) '&' ('not' q) implies M,v |= 'not' (p 'or' q) )
assume A1: M,v |= ('not' p) '&' ('not' q) ; :: thesis: M,v |= 'not' (p 'or' q)
then M,v |= 'not' q by ZF_MODEL:15;
then A2: not M,v |= q by ZF_MODEL:14;
M,v |= 'not' p by A1, ZF_MODEL:15;
then not M,v |= p by ZF_MODEL:14;
then not M,v |= p 'or' q by A2, ZF_MODEL:17;
hence M,v |= 'not' (p 'or' q) by ZF_MODEL:14; :: thesis: verum
end;
hence M,v |= (('not' p) '&' ('not' q)) => ('not' (p 'or' q)) by ZF_MODEL:18; :: thesis: verum
end;
hence ( M,v |= (('not' p) '&' ('not' q)) => ('not' (p 'or' q)) & M |= (('not' p) '&' ('not' q)) => ('not' (p 'or' q)) ) ; :: thesis: verum