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

State before:
V : Type u_1
inst✝ : Zermelo V
r x y z s : V
h : ran r ⊆ dom s
⊢ dom (rcomp s r) = dom r
Tactic:
ext t
State after:
case h
V : Type u_1
inst✝ : Zermelo V
r x y z s : V
h : ran r ⊆ dom s
t : V
⊢ t ∈ dom (rcomp s r) ↔ t ∈ dom r

State before:
case h
V : Type u_1
inst✝ : Zermelo V
r x y z s : V
h : ran r ⊆ dom s
t : V
⊢ t ∈ dom (rcomp s r) ↔ t ∈ dom r
Tactic:
simp only [mem_dom_iff, mem_rcomp_iff, opair_injective]
State after:
case h
V : Type u_1
inst✝ : Zermelo V
r x y z s : V
h : ran r ⊆ dom s
t : V
⊢ (∃ z a b c, (t = a ∧ z = c) ∧ opair b c ∈ s ∧ opair a b ∈ r) ↔ ∃ z, opair t z ∈ r

State before:
case h
V : Type u_1
inst✝ : Zermelo V
r x y z s : V
h : ran r ⊆ dom s
t : V
⊢ (∃ z a b c, (t = a ∧ z = c) ∧ opair b c ∈ s ∧ opair a b ∈ r) ↔ ∃ z, opair t z ∈ r
Tactic:
constructor
State after:
case h.mp
V : Type u_1
inst✝ : Zermelo V
r x y z s : V
h : ran r ⊆ dom s
t : V
⊢ (∃ z a b c, (t = a ∧ z = c) ∧ opair b c ∈ s ∧ opair a b ∈ r) → ∃ z, opair t z ∈ r

case h.mpr
V : Type u_1
inst✝ : Zermelo V
r x y z s : V
h : ran r ⊆ dom s
t : V
⊢ (∃ z, opair t z ∈ r) → ∃ z a b c, (t = a ∧ z = c) ∧ opair b c ∈ s ∧ opair a b ∈ r

State before:
case h.mp
V : Type u_1
inst✝ : Zermelo V
r x y z s : V
h : ran r ⊆ dom s
t : V
⊢ (∃ z a b c, (t = a ∧ z = c) ∧ opair b c ∈ s ∧ opair a b ∈ r) → ∃ z, opair t z ∈ r
Tactic:
rintro ⟨z, _, b, _, ⟨rfl, rfl⟩, _, hc⟩
State after:
case h.mp.intro.intro.intro.intro.intro.intro.intro
V : Type u_1
inst✝ : Zermelo V
r x y z✝ s : V
h : ran r ⊆ dom s
t z b : V
left✝ : opair b z ∈ s
hc : opair t b ∈ r
⊢ ∃ z, opair t z ∈ r

State before:
case h.mp.intro.intro.intro.intro.intro.intro.intro
V : Type u_1
inst✝ : Zermelo V
r x y z✝ s : V
h : ran r ⊆ dom s
t z b : V
left✝ : opair b z ∈ s
hc : opair t b ∈ r
⊢ ∃ z, opair t z ∈ r
Tactic:
exact ⟨_, hc⟩
State after:
no goals

State before:
case h.mpr
V : Type u_1
inst✝ : Zermelo V
r x y z s : V
h : ran r ⊆ dom s
t : V
⊢ (∃ z, opair t z ∈ r) → ∃ z a b c, (t = a ∧ z = c) ∧ opair b c ∈ s ∧ opair a b ∈ r
Tactic:
rintro ⟨b, hb⟩
State after:
case h.mpr.intro
V : Type u_1
inst✝ : Zermelo V
r x y z s : V
h : ran r ⊆ dom s
t b : V
hb : opair t b ∈ r
⊢ ∃ z a b c, (t = a ∧ z = c) ∧ opair b c ∈ s ∧ opair a b ∈ r

State before:
case h.mpr.intro
V : Type u_1
inst✝ : Zermelo V
r x y z s : V
h : ran r ⊆ dom s
t b : V
hb : opair t b ∈ r
⊢ ∃ z a b c, (t = a ∧ z = c) ∧ opair b c ∈ s ∧ opair a b ∈ r
Tactic:
have : b ∈ ran r := by
  rw [mem_ran_iff]
  exact ⟨t, hb⟩
State after:
case h.mpr.intro
V : Type u_1
inst✝ : Zermelo V
r x y z s : V
h : ran r ⊆ dom s
t b : V
hb : opair t b ∈ r
this : b ∈ ran r
⊢ ∃ z a b c, (t = a ∧ z = c) ∧ opair b c ∈ s ∧ opair a b ∈ r

State before:
case h.mpr.intro
V : Type u_1
inst✝ : Zermelo V
r x y z s : V
h : ran r ⊆ dom s
t b : V
hb : opair t b ∈ r
this : b ∈ ran r
⊢ ∃ z a b c, (t = a ∧ z = c) ∧ opair b c ∈ s ∧ opair a b ∈ r
Tactic:
have := h this
State after:
case h.mpr.intro
V : Type u_1
inst✝ : Zermelo V
r x y z s : V
h : ran r ⊆ dom s
t b : V
hb : opair t b ∈ r
this✝ : b ∈ ran r
this : b ∈ dom s
⊢ ∃ z a b c, (t = a ∧ z = c) ∧ opair b c ∈ s ∧ opair a b ∈ r

State before:
case h.mpr.intro
V : Type u_1
inst✝ : Zermelo V
r x y z s : V
h : ran r ⊆ dom s
t b : V
hb : opair t b ∈ r
this✝ : b ∈ ran r
this : b ∈ dom s
⊢ ∃ z a b c, (t = a ∧ z = c) ∧ opair b c ∈ s ∧ opair a b ∈ r
Tactic:
rw [mem_dom_iff] at this
State after:
case h.mpr.intro
V : Type u_1
inst✝ : Zermelo V
r x y z s : V
h : ran r ⊆ dom s
t b : V
hb : opair t b ∈ r
this✝ : b ∈ ran r
this : ∃ z, opair b z ∈ s
⊢ ∃ z a b c, (t = a ∧ z = c) ∧ opair b c ∈ s ∧ opair a b ∈ r

State before:
case h.mpr.intro
V : Type u_1
inst✝ : Zermelo V
r x y z s : V
h : ran r ⊆ dom s
t b : V
hb : opair t b ∈ r
this✝ : b ∈ ran r
this : ∃ z, opair b z ∈ s
⊢ ∃ z a b c, (t = a ∧ z = c) ∧ opair b c ∈ s ∧ opair a b ∈ r
Tactic:
obtain ⟨z, hz⟩ := this
State after:
case h.mpr.intro.intro
V : Type u_1
inst✝ : Zermelo V
r x y z✝ s : V
h : ran r ⊆ dom s
t b : V
hb : opair t b ∈ r
this : b ∈ ran r
z : V
hz : opair b z ∈ s
⊢ ∃ z a b c, (t = a ∧ z = c) ∧ opair b c ∈ s ∧ opair a b ∈ r

State before:
case h.mpr.intro.intro
V : Type u_1
inst✝ : Zermelo V
r x y z✝ s : V
h : ran r ⊆ dom s
t b : V
hb : opair t b ∈ r
this : b ∈ ran r
z : V
hz : opair b z ∈ s
⊢ ∃ z a b c, (t = a ∧ z = c) ∧ opair b c ∈ s ∧ opair a b ∈ r
Tactic:
exact ⟨z, _, b, _, ⟨rfl, rfl⟩, hz, hb⟩
State after:
no goals

State before:
V : Type u_1
inst✝ : Zermelo V
r x y z s : V
h : ran r ⊆ dom s
t b : V
hb : opair t b ∈ r
⊢ b ∈ ran r
Tactic:
rw [mem_ran_iff]
State after:
V : Type u_1
inst✝ : Zermelo V
r x y z s : V
h : ran r ⊆ dom s
t b : V
hb : opair t b ∈ r
⊢ ∃ z, opair z b ∈ r

State before:
V : Type u_1
inst✝ : Zermelo V
r x y z s : V
h : ran r ⊆ dom s
t b : V
hb : opair t b ∈ r
⊢ ∃ z, opair z b ∈ r
Tactic:
exact ⟨t, hb⟩
State after:
no goals