Theorem: SetTheory.interpret_memDom' (SetTheory/Relation.lean)

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
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

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
State after:
no goals