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 | ⊢ ( 𝜑 ↔ ¬ ∀ 𝑥 𝜑 ) | |
| Assertion | quantgodelALT | ⊢ ⊥ |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | quantgodel.s | ⊢ ( 𝜑 ↔ ¬ ∀ 𝑥 𝜑 ) | |
| 2 | alfal | ⊢ ∀ 𝑥 ¬ ⊥ | |
| 3 | falim | ⊢ ( ⊥ → ¬ ∀ 𝑥 ¬ ⊥ ) | |
| 4 | 3 | sps | ⊢ ( ∀ 𝑥 ⊥ → ¬ ∀ 𝑥 ¬ ⊥ ) |
| 5 | 2 4 | mt2 | ⊢ ¬ ∀ 𝑥 ⊥ |
| 6 | 1 | biimpi | ⊢ ( 𝜑 → ¬ ∀ 𝑥 𝜑 ) |
| 7 | 6 | alimi | ⊢ ( ∀ 𝑥 𝜑 → ∀ 𝑥 ¬ ∀ 𝑥 𝜑 ) |
| 8 | hba1 | ⊢ ( ∀ 𝑥 𝜑 → ∀ 𝑥 ∀ 𝑥 𝜑 ) | |
| 9 | pm2.21 | ⊢ ( ¬ ∀ 𝑥 𝜑 → ( ∀ 𝑥 𝜑 → ⊥ ) ) | |
| 10 | 9 | al2imi | ⊢ ( ∀ 𝑥 ¬ ∀ 𝑥 𝜑 → ( ∀ 𝑥 ∀ 𝑥 𝜑 → ∀ 𝑥 ⊥ ) ) |
| 11 | 7 8 10 | sylc | ⊢ ( ∀ 𝑥 𝜑 → ∀ 𝑥 ⊥ ) |
| 12 | 11 | con3i | ⊢ ( ¬ ∀ 𝑥 ⊥ → ¬ ∀ 𝑥 𝜑 ) |
| 13 | 12 1 | sylibr | ⊢ ( ¬ ∀ 𝑥 ⊥ → 𝜑 ) |
| 14 | 5 13 | ax-mp | ⊢ 𝜑 |
| 15 | 14 | ax-gen | ⊢ ∀ 𝑥 𝜑 |
| 16 | 14 6 | ax-mp | ⊢ ¬ ∀ 𝑥 𝜑 |
| 17 | 15 16 | pm2.24ii | ⊢ ⊥ |