# Mechanically proving element non-membership

I'm facing a (possibly simple) problem while proving a theorem.

I need to show that under several (true) assumptions, some element is not in a set. Such assumptions are all met and there is are lemmata that can be employed to reach the conclusion. The problem comes from the fact that the lemma for doing so must be applied an arbitrary number of times.

Lemma 1: $$\forall x:\big(x\in X \iff P(x) \big)$$

Lemma 2: $$\forall x,y : (P(x) \land Q(y) \land x\neq y) \Rightarrow qq \neq x$$

Lemma 3: $$\forall x : P(x) \Rightarrow Q(x)$$

Assumption: $$\vert X\vert=k \land k\ge 2 %\big(\forall x\in X.P(x)\big)$$

Desired result: $$qq\not\in X$$

What i tried so far:

Proof: Intuitively, it is easy to see that $$qq\not\in X$$ because I can choose two elements $$a$$ and $$b$$ of $$X$$ (they are distinct by definition), plug them in lemma 2, and get that $$qq\neq a$$. If we apply this idea $$k$$ times we get that $$qq$$ is not an element of $$X$$, hence it is not in $$X$$. $$\Box$$

When $$k=2$$ or bounded, this reasoning works.

The problem: $$k$$ is not known in advance and I can not mechanically apply Lemma 2 arbitrarily many times.

How can I prove this intuitive fact in a mechanical fashion? I've been (vaguely) suggested to employ a bijection but i still don't see how to do so.

• Is the issue that $X$ might not be countable? Because induction will work for a finite or countably infinite $X$. (Whenever you notice "If we apply this idea $k$ times, it works", try induction.) Aug 18, 2021 at 14:16
• I will give it a try, perhaps it's simpler than i think. Aug 18, 2021 at 19:21
• In my domain of discourse $X$ is countable and finite. Aug 18, 2021 at 20:28
• @j_random_hacker Induction is not going to cut it. The inductive hyp. ceases to hold very quickly. Aug 23, 2021 at 19:26
• What is your inductive hypothesis, and what are your base case(s)? Aug 24, 2021 at 2:27

The actual (mechanical) solution did require the employment of an inductive predicate that allows the human prover to instantiate the inductive hypothesis to a set $$X'$$.