Theorem quantgodelALT 47572

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

Hypothesis

Ref	Expression
quantgodel.s	⊢ (𝜑 ↔ ¬ ∀𝑥𝜑)

Assertion

Ref	Expression
quantgodelALT	⊢ ⊥

Proof of Theorem quantgodelALT

Step	Hyp	Ref	Expression
1		alfal 1838	. . . . 5 ⊢ ∀𝑥 ¬ ⊥
2		falim 1587	. . . . . 6 ⊢ (⊥ → ¬ ∀𝑥 ¬ ⊥)
3	2	sps 2221	. . . . 5 ⊢ (∀𝑥⊥ → ¬ ∀𝑥 ¬ ⊥)
4	1, 3	mt2 203	. . . 4 ⊢ ¬ ∀𝑥⊥
5		quantgodel.s	. . . . . . . . 9 ⊢ (𝜑 ↔ ¬ ∀𝑥𝜑)
6	5	biimpi 219	. . . . . . . 8 ⊢ (𝜑 → ¬ ∀𝑥𝜑)
7	6	alimi 1841	. . . . . . 7 ⊢ (∀𝑥𝜑 → ∀𝑥 ¬ ∀𝑥𝜑)
8		hba1 2328	. . . . . . 7 ⊢ (∀𝑥𝜑 → ∀𝑥∀𝑥𝜑)
9		pm2.21 124	. . . . . . . 8 ⊢ (¬ ∀𝑥𝜑 → (∀𝑥𝜑 → ⊥))
10	9	al2imi 1845	. . . . . . 7 ⊢ (∀𝑥 ¬ ∀𝑥𝜑 → (∀𝑥∀𝑥𝜑 → ∀𝑥⊥))
11	7, 8, 10	sylc 66	. . . . . 6 ⊢ (∀𝑥𝜑 → ∀𝑥⊥)
12	11	con3i 155	. . . . 5 ⊢ (¬ ∀𝑥⊥ → ¬ ∀𝑥𝜑)
13	12, 5	sylibr 237	. . . 4 ⊢ (¬ ∀𝑥⊥ → 𝜑)
14	4, 13	ax-mp 5	. . 3 ⊢ 𝜑
15	14	ax-gen 1825	. 2 ⊢ ∀𝑥𝜑
16	14, 6	ax-mp 5	. 2 ⊢ ¬ ∀𝑥𝜑
17	15, 16	pm2.24ii 121	1 ⊢ ⊥

Syntax hints:  ¬ wn 3   ↔ wb 209  ∀wal 1568  ⊥wfal 1582

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-10 2176  ax-12 2213

This theorem depends on definitions:  df-bi 210  df-or 861  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814

This theorem is referenced by: (None)