Description: Functionality of the Hilbert space identity operator. (Contributed by NM, 8-Aug-2006) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Assertion | hoif | ⊢ Iop : ℋ –1-1-onto→ ℋ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | f1oi | ⊢ ( I ↾ ℋ ) : ℋ –1-1-onto→ ℋ | |
2 | dfiop2 | ⊢ Iop = ( I ↾ ℋ ) | |
3 | f1oeq1 | ⊢ ( Iop = ( I ↾ ℋ ) → ( Iop : ℋ –1-1-onto→ ℋ ↔ ( I ↾ ℋ ) : ℋ –1-1-onto→ ℋ ) ) | |
4 | 2 3 | ax-mp | ⊢ ( Iop : ℋ –1-1-onto→ ℋ ↔ ( I ↾ ℋ ) : ℋ –1-1-onto→ ℋ ) |
5 | 1 4 | mpbir | ⊢ Iop : ℋ –1-1-onto→ ℋ |