# Theory ZF_Miscellanea

```section‹Various results missing from ZF.›

theory ZF_Miscellanea
imports
ZF
Nat_Miscellanea
begin

lemma rex_mono :
assumes "∃ d ∈ A . P(d)" "A⊆B"
shows "∃ d ∈ B. P(d)"
using assms by auto

lemma function_subset:
"function(f) ⟹ g⊆f ⟹ function(g)"
unfolding function_def subset_def by auto

lemma converse_refl : "refl(A,r) ⟹ refl(A,converse(r))"
unfolding refl_def by simp

lemma Ord_lt_subset : "Ord(b) ⟹ a<b ⟹ a⊆b"
by(intro subsetI,frule ltD,rule_tac Ord_trans,simp_all)

lemma funcI : "f ∈ A → B ⟹ a ∈ A ⟹ b= f ` a ⟹ ⟨a, b⟩ ∈ f"

lemma vimage_fun_sing:
assumes "f∈A→B" "b∈B"
shows "{a∈A . f`a=b} = f-``{b}"
using assms vimage_singleton_iff function_apply_equality Pi_iff funcI by auto

lemma image_fun_subset: "S∈A→B ⟹ C⊆A⟹ {S ` x . x∈ C} = S``C"
using image_function[symmetric,of S C] domain_of_fun Pi_iff by auto

lemma inj_range_Diff:
assumes "f ∈ inj(A,A')"
shows "f``A - f``T = f``(A - T)"
using inj_equality[OF _ _ assms] by auto

lemma subset_Diff_Un: "X ⊆ A ⟹ A = (A - X) ∪ X " by auto

lemma Diff_bij:
assumes "∀A∈F. X ⊆ A" shows "(λA∈F. A-X) ∈ bij(F, {A-X. A∈F})"
using assms unfolding bij_def inj_def surj_def
by (auto intro:lam_type, subst subset_Diff_Un[of X]) auto

lemma function_space_nonempty:
assumes "b∈B"
shows "(λx∈A. b) : A → B"
using assms lam_type by force

lemma lam_constant_eq_cartprod: "(λ_∈A. y) = A × {y}"
unfolding lam_def by auto

lemma vimage_lam: "(λx∈A. f(x)) -`` B = { x∈A . f(x) ∈ B }"
using lam_funtype[of A f, THEN [2] domain_type]
lam_funtype[of A f, THEN [2] apply_equality] lamI[of _ A f]
by auto blast

lemma range_fun_subset_codomain:
assumes "h:B → C"
shows "range(h) ⊆ C"
unfolding range_def domain_def converse_def using range_type[OF _ assms] by auto

lemma Pi_rangeD:
assumes "f∈Pi(A,B)" "b ∈ range(f)"
shows "∃a∈A. f`a = b"
using assms apply_equality[OF _ assms(1), of _ b]
domain_type[OF _ assms(1)] by auto

lemma Pi_range_eq: "f ∈ Pi(A,B) ⟹ range(f) = {f ` x . x ∈ A}"
using Pi_rangeD[of f A B] apply_rangeI[of f A B]
by blast

lemma Pi_vimage_subset : "f ∈ Pi(A,B) ⟹ f-``C ⊆ A"
unfolding Pi_def by auto

definition
minimum :: "i ⇒ i ⇒ i" where
"minimum(r,B) ≡ THE b. first(b,B,r)"

lemma minimum_in': "minimum(r,B) ∈ B ∪ {0}"
using the_0 first_is_elem unfolding minimum_def
by (cases "∃!b. first(b, B, r)")
(auto dest!:theI[of "λb. first(b, B, r)"])

lemma minimum_in: "⟦ well_ord(A,r); B⊆A; B≠0 ⟧ ⟹ minimum(r,B) ∈ B"
using the_first_in unfolding minimum_def by simp

lemma well_ord_surj_imp_inj_inverse:
assumes "well_ord(A,r)" "h ∈ surj(A,B)"
shows "(λb∈B. minimum(r, {a∈A. h`a=b})) ∈ inj(B,A)"
proof -
let ?f="λb∈B. minimum(r, {a∈A. h`a=b})"
have "minimum(r, {a ∈ A . h ` a = b}) ∈ {a∈A. h`a=b}" if "b∈B" for b
proof -
from ‹h ∈ surj(A,B)› that
have "{a∈A. h`a=b} ≠ 0"
unfolding surj_def by blast
with ‹well_ord(A,r)›
show "minimum(r,{a∈A. h`a=b}) ∈ {a∈A. h`a=b}"
using minimum_in by blast
qed
moreover from this
have "?f : B → A"
using lam_type[of B _ "λ_.A"] by simp
moreover
have "?f ` w = ?f ` x ⟹ w = x" if "w∈B" "x∈B" for w x
proof -
from calculation that
have "w = h ` minimum(r,{a∈A. h`a=w})"
"x = h ` minimum(r,{a∈A. h`a=x})"
by simp_all
moreover
assume "?f ` w = ?f ` x"
moreover from this and that
have "minimum(r, {a ∈ A . h ` a = w}) = minimum(r, {a ∈ A . h ` a = x})"
unfolding minimum_def by simp_all
moreover from calculation(1,2,4)
show "w=x" by simp
qed
ultimately
show ?thesis
unfolding inj_def by blast
qed

lemma well_ord_surj_imp_lepoll:
assumes "well_ord(A,r)" "h ∈ surj(A,B)"
shows "B≲A"
unfolding lepoll_def using well_ord_surj_imp_inj_inverse[OF assms]
by blast

― ‹New result›
lemma surj_imp_well_ord:
assumes "well_ord(A,r)" "h ∈ surj(A,B)"
shows "∃s. well_ord(B,s)"
using assms lepoll_well_ord[OF well_ord_surj_imp_lepoll]
by force

lemma Pow_sing : "Pow({a}) = {0,{a}}"
proof(intro equalityI,simp_all)
have "z ∈ {0,{a}}" if "z ⊆ {a}" for z
using that by auto
then
show " Pow({a}) ⊆ {0, {a}}" by auto
qed

lemma Pow_cons:
shows "Pow(cons(a,A)) = Pow(A) ∪ {{a} ∪ X . X: Pow(A)}"
using Un_Pow_subset Pow_sing
{
fix C D
assume "⋀ B . B∈Pow(A) ⟹ C ≠ {a} ∪ B" "C ⊆ {a} ∪ A" "D ∈ C"
moreover from this
have "∀x∈C . x=a ∨ x∈A" by auto
moreover from calculation
consider (a) "D=a" | (b) "D∈A" by auto
from this
have "D∈A"
proof(cases)
case a
with calculation show ?thesis by auto
next
case b
then show ?thesis by simp
qed
}
then show "⋀x xa. (∀xa∈Pow(A). x ≠ {a} ∪ xa) ⟹ x ⊆ cons(a, A) ⟹ xa ∈ x ⟹ xa ∈ A"
by auto
qed

lemma app_nm :
assumes "n∈nat" "m∈nat" "f∈n→m" "x ∈ nat"
shows "f`x ∈ nat"
proof(cases "x∈n")
case True
then show ?thesis using assms in_n_in_nat apply_type by simp
next
case False
then show ?thesis using assms apply_0 domain_of_fun by simp
qed

lemma Upair_eq_cons: "Upair(a,b) = {a,b}"
unfolding cons_def by auto

lemma converse_apply_eq : "converse(f) ` x = ⋃(f -`` {x})"
unfolding apply_def vimage_def by simp

lemmas app_fun = apply_iff[THEN iffD1]

lemma Finite_imp_lesspoll_nat:
assumes "Finite(A)"
shows "A ≺ nat"
using assms subset_imp_lepoll[OF naturals_subset_nat] eq_lepoll_trans
n_lesspoll_nat eq_lesspoll_trans
unfolding Finite_def lesspoll_def by auto

definition curry :: "[i,i,i] ⇒ i" where
"curry(A,B,f) ≡ λx∈A . λy∈B . f`⟨x,y⟩"

lemma curry_type :
assumes "f ∈ A×B → C"
shows "curry(A,B,f) ∈ A → (B → C)"
using assms lam_funtype
unfolding curry_def
by auto

end```