Metamath Proof Explorer

Theorem alsi-no-surprise

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-alsi ; the proof itself builds on alimp-no-surprise . For a contrast, see alimp-surprise . (Contributed by David A. Wheeler, 27-Oct-2018)

Ref Expression
Assertion alsi-no-surprise 
|- -. ( A! x ( ph -> ps ) /\ A! x ( ph -> -. ps ) )

Proof

Step Hyp Ref Expression
1 alimp-no-surprise 
 |-  -. ( A. x ( ph -> ps ) /\ A. x ( ph -> -. ps ) /\ E. x ph )
2 df-alsi 
 |-  ( A! x ( ph -> ps ) <-> ( A. x ( ph -> ps ) /\ E. x ph ) )
3 df-alsi 
 |-  ( A! x ( ph -> -. ps ) <-> ( A. x ( ph -> -. ps ) /\ E. x ph ) )
4 2 3 anbi12i 
 |-  ( ( A! x ( ph -> ps ) /\ A! x ( ph -> -. ps ) ) <-> ( ( A. x ( ph -> ps ) /\ E. x ph ) /\ ( A. x ( ph -> -. ps ) /\ E. x ph ) ) )
5 anandi3r 
 |-  ( ( A. x ( ph -> ps ) /\ E. x ph /\ A. x ( ph -> -. ps ) ) <-> ( ( A. x ( ph -> ps ) /\ E. x ph ) /\ ( A. x ( ph -> -. ps ) /\ E. x ph ) ) )
6 3ancomb 
 |-  ( ( A. x ( ph -> ps ) /\ E. x ph /\ A. x ( ph -> -. ps ) ) <-> ( A. x ( ph -> ps ) /\ A. x ( ph -> -. ps ) /\ E. x ph ) )
7 4 5 6 3bitr2i 
 |-  ( ( A! x ( ph -> ps ) /\ A! x ( ph -> -. ps ) ) <-> ( A. x ( ph -> ps ) /\ A. x ( ph -> -. ps ) /\ E. x ph ) )
8 1 7 mtbir 
 |-  -. ( A! x ( ph -> ps ) /\ A! x ( ph -> -. ps ) )