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 ( 𝜑 ↔ ¬ Prv 𝜑 )
bj-godellob.1 ¬ Prv ⊥
Assertion bj-godellob

Proof

Step Hyp Ref Expression
1 bj-godellob.s ( 𝜑 ↔ ¬ Prv 𝜑 )
2 bj-godellob.1 ¬ Prv ⊥
3 dfnot ( ¬ Prv 𝜑 ↔ ( Prv 𝜑 → ⊥ ) )
4 1 3 bitri ( 𝜑 ↔ ( Prv 𝜑 → ⊥ ) )
5 2 pm2.21i ( Prv ⊥ → ⊥ )
6 4 5 bj-babylob