Theorem hon0

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

	Ref	Expression
Assertion	hon0	⊢ ( 𝑇 : ℋ ⟶ ℋ → ¬ 𝑇 = ∅ )

Proof

Step	Hyp	Ref	Expression
1		ax-hv0cl	⊢ 0ℎ ∈ ℋ
2	1	n0ii	⊢ ¬ ℋ = ∅
3		fn0	⊢ ( 𝑇 Fn ∅ ↔ 𝑇 = ∅ )
4		ffn	⊢ ( 𝑇 : ℋ ⟶ ℋ → 𝑇 Fn ℋ )
5		fndmu	⊢ ( ( 𝑇 Fn ℋ ∧ 𝑇 Fn ∅ ) → ℋ = ∅ )
6	5	ex	⊢ ( 𝑇 Fn ℋ → ( 𝑇 Fn ∅ → ℋ = ∅ ) )
7	4 6	syl	⊢ ( 𝑇 : ℋ ⟶ ℋ → ( 𝑇 Fn ∅ → ℋ = ∅ ) )
8	3 7	syl5bir	⊢ ( 𝑇 : ℋ ⟶ ℋ → ( 𝑇 = ∅ → ℋ = ∅ ) )
9	2 8	mtoi	⊢ ( 𝑇 : ℋ ⟶ ℋ → ¬ 𝑇 = ∅ )