Metamath Proof Explorer

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 ⊢ ¬ ∀∃ x φ → ψ ∧ ∀∃ x φ → ¬ ψ

Proof

Step Hyp Ref Expression
1 alimp-no-surprise ⊢ ¬ ∀ x φ → ψ ∧ ∀ x φ → ¬ ψ ∧ ∃ x φ
2 df-als ⊢ ∀∃ x φ → ψ ↔ ∀ x φ → ψ ∧ ∃ x φ
3 df-als ⊢ ∀∃ x φ → ¬ ψ ↔ ∀ x φ → ¬ ψ ∧ ∃ x φ
4 2 3 anbi12i ⊢ ∀∃ x φ → ψ ∧ ∀∃ x φ → ¬ ψ ↔ ∀ x φ → ψ ∧ ∃ x φ ∧ ∀ x φ → ¬ ψ ∧ ∃ x φ
5 anandi3r ⊢ ∀ x φ → ψ ∧ ∃ x φ ∧ ∀ x φ → ¬ ψ ↔ ∀ x φ → ψ ∧ ∃ x φ ∧ ∀ x φ → ¬ ψ ∧ ∃ x φ
6 3ancomb ⊢ ∀ x φ → ψ ∧ ∃ x φ ∧ ∀ x φ → ¬ ψ ↔ ∀ x φ → ψ ∧ ∀ x φ → ¬ ψ ∧ ∃ x φ
7 4 5 6 3bitr2i ⊢ ∀∃ x φ → ψ ∧ ∀∃ x φ → ¬ ψ ↔ ∀ x φ → ψ ∧ ∀ x φ → ¬ ψ ∧ ∃ x φ
8 1 7 mtbir ⊢ ¬ ∀∃ x φ → ψ ∧ ∀∃ x φ → ¬ ψ