Theorem bj-godellob

Description: Proof of Gödel's theorem from Löb's theorem (see comments at bj-babygodel and bj-babylob for details). (Contributed by BJ, 20-Apr-2019) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypotheses	bj-godellob.s	$$⊢\phi \leftrightarrow \neg Prv\phi$$
	bj-godellob.1	$$⊢\neg Prv\perp$$
Assertion	bj-godellob	$$⊢\perp$$

Proof

Step	Hyp	Ref	Expression
1		bj-godellob.s	$$⊢\phi \leftrightarrow \neg Prv\phi$$
2		bj-godellob.1	$$⊢\neg Prv\perp$$
3		dfnot	$$⊢\neg Prv\phi \leftrightarrow \left(Prv\phi \to \perp \right)$$
4	1 3	bitri	$$⊢\phi \leftrightarrow \left(Prv\phi \to \perp \right)$$
5	2	pm2.21i	$$⊢Prv\perp \to \perp$$
6	4 5	bj-babylob	$$⊢\perp$$