Theorem quantgodelALT 47325

Description: There can be no formula asserting its own non-universality; follows the steps of bj-babygodel 36921. (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 1815	. . . . 5 ⊢ ∀𝑥 ¬ ⊥
2		falim 1564	. . . . . 6 ⊢ (⊥ → ¬ ∀𝑥 ¬ ⊥)
3	2	sps 2197	. . . . 5 ⊢ (∀𝑥⊥ → ¬ ∀𝑥 ¬ ⊥)
4	1, 3	mt2 201	. . . 4 ⊢ ¬ ∀𝑥⊥
5		quantgodel.s	. . . . . . . . 9 ⊢ (𝜑 ↔ ¬ ∀𝑥𝜑)
6	5	biimpi 217	. . . . . . . 8 ⊢ (𝜑 → ¬ ∀𝑥𝜑)
7	6	alimi 1818	. . . . . . 7 ⊢ (∀𝑥𝜑 → ∀𝑥 ¬ ∀𝑥𝜑)
8		hba1 2304	. . . . . . 7 ⊢ (∀𝑥𝜑 → ∀𝑥∀𝑥𝜑)
9		pm2.21 123	. . . . . . . 8 ⊢ (¬ ∀𝑥𝜑 → (∀𝑥𝜑 → ⊥))
10	9	al2imi 1822	. . . . . . 7 ⊢ (∀𝑥 ¬ ∀𝑥𝜑 → (∀𝑥∀𝑥𝜑 → ∀𝑥⊥))
11	7, 8, 10	sylc 65	. . . . . 6 ⊢ (∀𝑥𝜑 → ∀𝑥⊥)
12	11	con3i 154	. . . . 5 ⊢ (¬ ∀𝑥⊥ → ¬ ∀𝑥𝜑)
13	12, 5	sylibr 235	. . . 4 ⊢ (¬ ∀𝑥⊥ → 𝜑)
14	4, 13	ax-mp 5	. . 3 ⊢ 𝜑
15	14	ax-gen 1802	. 2 ⊢ ∀𝑥𝜑
16	14, 6	ax-mp 5	. 2 ⊢ ¬ ∀𝑥𝜑
17	15, 16	pm2.24ii 120	1 ⊢ ⊥

Syntax hints:  ¬ wn 3   ↔ wb 207  ∀wal 1545  ⊥wfal 1559

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-10 2152  ax-12 2189

This theorem depends on definitions:  df-bi 208  df-or 854  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791

This theorem is referenced by: (None)