[STATEMENT]
lemma open_image_fst:
  assumes "open S"
  shows "open (fst ` S)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. open (fst ` S)
[PROOF STEP]
proof (rule openI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> fst ` S \<Longrightarrow> \<exists>T. open T \<and> x \<in> T \<and> T \<subseteq> fst ` S
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> fst ` S \<Longrightarrow> \<exists>T. open T \<and> x \<in> T \<and> T \<subseteq> fst ` S
[PROOF STEP]
assume "x \<in> fst ` S"
[PROOF STATE]
proof (state)
this:
x \<in> fst ` S

goal (1 subgoal):
 1. \<And>x. x \<in> fst ` S \<Longrightarrow> \<exists>T. open T \<and> x \<in> T \<and> T \<subseteq> fst ` S
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> fst ` S
[PROOF STEP]
obtain y where "(x, y) \<in> S"
[PROOF STATE]
proof (prove)
using this:
x \<in> fst ` S

goal (1 subgoal):
 1. (\<And>y. (x, y) \<in> S \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(x, y) \<in> S

goal (1 subgoal):
 1. \<And>x. x \<in> fst ` S \<Longrightarrow> \<exists>T. open T \<and> x \<in> T \<and> T \<subseteq> fst ` S
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(x, y) \<in> S
[PROOF STEP]
obtain A B where "open A" "open B" "x \<in> A" "y \<in> B" "A \<times> B \<subseteq> S"
[PROOF STATE]
proof (prove)
using this:
(x, y) \<in> S

goal (1 subgoal):
 1. (\<And>A B. \<lbrakk>open A; open B; x \<in> A; y \<in> B; A \<times> B \<subseteq> S\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using \<open>open S\<close>
[PROOF STATE]
proof (prove)
using this:
(x, y) \<in> S
open S

goal (1 subgoal):
 1. (\<And>A B. \<lbrakk>open A; open B; x \<in> A; y \<in> B; A \<times> B \<subseteq> S\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding open_prod_def
[PROOF STATE]
proof (prove)
using this:
(x, y) \<in> S
\<forall>x\<in>S. \<exists>A B. open A \<and> open B \<and> x \<in> A \<times> B \<and> A \<times> B \<subseteq> S

goal (1 subgoal):
 1. (\<And>A B. \<lbrakk>open A; open B; x \<in> A; y \<in> B; A \<times> B \<subseteq> S\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
open A
open B
x \<in> A
y \<in> B
A \<times> B \<subseteq> S

goal (1 subgoal):
 1. \<And>x. x \<in> fst ` S \<Longrightarrow> \<exists>T. open T \<and> x \<in> T \<and> T \<subseteq> fst ` S
[PROOF STEP]
from \<open>A \<times> B \<subseteq> S\<close> \<open>y \<in> B\<close>
[PROOF STATE]
proof (chain)
picking this:
A \<times> B \<subseteq> S
y \<in> B
[PROOF STEP]
have "A \<subseteq> fst ` S"
[PROOF STATE]
proof (prove)
using this:
A \<times> B \<subseteq> S
y \<in> B

goal (1 subgoal):
 1. A \<subseteq> fst ` S
[PROOF STEP]
by (rule subset_fst_imageI)
[PROOF STATE]
proof (state)
this:
A \<subseteq> fst ` S

goal (1 subgoal):
 1. \<And>x. x \<in> fst ` S \<Longrightarrow> \<exists>T. open T \<and> x \<in> T \<and> T \<subseteq> fst ` S
[PROOF STEP]
with \<open>open A\<close> \<open>x \<in> A\<close>
[PROOF STATE]
proof (chain)
picking this:
open A
x \<in> A
A \<subseteq> fst ` S
[PROOF STEP]
have "open A \<and> x \<in> A \<and> A \<subseteq> fst ` S"
[PROOF STATE]
proof (prove)
using this:
open A
x \<in> A
A \<subseteq> fst ` S

goal (1 subgoal):
 1. open A \<and> x \<in> A \<and> A \<subseteq> fst ` S
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
open A \<and> x \<in> A \<and> A \<subseteq> fst ` S

goal (1 subgoal):
 1. \<And>x. x \<in> fst ` S \<Longrightarrow> \<exists>T. open T \<and> x \<in> T \<and> T \<subseteq> fst ` S
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
open A \<and> x \<in> A \<and> A \<subseteq> fst ` S
[PROOF STEP]
show "\<exists>T. open T \<and> x \<in> T \<and> T \<subseteq> fst ` S"
[PROOF STATE]
proof (prove)
using this:
open A \<and> x \<in> A \<and> A \<subseteq> fst ` S

goal (1 subgoal):
 1. \<exists>T. open T \<and> x \<in> T \<and> T \<subseteq> fst ` S
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
\<exists>T. open T \<and> x \<in> T \<and> T \<subseteq> fst ` S

goal:
No subgoals!
[PROOF STEP]
qed