[STATEMENT]
lemma univ_preserves:
  assumes ECH: "equiv A r" and RES: "f respects r" and PRES: "\<forall>x \<in> A. f x \<in> B"
  shows "\<forall>X \<in> A//r. univ f X \<in> B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>X\<in>A // r. univ f X \<in> B
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>X. X \<in> A // r \<Longrightarrow> univ f X \<in> B
[PROOF STEP]
fix X
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>X. X \<in> A // r \<Longrightarrow> univ f X \<in> B
[PROOF STEP]
assume "X \<in> A//r"
[PROOF STATE]
proof (state)
this:
X \<in> A // r

goal (1 subgoal):
 1. \<And>X. X \<in> A // r \<Longrightarrow> univ f X \<in> B
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
X \<in> A // r
[PROOF STEP]
obtain x where x: "x \<in> A" and X: "X = proj r x"
[PROOF STATE]
proof (prove)
using this:
X \<in> A // r

goal (1 subgoal):
 1. (\<And>x. \<lbrakk>x \<in> A; X = proj r x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using ECH proj_image[of r A]
[PROOF STATE]
proof (prove)
using this:
X \<in> A // r
equiv A r
proj r ` A = A // r

goal (1 subgoal):
 1. (\<And>x. \<lbrakk>x \<in> A; X = proj r x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
x \<in> A
X = proj r x

goal (1 subgoal):
 1. \<And>X. X \<in> A // r \<Longrightarrow> univ f X \<in> B
[PROOF STEP]
hence "univ f X = f x"
[PROOF STATE]
proof (prove)
using this:
x \<in> A
X = proj r x

goal (1 subgoal):
 1. univ f X = f x
[PROOF STEP]
using ECH RES univ_commute
[PROOF STATE]
proof (prove)
using this:
x \<in> A
X = proj r x
equiv A r
f respects r
\<lbrakk>equiv ?A ?r; ?f respects ?r; ?x \<in> ?A\<rbrakk> \<Longrightarrow> univ ?f (proj ?r ?x) = ?f ?x

goal (1 subgoal):
 1. univ f X = f x
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
univ f X = f x

goal (1 subgoal):
 1. \<And>X. X \<in> A // r \<Longrightarrow> univ f X \<in> B
[PROOF STEP]
thus "univ f X \<in> B"
[PROOF STATE]
proof (prove)
using this:
univ f X = f x

goal (1 subgoal):
 1. univ f X \<in> B
[PROOF STEP]
using x PRES
[PROOF STATE]
proof (prove)
using this:
univ f X = f x
x \<in> A
\<forall>x\<in>A. f x \<in> B

goal (1 subgoal):
 1. univ f X \<in> B
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
univ f X \<in> B

goal:
No subgoals!
[PROOF STEP]
qed