Theorem: SetTheory.mem_image_iff (SetTheory/Relation.lean)

State before:
V : Type u_1
inst✝ : Zermelo V
r x y z : V
⊢ x ∈ image r y ↔ ∃ z, z ∈ y ∧ opair z x ∈ r
Tactic:
unfold image
State after:
V : Type u_1
inst✝ : Zermelo V
r x y z : V
⊢ x ∈
      sep (BoundedFormula.memImage (Sum.inr 0) (Sum.inl false) (Sum.inl true)) (fun i => if i = true then r else y)
        (ran r) ↔
    ∃ z, z ∈ y ∧ opair z x ∈ r

State before:
V : Type u_1
inst✝ : Zermelo V
r x y z : V
⊢ x ∈
      sep (BoundedFormula.memImage (Sum.inr 0) (Sum.inl false) (Sum.inl true)) (fun i => if i = true then r else y)
        (ran r) ↔
    ∃ z, z ∈ y ∧ opair z x ∈ r
Tactic:
simp only [mem_sep_iff, mem_ran_iff, interpret_memImage']
State after:
V : Type u_1
inst✝ : Zermelo V
r x y z : V
⊢ ((∃ z, opair z x ∈ r) ∧
      ∃ z,
        z ∈ interpretTerm V (fun i => if i = true then r else y) (fun x_1 => x) (Sum.inl false) ∧
          opair z (interpretTerm V (fun i => if i = true then r else y) (fun x_1 => x) (Sum.inr 0)) ∈
            interpretTerm V (fun i => if i = true then r else y) (fun x_1 => x) (Sum.inl true)) ↔
    ∃ z, z ∈ y ∧ opair z x ∈ r

State before:
V : Type u_1
inst✝ : Zermelo V
r x y z : V
⊢ ((∃ z, opair z x ∈ r) ∧
      ∃ z,
        z ∈ interpretTerm V (fun i => if i = true then r else y) (fun x_1 => x) (Sum.inl false) ∧
          opair z (interpretTerm V (fun i => if i = true then r else y) (fun x_1 => x) (Sum.inr 0)) ∈
            interpretTerm V (fun i => if i = true then r else y) (fun x_1 => x) (Sum.inl true)) ↔
    ∃ z, z ∈ y ∧ opair z x ∈ r
Tactic:
aesop
State after:
no goals