I got a little caught up on on the proof of (no) infinite descent by well-founded induction without a base case. I thought, "something is wrong; (∀y∈X.y⊏x⟹¬Φ(y)) only implies ¬Φ(x) if you assume (∀y∈X.y⊏x⟹¬Φ(y)) in the firsts place". But that's actually fine, because the principle of well-founded induction lets you assume it out of thin air, and as long as it implies ¬Φ(x), you're good.
The intuition of this, to me at least, is that well-founded induction has an implicit base case of the empty set. (∀y∈X.y⊏x⟹Ψ(y))⟹Ψ(x) means Ψ(x) is required to be automatically true if ∄y∈X, so (∀y∈X.y⊏x⟹Ψ(y)) may be assumed out of thin air and then used inductively for all the cases where ∃y∈X.
Back to the specific example, ¬Φ(x) is automatically true if ∄y∈X because Φ(x) implies ∃y∈X. However note that this base case doesn't need to be explicitly shown, because it's included in the general case.