Metamath Proof Explorer

Theorem quantgodelALT

Description: There can be no formula asserting its own non-universality; follows the steps of bj-babygodel . (Contributed by Ender Ting, 7-May-2026) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Hypothesis quantgodel.s 
|- ( ph <-> -. A. x ph )
Assertion quantgodelALT 
|- F.

Proof

Step Hyp Ref Expression
1 quantgodel.s 
 |-  ( ph <-> -. A. x ph )
2 alfal 
 |-  A. x -. F.
3 falim 
 |-  ( F. -> -. A. x -. F. )
4 3 sps 
 |-  ( A. x F. -> -. A. x -. F. )
5 2 4 mt2 
 |-  -. A. x F.
6 1 biimpi 
 |-  ( ph -> -. A. x ph )
7 6 alimi 
 |-  ( A. x ph -> A. x -. A. x ph )
8 hba1 
 |-  ( A. x ph -> A. x A. x ph )
9 pm2.21 
 |-  ( -. A. x ph -> ( A. x ph -> F. ) )
10 9 al2imi 
 |-  ( A. x -. A. x ph -> ( A. x A. x ph -> A. x F. ) )
11 7 8 10 sylc 
 |-  ( A. x ph -> A. x F. )
12 11 con3i 
 |-  ( -. A. x F. -> -. A. x ph )
13 12 1 sylibr 
 |-  ( -. A. x F. -> ph )
14 5 13 ax-mp 
 |-  ph
15 14 ax-gen 
 |-  A. x ph
16 14 6 ax-mp 
 |-  -. A. x ph
17 15 16 pm2.24ii 
 |-  F.