Theorem cnvbracl

Description: Closure of the converse of the bra function. (Contributed by NM, 26-May-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	cnvbracl	$$⊢T\in \left(\mathrm{LinFn}\cap \mathrm{ContFn}\right)\to {\mathrm{bra}}^{-1}\left(T\right)\in \mathscr{H}$$

Proof

Step	Hyp	Ref	Expression
1		bra11	$$⊢\mathrm{bra}:\mathscr{H}\underset{1-1\; onto}{⟶}\mathrm{LinFn}\cap \mathrm{ContFn}$$
2		f1ocnvdm	$$⊢\left(\mathrm{bra}:\mathscr{H}\underset{1-1\; onto}{⟶}\mathrm{LinFn}\cap \mathrm{ContFn}\wedge T\in \left(\mathrm{LinFn}\cap \mathrm{ContFn}\right)\right)\to {\mathrm{bra}}^{-1}\left(T\right)\in \mathscr{H}$$
3	1 2	mpan	$$⊢T\in \left(\mathrm{LinFn}\cap \mathrm{ContFn}\right)\to {\mathrm{bra}}^{-1}\left(T\right)\in \mathscr{H}$$