Theorem: SetTheory.interpret_maps (SetTheory/Function.lean)

State before:
V : Type u_1
inst✝ : Zermelo V
r x✝ y✝ z a b c : V
α : Type
n : Nat
v : α → V
l : Fin n → V
f x y : α ⊕ Fin n
⊢ Interpret V (BoundedFormula.maps f x y) v l ↔
    opair (interpretTerm V v l x) (interpretTerm V v l y) ∈ interpretTerm V v l f
Tactic:
unfold BoundedFormula.maps
State after:
V : Type u_1
inst✝ : Zermelo V
r x✝ y✝ z a b c : V
α : Type
n : Nat
v : α → V
l : Fin n → V
f x y : α ⊕ Fin n
⊢ Interpret V
      (BoundedFormula.exists
        (BoundedFormula.and (BoundedFormula.eqOPair (Sum.inr (Fin.last n)) (termSucc x) (termSucc y))
          (BoundedFormula.mem (Sum.inr (Fin.last n)) (termSucc f))))
      v l ↔
    opair (interpretTerm V v l x) (interpretTerm V v l y) ∈ interpretTerm V v l f

State before:
V : Type u_1
inst✝ : Zermelo V
r x✝ y✝ z a b c : V
α : Type
n : Nat
v : α → V
l : Fin n → V
f x y : α ⊕ Fin n
⊢ Interpret V
      (BoundedFormula.exists
        (BoundedFormula.and (BoundedFormula.eqOPair (Sum.inr (Fin.last n)) (termSucc x) (termSucc y))
          (BoundedFormula.mem (Sum.inr (Fin.last n)) (termSucc f))))
      v l ↔
    opair (interpretTerm V v l x) (interpretTerm V v l y) ∈ interpretTerm V v l f
Tactic:
simp
State after:
no goals