simp only [mem_ran_iff, mem_rcomp_iff, opair_injective]
V : Type u_1
inst✝ : Zermelo V
r x y z s t : V
⊢ t ∈ ran (rcomp s r) → t ∈ ran s
V : Type u_1
inst✝ : Zermelo V
r x y z s t : V
⊢ (∃ z a b c, (z = a ∧ t = c) ∧ opair b c ∈ s ∧ opair a b ∈ r) → ∃ z, opair z t ∈ s