Theorem als-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-als ; 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	als-no-surprise	Could not format assertion : No typesetting found for |- -. ( AE x ( ph -> ps ) /\ AE x ( ph -> -. ps ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		alimp-no-surprise	$$⊢\neg \left(\forall x\left(\phi \to \psi \right)\wedge \forall x\left(\phi \to \neg \psi \right)\wedge \exists x\phi \right)$$
2		df-als	Could not format ( AE x ( ph -> ps ) <-> ( A. x ( ph -> ps ) /\ E. x ph ) ) : No typesetting found for |- ( AE x ( ph -> ps ) <-> ( A. x ( ph -> ps ) /\ E. x ph ) ) with typecode |-
3		df-als	Could not format ( AE x ( ph -> -. ps ) <-> ( A. x ( ph -> -. ps ) /\ E. x ph ) ) : No typesetting found for |- ( AE x ( ph -> -. ps ) <-> ( A. x ( ph -> -. ps ) /\ E. x ph ) ) with typecode |-
4	2 3	anbi12i	Could not format ( ( AE x ( ph -> ps ) /\ AE x ( ph -> -. ps ) ) <-> ( ( A. x ( ph -> ps ) /\ E. x ph ) /\ ( A. x ( ph -> -. ps ) /\ E. x ph ) ) ) : No typesetting found for |- ( ( AE x ( ph -> ps ) /\ AE x ( ph -> -. ps ) ) <-> ( ( A. x ( ph -> ps ) /\ E. x ph ) /\ ( A. x ( ph -> -. ps ) /\ E. x ph ) ) ) with typecode |-
5		anandi3r	$$⊢\left(\forall x\left(\phi \to \psi \right)\wedge \exists x\phi \wedge \forall x\left(\phi \to \neg \psi \right)\right)\leftrightarrow \left(\left(\forall x\left(\phi \to \psi \right)\wedge \exists x\phi \right)\wedge \left(\forall x\left(\phi \to \neg \psi \right)\wedge \exists x\phi \right)\right)$$
6		3ancomb	$$⊢\left(\forall x\left(\phi \to \psi \right)\wedge \exists x\phi \wedge \forall x\left(\phi \to \neg \psi \right)\right)\leftrightarrow \left(\forall x\left(\phi \to \psi \right)\wedge \forall x\left(\phi \to \neg \psi \right)\wedge \exists x\phi \right)$$
7	4 5 6	3bitr2i	Could not format ( ( AE x ( ph -> ps ) /\ AE x ( ph -> -. ps ) ) <-> ( A. x ( ph -> ps ) /\ A. x ( ph -> -. ps ) /\ E. x ph ) ) : No typesetting found for |- ( ( AE x ( ph -> ps ) /\ AE x ( ph -> -. ps ) ) <-> ( A. x ( ph -> ps ) /\ A. x ( ph -> -. ps ) /\ E. x ph ) ) with typecode |-
8	1 7	mtbir	Could not format -. ( AE x ( ph -> ps ) /\ AE x ( ph -> -. ps ) ) : No typesetting found for |- -. ( AE x ( ph -> ps ) /\ AE x ( ph -> -. ps ) ) with typecode |-