Metamath Proof Explorer

Theorem alimp-no-surprise

Description: There is no "surprise" in a for-all with implication if there exists a value where the antecedent is true. This is one way to prevent for-all with implication from allowing anything. For a contrast, see alimp-surprise . The allsome quantifier also counters this problem, see df-als . (Contributed by David A. Wheeler, 27-Oct-2018)

Ref Expression
Assertion alimp-no-surprise ⊢ ¬ ∀ x φ → ψ ∧ ∀ x φ → ¬ ψ ∧ ∃ x φ

Proof

Step Hyp Ref Expression
1 pm4.82 ⊢ φ → ψ ∧ φ → ¬ ψ ↔ ¬ φ
2 1 albii ⊢ ∀ x φ → ψ ∧ φ → ¬ ψ ↔ ∀ x ¬ φ
3 alnex ⊢ ∀ x ¬ φ ↔ ¬ ∃ x φ
4 2 3 sylbb ⊢ ∀ x φ → ψ ∧ φ → ¬ ψ → ¬ ∃ x φ
5 imnan ⊢ ∀ x φ → ψ ∧ φ → ¬ ψ → ¬ ∃ x φ ↔ ¬ ∀ x φ → ψ ∧ φ → ¬ ψ ∧ ∃ x φ
6 4 5 mpbi ⊢ ¬ ∀ x φ → ψ ∧ φ → ¬ ψ ∧ ∃ x φ
7 19.26 ⊢ ∀ x φ → ψ ∧ φ → ¬ ψ ↔ ∀ x φ → ψ ∧ ∀ x φ → ¬ ψ
8 7 anbi2ci ⊢ ∀ x φ → ψ ∧ φ → ¬ ψ ∧ ∃ x φ ↔ ∃ x φ ∧ ∀ x φ → ψ ∧ ∀ x φ → ¬ ψ
9 3anass ⊢ ∃ x φ ∧ ∀ x φ → ψ ∧ ∀ x φ → ¬ ψ ↔ ∃ x φ ∧ ∀ x φ → ψ ∧ ∀ x φ → ¬ ψ
10 3anrot ⊢ ∃ x φ ∧ ∀ x φ → ψ ∧ ∀ x φ → ¬ ψ ↔ ∀ x φ → ψ ∧ ∀ x φ → ¬ ψ ∧ ∃ x φ
11 8 9 10 3bitr2i ⊢ ∀ x φ → ψ ∧ φ → ¬ ψ ∧ ∃ x φ ↔ ∀ x φ → ψ ∧ ∀ x φ → ¬ ψ ∧ ∃ x φ
12 6 11 mtbi ⊢ ¬ ∀ x φ → ψ ∧ ∀ x φ → ¬ ψ ∧ ∃ x φ