Tarski-Grothendieck Axioms

[CoghettoR]

I try to translate (and add) axioms of Tarski-Grothendieck (Mizar Tarski_0.miz) in Isabelle/ZF.

theory AxTarski imports ZF.ZF_Base

begin

(* :: Set axiom
theorem :: TARSKI_0:1
  for x being object holds x is set;
*)

theorem TARSKI_0_1:
  fixes x :: i
  shows "∃ y. x = { a ∈ y. True}" by auto

(* 
:: Extensionality axiom
theorem :: TARSKI_0:2
  (for x being object holds x in X iff x in Y) implies X = Y;
*)

theorem TARSKI_0_2:
  fixes X Y :: i
  assumes "∀ x.(x ∈ X ⟷ x ∈ Y)" 
  shows "X = Y" 
    using extension assms by auto

(*
:: Axiom of pair
theorem :: TARSKI_0:3
  for x,y being object ex z being set st
    for a being object holds
      a in z iff a = x or a = y;
*)

theorem TARSKI_0_3_a_R1:
  fixes x y
  shows "∀ a. (a ∈ ⟨x,y⟩ ⟶ (a = x ∨ a = y))" 
proof -
  {
    fix a
    assume "a ∈ ⟨x,y⟩"
    hence "a = x ∨ a = y" sorry
  }
  thus ?thesis by blast
qed

theorem TARSKI_0_3_a_R2:
  fixes x y
  shows "∀ a. ((a = x ∨ a = y) ⟶ a ∈ ⟨x,y⟩)" 
proof -
  {
  fix a
  assume "a = x ∨ a = y"
  hence "a ∈ ⟨x,y⟩" sorry
}
  thus ?thesis by blast
qed

theorem TARSKI_0_3_a:
  fixes x y ::i
  shows "∀ a :: i. (a ∈ ⟨x,y⟩ ⟷ (a = x ∨ a = y))" 
  using TARSKI_0_3_a_R1 TARSKI_0_3_a_R2 by blast

theorem TARSKI_0_3:
  shows "∃ z. ∀ a. (a ∈ z ⟷ (a = x ∨ a = y))"
proof - 
  let ?z = "⟨x,y⟩"
  { 
    fix a :: i
    assume "a ∈ ?z"
    hence "a = x ∨ a = y" using TARSKI_0_3_a by blast
  }
  moreover
  {
    fix a :: i
    assume "a = x ∨ a = y" 
    hence "a ∈ ?z" using TARSKI_0_3_a by blast
  }
  ultimately show ?thesis by blast
qed

(*
:: Axiom of union
theorem :: TARSKI_0:4
  for X being set
   ex Z being set st
    for x being object holds
      x in Z iff ex Y being set st x in Y & Y in X;
*)

theorem TARSKI_0_4:
  shows "∃ Z. ∀ x. (x ∈ Z ⟷ (∃ Y. x ∈ Y ∧ Y ∈ X))" by auto

(*
:: Axiom of regularity
theorem :: TARSKI_0:5
  x in X implies ex Y st Y in X & not ex x st x in X & x in Y;
*)

theorem TARSKI_0_5:
  assumes "x ∈ X"
  shows "∃ Y. Y ∈ X ∧ ¬ (∃ y. y ∈ X ∧ y ∈ Y)" 
proof -
  have "¬ X = 0" 
    using assms by blast
  hence "(∃x∈X. ∀y∈x. y∉X)" 
    using foundation by blast
  then obtain Y where "Y ∈ X" and "∀y∈Y. y∉X" by blast
  thus ?thesis by blast
qed

end

In the code I have 2 "sorry". Should I extend my "import ZF.ZF_base" with a file from IsarMathLib that would allow to find a proof?

Is there something similar to "object (Mizar)" in IsarMathLib?

Any ideas are welcome.

[dan323]

This is wrong because

⟨x,y⟩ = {{x},{x,y}}

hece

a ∈ ⟨x,y⟩   ⟷  a = {x} ∨ a = {x,y}

I guess you made a mistake using ⟨x,y⟩ instead of {x,y}