rintro ⟨a, b, rfl, ha⟩
case mpr
V : Type u_1
inst✝ : Zermelo V
r x y z : V
⊢ (∃ y z, x = opair y z ∧ opair z y ∈ r) →
    x ∈ prod (ran r) (dom r) ∧
      ∃ y z,
        interpretTerm V (fun x => r) (fun x_1 => x) (Sum.inr 0) = opair y z ∧
          opair z y ∈ interpretTerm V (fun x => r) (fun x_1 => x) (Sum.inl ())
case mpr.intro.intro.intro
V : Type u_1
inst✝ : Zermelo V
r y z a b : V
ha : opair b a ∈ r
⊢ opair a b ∈ prod (ran r) (dom r) ∧
    ∃ y z,
      interpretTerm V (fun x => r) (fun x => opair a b) (Sum.inr 0) = opair y z ∧
        opair z y ∈ interpretTerm V (fun x => r) (fun x => opair a b) (Sum.inl ())