Proof of a theorem in first order logic using indirect proof

Question

I want to prove the theorem ∃x(A(x)→∀x A(x)). Because it is a theorem, it has no premises. The hint in the textbook says to only use the basic rules of TFL (truth-functional logic) and basic quantifier rules. It also says that it requires the use of IP (indirect proof). Thus, I know I probably shouldn't use identity rules but I don't see another way how. I have tried the following proof:

1     -∃x(P(x) → ∀xP(x)):Assumption
2         P(a):Assumption
3             -P(b):Assumption
4                 a=b:Assumption
5                 a=a:=Intro
6                 b=a:=Elim lines 4,5
7             a=b->b=a:-> Intro lines 4-6
8                 -a=b:Assumption
9                 I'm stuck here
10                !?:Negation Elim, I plan on using
11            a=b:IP lines 8-10
12            P(b):= Elim lines 2,11
13            !?:Negation Elim lines 3,12
14        P(b):IP lines 3-13
15        AxP(x):Universal Intro line 14
16    P(a)->AxP(x):->Intro lines 2-15
17    ∃x(P(x) → ∀xP(x)):Existential Intro line 16
18    !?:Negation Elim lines 1,17
19 ∃x(P(x) → ∀xP(x)): IP lines 1-18

I'm stuck on line 9 but I don't think I should even be using identity rules. So I think most of my proof is wrong anyways. Thanks for any guidance on this proof.

Answer 1

Right... don’t use identity rules. Here’s a hint: within this IP, do another IP, assuming $\forall x \ A(x)$. That quickly leads to a contradiction, so now you have $\neg \forall x \ A(x)$, and from that you can derive (using another IP) $\exists x \ \neg A(x)$, and using that you can get the contradiction for the outside IP to complete the proof