Theorem: SetTheory.interpret_isFunction (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 : α ⊕ Fin n
⊢ Interpret V (BoundedFormula.isFunction f) v l ↔ IsFunction (interpretTerm V v l f)
Tactic:
unfold BoundedFormula.isFunction IsFunction
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 : α ⊕ Fin n
⊢ Interpret V
      (BoundedFormula.and (BoundedFormula.isRelation f)
        (BoundedFormula.all
          (BoundedFormula.all
            (BoundedFormula.all
              (BoundedFormula.all
                (BoundedFormula.all
                  (BoundedFormula.imp
                    (BoundedFormula.eqOPair (Sum.inr { val := n + 3, isLt := (_ : n + 3 < n + 3 + (1 + 1)) })
                      (Sum.inr { val := n, isLt := (_ : n < n + (4 + 1)) })
                      (Sum.inr { val := n + 1, isLt := (_ : n + 1 < n + 1 + (3 + 1)) }))
                    (BoundedFormula.imp
                      (BoundedFormula.eqOPair (Sum.inr { val := n + 4, isLt := (_ : n + 4 < n + 4 + (0 + 1)) })
                        (Sum.inr { val := n, isLt := (_ : n < n + (4 + 1)) })
                        (Sum.inr { val := n + 2, isLt := (_ : n + 2 < n + 2 + (2 + 1)) }))
                      (BoundedFormula.imp
                        (BoundedFormula.mem (Sum.inr { val := n + 3, isLt := (_ : n + 3 < n + 3 + (1 + 1)) })
                          (termSucc (termSucc (termSucc (termSucc (termSucc f))))))
                        (BoundedFormula.imp
                          (BoundedFormula.mem (Sum.inr { val := n + 4, isLt := (_ : n + 4 < n + 4 + (0 + 1)) })
                            (termSucc (termSucc (termSucc (termSucc (termSucc f))))))
                          (BoundedFormula.eq (Sum.inr { val := n + 1, isLt := (_ : n + 1 < n + 1 + (3 + 1)) })
                            (Sum.inr { val := n + 2, isLt := (_ : n + 2 < n + 2 + (2 + 1)) }))))))))))))
      v l ↔
    IsRelation (interpretTerm V v l f) ∧
      ∀ (x s t : V), opair x s ∈ interpretTerm V v l f → opair x t ∈ interpretTerm V v l f → s = t

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 : α ⊕ Fin n
⊢ Interpret V
      (BoundedFormula.and (BoundedFormula.isRelation f)
        (BoundedFormula.all
          (BoundedFormula.all
            (BoundedFormula.all
              (BoundedFormula.all
                (BoundedFormula.all
                  (BoundedFormula.imp
                    (BoundedFormula.eqOPair (Sum.inr { val := n + 3, isLt := (_ : n + 3 < n + 3 + (1 + 1)) })
                      (Sum.inr { val := n, isLt := (_ : n < n + (4 + 1)) })
                      (Sum.inr { val := n + 1, isLt := (_ : n + 1 < n + 1 + (3 + 1)) }))
                    (BoundedFormula.imp
                      (BoundedFormula.eqOPair (Sum.inr { val := n + 4, isLt := (_ : n + 4 < n + 4 + (0 + 1)) })
                        (Sum.inr { val := n, isLt := (_ : n < n + (4 + 1)) })
                        (Sum.inr { val := n + 2, isLt := (_ : n + 2 < n + 2 + (2 + 1)) }))
                      (BoundedFormula.imp
                        (BoundedFormula.mem (Sum.inr { val := n + 3, isLt := (_ : n + 3 < n + 3 + (1 + 1)) })
                          (termSucc (termSucc (termSucc (termSucc (termSucc f))))))
                        (BoundedFormula.imp
                          (BoundedFormula.mem (Sum.inr { val := n + 4, isLt := (_ : n + 4 < n + 4 + (0 + 1)) })
                            (termSucc (termSucc (termSucc (termSucc (termSucc f))))))
                          (BoundedFormula.eq (Sum.inr { val := n + 1, isLt := (_ : n + 1 < n + 1 + (3 + 1)) })
                            (Sum.inr { val := n + 2, isLt := (_ : n + 2 < n + 2 + (2 + 1)) }))))))))))))
      v l ↔
    IsRelation (interpretTerm V v l f) ∧
      ∀ (x s t : V), opair x s ∈ interpretTerm V v l f → opair x t ∈ interpretTerm V v l f → s = t
Tactic:
aesop
State after:
no goals