Theorem: SetTheory.interpret_isRelation (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
r : α ⊕ Fin n
⊢ Interpret V (BoundedFormula.isRelation r) v l ↔ IsRelation (interpretTerm V v l r)
Tactic:
unfold BoundedFormula.isRelation IsRelation
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

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