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