proving cantor_injective

Stream: new members

[Joseph O]

So I have this proof, with two sorrys. I am currently worried about the first, in between the begin ... end

theorem cantor_injective {α : Type} (f : set α → α) :
  ¬function.injective f :=
begin
  set B := {x : set α | f x ∉ x},
  set B' := {y : α | ∃ x : set α, f x = y ∧ x ∈ B},
  by_contradiction,
  apply p_equiv_np_implies_false (f B' ∈ B'),
  split,
  { intros fi fn,
    have : ∃ (x : set α), f(x) = f(B') ∧ x ∈ B,
    { apply (mem_set_of.mp fi), },
    { rcases this with ⟨x, fs_eq_gB', x_in_B⟩,
      have fB'_notin_B' : f B' ∉ B' :=
      begin
        sorry,
      end,
      exact x_in_B (false.rec (f x ∈ x) (fB'_notin_B' fi)), } },
  { intro fn,
    refine mem_set_of.mpr _,
    by_contradiction,
    apply (mem_set_of.mpr fn),
    sorry, }
end

So before I start implementing it in lean, im still confused how the math proof will go.

[Eric Wieser]

That's not a #mwe (it has no imports and p_equiv_np_implies_false is presumably your own code), so it will be difficult for anyone to help you

[Notification Bot]

This topic was moved here from #maths > Stuck on mathematical proof by Eric Wieser.

[Eric Wieser]

(I've move the thread to #new members since this is more a request for help with lean and proving rather than a more in-depth question about formalizing a specific piece of math)

[Joseph O]

Eric Wieser said:

That's not a #mwe (it has no imports and p_equiv_np_implies_false is presumably your own code), so it will be difficult for anyone to help you

Sure.

import init.data.set
import set_theory.cardinal.basic

open set
open nat

lemma p_equiv_np_implies_false : ∀ P, ¬(P ↔ ¬P) :=
begin
  intro P,
  by_contradiction,
  have h := classical.em P, cases h,
  { have np := h.mp h_1,
    apply (np h_1), },
  { have p := h.mpr h_1,
    apply (h_1 p), }
end

theorem cantor_injective {α : Type} (f : set α → α) :
  ¬function.injective f :=
begin
  set B := {x : set α | f x ∉ x},
  set B' := {y : α | ∃ x : set α, f x = y ∧ x ∈ B},
  by_contradiction,
  apply p_equiv_np_implies_false (f B' ∈ B'),
  split,
  { intros fi fn,
    have : ∃ (x : set α), f(x) = f(B') ∧ x ∈ B,
    { apply (mem_set_of.mp fi), },
    { rcases this with ⟨x, fs_eq_gB', x_in_B⟩,
      have fB'_notin_B' : f B' ∉ B' :=
      begin
        sorry,
      end,
      exact x_in_B (false.rec (f x ∈ x) (fB'_notin_B' fi)), } },
  { intro fn,
    refine mem_set_of.mpr _,
    by_contradiction,
    apply (mem_set_of.mpr fn),
    sorry, }
end

[Eric Wieser]

Your proof is going nowhere - the key piece of information you have is the h introduced by by_contradiction (normally you'd write by_contradiction h to make that clear). You need to come up with a clever way to apply h. The statement is impossible to prove without h.

[Joseph O]

I havent found a way to apply h

[Eric Wieser]

I suggest you try and work that out on paper where it's sometimes easier to see you're going in circles

[Eric Wieser]

Are you trying to find a proof from scratch, or trying to formalize a "paper" one you've seen elsewhere?

[Joseph O]

Eric Wieser said:

Are you trying to find a proof from scratch, or trying to formalize a "paper" one you've seen elsewhere?

The proof I am trying to formalize currently was given to me by someone, not from a paper

[Joseph O]

This was it:

First notice that B' ⊆ A. Now suppose f(B') ∈ B, then there is X ⊆ A such that f(B') = f(X) with f(X) ∉ X, but f is injective by assumption and so B' = X. So together with f(X) ∉ X we get f(B') ∉ B'. Conversely if f(B') ∉ B' then combined with B' ⊆ A and f(B') = f(B') we have that ∃X [f(B') = f(X) ∧ f(X) ∉ X ∧ X ⊆ A], namely X = B'. But that means that f(B') ∈ B.

[Yaël Dillies]

Ah so when you wanted to prove ∃ X, f B' = f X, what you were really after was ∃ X, f B' = f X ∧ f X ∉ X!

[Joseph O]

yes!

[Joseph O]

theorem cantor_injective {α : Type} (f : set α → α) :
  ¬function.injective f :=
begin
  set B := {x : set α | f x ∉ x},
  set B' := {y : α | ∃ x : set α, f x = y ∧ x ∈ B},
  by_contradiction h,
  have : ∃ x : set α, f(x) = f(B') ∧ f(x) ∉ x,
  { sorry, },
  { sorry, }
end

i still feel like ive seen this before... am i going around in circles?

[Eric Wieser]

Note that "now suppose P (and then later not P)" is captured best with by_cases hp : P

[Eric Wieser]

In particular, your "paper" proof says you need to do that before you can construct that existential

[Joseph O]

Eric Wieser said:

Note that "now suppose P (and then later not P)" is captured best with by_cases hp : P

That would probably be by_cases hp : f(B') ∈ B',

[Joseph O]

Lets see how far in I can get

[Joseph O]

Wait this made three goals

[Joseph O]

so i closed off the first

theorem cantor_injective {α : Type} (f : set α → α) :
  ¬function.injective f :=
begin
  set B := {x : set α | f x ∉ x},
  set B' := {y : α | ∃ x : set α, f x = y ∧ x ∈ B},
  by_contradiction h,
  by_cases hp : f(B') ∈ B',
  have : ∃ x : set α, f(x) = f(B') ∧ f(x) ∉ x,
  { apply (mem_set_of.mp hp), },
  { sorry, },
  { sorry, }
end

[Arthur Paulino]

by_cases turns a goal into two. Then, when trying to prove the first, you used have without providing a proof term, which creates another goal

[Joseph O]

Makes sense

[Joseph O]

So the next part of the proof says

but f is injective by assumption and so B' = X.

this is most likely the part where we apply h, but I'm not exactly sure where and how to do that with the proof in it's current state

[Joseph O]

Any thoughts?

[Arthur Paulino]

I haven't tested your code, but if but f is injective by assumption and so B' = X. should work at this point, it sounds like the contradiction tactic to me

[Arthur Paulino]

That is, you have two contradictory hypotheses in your context

[Yaël Dillies]

have := h the_proof_that_f_B'_eq_f_X is the next step forward

[Yaël Dillies]

I don't think it's that immediate, Arthur. We still need to use injectivity.

[Arthur Paulino]

cases this with s hs, -- extracts an `s` and `hs : P s` from "exists s such that `P s`"
rw ← (h hs.1) at hp,  -- uses injectivity
have hp' := hs.2,     -- `hp': f s ∉ s`, which contradicts `hp: f s ∈ s`
contradiction,

[Joseph O]

Yaël Dillies said:

have := h the_proof_that_f_B'_eq_f_X is the next step forward

So I have to extract that proof

[Joseph O]

Arthur Paulino said:

cases this with s hs, -- extracts an `s` and `hs : P s` from "exists s such that `P s`"
rw ← (h hs.1) at hp,  -- uses injectivity
have hp' := hs.2,     -- `hp': f s ∉ s`, which contradicts `hp: f s ∈ s`
contradiction,

I never knew you could do hs.1, that's cool

[Joseph O]

Wow thanks for helping out, and I never knew the contradiction tactic existed.

[Joseph O]

Now the goal of the last sorry is

α: Type
f: set α → α
B: set (set α) := {x : set α | f x ∉ x}
B': set α := {y : α | ∃ (x : set α), f x = y ∧ x ∈ B}
h: function.injective f
hp: f B' ∉ B'
⊢ false

I would like to try to figure this one out myself, though I am a bit confused which part of the written proof this corresponds to.

[Arthur Paulino]

"Conversely if f(B') ∉ B'..."

[Arthur Paulino]

You're now on the complementary side of the by_cases tactic

[Joseph O]

Right

[Joseph O]

Then next line says we have that ∃X [f(B') = f(X) ∧ f(X) ∉ X ∧ X ⊆ A],, which is essentially have : ∃ X, f(X) = f(B') ∧ f(X) ∉ X, all over again

[Joseph O]

This is what I was able to get so far on the last part. Does it look good so far?

theorem cantor_injective {α : Type} (f : set α → α) :
  ¬function.injective f :=
begin
  set B := {x : set α | f x ∉ x},
  set B' := {y : α | ∃ x : set α, f x = y ∧ x ∈ B},
  by_contradiction h,
  by_cases hp : f(B') ∈ B',
  have : ∃ X, f(X) = f(B') ∧ f(X) ∉ X,
  { apply (mem_set_of.mp hp), },
  { cases this with s hs,
    rw ← (h hs.1) at hp,
    have hp' := hs.2,
    contradiction, },
  { have hB' : f(B') = f(B'),
    refl,
    have : ∃ X, X = B',
    sorry,
    sorry, }
end

[Arthur Paulino]

What do you want to do with hB'? It doesn't seem to bring in much value

[Joseph O]

Arthur Paulino said:

What do you want to do with hB'? It doesn't seem to bring in much value

I don't know either. I am just trying to follow the proof.

-- Conversely if f(B') ∉ B' then combined with B' ⊆ A and f(B') = f(B'),
-- we have that ∃X [f(B') = f(X) ∧ f(X) ∉ X ∧ X ⊆ A],
-- namely X = B'. But that means that f(B') ∈ B.

[Joseph O]

I also dont want to do have : ∃ X, f(X) = f(B') ∧ f(X) ∉ X, again

[Arthur Paulino]

Then place it before by_cases (and bring its proof along)

[Joseph O]

Oh ok

[Joseph O]

But then things get really moved around

[Joseph O]

Like for this goal:

α: Type
f: set α → α
B: set (set α) := {x : set α | f x ∉ x}
B': set α := {y : α | ∃ (x : set α), f x = y ∧ x ∈ B}
h: function.injective f
this: ∃ (X : set α), f X = f B' ∧ f X ∉ X
⊢ false

this proof doesnt work anymore because the is no hp anymore

cases this with s hs,
    rw ← (h hs.1) at hp,
    have hp' := hs.2,
    contradiction,

[Arthur Paulino]

Wait, if you need f(B') ∈ B' to be true in order to prove that ∃ X, f(X) = f(B') ∧ f(X) ∉ X then how would you prove it in the other by_cases section, supposing you were willing to do it "all over again"?

[Joseph O]

@Arthur Paulino well we have these three goals:

3 goals
α: Type
f: set α → α
B: set (set α) := {x : set α | f x ∉ x}
B': set α := {y : α | ∃ (x : set α), f x = y ∧ x ∈ B}
h: function.injective f
hp: f B' ∈ B'
⊢ ∃ (X : set α), f X = f B' ∧ f X ∉ X
α: Type
f: set α → α
B: set (set α) := {x : set α | f x ∉ x}
B': set α := {y : α | ∃ (x : set α), f x = y ∧ x ∈ B}
h: function.injective f
hp: f B' ∉ B'
⊢ ∃ (X : set α), f X = f B' ∧ f X ∉ X
α: Type
f: set α → α
B: set (set α) := {x : set α | f x ∉ x}
B': set α := {y : α | ∃ (x : set α), f x = y ∧ x ∈ B}
h: function.injective f
this: ∃ (X : set α), f X = f B' ∧ f X ∉ X
⊢ false

[Arthur Paulino]

Hm, can you come up with a proof of your own? I feel like syntactically following that proof (rather than semantically) is getting you more lost

[Joseph O]

I don't have a proof of my own.

[Arthur Paulino]

Can you write the one you have with your own words? As if you were explaining it to someone

[Joseph O]

Ok so going back to

theorem cantor_injective {α : Type} (f : set α → α) :
  ¬function.injective f :=
begin
  set B := {x : set α | f x ∉ x},
  set B' := {y : α | ∃ x : set α, f x = y ∧ x ∈ B},
  by_contradiction h,
  by_cases hp : f(B') ∈ B',
  have : ∃ X, f(X) = f(B') ∧ f(X) ∉ X,
  { apply (mem_set_of.mp hp), },
  { cases this with s hs,
    rw ← (h hs.1) at hp,
    have hp' := hs.2,
    contradiction, },
  { have : ∃ X, X = B',
    { exact exists_eq, },
    { sorry, } }
end

the last sorry has a goal of

α: Type
f: set α → α
B: set (set α) := {x : set α | f x ∉ x}
B': set α := {y : α | ∃ (x : set α), f x = y ∧ x ∈ B}
h: function.injective f
hp: f B' ∉ B'
this: ∃ (X : set α), X = B'
⊢ false

and this corresponds with

namely X = B'. But that means that f(B') ∈ B.

Do you know how to get f(B') ∈ B out of the current goal

[Yaël Dillies]

exact hp

[Joseph O]

That doesnt work.

[Joseph O]

invalid type ascription, term has type
  f B' ∉ B'
but is expected to have type
  false

[Arthur Paulino]

Your proof starts off as "First notice that B' ⊆ A". What is A?

[Eric Wieser]

I think it's set.univ : set α

[Eric Wieser]

@Joseph O, note that when you use by_cases it splits into two goals - you should have two pairs of {} at that point to keep things clear

[Arthur Paulino]

:point_up:

import set_theory.cardinal.basic

open set

theorem cantor_injective {α : Type} (f : set α → α) :
  ¬function.injective f :=
begin
  set B := {x : set α | f x ∉ x},
  set B' := {y : α | ∃ x : set α, f x = y ∧ x ∈ B},
  by_contradiction h,
  by_cases hp : f(B') ∈ B',
  { have : ∃ X, f(X) = f(B') ∧ f(X) ∉ X := mem_set_of.mp hp,
    cases this with s hs,
    rw ← (h hs.1) at hp,
    have hp' := hs.2,
    contradiction, },
  { have : ∃ X, X = B' := exists_eq,
    sorry, }
end

[Joseph O]

Oh right I see, that was my mistake

[Joseph O]

Thanks

[Joseph O]

Im still confused on how to translate But that means that f(B') ∈ B. into lean

[Joseph O]

From

{ have : ∃ X, X = B' := exists_eq,
    sorry, }

[Arthur Paulino]

Do you understand why that is so in a math level? Note: I'm not claiming that it's true nor that I understand. I'm just saying that this will be a super hard task if you don't see it as true and understand precisely why it is

[Joseph O]

Well we have this hypothesis: hp: f B' ∉ B', which seems contradictory

[Arthur Paulino]

Why is it so?

[Joseph O]

Because we are saying that f B' ∈ B'

[Joseph O]

or we are trying to prove that

[Joseph O]

Well, what im confused is how they got f B' ∈ B' from X = B'

[Joseph O]

Did it say anywhere that f X ∈ X

[Arthur Paulino]

Joseph O said:

Because we are saying that f B' ∈ B'

Are you talking about hp? Because by_cases hp : ⋯ is not like saying that hp is true. It's a way to prove what you want in both scenarios (when it's true and when it's false)

[Joseph O]

Well does this look correct so far?

theorem cantor_injective {α : Type} (f : set α → α) :
  ¬function.injective f :=
begin
  set B := {x : set α | f x ∉ x},
  set B' := {y : α | ∃ x : set α, f x = y ∧ x ∈ B},
  by_contradiction h,
  by_cases hp : f(B') ∈ B',
  { have : ∃ X, f(X) = f(B') ∧ f(X) ∉ X := mem_set_of.mp hp,
    cases this with s hs,
    rw ← (h hs.1) at hp,
    have hp' := hs.2,
    contradiction, },
  { have : ∃ X, X = B' := exists_eq,
    cases this with X hXB',
    have hI : f(X) ∈ X,
    { sorry, },
    { rw hXB' at hI,
      contradiction, } }
end

the goal of the last sorry is

α: Type
f: set α → α
B: set (set α) := {x : set α | f x ∉ x}
B': set α := {y : α | ∃ (x : set α), f x = y ∧ x ∈ B}
h: function.injective f
hp: f B' ∉ B'
X: set α
hXB': X = B'
⊢ f X ∈ X

which I have no idea how to prove

[Arthur Paulino]

Joseph O said:

Well, what im confused is how they got f B' ∈ B' from X = B'

If that part of the proof is too mysterious for you, then ask for more detailed steps. Think of it as a convincing game. You're trying to prove something you're not convinced of. And this path is a painful one

[Arthur Paulino]

Once you're convinced, then you'll have a better chance at convincing a machine

[Joseph O]

Sure Im asking them about it

[Ruben Van de Velde]

I feel like introducing X here only confuses things - do you agree the proof is finished if you can prove f B' ∈ B'?

[Joseph O]

Ruben Van de Velde said:

I feel like introducing X here only confuses things - do you agree the proof is finished if you can prove f B' ∈ B'?

Yes

[Joseph O]

Now the question is how do we prove that.

[Ruben Van de Velde]

If you need to prove that something is an element of a set defined by { a | something about a }, the lemma set.mem_set_of_eq is a good first step

[Joseph O]

B' is defined as set B' := {y : α | ∃ x : set α, f x = y ∧ x ∈ B}, so would it work?

[Joseph O]

Because with

have : f(B') ∈ B' :=
    begin
      mem_set_of_eq,
    end,

i get sortof an ugly error

[Joseph O]

type mismatch at application
  tactic.istep 54 6 54 6 182 mem_set_of_eq
term
  mem_set_of_eq
has type
  ?m_2 ∈ {x : ?m_1 | ?m_3 x} = ?m_3 ?m_2 : Prop
but is expected to have type
  tactic ?m_1 : Type ?
state:
α : Type,
f : set α → α,
B : set (set α) := {x : set α | f x ∉ x},
B' : set α := {y : α | ∃ (x : set α), f x = y ∧ x ∈ B},
h : function.injective f,
hp : f B' ∉ B'
⊢ false

[Ruben Van de Velde]

Right, mem_set_of_eq is a lemma, so you'd write rw mem_set_of_eq

[Joseph O]

Oh right

[Joseph O]

Now our goal is

α: Type
f: set α → α
B: set (set α) := {x : set α | f x ∉ x}
B': set α := {y : α | ∃ (x : set α), f x = y ∧ x ∈ B}
h: function.injective f
hp: f B' ∉ B'
⊢ ∃ (x : set α), f x = f B' ∧ x ∈ B

[Ruben Van de Velde]

Okay, so how do you prove an existential?

[Joseph O]

mem_set_of

[Joseph O]

I believe

[Arthur Paulino]

How would you prove this?

example : ∃ n : ℕ, n + n = 10 :=
begin
  sorry,
end

[Joseph O]

I honestly dont know.

[Joseph O]

Is there a tactic for that?

[Ruben Van de Velde]

Generally, the easiest way to prove something exists with some property is by saying "look, this object works", and the tactic is use B'

[Ruben Van de Velde]

Or in Arthur's example, use 5

[Joseph O]

I see.

[Joseph O]

Now the goal is

α: Type
f: set α → α
B: set (set α) := {x : set α | f x ∉ x}
B': set α := {y : α | ∃ (x : set α), f x = y ∧ x ∈ B}
h: function.injective f
hp: f B' ∉ B'
⊢ f B' = f B' ∧ B' ∈ B

[Arthur Paulino]

If you do use 5 Lean will close the goal automatically because the property is too simple. But that's not always the case. If Lean can't prove the property automatically, it will turn the property into a goal for you to prove it

[Joseph O]

Joseph O said:

Now the goal is

α: Type
f: set α → α
B: set (set α) := {x : set α | f x ∉ x}
B': set α := {y : α | ∃ (x : set α), f x = y ∧ x ∈ B}
h: function.injective f
hp: f B' ∉ B'
⊢ f B' = f B' ∧ B' ∈ B

If we split the goal the first can be proved with refl, but the second...

[Ruben Van de Velde]

The second is again of the form something in { ... | ... }

[Joseph O]

Oh we can use mem_set_of_eq

[Joseph O]

Ok i proved it

have : f(B') ∈ B' :=
    begin
      rw mem_set_of_eq,
      use B',
      split,
      { refl, },
      { rw mem_set_of_eq,
        exact hp, }
    end,

[Joseph O]

The final proof, completed!

theorem cantor_injective {α : Type} (f : set α → α) :
  ¬function.injective f :=
begin
  set B := {x : set α | f x ∉ x},
  set B' := {y : α | ∃ x : set α, f x = y ∧ x ∈ B},
  by_contradiction h,
  by_cases hp : f(B') ∈ B',
  { have : ∃ X, f(X) = f(B') ∧ f(X) ∉ X := mem_set_of.mp hp,
    cases this with s hs,
    rw ← (h hs.1) at hp,
    have hp' := hs.2,
    contradiction, },
  { have : f(B') ∈ B' :=
    begin
      rw mem_set_of_eq,
      use B',
      split,
      { refl, },
      { rw mem_set_of_eq,
        exact hp, }
    end,
    contradiction, }
end

[Joseph O]

and lean says its correct!

[Ruben Van de Velde]

(I'm not sure why we have both mem_set_of and mem_set_of_eq, but either works here)

[Arthur Paulino]

This is the formatting you'll see more often in mathlib:

theorem cantor_injective {α : Type} (f : set α → α) :
  ¬function.injective f :=
begin
  set B := {x : set α | f x ∉ x},
  set B' := {y : α | ∃ x : set α, f x = y ∧ x ∈ B},
  by_contradiction h,
  by_cases hp : f(B') ∈ B',
  { have : ∃ X, f(X) = f(B') ∧ f(X) ∉ X := mem_set_of.mp hp,
    cases this with s hs,
    rw ← (h hs.1) at hp,
    have hp' := hs.2,
    contradiction, },
  { have : f(B') ∈ B',
    { rw mem_set_of_eq,
      use B',
      split,
      { refl, },
      { rw mem_set_of_eq,
        exact hp, }, },
    contradiction, },
end

[Eric Wieser]

(docs#set.mem_set_of_eq is in core, and stated weirdly; docs#set.mem_set_of is newer and is less weird)

[Joseph O]

Yeah I switched them all to mem_set_of

[Arthur Paulino]

Now this is something I recall reading from one of those backstage interviews: that sometimes the focus on typechecking can obfuscate the bigger mathematical picture. Now that you've proven it in Lean, would you be able to write a proof of your own, with your words?

[Arthur Paulino]

Not that I'm saying that you should post it here. It's an investigation that you can do on your own. It's definitely something I do

[Ruben Van de Velde]

Optional: you might be able to learn some tricks by comparing your version with this shorter version:

theorem cantor_injective {α : Type} (f : set α → α) :
  ¬function.injective f :=
begin
  set B := {x : set α | f x ∉ x},
  set B' := {y : α | ∃ x : set α, f x = y ∧ x ∈ B},
  intro h,
  by_cases hp : f B' ∈ B',
  { obtain ⟨s, hs⟩ : ∃ X, f X = f B' ∧ f X ∉ X := set.mem_set_of_eq.mp hp,
    rw ← (h hs.1) at hp,
    exact hs.2 hp, },
  { exact hp ⟨B', rfl, hp⟩, }
end

[Joseph O]

Oh man thats crazy

[Joseph O]

Ruben Van de Velde said:

Optional: you might be able to learn some tricks by comparing your version with this shorter version:

theorem cantor_injective {α : Type} (f : set α → α) :
  ¬function.injective f :=
begin
  set B := {x : set α | f x ∉ x},
  set B' := {y : α | ∃ x : set α, f x = y ∧ x ∈ B},
  intro h,
  by_cases hp : f B' ∈ B',
  { obtain ⟨s, hs⟩ : ∃ X, f X = f B' ∧ f X ∉ X := set.mem_set_of_eq.mp hp,
    rw ← (h hs.1) at hp,
    exact hs.2 hp, },
  { exact hp ⟨B', rfl, hp⟩, }
end

Ill keep this on the side as a shorter variation, though I will stick to my version for now as a beginner and its more expressive despite being verbose

[Joseph O]

deleted

[Joseph O]

There are so many things I dont understand about the proof though

[Joseph O]

Well actually I understand it

[Joseph O]

My biggest question is how

⟨B', rfl, hp⟩

is equivalent to

have : f(B') ∈ B',
    { rw mem_set_of,
      use B',
      split,
      { refl, },
      { rw mem_set_of,
        exact hp, }, },

[Joseph O]

Thats it

[Yaël Dillies]

rw mem_set_of is a "no-op" because its proof is iff.rfl, that is both sides are definitionally equal. use B', is the same as refine ⟨B', _⟩, split is the same as refine ⟨_, _⟩.

[Joseph O]

That makes sense, though Im still confused how rw mem_set_of is implicitly applied

[Yaël Dillies]

It's not applied or anything. It's simply that, when you give Lean something, it tries to "unify" it, which means performing a bunch of operations, notably replacing everything by its definition.

[Yaël Dillies]

The definition of f B' ∈ B' is f B' ∈ {y : α | ∃ x : set α, f x = y ∧ x ∈ B}, whose definition is ∃ x : set α, f x = f B' ∧ x ∈ B}.