A Concise Introduction to Logic, 9th edition, P. Hurley, 8.7, III (10)

This problem is solved in the book but I thought to incude it in my answers because my translation of the last premise is slightly different than Hurley's and because the conclusion can be derived without having to use Indirect Proof. The problem:

The tallest building in North America is the Sears Tower. The tallest building in North America is located in Chicago. If one thing is taller than another, then the latter is not taller than the former. Therefore, the Sears Tower is located in Chicago. (Bx: x is a building in North America; Txy: x is taller than y; Cx: x is located in Chicago; s: the Sears Tower)

Hurley translates the last premise as (x)(y)(Txy ⊃¬ Tyx). I show that we will get the same result if we make explicit the fact that x and y are not the same things: (x)(y){[¬(x=y) • Txy] ⊃¬ Tyx}.

1. (x){[Bx • ¬ (x=s)] ⊃Tsx} • Bs
2. (∃x){Bx • (y){[By • ¬ (y=x)] ⊃Txy} • Cx}
3. (x)(y){[¬(x=y) • Txy] ⊃¬ Tyx}
4. ∴Cs
5. Ba • (y){[By • ¬ (y=a)] ⊃Tay} • Ca / 2 EI
6. (y){[By • ¬ (y=a)] ⊃Tay / 5 Simp
7. [Bs • ¬ (s=a)] ⊃Tas / 6 UI
8. Bs ⊃[¬ (s=a) ⊃Tas] / 7 Exp
9. Bx / 1 Simp
10. ¬ (s=a) ⊃Tas / 9, 8 MP
11. [Ba • ¬ (a=s)] ⊃Tsa / 1 UI
12. (y){[¬(a=y) • Tay] ⊃¬ Tya / 3 UI
13. [¬(a=s) • Tas] ⊃¬ Tsa / 12 UI
14. Tsa ⊃¬ [¬(a=s) • Tas] / 13 Contrap
15. [Ba • ¬ (a=s)] ⊃¬ [¬(a=s) • Tas] / 11, 14 HS
16. ¬ [Ba • ¬ (a=s)] ∨¬ [¬(a=s) • Tas] / 15 Impl
17. [¬ Ba ∨ (a=s)] ∨[(a=s) ∨¬ Tas] / 16 DeM
18. ¬ Ba ∨ [(a=s) ∨(a=s) ∨¬ Tas] / 17 Assoc
19. Ba / 5 Simp
20. (a=s) ∨(a=s) ∨¬ Tas / 18, 19 DS
21. (a=s) ∨¬ Tas / 20 Taut
22. ¬ Tas ∨(a=s) / 21 Comm
23. Tas ⊃ (a=s) / 22 Impl
24. ¬ (s=a) ⊃(a=s) / 10, 23 HS
25. (s=a) ∨ (a=s) / 24 Impl
26. (a=s) ∨(a=s) / Id
27. a=s / Taut
28. Ca / 5 Simp
29. Cs / Id