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

State before:
V : Type u_1
inst✝ : Zermelo V
r x y z s : V
hr : IsRelation r
⊢ IsRelation (rcomp s r)
Tactic:
intro x hx
State after:
V : Type u_1
inst✝ : Zermelo V
r x✝ y z s : V
hr : IsRelation r
x : V
hx : x ∈ rcomp s r
⊢ IsOPair x

State before:
V : Type u_1
inst✝ : Zermelo V
r x✝ y z s : V
hr : IsRelation r
x : V
hx : x ∈ rcomp s r
⊢ IsOPair x
Tactic:
rw [mem_rcomp_iff] at hx
State after:
V : Type u_1
inst✝ : Zermelo V
r x✝ y z s : V
hr : IsRelation r
x : V
hx : ∃ a b c, x = opair a c ∧ opair b c ∈ s ∧ opair a b ∈ r
⊢ IsOPair x

State before:
V : Type u_1
inst✝ : Zermelo V
r x✝ y z s : V
hr : IsRelation r
x : V
hx : ∃ a b c, x = opair a c ∧ opair b c ∈ s ∧ opair a b ∈ r
⊢ IsOPair x
Tactic:
aesop
State after:
no goals