internlm/Lean-Github huggingface dataset:
Theorem: SetTheory.interpret_isInductive
Proof state before:
V : Type u_1
inst✝ : Zermelo V
α : Type
n : Nat
v : α → V
l : Fin n → V
x : α ⊕ Fin n
⊢ Interpret V (BoundedFormula.isInductive x) v l ↔ Inductive (interpretTerm V v l x)
Tactic:
unfold BoundedFormula.isInductive
Proof state after:
V : Type u_1
inst✝ : Zermelo V
α : Type
n : Nat
v : α → V
l : Fin n → V
x : α ⊕ Fin n
⊢ Interpret V
      (BoundedFormula.and
        (BoundedFormula.exists
          (BoundedFormula.and (BoundedFormula.eqEmpty (Sum.inr (Fin.last n)))
            (BoundedFormula.mem (Sum.inr (Fin.last n)) (termSucc x))))
        (BoundedFormula.succClosed x))
      v l ↔
    Inductive (interpretTerm V v l x)
Theorem: SetTheory.interpret_isInductive
Proof state before:
V : Type u_1
inst✝ : Zermelo V
α : Type
n : Nat
v : α → V
l : Fin n → V
x : α ⊕ Fin n
⊢ Interpret V
      (BoundedFormula.and
        (BoundedFormula.exists
          (BoundedFormula.and (BoundedFormula.eqEmpty (Sum.inr (Fin.last n)))
            (BoundedFormula.mem (Sum.inr (Fin.last n)) (termSucc x))))
        (BoundedFormula.succClosed x))
      v l ↔
    Inductive (interpretTerm V v l x)
Tactic:
rw [inductive_iff]
Proof state after:
V : Type u_1
inst✝ : Zermelo V
α : Type
n : Nat
v : α → V
l : Fin n → V
x : α ⊕ Fin n
⊢ Interpret V
      (BoundedFormula.and
        (BoundedFormula.exists
          (BoundedFormula.and (BoundedFormula.eqEmpty (Sum.inr (Fin.last n)))
            (BoundedFormula.mem (Sum.inr (Fin.last n)) (termSucc x))))
        (BoundedFormula.succClosed x))
      v l ↔
    ∅ ∈ interpretTerm V v l x ∧ ∀ (y : V), y ∈ interpretTerm V v l x → succ y ∈ interpretTerm V v l x
Theorem: SetTheory.interpret_isInductive
Proof state before:
V : Type u_1
inst✝ : Zermelo V
α : Type
n : Nat
v : α → V
l : Fin n → V
x : α ⊕ Fin n
⊢ Interpret V
      (BoundedFormula.and
        (BoundedFormula.exists
          (BoundedFormula.and (BoundedFormula.eqEmpty (Sum.inr (Fin.last n)))
            (BoundedFormula.mem (Sum.inr (Fin.last n)) (termSucc x))))
        (BoundedFormula.succClosed x))
      v l ↔
    ∅ ∈ interpretTerm V v l x ∧ ∀ (y : V), y ∈ interpretTerm V v l x → succ y ∈ interpretTerm V v l x
Tactic:
simp
Proof state after:
no goals
Theorem: SetTheory.interpret_isNat'
Proof state before:
V : Type u_1
inst✝ : Zermelo V
α : Type
n : Nat
v : α → V
l : Fin n → V
x : α ⊕ Fin n
⊢ Interpret V (BoundedFormula.isNat x) v l ↔ ∀ (y : V), Inductive y → interpretTerm V v l x ∈ y
Tactic:
unfold BoundedFormula.isNat
Proof state after:
V : Type u_1
inst✝ : Zermelo V
α : Type
n : Nat
v : α → V
l : Fin n → V
x : α ⊕ Fin n
⊢ Interpret V
      (BoundedFormula.all
        (BoundedFormula.imp (BoundedFormula.isInductive (Sum.inr (Fin.last n)))
          (BoundedFormula.mem (termSucc x) (Sum.inr (Fin.last n)))))
      v l ↔
    ∀ (y : V), Inductive y → interpretTerm V v l x ∈ y
Theorem: SetTheory.interpret_isNat'
Proof state before:
V : Type u_1
inst✝ : Zermelo V
α : Type
n : Nat
v : α → V
l : Fin n → V
x : α ⊕ Fin n
⊢ Interpret V
      (BoundedFormula.all
        (BoundedFormula.imp (BoundedFormula.isInductive (Sum.inr (Fin.last n)))
          (BoundedFormula.mem (termSucc x) (Sum.inr (Fin.last n)))))
      v l ↔
    ∀ (y : V), Inductive y → interpretTerm V v l x ∈ y
Tactic:
simp
Proof state after:
no goals
Theorem: SetTheory.mem_ω_iff
Proof state before:
V : Type u_1
inst✝ : Zermelo V
n : V
⊢ n ∈ ω ↔ ∀ (s : V), Inductive s → n ∈ s
Tactic:
unfold ω
Proof state after:
V : Type u_1
inst✝ : Zermelo V
n : V
⊢ n ∈ sep (BoundedFormula.isNat (Sum.inr 0)) (fun i => Empty.elim i) Infinity.inductiveSet ↔
    ∀ (s : V), Inductive s → n ∈ s
Theorem: SetTheory.mem_ω_iff
Proof state before:
V : Type u_1
inst✝ : Zermelo V
n : V
⊢ n ∈ sep (BoundedFormula.isNat (Sum.inr 0)) (fun i => Empty.elim i) Infinity.inductiveSet ↔
    ∀ (s : V), Inductive s → n ∈ s
Tactic:
simp only [mem_sep_iff, interpret_isNat', interpret_inr, and_iff_right_iff_imp]
Proof state after:
V : Type u_1
inst✝ : Zermelo V
n : V
⊢ (∀ (y : V), Inductive y → n ∈ y) → n ∈ Infinity.inductiveSet
Theorem: SetTheory.mem_ω_iff
Proof state before:
V : Type u_1
inst✝ : Zermelo V
n : V
⊢ (∀ (y : V), Inductive y → n ∈ y) → n ∈ Infinity.inductiveSet
Tactic:
intro hn
Proof state after:
V : Type u_1
inst✝ : Zermelo V
n : V
hn : ∀ (y : V), Inductive y → n ∈ y
⊢ n ∈ Infinity.inductiveSet
Theorem: SetTheory.mem_ω_iff
Proof state before:
V : Type u_1
inst✝ : Zermelo V
n : V
hn : ∀ (y : V), Inductive y → n ∈ y
⊢ n ∈ Infinity.inductiveSet
Tactic:
exact hn _ Infinity.inductiveSet_inductive
Proof state after:
no goals
Theorem: SetTheory.interpret_isNat
Proof state before:
V : Type u_1
inst✝ : Zermelo V
α : Type
n : Nat
v : α → V
l : Fin n → V
x : α ⊕ Fin n
⊢ Interpret V (BoundedFormula.isNat x) v l ↔ interpretTerm V v l x ∈ ω
Tactic:
rw [mem_ω_iff, interpret_isNat']
Proof state after:
no goals
Theorem: SetTheory.empty_mem_ω
Proof state before:
V : Type u_1
inst✝ : Zermelo V
⊢ ∅ ∈ ω
Tactic:
rw [mem_ω_iff]
Proof state after:
V : Type u_1
inst✝ : Zermelo V
⊢ ∀ (s : V), Inductive s → ∅ ∈ s
Theorem: SetTheory.empty_mem_ω
Proof state before:
V : Type u_1
inst✝ : Zermelo V
⊢ ∀ (s : V), Inductive s → ∅ ∈ s
Tactic:
intro s hs
Proof state after:
V : Type u_1
inst✝ : Zermelo V
s : V
hs : Inductive s
⊢ ∅ ∈ s
Theorem: SetTheory.empty_mem_ω
Proof state before:
V : Type u_1
inst✝ : Zermelo V
s : V
hs : Inductive s
⊢ ∅ ∈ s
Tactic:
exact hs.empty_mem
Proof state after:
no goals
Theorem: SetTheory.succ_mem_ω
Proof state before:
V : Type u_1
inst✝ : Zermelo V
n : V
hn : n ∈ ω
⊢ succ n ∈ ω
Tactic:
rw [mem_ω_iff] at hn ⊢
Proof state after:
V : Type u_1
inst✝ : Zermelo V
n : V
hn : ∀ (s : V), Inductive s → n ∈ s
⊢ ∀ (s : V), Inductive s → succ n ∈ s
Theorem: SetTheory.succ_mem_ω
Proof state before:
V : Type u_1
inst✝ : Zermelo V
n : V
hn : ∀ (s : V), Inductive s → n ∈ s
⊢ ∀ (s : V), Inductive s → succ n ∈ s
Tactic:
intro s hs
Proof state after:
V : Type u_1
inst✝ : Zermelo V
n : V
hn : ∀ (s : V), Inductive s → n ∈ s
s : V
hs : Inductive s
⊢ succ n ∈ s
Theorem: SetTheory.succ_mem_ω
Proof state before:
V : Type u_1
inst✝ : Zermelo V
n : V
hn : ∀ (s : V), Inductive s → n ∈ s
s : V
hs : Inductive s
⊢ succ n ∈ s
Tactic:
exact hs.succ_mem n (hn s hs)
Proof state after:
no goals
Theorem: SetTheory.one_def
Proof state before:
V : Type u_1
inst✝ : Zermelo V
⊢ 1 = {∅}
Tactic:
show ∅ ∪ {∅} = {∅}
Proof state after:
V : Type u_1
inst✝ : Zermelo V
⊢ ∅ ∪ {∅} = {∅}
Theorem: SetTheory.one_def
Proof state before:
V : Type u_1
inst✝ : Zermelo V
⊢ ∅ ∪ {∅} = {∅}
Tactic:
simp
Proof state after:
no goals
Theorem: SetTheory.interpret_isRelation
Proof state before:
V : Type u_1
inst✝ : Zermelo V
r✝ x y z : V
α : Type
n : Nat
v : α → V
l : Fin n → V
r : α ⊕ Fin n
⊢ Interpret V (BoundedFormula.isRelation r) v l ↔ IsRelation (interpretTerm V v l r)
Tactic:
unfold BoundedFormula.isRelation IsRelation
Proof state after:
V : Type u_1
inst✝ : Zermelo V
r✝ x y z : V
α : Type
n : Nat
v : α → V
l : Fin n → V
r : α ⊕ Fin n
⊢ Interpret V
      (BoundedFormula.all
        (BoundedFormula.imp (BoundedFormula.mem (Sum.inr (Fin.last n)) (termSucc r))
          (BoundedFormula.isOPair (Sum.inr (Fin.last n)))))
      v l ↔
    ∀ (p : V), p ∈ interpretTerm V v l r → IsOPair p
Theorem: SetTheory.interpret_isRelation
Proof state before:
V : Type u_1
inst✝ : Zermelo V
r✝ x y z : V
α : Type
n : Nat
v : α → V
l : Fin n → V
r : α ⊕ Fin n
⊢ Interpret V
      (BoundedFormula.all
        (BoundedFormula.imp (BoundedFormula.mem (Sum.inr (Fin.last n)) (termSucc r))
          (BoundedFormula.isOPair (Sum.inr (Fin.last n)))))
      v l ↔
    ∀ (p : V), p ∈ interpretTerm V v l r → IsOPair p
Tactic:
simp
Proof state after:
no goals
Theorem: SetTheory.opair_left_mem_sUnion_sUnion
Proof state before:
V : Type u_1
inst✝ : Zermelo V
r x y z : V
hxyr : opair x y ∈ r
⊢ x ∈ ⋃ ⋃ r
Tactic:
simp only [mem_sUnion_iff]
Proof state after:
V : Type u_1
inst✝ : Zermelo V
r x y z : V
hxyr : opair x y ∈ r
⊢ ∃ t, (∃ t_1, t_1 ∈ r ∧ t ∈ t_1) ∧ x ∈ t
Theorem: SetTheory.opair_left_mem_sUnion_sUnion
Proof state before:
V : Type u_1
inst✝ : Zermelo V
r x y z : V
hxyr : opair x y ∈ r
⊢ ∃ t, (∃ t_1, t_1 ∈ r ∧ t ∈ t_1) ∧ x ∈ t
Tactic:
refine ⟨{x}, ⟨_, hxyr, ?_⟩, ?_⟩
Proof state after:
case refine_1
V : Type u_1
inst✝ : Zermelo V
r x y z : V
hxyr : opair x y ∈ r
⊢ {x} ∈ opair x y

case refine_2
V : Type u_1
inst✝ : Zermelo V
r x y z : V
hxyr : opair x y ∈ r
⊢ x ∈ {x}
Theorem: SetTheory.opair_left_mem_sUnion_sUnion
Proof state before:
case refine_1
V : Type u_1
inst✝ : Zermelo V
r x y z : V
hxyr : opair x y ∈ r
⊢ {x} ∈ opair x y
Tactic:
simp only [opair, mem_pair_iff, true_or]
Proof state after:
no goals
Theorem: SetTheory.opair_left_mem_sUnion_sUnion
Proof state before:
case refine_2
V : Type u_1
inst✝ : Zermelo V
r x y z : V
hxyr : opair x y ∈ r
⊢ x ∈ {x}
Tactic:
rw [mem_singleton_iff]
Proof state after:
no goals
Theorem: SetTheory.opair_right_mem_sUnion_sUnion
Proof state before:
V : Type u_1
inst✝ : Zermelo V
r x y z : V
hxyr : opair x y ∈ r
⊢ y ∈ ⋃ ⋃ r
Tactic:
simp only [mem_sUnion_iff]
Proof state after:
V : Type u_1
inst✝ : Zermelo V
r x y z : V
hxyr : opair x y ∈ r
⊢ ∃ t, (∃ t_1, t_1 ∈ r ∧ t ∈ t_1) ∧ y ∈ t
Theorem: SetTheory.opair_right_mem_sUnion_sUnion
Proof state before:
V : Type u_1
inst✝ : Zermelo V
r x y z : V
hxyr : opair x y ∈ r
⊢ ∃ t, (∃ t_1, t_1 ∈ r ∧ t ∈ t_1) ∧ y ∈ t
Tactic:
refine ⟨pair x y, ⟨_, hxyr, ?_⟩, ?_⟩
Proof state after:
case refine_1
V : Type u_1
inst✝ : Zermelo V
r x y z : V
hxyr : opair x y ∈ r
⊢ pair x y ∈ opair x y

case refine_2
V : Type u_1
inst✝ : Zermelo V
r x y z : V
hxyr : opair x y ∈ r
⊢ y ∈ pair x y
Theorem: SetTheory.opair_right_mem_sUnion_sUnion
Proof state before:
case refine_1
V : Type u_1
inst✝ : Zermelo V
r x y z : V
hxyr : opair x y ∈ r
⊢ pair x y ∈ opair x y
Tactic:
simp only [opair, mem_pair_iff, or_true]
Proof state after:
no goals
Theorem: SetTheory.opair_right_mem_sUnion_sUnion
Proof state before:
case refine_2
V : Type u_1
inst✝ : Zermelo V
r x y z : V
hxyr : opair x y ∈ r
⊢ y ∈ pair x y
Tactic:
exact right_mem_pair
Proof state after:
no goals
Theorem: SetTheory.interpret_memDom'
Proof state before:
V : Type u_1
inst✝ : Zermelo V
r✝ x✝ y z : V
α : Type
n : Nat
v : α → V
l : Fin n → V
x r : α ⊕ Fin n
⊢ Interpret V (BoundedFormula.memDom x r) v l ↔ ∃ z, opair (interpretTerm V v l x) z ∈ interpretTerm V v l r
Tactic:
unfold BoundedFormula.memDom
Proof state after:
V : Type u_1
inst✝ : Zermelo V
r✝ x✝ y z : V
α : Type
n : Nat
v : α → V
l : Fin n → V
x r : α ⊕ Fin n
⊢ Interpret V
      (BoundedFormula.exists
        (BoundedFormula.exists
          (BoundedFormula.and
            (BoundedFormula.eqOPair (Sum.inr { val := n + 1, isLt := (_ : n + 1 < n + 1 + (0 + 1)) })
              (termSucc (termSucc x)) (Sum.inr { val := n, isLt := (_ : n < n + (1 + 1)) }))
            (BoundedFormula.mem (Sum.inr { val := n + 1, isLt := (_ : n + 1 < n + 1 + (0 + 1)) })
              (termSucc (termSucc r))))))
      v l ↔
    ∃ z, opair (interpretTerm V v l x) z ∈ interpretTerm V v l r
Theorem: SetTheory.interpret_memDom'
Proof state before:
V : Type u_1
inst✝ : Zermelo V
r✝ x✝ y z : V
α : Type
n : Nat
v : α → V
l : Fin n → V
x r : α ⊕ Fin n
⊢ Interpret V
      (BoundedFormula.exists
        (BoundedFormula.exists
          (BoundedFormula.and
            (BoundedFormula.eqOPair (Sum.inr { val := n + 1, isLt := (_ : n + 1 < n + 1 + (0 + 1)) })
              (termSucc (termSucc x)) (Sum.inr { val := n, isLt := (_ : n < n + (1 + 1)) }))
            (BoundedFormula.mem (Sum.inr { val := n + 1, isLt := (_ : n + 1 < n + 1 + (0 + 1)) })
              (termSucc (termSucc r))))))
      v l ↔
    ∃ z, opair (interpretTerm V v l x) z ∈ interpretTerm V v l r
Tactic:
simp
Proof state after:
no goals
Theorem: SetTheory.mem_dom_iff
Proof state before:
V : Type u_1
inst✝ : Zermelo V
r x y z : V
⊢ x ∈ dom r ↔ ∃ z, opair x z ∈ r
Tactic:
unfold dom
Proof state after:
V : Type u_1
inst✝ : Zermelo V
r x y z : V
⊢ x ∈ sep (BoundedFormula.memDom (Sum.inr 0) (Sum.inl ())) (fun x => r) (⋃ ⋃ r) ↔ ∃ z, opair x z ∈ r
Theorem: SetTheory.mem_dom_iff
Proof state before:
V : Type u_1
inst✝ : Zermelo V
r x y z : V
⊢ x ∈ sep (BoundedFormula.memDom (Sum.inr 0) (Sum.inl ())) (fun x => r) (⋃ ⋃ r) ↔ ∃ z, opair x z ∈ r
Tactic:
simp only [mem_sep_iff, interpret_memDom', interpret_inr, interpret_inl,
  and_iff_right_iff_imp, forall_exists_index]
Proof state after:
V : Type u_1
inst✝ : Zermelo V
r x y z : V
⊢ ∀ (x_1 : V), opair x x_1 ∈ r → x ∈ ⋃ ⋃ r
Theorem: SetTheory.mem_dom_iff
Proof state before:
V : Type u_1
inst✝ : Zermelo V
r x y z : V
⊢ ∀ (x_1 : V), opair x x_1 ∈ r → x ∈ ⋃ ⋃ r
Tactic:
intro t
Proof state after:
V : Type u_1
inst✝ : Zermelo V
r x y z t : V
⊢ opair x t ∈ r → x ∈ ⋃ ⋃ r
Theorem: SetTheory.mem_dom_iff
Proof state before:
V : Type u_1
inst✝ : Zermelo V
r x y z t : V
⊢ opair x t ∈ r → x ∈ ⋃ ⋃ r
Tactic:
exact opair_left_mem_sUnion_sUnion
Proof state after:
no goals
Theorem: SetTheory.interpret_memDom
Proof state before:
V : Type u_1
inst✝ : Zermelo V
r✝ x✝ y z : V
α : Type
n : Nat
v : α → V
l : Fin n → V
x r : α ⊕ Fin n
⊢ Interpret V (BoundedFormula.memDom x r) v l ↔ interpretTerm V v l x ∈ dom (interpretTerm V v l r)
Tactic:
rw [mem_dom_iff, interpret_memDom']
Proof state after:
no goals
Theorem: SetTheory.interpret_memRan'
Proof state before:
V : Type u_1
inst✝ : Zermelo V
r✝ x✝ y z : V
α : Type
n : Nat
v : α → V
l : Fin n → V
x r : α ⊕ Fin n
⊢ Interpret V (BoundedFormula.memRan x r) v l ↔ ∃ z, opair z (interpretTerm V v l x) ∈ interpretTerm V v l r
Tactic:
unfold BoundedFormula.memRan
Proof state after:
V : Type u_1
inst✝ : Zermelo V
r✝ x✝ y z : V
α : Type
n : Nat
v : α → V
l : Fin n → V
x r : α ⊕ Fin n
⊢ Interpret V
      (BoundedFormula.exists
        (BoundedFormula.exists
          (BoundedFormula.and
            (BoundedFormula.eqOPair (Sum.inr { val := n + 1, isLt := (_ : n + 1 < n + 1 + (0 + 1)) })
              (Sum.inr { val := n, isLt := (_ : n < n + (1 + 1)) }) (termSucc (termSucc x)))
            (BoundedFormula.mem (Sum.inr { val := n + 1, isLt := (_ : n + 1 < n + 1 + (0 + 1)) })
              (termSucc (termSucc r))))))
      v l ↔
    ∃ z, opair z (interpretTerm V v l x) ∈ interpretTerm V v l r
Theorem: SetTheory.interpret_memRan'
Proof state before:
V : Type u_1
inst✝ : Zermelo V
r✝ x✝ y z : V
α : Type
n : Nat
v : α → V
l : Fin n → V
x r : α ⊕ Fin n
⊢ Interpret V
      (BoundedFormula.exists
        (BoundedFormula.exists
          (BoundedFormula.and
            (BoundedFormula.eqOPair (Sum.inr { val := n + 1, isLt := (_ : n + 1 < n + 1 + (0 + 1)) })
              (Sum.inr { val := n, isLt := (_ : n < n + (1 + 1)) }) (termSucc (termSucc x)))
            (BoundedFormula.mem (Sum.inr { val := n + 1, isLt := (_ : n + 1 < n + 1 + (0 + 1)) })
              (termSucc (termSucc r))))))
      v l ↔
    ∃ z, opair z (interpretTerm V v l x) ∈ interpretTerm V v l r
Tactic:
simp
Proof state after:
no goals
Theorem: SetTheory.mem_ran_iff
Proof state before:
V : Type u_1
inst✝ : Zermelo V
r x y z : V
⊢ x ∈ ran r ↔ ∃ z, opair z x ∈ r
Tactic:
unfold ran
Proof state after:
V : Type u_1
inst✝ : Zermelo V
r x y z : V
⊢ x ∈ sep (BoundedFormula.memRan (Sum.inr 0) (Sum.inl ())) (fun x => r) (⋃ ⋃ r) ↔ ∃ z, opair z x ∈ r
Theorem: SetTheory.mem_ran_iff
Proof state before:
V : Type u_1
inst✝ : Zermelo V
r x y z : V
⊢ x ∈ sep (BoundedFormula.memRan (Sum.inr 0) (Sum.inl ())) (fun x => r) (⋃ ⋃ r) ↔ ∃ z, opair z x ∈ r
Tactic:
simp only [mem_sep_iff, interpret_memRan', interpret_inr, interpret_inl,
  and_iff_right_iff_imp, forall_exists_index]
Proof state after:
V : Type u_1
inst✝ : Zermelo V
r x y z : V
⊢ ∀ (x_1 : V), opair x_1 x ∈ r → x ∈ ⋃ ⋃ r
Theorem: SetTheory.mem_ran_iff
Proof state before:
V : Type u_1
inst✝ : Zermelo V
r x y z : V
⊢ ∀ (x_1 : V), opair x_1 x ∈ r → x ∈ ⋃ ⋃ r
Tactic:
intro t
Proof state after:
V : Type u_1
inst✝ : Zermelo V
r x y z t : V
⊢ opair t x ∈ r → x ∈ ⋃ ⋃ r
Theorem: SetTheory.mem_ran_iff
Proof state before:
V : Type u_1
inst✝ : Zermelo V
r x y z t : V
⊢ opair t x ∈ r → x ∈ ⋃ ⋃ r
Tactic:
exact opair_right_mem_sUnion_sUnion
Proof state after:
no goals
Theorem: SetTheory.interpret_memRan
Proof state before:
V : Type u_1
inst✝ : Zermelo V
r✝ x✝ y z : V
α : Type
n : Nat
v : α → V
l : Fin n → V
x r : α ⊕ Fin n
⊢ Interpret V (BoundedFormula.memRan x r) v l ↔ interpretTerm V v l x ∈ ran (interpretTerm V v l r)
Tactic:
rw [mem_ran_iff, interpret_memRan']
Proof state after:
no goals
Theorem: SetTheory.interpret_memImage'
Proof state before:
V : Type u_1
inst✝ : Zermelo V
r✝ x✝ y✝ z : V
α : Type
n : Nat
v : α → V
l : Fin n → V
x y r : α ⊕ Fin n
⊢ Interpret V (BoundedFormula.memImage x y r) v l ↔
    ∃ z, z ∈ interpretTerm V v l y ∧ opair z (interpretTerm V v l x) ∈ interpretTerm V v l r
Tactic:
unfold BoundedFormula.memImage
Proof state after:
V : Type u_1
inst✝ : Zermelo V
r✝ x✝ y✝ z : V
α : Type
n : Nat
v : α → V
l : Fin n → V
x y r : α ⊕ Fin n
⊢ Interpret V
      (BoundedFormula.exists
        (BoundedFormula.exists
          (BoundedFormula.and
            (BoundedFormula.and
              (BoundedFormula.mem (Sum.inr { val := n, isLt := (_ : n < n + (1 + 1)) }) (termSucc (termSucc y)))
              (BoundedFormula.eqOPair (Sum.inr { val := n + 1, isLt := (_ : n + 1 < n + 1 + (0 + 1)) })
                (Sum.inr { val := n, isLt := (_ : n < n + (1 + 1)) }) (termSucc (termSucc x))))
            (BoundedFormula.mem (Sum.inr { val := n + 1, isLt := (_ : n + 1 < n + 1 + (0 + 1)) })
              (termSucc (termSucc r))))))
      v l ↔
    ∃ z, z ∈ interpretTerm V v l y ∧ opair z (interpretTerm V v l x) ∈ interpretTerm V v l r
Theorem: SetTheory.interpret_memImage'
Proof state before:
V : Type u_1
inst✝ : Zermelo V
r✝ x✝ y✝ z : V
α : Type
n : Nat
v : α → V
l : Fin n → V
x y r : α ⊕ Fin n
⊢ Interpret V
      (BoundedFormula.exists
        (BoundedFormula.exists
          (BoundedFormula.and
            (BoundedFormula.and
              (BoundedFormula.mem (Sum.inr { val := n, isLt := (_ : n < n + (1 + 1)) }) (termSucc (termSucc y)))
              (BoundedFormula.eqOPair (Sum.inr { val := n + 1, isLt := (_ : n + 1 < n + 1 + (0 + 1)) })
                (Sum.inr { val := n, isLt := (_ : n < n + (1 + 1)) }) (termSucc (termSucc x))))
            (BoundedFormula.mem (Sum.inr { val := n + 1, isLt := (_ : n + 1 < n + 1 + (0 + 1)) })
              (termSucc (termSucc r))))))
      v l ↔
    ∃ z, z ∈ interpretTerm V v l y ∧ opair z (interpretTerm V v l x) ∈ interpretTerm V v l r
Tactic:
aesop
Proof state after:
no goals
Theorem: SetTheory.mem_image_iff
Proof state before:
V : Type u_1
inst✝ : Zermelo V
r x y z : V
⊢ x ∈ image r y ↔ ∃ z, z ∈ y ∧ opair z x ∈ r
Tactic:
unfold image
Proof state after:
V : Type u_1
inst✝ : Zermelo V
r x y z : V
⊢ x ∈
      sep (BoundedFormula.memImage (Sum.inr 0) (Sum.inl false) (Sum.inl true)) (fun i => if i = true then r else y)
        (ran r) ↔
    ∃ z, z ∈ y ∧ opair z x ∈ r
Theorem: SetTheory.mem_image_iff
Proof state before:
V : Type u_1
inst✝ : Zermelo V
r x y z : V
⊢ x ∈
      sep (BoundedFormula.memImage (Sum.inr 0) (Sum.inl false) (Sum.inl true)) (fun i => if i = true then r else y)
        (ran r) ↔
    ∃ z, z ∈ y ∧ opair z x ∈ r
Tactic:
simp only [mem_sep_iff, mem_ran_iff, interpret_memImage']
Proof state after:
V : Type u_1
inst✝ : Zermelo V
r x y z : V
⊢ ((∃ z, opair z x ∈ r) ∧
      ∃ z,
        z ∈ interpretTerm V (fun i => if i = true then r else y) (fun x_1 => x) (Sum.inl false) ∧
          opair z (interpretTerm V (fun i => if i = true then r else y) (fun x_1 => x) (Sum.inr 0)) ∈
            interpretTerm V (fun i => if i = true then r else y) (fun x_1 => x) (Sum.inl true)) ↔
    ∃ z, z ∈ y ∧ opair z x ∈ r
Theorem: SetTheory.mem_image_iff
Proof state before:
V : Type u_1
inst✝ : Zermelo V
r x y z : V
⊢ ((∃ z, opair z x ∈ r) ∧
      ∃ z,
        z ∈ interpretTerm V (fun i => if i = true then r else y) (fun x_1 => x) (Sum.inl false) ∧
          opair z (interpretTerm V (fun i => if i = true then r else y) (fun x_1 => x) (Sum.inr 0)) ∈
            interpretTerm V (fun i => if i = true then r else y) (fun x_1 => x) (Sum.inl true)) ↔
    ∃ z, z ∈ y ∧ opair z x ∈ r
Tactic:
aesop
Proof state after:
no goals
Theorem: SetTheory.interpret_memImage
Proof state before:
V : Type u_1
inst✝ : Zermelo V
r✝ x✝ y✝ z : V
α : Type
n : Nat
v : α → V
l : Fin n → V
x y r : α ⊕ Fin n
⊢ Interpret V (BoundedFormula.memImage x y r) v l ↔
    interpretTerm V v l x ∈ image (interpretTerm V v l r) (interpretTerm V v l y)
Tactic:
rw [mem_image_iff, interpret_memImage']
Proof state after:
no goals
Theorem: SetTheory.interpret_memPreimage'
Proof state before:
V : Type u_1
inst✝ : Zermelo V
r✝ x✝ y✝ z : V
α : Type
n : Nat
v : α → V
l : Fin n → V
x y r : α ⊕ Fin n
⊢ Interpret V (BoundedFormula.memPreimage x y r) v l ↔
    ∃ z, z ∈ interpretTerm V v l y ∧ opair (interpretTerm V v l x) z ∈ interpretTerm V v l r
Tactic:
unfold BoundedFormula.memPreimage
Proof state after:
V : Type u_1
inst✝ : Zermelo V
r✝ x✝ y✝ z : V
α : Type
n : Nat
v : α → V
l : Fin n → V
x y r : α ⊕ Fin n
⊢ Interpret V
      (BoundedFormula.exists
        (BoundedFormula.exists
          (BoundedFormula.and
            (BoundedFormula.and
              (BoundedFormula.mem (Sum.inr { val := n, isLt := (_ : n < n + (1 + 1)) }) (termSucc (termSucc y)))
              (BoundedFormula.eqOPair (Sum.inr { val := n + 1, isLt := (_ : n + 1 < n + 1 + (0 + 1)) })
                (termSucc (termSucc x)) (Sum.inr { val := n, isLt := (_ : n < n + (1 + 1)) })))
            (BoundedFormula.mem (Sum.inr { val := n + 1, isLt := (_ : n + 1 < n + 1 + (0 + 1)) })
              (termSucc (termSucc r))))))
      v l ↔
    ∃ z, z ∈ interpretTerm V v l y ∧ opair (interpretTerm V v l x) z ∈ interpretTerm V v l r
Theorem: SetTheory.interpret_memPreimage'
Proof state before:
V : Type u_1
inst✝ : Zermelo V
r✝ x✝ y✝ z : V
α : Type
n : Nat
v : α → V
l : Fin n → V
x y r : α ⊕ Fin n
⊢ Interpret V
      (BoundedFormula.exists
        (BoundedFormula.exists
          (BoundedFormula.and
            (BoundedFormula.and
              (BoundedFormula.mem (Sum.inr { val := n, isLt := (_ : n < n + (1 + 1)) }) (termSucc (termSucc y)))
              (BoundedFormula.eqOPair (Sum.inr { val := n + 1, isLt := (_ : n + 1 < n + 1 + (0 + 1)) })
                (termSucc (termSucc x)) (Sum.inr { val := n, isLt := (_ : n < n + (1 + 1)) })))
            (BoundedFormula.mem (Sum.inr { val := n + 1, isLt := (_ : n + 1 < n + 1 + (0 + 1)) })
              (termSucc (termSucc r))))))
      v l ↔
    ∃ z, z ∈ interpretTerm V v l y ∧ opair (interpretTerm V v l x) z ∈ interpretTerm V v l r
Tactic:
aesop
Proof state after:
no goals
Theorem: SetTheory.mem_preimage_iff
Proof state before:
V : Type u_1
inst✝ : Zermelo V
r x y z : V
⊢ x ∈ preimage r y ↔ ∃ z, z ∈ y ∧ opair x z ∈ r
Tactic:
unfold preimage
Proof state after:
V : Type u_1
inst✝ : Zermelo V
r x y z : V
⊢ x ∈
      sep (BoundedFormula.memPreimage (Sum.inr 0) (Sum.inl false) (Sum.inl true)) (fun i => if i = true then r else y)
        (dom r) ↔
    ∃ z, z ∈ y ∧ opair x z ∈ r
Theorem: SetTheory.mem_preimage_iff
Proof state before:
V : Type u_1
inst✝ : Zermelo V
r x y z : V
⊢ x ∈
      sep (BoundedFormula.memPreimage (Sum.inr 0) (Sum.inl false) (Sum.inl true)) (fun i => if i = true then r else y)
        (dom r) ↔
    ∃ z, z ∈ y ∧ opair x z ∈ r
Tactic:
simp only [mem_sep_iff, mem_dom_iff, interpret_memPreimage']
Proof state after:
V : Type u_1
inst✝ : Zermelo V
r x y z : V
⊢ ((∃ z, opair x z ∈ r) ∧
      ∃ z,
        z ∈ interpretTerm V (fun i => if i = true then r else y) (fun x_1 => x) (Sum.inl false) ∧
          opair (interpretTerm V (fun i => if i = true then r else y) (fun x_1 => x) (Sum.inr 0)) z ∈
            interpretTerm V (fun i => if i = true then r else y) (fun x_1 => x) (Sum.inl true)) ↔
    ∃ z, z ∈ y ∧ opair x z ∈ r
Theorem: SetTheory.mem_preimage_iff
Proof state before:
V : Type u_1
inst✝ : Zermelo V
r x y z : V
⊢ ((∃ z, opair x z ∈ r) ∧
      ∃ z,
        z ∈ interpretTerm V (fun i => if i = true then r else y) (fun x_1 => x) (Sum.inl false) ∧
          opair (interpretTerm V (fun i => if i = true then r else y) (fun x_1 => x) (Sum.inr 0)) z ∈
            interpretTerm V (fun i => if i = true then r else y) (fun x_1 => x) (Sum.inl true)) ↔
    ∃ z, z ∈ y ∧ opair x z ∈ r
Tactic:
aesop
Proof state after:
no goals