Theorem als-no-surprise 17055

Description: Demonstrate that there is never a "surprise" when using the allsome quantifier, that is, it is never possible for the consequent to be both always true and always false. This uses the definition of df-als 17036: the universal parts give ∀𝑥¬ 𝜑, which contradicts the witness that the allsome quantifier supplies. Ordinary "for all" with implication has no such property, since ∀𝑥(𝜑 → 𝜓) and ∀𝑥(𝜑 → ¬ 𝜓) can both hold when nothing satisfies 𝜑. (Contributed by David A. Wheeler, 27-Oct-2018.) (Revised by David A. Wheeler, 20-Jul-2026.)

Assertion

Ref	Expression
als-no-surprise	⊢ ¬ (∀∃𝑥(𝜑 → 𝜓) ∧ ∀∃𝑥(𝜑 → ¬ 𝜓))

Proof of Theorem als-no-surprise

Step	Hyp	Ref	Expression
1		simpl 109	. . 3 ⊢ ((∀∃𝑥(𝜑 → 𝜓) ∧ ∀∃𝑥(𝜑 → ¬ 𝜓)) → ∀∃𝑥(𝜑 → 𝜓))
2		df-als 17036	. . . 4 ⊢ (∀∃𝑥(𝜑 → 𝜓) ↔ (∀𝑥(𝜑 → 𝜓) ∧ ∃𝑥𝜑))
3	2	simprbi 275	. . 3 ⊢ (∀∃𝑥(𝜑 → 𝜓) → ∃𝑥𝜑)
4	1, 3	syl 14	. 2 ⊢ ((∀∃𝑥(𝜑 → 𝜓) ∧ ∀∃𝑥(𝜑 → ¬ 𝜓)) → ∃𝑥𝜑)
5	2	simplbi 274	. . . 4 ⊢ (∀∃𝑥(𝜑 → 𝜓) → ∀𝑥(𝜑 → 𝜓))
6		df-als 17036	. . . . 5 ⊢ (∀∃𝑥(𝜑 → ¬ 𝜓) ↔ (∀𝑥(𝜑 → ¬ 𝜓) ∧ ∃𝑥𝜑))
7	6	simplbi 274	. . . 4 ⊢ (∀∃𝑥(𝜑 → ¬ 𝜓) → ∀𝑥(𝜑 → ¬ 𝜓))
8	5, 7	anim12i 338	. . 3 ⊢ ((∀∃𝑥(𝜑 → 𝜓) ∧ ∀∃𝑥(𝜑 → ¬ 𝜓)) → (∀𝑥(𝜑 → 𝜓) ∧ ∀𝑥(𝜑 → ¬ 𝜓)))
9		19.26 1534	. . . 4 ⊢ (∀𝑥((𝜑 → 𝜓) ∧ (𝜑 → ¬ 𝜓)) ↔ (∀𝑥(𝜑 → 𝜓) ∧ ∀𝑥(𝜑 → ¬ 𝜓)))
10		pm2.65 669	. . . . . . 7 ⊢ ((𝜑 → 𝜓) → ((𝜑 → ¬ 𝜓) → ¬ 𝜑))
11	10	imp 124	. . . . . 6 ⊢ (((𝜑 → 𝜓) ∧ (𝜑 → ¬ 𝜓)) → ¬ 𝜑)
12	11	alimi 1508	. . . . 5 ⊢ (∀𝑥((𝜑 → 𝜓) ∧ (𝜑 → ¬ 𝜓)) → ∀𝑥 ¬ 𝜑)
13		alnex 1552	. . . . . 6 ⊢ (∀𝑥 ¬ 𝜑 ↔ ¬ ∃𝑥𝜑)
14	13	biimpi 120	. . . . 5 ⊢ (∀𝑥 ¬ 𝜑 → ¬ ∃𝑥𝜑)
15	12, 14	syl 14	. . . 4 ⊢ (∀𝑥((𝜑 → 𝜓) ∧ (𝜑 → ¬ 𝜓)) → ¬ ∃𝑥𝜑)
16	9, 15	sylbir 135	. . 3 ⊢ ((∀𝑥(𝜑 → 𝜓) ∧ ∀𝑥(𝜑 → ¬ 𝜓)) → ¬ ∃𝑥𝜑)
17	8, 16	syl 14	. 2 ⊢ ((∀∃𝑥(𝜑 → 𝜓) ∧ ∀∃𝑥(𝜑 → ¬ 𝜓)) → ¬ ∃𝑥𝜑)
18	4, 17	pm2.65i 648	1 ⊢ ¬ (∀∃𝑥(𝜑 → 𝜓) ∧ ∀∃𝑥(𝜑 → ¬ 𝜓))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 104  ∀wal 1400  ∃wex 1545  ∀∃wals 17034

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 623  ax-in2 624  ax-5 1500  ax-gen 1502  ax-ie2 1547

This theorem depends on definitions:  df-bi 117  df-tru 1405  df-fal 1408  df-als 17036

This theorem is referenced by:  rals-no-surprise  17056