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	$$⊢\phi \leftrightarrow \neg \forall x\phi$$
Assertion	quantgodelALT	$$⊢\perp$$

Proof

Step	Hyp	Ref	Expression
1		quantgodel.s	$$⊢\phi \leftrightarrow \neg \forall x\phi$$
2		alfal	$$⊢\forall x\neg \perp$$
3		falim	$$⊢\perp \to \neg \forall x\neg \perp$$
4	3	sps	$$⊢\forall x\perp \to \neg \forall x\neg \perp$$
5	2 4	mt2	$$⊢\neg \forall x\perp$$
6	1	biimpi	$$⊢\phi \to \neg \forall x\phi$$
7	6	alimi	$$⊢\forall x\phi \to \forall x\neg \forall x\phi$$
8		hba1	$$⊢\forall x\phi \to \forall x\forall x\phi$$
9		pm2.21	$$⊢\neg \forall x\phi \to \left(\forall x\phi \to \perp \right)$$
10	9	al2imi	$$⊢\forall x\neg \forall x\phi \to \left(\forall x\forall x\phi \to \forall x\perp \right)$$
11	7 8 10	sylc	$$⊢\forall x\phi \to \forall x\perp$$
12	11	con3i	$$⊢\neg \forall x\perp \to \neg \forall x\phi$$
13	12 1	sylibr	$$⊢\neg \forall x\perp \to \phi$$
14	5 13	ax-mp	$$⊢\phi$$
15	14	ax-gen	$$⊢\forall x\phi$$
16	14 6	ax-mp	$$⊢\neg \forall x\phi$$
17	15 16	pm2.24ii	$$⊢\perp$$