Theorem quantgodelALT 47303

Description: There can be no formula asserting its own non-universality; follows the steps of bj-babygodel 36868. (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 1810	. . . . 5 ⊢ ∀𝑥 ¬ ⊥
2		falim 1559	. . . . . 6 ⊢ (⊥ → ¬ ∀𝑥 ¬ ⊥)
3	2	sps 2193	. . . . 5 ⊢ (∀𝑥⊥ → ¬ ∀𝑥 ¬ ⊥)
4	1, 3	mt2 200	. . . 4 ⊢ ¬ ∀𝑥⊥
5		quantgodel.s	. . . . . . . . 9 ⊢ (𝜑 ↔ ¬ ∀𝑥𝜑)
6	5	biimpi 216	. . . . . . . 8 ⊢ (𝜑 → ¬ ∀𝑥𝜑)
7	6	alimi 1813	. . . . . . 7 ⊢ (∀𝑥𝜑 → ∀𝑥 ¬ ∀𝑥𝜑)
8		hba1 2300	. . . . . . 7 ⊢ (∀𝑥𝜑 → ∀𝑥∀𝑥𝜑)
9		pm2.21 123	. . . . . . . 8 ⊢ (¬ ∀𝑥𝜑 → (∀𝑥𝜑 → ⊥))
10	9	al2imi 1817	. . . . . . 7 ⊢ (∀𝑥 ¬ ∀𝑥𝜑 → (∀𝑥∀𝑥𝜑 → ∀𝑥⊥))
11	7, 8, 10	sylc 65	. . . . . 6 ⊢ (∀𝑥𝜑 → ∀𝑥⊥)
12	11	con3i 154	. . . . 5 ⊢ (¬ ∀𝑥⊥ → ¬ ∀𝑥𝜑)
13	12, 5	sylibr 234	. . . 4 ⊢ (¬ ∀𝑥⊥ → 𝜑)
14	4, 13	ax-mp 5	. . 3 ⊢ 𝜑
15	14	ax-gen 1797	. 2 ⊢ ∀𝑥𝜑
16	14, 6	ax-mp 5	. 2 ⊢ ¬ ∀𝑥𝜑
17	15, 16	pm2.24ii 120	1 ⊢ ⊥

Syntax hints:  ¬ wn 3   ↔ wb 206  ∀wal 1540  ⊥wfal 1554

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-10 2147  ax-12 2185

This theorem depends on definitions:  df-bi 207  df-or 849  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786

This theorem is referenced by: (None)