Metamath Proof Explorer


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
|- ( ph <-> -. Prv ph )
bj-godellob.1
|- -. Prv F.
Assertion bj-godellob
|- F.

Proof

Step Hyp Ref Expression
1 bj-godellob.s
 |-  ( ph <-> -. Prv ph )
2 bj-godellob.1
 |-  -. Prv F.
3 dfnot
 |-  ( -. Prv ph <-> ( Prv ph -> F. ) )
4 1 3 bitri
 |-  ( ph <-> ( Prv ph -> F. ) )
5 2 pm2.21i
 |-  ( Prv F. -> F. )
6 4 5 bj-babylob
 |-  F.