Theorem nmotru

Description: There does not exist at most one set such that T. is true. (Contributed by Anthony Hart, 13-Sep-2011)

	Ref	Expression
Assertion	nmotru	⊢ ¬ ∃* 𝑥 ⊤

Proof

Step	Hyp	Ref	Expression
1		extru	⊢ ∃ 𝑥 ⊤
2		neutru	⊢ ¬ ∃! 𝑥 ⊤
3		jcn	⊢ ( ∃ 𝑥 ⊤ → ( ¬ ∃! 𝑥 ⊤ → ¬ ( ∃ 𝑥 ⊤ → ∃! 𝑥 ⊤ ) ) )
4	1 2 3	mp2	⊢ ¬ ( ∃ 𝑥 ⊤ → ∃! 𝑥 ⊤ )
5		moeu	⊢ ( ∃* 𝑥 ⊤ ↔ ( ∃ 𝑥 ⊤ → ∃! 𝑥 ⊤ ) )
6	4 5	mtbir	⊢ ¬ ∃* 𝑥 ⊤