[STATEMENT]
lemma topological_space_transfer[transfer_rule]:
  includes lifting_syntax
  assumes [transfer_rule]: "right_total T" "bi_unique T"
  shows "((rel_set T ===> (=)) ===> (=)) (topological_space_on_with (Collect (Domainp T)))
    class.topological_space"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((rel_set T ===> (=)) ===> (=)) (topological_space_on_with (Collect (Domainp T))) class.topological_space
[PROOF STEP]
unfolding topological_space_on_with_def[abs_def] class.topological_space_def[abs_def]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((rel_set T ===> (=)) ===> (=)) (\<lambda>open. open (Collect (Domainp T)) \<and> (\<forall>S\<subseteq>Collect (Domainp T). \<forall>Ta\<subseteq>Collect (Domainp T). open S \<longrightarrow> open Ta \<longrightarrow> open (S \<inter> Ta)) \<and> (\<forall>K\<subseteq>Pow (Collect (Domainp T)). Ball K open \<longrightarrow> open (\<Union> K))) (\<lambda>open. open UNIV \<and> (\<forall>S T. open S \<longrightarrow> open T \<longrightarrow> open (S \<inter> T)) \<and> (\<forall>K. (\<forall>S\<in>K. open S) \<longrightarrow> open (\<Union> K)))
[PROOF STEP]
apply transfer_prover_start
[PROOF STATE]
proof (prove)
goal (13 subgoals):
 1. Transfer.Rel (?Rl27 ===> rel_set T) ?ak27 \<Union>
 2. Transfer.Rel (?Rl27 ===> (rel_set T ===> (=)) ===> ?Rn27) ?aj27 Ball
 3. Transfer.Rel (?Rn27 ===> (=) ===> ?Rm27) ?ai27 (\<longrightarrow>)
 4. Transfer.Rel ((?Rl27 ===> ?Rm27) ===> ?Rh27) ?ah27 All
 5. Transfer.Rel (rel_set T ===> rel_set T ===> rel_set T) ?ag27 (\<inter>)
 6. Transfer.Rel ((=) ===> (=) ===> ?Rk27) ?af27 (\<longrightarrow>)
 7. Transfer.Rel ((=) ===> ?Rk27 ===> ?Rj27) ?ae27 (\<longrightarrow>)
 8. Transfer.Rel ((rel_set T ===> ?Rj27) ===> ?Ri27) ?ad27 All
 9. Transfer.Rel ((rel_set T ===> ?Ri27) ===> ?Rg27) ?ac27 All
 10. Transfer.Rel (?Rg27 ===> ?Rh27 ===> ?Re27) ?ab27 (\<and>)
A total of 13 subgoals...
[PROOF STEP]
apply transfer_step+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>open. open (Collect (Domainp T)) \<and> (\<forall>S\<subseteq>Collect (Domainp T). \<forall>Ta\<subseteq>Collect (Domainp T). open S \<longrightarrow> open Ta \<longrightarrow> open (S \<inter> Ta)) \<and> (\<forall>K\<subseteq>Pow (Collect (Domainp T)). Ball K open \<longrightarrow> open (\<Union> K))) = (\<lambda>open. open (Collect (Domainp T)) \<and> (\<forall>S\<in>{A. Ball A (Domainp T)}. \<forall>T\<in>{A. Ball A (Domainp T)}. open S \<longrightarrow> open T \<longrightarrow> open (S \<inter> T)) \<and> (\<forall>K\<in>{A. \<forall>A\<in>A. Ball A (Domainp T)}. (\<forall>S\<in>K. open S) \<longrightarrow> open (\<Union> K)))
[PROOF STEP]
unfolding Pow_def Ball_Collect[symmetric]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>open. open (Collect (Domainp T)) \<and> (\<forall>S. Ball S (Domainp T) \<longrightarrow> (\<forall>Ta. Ball Ta (Domainp T) \<longrightarrow> open S \<longrightarrow> open Ta \<longrightarrow> open (S \<inter> Ta))) \<and> (\<forall>K. (\<forall>B\<in>K. Ball B (Domainp T)) \<longrightarrow> Ball K open \<longrightarrow> open (\<Union> K))) = (\<lambda>open. open (Collect (Domainp T)) \<and> (\<forall>S\<in>{A. Ball A (Domainp T)}. \<forall>T\<in>{A. Ball A (Domainp T)}. open S \<longrightarrow> open T \<longrightarrow> open (S \<inter> T)) \<and> (\<forall>K\<in>{A. \<forall>A\<in>A. Ball A (Domainp T)}. (\<forall>S\<in>K. open S) \<longrightarrow> open (\<Union> K)))
[PROOF STEP]
by blast