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 A. x -. ph, which contradicts the witness that the allsome quantifier supplies. Ordinary "for all" with implication has no such property, since A. x ( ph -> ps ) and A. x ( ph -> -. ps ) can both hold when nothing satisfies ph. (Contributed by David A. Wheeler, 27-Oct-2018.) (Revised by David A. Wheeler, 20-Jul-2026.)

Assertion

Ref	Expression
als-no-surprise	|- -. ( A.E. x ( ph -> ps ) /\ A.E. x ( ph -> -. ps ) )

Proof of Theorem als-no-surprise

Step	Hyp	Ref	Expression
1		simpl 109	. . 3 |- ( ( A.E. x ( ph -> ps ) /\ A.E. x ( ph -> -. ps ) ) -> A.E. x ( ph -> ps ) )
2		df-als 17036	. . . 4 |- ( A.E. x ( ph -> ps ) <-> ( A. x ( ph -> ps ) /\ E. x ph ) )
3	2	simprbi 275	. . 3 |- ( A.E. x ( ph -> ps ) -> E. x ph )
4	1, 3	syl 14	. 2 |- ( ( A.E. x ( ph -> ps ) /\ A.E. x ( ph -> -. ps ) ) -> E. x ph )
5	2	simplbi 274	. . . 4 |- ( A.E. x ( ph -> ps ) -> A. x ( ph -> ps ) )
6		df-als 17036	. . . . 5 |- ( A.E. x ( ph -> -. ps ) <-> ( A. x ( ph -> -. ps ) /\ E. x ph ) )
7	6	simplbi 274	. . . 4 |- ( A.E. x ( ph -> -. ps ) -> A. x ( ph -> -. ps ) )
8	5, 7	anim12i 338	. . 3 |- ( ( A.E. x ( ph -> ps ) /\ A.E. x ( ph -> -. ps ) ) -> ( A. x ( ph -> ps ) /\ A. x ( ph -> -. ps ) ) )
9		19.26 1534	. . . 4 |- ( A. x ( ( ph -> ps ) /\ ( ph -> -. ps ) ) <-> ( A. x ( ph -> ps ) /\ A. x ( ph -> -. ps ) ) )
10		pm2.65 669	. . . . . . 7 |- ( ( ph -> ps ) -> ( ( ph -> -. ps ) -> -. ph ) )
11	10	imp 124	. . . . . 6 |- ( ( ( ph -> ps ) /\ ( ph -> -. ps ) ) -> -. ph )
12	11	alimi 1508	. . . . 5 |- ( A. x ( ( ph -> ps ) /\ ( ph -> -. ps ) ) -> A. x -. ph )
13		alnex 1552	. . . . . 6 |- ( A. x -. ph <-> -. E. x ph )
14	13	biimpi 120	. . . . 5 |- ( A. x -. ph -> -. E. x ph )
15	12, 14	syl 14	. . . 4 |- ( A. x ( ( ph -> ps ) /\ ( ph -> -. ps ) ) -> -. E. x ph )
16	9, 15	sylbir 135	. . 3 |- ( ( A. x ( ph -> ps ) /\ A. x ( ph -> -. ps ) ) -> -. E. x ph )
17	8, 16	syl 14	. 2 |- ( ( A.E. x ( ph -> ps ) /\ A.E. x ( ph -> -. ps ) ) -> -. E. x ph )
18	4, 17	pm2.65i 648	1 |- -. ( A.E. x ( ph -> ps ) /\ A.E. x ( ph -> -. ps ) )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 104   A.wal 1400   E.wex 1545   A.E.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