MHB Help with Logic Proof: Establishing 7.

[agapito]

Consider the following proof from Copi's "Symbolic Logic", p. 109:

1. (∃x) ¬Fx Assumption

2. ¬Fy Assumption

3. (∀x) Fx Assumption

4. Fy 3, UI

5. (∀x) Fx ⇒ Fy 3-4, CP

6. ¬(∀x) Fx 5,2 MT

7. ¬(∀x) Fx 1,2-6, EI

8. (∃x) ¬Fx ⇒ ¬(∀x) Fx 1-7, CP

9. (∀x) Fx ⇒ ¬(∃x) ¬Fx 8, Trans, DN

I cannot understand how 7.- is established, everything else is clear. Can someone explain how 1,2-6, EI results in 7. ?

 

[HOI]

Don't (1), "There exist x such that Fx is not true", and (3), "for all x Fx is true", contradict one another?