theory Set_Theory_Exercises
imports Main
begin
(*use rule, erule, and so on combined with basic elimination and introduction rules. do not use
any automation...*)
lemma
assumes "P \ Q" and "Q \ R"
shows "P \ R"
sorry
lemma
shows "P \ Q \ P \ Q = P"
sorry
lemma
assumes "x \ { x. P x \ Q x }"
and "\x. P x \ R x"
shows "R x"
sorry
lemma
assumes "P \ Q = {}"
shows "x \ P \ x \ Q"
sorry
lemma
shows "P \ Q = {} \ P = {} \ Q = {}"
sorry
lemma
shows "P - UNIV = {}"
sorry
lemma
assumes "S \ T = {}"
shows "(P - S) - T = (P - T) - S"
sorry
lemma
assumes "U \ S"
and "U \ T"
shows "U \ S \ T"
sorry
lemma
assumes "x \ (\i\I. f i)"
shows "\i\I. x \ f i"
sorry
lemma
shows "(\i\I. f i \ g i) = ((\i\I. f i) \ (\i\I. g i))"
sorry
lemma
assumes "\i\I. f i = {}"
shows "(\i\I. f i) = {}"
sorry
lemma
shows "f ` S \ T \ (\x\S. f x \ T)"
sorry
lemma
assumes "\x. f x = x"
shows "f ` S = S"
sorry
lemma
shows "(\x\S\T. f x) \ ((\x\S. f x) \ (\x\T. f x))"
sorry
lemma
assumes "x \ T"
and "x \ S"
and "\z\S. z \ x \ z \ T"
shows "S \ T"
sorry
end