[STATEMENT]
lemma (in vsv) vsv_vrange_VLambda_app:
  assumes "g ` elts A = elts (\<D>\<^sub>\<circ> r)"
  shows "\<R>\<^sub>\<circ> (\<lambda>x\<in>\<^sub>\<circ>A. r\<lparr>g x\<rparr>) = \<R>\<^sub>\<circ> r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<R>\<^sub>\<circ> (\<lambda>x\<in>\<^sub>\<circ>A. r\<lparr>g x\<rparr>) = \<R>\<^sub>\<circ> r
[PROOF STEP]
proof(intro vsubset_antisym vsv.vsv_vrange_vsubset, unfold vdomain_VLambda)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. vsv (\<lambda>x\<in>\<^sub>\<circ>A. r\<lparr>g x\<rparr>)
 2. \<And>x. x \<in>\<^sub>\<circ> A \<Longrightarrow> (\<lambda>x\<in>\<^sub>\<circ>A. r\<lparr>g x\<rparr>)\<lparr>x\<rparr> \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> r
 3. vsv r
 4. \<And>x. x \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> r \<Longrightarrow> r\<lparr>x\<rparr> \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (\<lambda>x\<in>\<^sub>\<circ>A. r\<lparr>g x\<rparr>)
[PROOF STEP]
show "(\<lambda>x\<in>\<^sub>\<circ>A. r\<lparr>g x\<rparr>)\<lparr>x\<rparr> \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> r" if "x \<in>\<^sub>\<circ> A" for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x\<in>\<^sub>\<circ>A. r\<lparr>g x\<rparr>)\<lparr>x\<rparr> \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> r
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<lambda>x\<in>\<^sub>\<circ>A. r\<lparr>g x\<rparr>)\<lparr>x\<rparr> \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> r
[PROOF STEP]
from assms that
[PROOF STATE]
proof (chain)
picking this:
g ` elts A = elts (\<D>\<^sub>\<circ> r)
x \<in>\<^sub>\<circ> A
[PROOF STEP]
have "g x \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> r"
[PROOF STATE]
proof (prove)
using this:
g ` elts A = elts (\<D>\<^sub>\<circ> r)
x \<in>\<^sub>\<circ> A

goal (1 subgoal):
 1. g x \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> r
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
g x \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> r

goal (1 subgoal):
 1. (\<lambda>x\<in>\<^sub>\<circ>A. r\<lparr>g x\<rparr>)\<lparr>x\<rparr> \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> r
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
g x \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> r
[PROOF STEP]
have "r\<lparr>g x\<rparr> \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> r"
[PROOF STATE]
proof (prove)
using this:
g x \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> r

goal (1 subgoal):
 1. r\<lparr>g x\<rparr> \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> r
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
r\<lparr>g x\<rparr> \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> r

goal (1 subgoal):
 1. (\<lambda>x\<in>\<^sub>\<circ>A. r\<lparr>g x\<rparr>)\<lparr>x\<rparr> \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> r
[PROOF STEP]
with that
[PROOF STATE]
proof (chain)
picking this:
x \<in>\<^sub>\<circ> A
r\<lparr>g x\<rparr> \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> r
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x \<in>\<^sub>\<circ> A
r\<lparr>g x\<rparr> \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> r

goal (1 subgoal):
 1. (\<lambda>x\<in>\<^sub>\<circ>A. r\<lparr>g x\<rparr>)\<lparr>x\<rparr> \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> r
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<lambda>x\<in>\<^sub>\<circ>A. r\<lparr>g x\<rparr>)\<lparr>x\<rparr> \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> r

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?x \<in>\<^sub>\<circ> A \<Longrightarrow> (\<lambda>x\<in>\<^sub>\<circ>A. r\<lparr>g x\<rparr>)\<lparr>?x\<rparr> \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> r

goal (3 subgoals):
 1. vsv (\<lambda>x\<in>\<^sub>\<circ>A. r\<lparr>g x\<rparr>)
 2. vsv r
 3. \<And>x. x \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> r \<Longrightarrow> r\<lparr>x\<rparr> \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (\<lambda>x\<in>\<^sub>\<circ>A. r\<lparr>g x\<rparr>)
[PROOF STEP]
show "r\<lparr>x\<rparr> \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (\<lambda>x\<in>\<^sub>\<circ>A. r\<lparr>g x\<rparr>)" if "x \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> r" for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r\<lparr>x\<rparr> \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (\<lambda>x\<in>\<^sub>\<circ>A. r\<lparr>g x\<rparr>)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. r\<lparr>x\<rparr> \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (\<lambda>x\<in>\<^sub>\<circ>A. r\<lparr>g x\<rparr>)
[PROOF STEP]
from that assms
[PROOF STATE]
proof (chain)
picking this:
x \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> r
g ` elts A = elts (\<D>\<^sub>\<circ> r)
[PROOF STEP]
have "x \<in> g ` elts A"
[PROOF STATE]
proof (prove)
using this:
x \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> r
g ` elts A = elts (\<D>\<^sub>\<circ> r)

goal (1 subgoal):
 1. x \<in> g ` elts A
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x \<in> g ` elts A

goal (1 subgoal):
 1. r\<lparr>x\<rparr> \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (\<lambda>x\<in>\<^sub>\<circ>A. r\<lparr>g x\<rparr>)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> g ` elts A
[PROOF STEP]
obtain c where c: "c \<in>\<^sub>\<circ> A" and x_def: "x = g c"
[PROOF STATE]
proof (prove)
using this:
x \<in> g ` elts A

goal (1 subgoal):
 1. (\<And>c. \<lbrakk>c \<in>\<^sub>\<circ> A; x = g c\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by clarsimp
[PROOF STATE]
proof (state)
this:
c \<in>\<^sub>\<circ> A
x = g c

goal (1 subgoal):
 1. r\<lparr>x\<rparr> \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (\<lambda>x\<in>\<^sub>\<circ>A. r\<lparr>g x\<rparr>)
[PROOF STEP]
from c
[PROOF STATE]
proof (chain)
picking this:
c \<in>\<^sub>\<circ> A
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
c \<in>\<^sub>\<circ> A

goal (1 subgoal):
 1. r\<lparr>x\<rparr> \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (\<lambda>x\<in>\<^sub>\<circ>A. r\<lparr>g x\<rparr>)
[PROOF STEP]
unfolding x_def
[PROOF STATE]
proof (prove)
using this:
c \<in>\<^sub>\<circ> A

goal (1 subgoal):
 1. r\<lparr>g c\<rparr> \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (\<lambda>x\<in>\<^sub>\<circ>A. r\<lparr>g x\<rparr>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
r\<lparr>x\<rparr> \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (\<lambda>x\<in>\<^sub>\<circ>A. r\<lparr>g x\<rparr>)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?x \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> r \<Longrightarrow> r\<lparr>?x\<rparr> \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (\<lambda>x\<in>\<^sub>\<circ>A. r\<lparr>g x\<rparr>)

goal (2 subgoals):
 1. vsv (\<lambda>x\<in>\<^sub>\<circ>A. r\<lparr>g x\<rparr>)
 2. vsv r
[PROOF STEP]
qed auto