Theorem: SetTheory.interpret_isPair (SetTheory/OPair.lean)

State before:
V : Type u_1
inst✝ : Zermelo V
x✝ y z : V
α : Type
n : Nat
v : α → V
l : Fin n → V
x : α ⊕ Fin n
⊢ Interpret V (BoundedFormula.isPair x) v l ↔ IsPair (interpretTerm V v l x)
Tactic:
unfold BoundedFormula.isPair IsPair
State after:
V : Type u_1
inst✝ : Zermelo V
x✝ y z : V
α : Type
n : Nat
v : α → V
l : Fin n → V
x : α ⊕ Fin n
⊢ Interpret V
      (BoundedFormula.exists
        (BoundedFormula.exists
          (BoundedFormula.eqPair (termSucc (termSucc x)) (Sum.inr { val := n, isLt := (_ : n < n + (1 + 1)) })
            (Sum.inr (Fin.last (n + 1))))))
      v l ↔
    ∃ y z, interpretTerm V v l x = pair y z

State before:
V : Type u_1
inst✝ : Zermelo V
x✝ y z : V
α : Type
n : Nat
v : α → V
l : Fin n → V
x : α ⊕ Fin n
⊢ Interpret V
      (BoundedFormula.exists
        (BoundedFormula.exists
          (BoundedFormula.eqPair (termSucc (termSucc x)) (Sum.inr { val := n, isLt := (_ : n < n + (1 + 1)) })
            (Sum.inr (Fin.last (n + 1))))))
      v l ↔
    ∃ y z, interpretTerm V v l x = pair y z
Tactic:
simp
State after:
no goals