Theorem quantgodelALT 47413

Description: There can be no formula asserting its own non-universality; follows the steps of bj-babygodel 37010. (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 1827	. . . . 5 ⊢ ∀𝑥 ¬ ⊥
2		falim 1576	. . . . . 6 ⊢ (⊥ → ¬ ∀𝑥 ¬ ⊥)
3	2	sps 2219	. . . . 5 ⊢ (∀𝑥⊥ → ¬ ∀𝑥 ¬ ⊥)
4	1, 3	mt2 202	. . . 4 ⊢ ¬ ∀𝑥⊥
5		quantgodel.s	. . . . . . . . 9 ⊢ (𝜑 ↔ ¬ ∀𝑥𝜑)
6	5	biimpi 218	. . . . . . . 8 ⊢ (𝜑 → ¬ ∀𝑥𝜑)
7	6	alimi 1830	. . . . . . 7 ⊢ (∀𝑥𝜑 → ∀𝑥 ¬ ∀𝑥𝜑)
8		hba1 2326	. . . . . . 7 ⊢ (∀𝑥𝜑 → ∀𝑥∀𝑥𝜑)
9		pm2.21 123	. . . . . . . 8 ⊢ (¬ ∀𝑥𝜑 → (∀𝑥𝜑 → ⊥))
10	9	al2imi 1834	. . . . . . 7 ⊢ (∀𝑥 ¬ ∀𝑥𝜑 → (∀𝑥∀𝑥𝜑 → ∀𝑥⊥))
11	7, 8, 10	sylc 65	. . . . . 6 ⊢ (∀𝑥𝜑 → ∀𝑥⊥)
12	11	con3i 154	. . . . 5 ⊢ (¬ ∀𝑥⊥ → ¬ ∀𝑥𝜑)
13	12, 5	sylibr 236	. . . 4 ⊢ (¬ ∀𝑥⊥ → 𝜑)
14	4, 13	ax-mp 5	. . 3 ⊢ 𝜑
15	14	ax-gen 1814	. 2 ⊢ ∀𝑥𝜑
16	14, 6	ax-mp 5	. 2 ⊢ ¬ ∀𝑥𝜑
17	15, 16	pm2.24ii 120	1 ⊢ ⊥

Syntax hints:  ¬ wn 3   ↔ wb 208  ∀wal 1557  ⊥wfal 1571

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-10 2174  ax-12 2211

This theorem depends on definitions:  df-bi 209  df-or 859  df-tru 1562  df-fal 1572  df-ex 1799  df-nf 1803

This theorem is referenced by: (None)