Metamath Proof Explorer

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 ( 𝑇 ∈ ( LinFn ∩ ContFn ) → ( ◡ bra ‘ 𝑇 ) ∈ ℋ )

Proof

Step Hyp Ref Expression
1 bra11 ⊢ bra : ℋ –1-1-onto→ ( LinFn ∩ ContFn )
2 f1ocnvdm ⊢ ( ( bra : ℋ –1-1-onto→ ( LinFn ∩ ContFn ) ∧ 𝑇 ∈ ( LinFn ∩ ContFn ) ) → ( ◡ bra ‘ 𝑇 ) ∈ ℋ )
3 1 2 mpan ⊢ ( 𝑇 ∈ ( LinFn ∩ ContFn ) → ( ◡ bra ‘ 𝑇 ) ∈ ℋ )