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