This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem pjrni

Description: The range of a projection. Part of Theorem 26.2 of Halmos p. 44. (Contributed by NM, 30-Oct-1999) (Revised by Mario Carneiro, 10-Sep-2015) (New usage is discouraged.)

Ref Expression
Hypothesis pjfn.1 
|- H e. CH
Assertion pjrni 
|- ran ( projh ` H ) = H

Proof

Step Hyp Ref Expression
1 pjfn.1 
 |-  H e. CH
2 1 pjfni 
 |-  ( projh ` H ) Fn ~H
3 1 pjcli 
 |-  ( x e. ~H -> ( ( projh ` H ) ` x ) e. H )
4 3 rgen 
 |-  A. x e. ~H ( ( projh ` H ) ` x ) e. H
5 ffnfv 
 |-  ( ( projh ` H ) : ~H --> H <-> ( ( projh ` H ) Fn ~H /\ A. x e. ~H ( ( projh ` H ) ` x ) e. H ) )
6 2 4 5 mpbir2an 
 |-  ( projh ` H ) : ~H --> H
7 frn 
 |-  ( ( projh ` H ) : ~H --> H -> ran ( projh ` H ) C_ H )
8 6 7 ax-mp 
 |-  ran ( projh ` H ) C_ H
9 pjid 
 |-  ( ( H e. CH /\ y e. H ) -> ( ( projh ` H ) ` y ) = y )
10 1 9 mpan 
 |-  ( y e. H -> ( ( projh ` H ) ` y ) = y )
11 1 cheli 
 |-  ( y e. H -> y e. ~H )
12 fnfvelrn 
 |-  ( ( ( projh ` H ) Fn ~H /\ y e. ~H ) -> ( ( projh ` H ) ` y ) e. ran ( projh ` H ) )
13 2 11 12 sylancr 
 |-  ( y e. H -> ( ( projh ` H ) ` y ) e. ran ( projh ` H ) )
14 10 13 eqeltrrd 
 |-  ( y e. H -> y e. ran ( projh ` H ) )
15 14 ssriv 
 |-  H C_ ran ( projh ` H )
16 8 15 eqssi 
 |-  ran ( projh ` H ) = H