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 ⊢ 𝐻 ∈ 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ℎ ‘ 𝐻 ) = 𝐻