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-alsi . (Contributed by David A. Wheeler, 27-Oct-2018)

	Ref	Expression
Assertion	alimp-no-surprise	⊢ ¬ ( ∀ 𝑥 ( 𝜑 → 𝜓 ) ∧ ∀ 𝑥 ( 𝜑 → ¬ 𝜓 ) ∧ ∃ 𝑥 𝜑 )

Proof

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