[STATEMENT]
lemma induced_pow_fun_surj:
  "((`) f) ` (Pow A) = Pow (f`A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (`) f ` Pow A = Pow (f ` A)
[PROOF STEP]
proof (rule seteqI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x \<in> (`) f ` Pow A \<Longrightarrow> x \<in> Pow (f ` A)
 2. \<And>x. x \<in> Pow (f ` A) \<Longrightarrow> x \<in> (`) f ` Pow A
[PROOF STEP]
fix X
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x \<in> (`) f ` Pow A \<Longrightarrow> x \<in> Pow (f ` A)
 2. \<And>x. x \<in> Pow (f ` A) \<Longrightarrow> x \<in> (`) f ` Pow A
[PROOF STEP]
show "X \<in> ((`) f) ` (Pow A) \<Longrightarrow> X \<in> Pow (f`A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. X \<in> (`) f ` Pow A \<Longrightarrow> X \<in> Pow (f ` A)
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
X \<in> (`) f ` Pow A \<Longrightarrow> X \<in> Pow (f ` A)

goal (1 subgoal):
 1. \<And>x. x \<in> Pow (f ` A) \<Longrightarrow> x \<in> (`) f ` Pow A
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> Pow (f ` A) \<Longrightarrow> x \<in> (`) f ` Pow A
[PROOF STEP]
fix Y
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> Pow (f ` A) \<Longrightarrow> x \<in> (`) f ` Pow A
[PROOF STEP]
assume Y: "Y \<in> Pow (f`A)"
[PROOF STATE]
proof (state)
this:
Y \<in> Pow (f ` A)

goal (1 subgoal):
 1. \<And>x. x \<in> Pow (f ` A) \<Longrightarrow> x \<in> (`) f ` Pow A
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Y \<in> Pow (f ` A)

goal (1 subgoal):
 1. \<And>x. x \<in> Pow (f ` A) \<Longrightarrow> x \<in> (`) f ` Pow A
[PROOF STEP]
hence "Y = f`{a\<in>A. f a \<in> Y}"
[PROOF STATE]
proof (prove)
using this:
Y \<in> Pow (f ` A)

goal (1 subgoal):
 1. Y = f ` {a \<in> A. f a \<in> Y}
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
Y = f ` {a \<in> A. f a \<in> Y}

goal (1 subgoal):
 1. \<And>x. x \<in> Pow (f ` A) \<Longrightarrow> x \<in> (`) f ` Pow A
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
Y \<in> Pow (f ` A)
Y = f ` {a \<in> A. f a \<in> Y}
[PROOF STEP]
show "Y\<in> ((`) f) ` (Pow A)"
[PROOF STATE]
proof (prove)
using this:
Y \<in> Pow (f ` A)
Y = f ` {a \<in> A. f a \<in> Y}

goal (1 subgoal):
 1. Y \<in> (`) f ` Pow A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Y \<in> (`) f ` Pow A

goal:
No subgoals!
[PROOF STEP]
qed