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	⊢ ¬ ( ∀! 𝑥 ( 𝜑 → 𝜓 ) ∧ ∀! 𝑥 ( 𝜑 → ¬ 𝜓 ) )

Proof

Step	Hyp	Ref	Expression
1		alimp-no-surprise	⊢ ¬ ( ∀ 𝑥 ( 𝜑 → 𝜓 ) ∧ ∀ 𝑥 ( 𝜑 → ¬ 𝜓 ) ∧ ∃ 𝑥 𝜑 )
2		df-alsi	⊢ ( ∀! 𝑥 ( 𝜑 → 𝜓 ) ↔ ( ∀ 𝑥 ( 𝜑 → 𝜓 ) ∧ ∃ 𝑥 𝜑 ) )
3		df-alsi	⊢ ( ∀! 𝑥 ( 𝜑 → ¬ 𝜓 ) ↔ ( ∀ 𝑥 ( 𝜑 → ¬ 𝜓 ) ∧ ∃ 𝑥 𝜑 ) )
4	2 3	anbi12i	⊢ ( ( ∀! 𝑥 ( 𝜑 → 𝜓 ) ∧ ∀! 𝑥 ( 𝜑 → ¬ 𝜓 ) ) ↔ ( ( ∀ 𝑥 ( 𝜑 → 𝜓 ) ∧ ∃ 𝑥 𝜑 ) ∧ ( ∀ 𝑥 ( 𝜑 → ¬ 𝜓 ) ∧ ∃ 𝑥 𝜑 ) ) )
5		anandi3r	⊢ ( ( ∀ 𝑥 ( 𝜑 → 𝜓 ) ∧ ∃ 𝑥 𝜑 ∧ ∀ 𝑥 ( 𝜑 → ¬ 𝜓 ) ) ↔ ( ( ∀ 𝑥 ( 𝜑 → 𝜓 ) ∧ ∃ 𝑥 𝜑 ) ∧ ( ∀ 𝑥 ( 𝜑 → ¬ 𝜓 ) ∧ ∃ 𝑥 𝜑 ) ) )
6		3ancomb	⊢ ( ( ∀ 𝑥 ( 𝜑 → 𝜓 ) ∧ ∃ 𝑥 𝜑 ∧ ∀ 𝑥 ( 𝜑 → ¬ 𝜓 ) ) ↔ ( ∀ 𝑥 ( 𝜑 → 𝜓 ) ∧ ∀ 𝑥 ( 𝜑 → ¬ 𝜓 ) ∧ ∃ 𝑥 𝜑 ) )
7	4 5 6	3bitr2i	⊢ ( ( ∀! 𝑥 ( 𝜑 → 𝜓 ) ∧ ∀! 𝑥 ( 𝜑 → ¬ 𝜓 ) ) ↔ ( ∀ 𝑥 ( 𝜑 → 𝜓 ) ∧ ∀ 𝑥 ( 𝜑 → ¬ 𝜓 ) ∧ ∃ 𝑥 𝜑 ) )
8	1 7	mtbir	⊢ ¬ ( ∀! 𝑥 ( 𝜑 → 𝜓 ) ∧ ∀! 𝑥 ( 𝜑 → ¬ 𝜓 ) )