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	⊢ 𝐻 ∈ Cℋ
Assertion	pjrni	⊢ ran ( projℎ ‘ 𝐻 ) = 𝐻

Proof

Step	Hyp	Ref	Expression
1		pjfn.1	⊢ 𝐻 ∈ Cℋ
2	1	pjfni	⊢ ( projℎ ‘ 𝐻 ) Fn ℋ
3	1	pjcli	⊢ ( 𝑥 ∈ ℋ → ( ( projℎ ‘ 𝐻 ) ‘ 𝑥 ) ∈ 𝐻 )
4	3	rgen	⊢ ∀ 𝑥 ∈ ℋ ( ( projℎ ‘ 𝐻 ) ‘ 𝑥 ) ∈ 𝐻
5		ffnfv	⊢ ( ( projℎ ‘ 𝐻 ) : ℋ ⟶ 𝐻 ↔ ( ( projℎ ‘ 𝐻 ) Fn ℋ ∧ ∀ 𝑥 ∈ ℋ ( ( projℎ ‘ 𝐻 ) ‘ 𝑥 ) ∈ 𝐻 ) )
6	2 4 5	mpbir2an	⊢ ( projℎ ‘ 𝐻 ) : ℋ ⟶ 𝐻
7		frn	⊢ ( ( projℎ ‘ 𝐻 ) : ℋ ⟶ 𝐻 → ran ( projℎ ‘ 𝐻 ) ⊆ 𝐻 )
8	6 7	ax-mp	⊢ ran ( projℎ ‘ 𝐻 ) ⊆ 𝐻
9		pjid	⊢ ( ( 𝐻 ∈ Cℋ ∧ 𝑦 ∈ 𝐻 ) → ( ( projℎ ‘ 𝐻 ) ‘ 𝑦 ) = 𝑦 )
10	1 9	mpan	⊢ ( 𝑦 ∈ 𝐻 → ( ( projℎ ‘ 𝐻 ) ‘ 𝑦 ) = 𝑦 )
11	1	cheli	⊢ ( 𝑦 ∈ 𝐻 → 𝑦 ∈ ℋ )
12		fnfvelrn	⊢ ( ( ( projℎ ‘ 𝐻 ) Fn ℋ ∧ 𝑦 ∈ ℋ ) → ( ( projℎ ‘ 𝐻 ) ‘ 𝑦 ) ∈ ran ( projℎ ‘ 𝐻 ) )
13	2 11 12	sylancr	⊢ ( 𝑦 ∈ 𝐻 → ( ( projℎ ‘ 𝐻 ) ‘ 𝑦 ) ∈ ran ( projℎ ‘ 𝐻 ) )
14	10 13	eqeltrrd	⊢ ( 𝑦 ∈ 𝐻 → 𝑦 ∈ ran ( projℎ ‘ 𝐻 ) )
15	14	ssriv	⊢ 𝐻 ⊆ ran ( projℎ ‘ 𝐻 )
16	8 15	eqssi	⊢ ran ( projℎ ‘ 𝐻 ) = 𝐻