Theorem hon0

Description: A Hilbert space operator is not empty. (Contributed by NM, 24-Mar-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	hon0	$$⊢T:\mathscr{H}⟶\mathscr{H}\to \neg T=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		ax-hv0cl	$$⊢0_{ℎ}\in \mathscr{H}$$
2	1	n0ii	$$⊢\neg \mathscr{H}=\varnothing$$
3		fn0	$$⊢TFn\varnothing \leftrightarrow T=\varnothing$$
4		ffn	$$⊢T:\mathscr{H}⟶\mathscr{H}\to TFn\mathscr{H}$$
5		fndmu	$$⊢\left(TFn\mathscr{H}\wedge TFn\varnothing \right)\to \mathscr{H}=\varnothing$$
6	5	ex	$$⊢TFn\mathscr{H}\to \left(TFn\varnothing \to \mathscr{H}=\varnothing \right)$$
7	4 6	syl	$$⊢T:\mathscr{H}⟶\mathscr{H}\to \left(TFn\varnothing \to \mathscr{H}=\varnothing \right)$$
8	3 7	syl5bir	$$⊢T:\mathscr{H}⟶\mathscr{H}\to \left(T=\varnothing \to \mathscr{H}=\varnothing \right)$$
9	2 8	mtoi	$$⊢T:\mathscr{H}⟶\mathscr{H}\to \neg T=\varnothing$$