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 \in C_{ℋ}$
	Assertion	pjrni	$⊢ ran {proj}_{ℎ} (H) = H$

Proof

Step	Hyp	Ref	Expression
1		pjfn.1	$⊢ H \in C_{ℋ}$
2	1	pjfni	$⊢ {proj}_{ℎ} (H) Fn ℋ$
3	1	pjcli	$⊢ x \in ℋ \to {proj}_{ℎ} (H) (x) \in H$
4	3	rgen	$⊢ \forall x \in ℋ {proj}_{ℎ} (H) (x) \in H$
5		ffnfv	$⊢ {proj}_{ℎ} (H) : ℋ ⟶ H \leftrightarrow ({proj}_{ℎ} (H) Fn ℋ \land \forall x \in ℋ {proj}_{ℎ} (H) (x) \in H)$
6	2 4 5	mpbir2an	$⊢ {proj}_{ℎ} (H) : ℋ ⟶ H$
7		frn	$⊢ {proj}_{ℎ} (H) : ℋ ⟶ H \to ran {proj}_{ℎ} (H) \subseteq H$
8	6 7	ax-mp	$⊢ ran {proj}_{ℎ} (H) \subseteq H$
9		pjid	$⊢ (H \in C_{ℋ} \land y \in H) \to {proj}_{ℎ} (H) (y) = y$
10	1 9	mpan	$⊢ y \in H \to {proj}_{ℎ} (H) (y) = y$
11	1	cheli	$⊢ y \in H \to y \in ℋ$
12		fnfvelrn	$⊢ ({proj}_{ℎ} (H) Fn ℋ \land y \in ℋ) \to {proj}_{ℎ} (H) (y) \in ran {proj}_{ℎ} (H)$
13	2 11 12	sylancr	$⊢ y \in H \to {proj}_{ℎ} (H) (y) \in ran {proj}_{ℎ} (H)$
14	10 13	eqeltrrd	$⊢ y \in H \to y \in ran {proj}_{ℎ} (H)$
15	14	ssriv	$⊢ H \subseteq ran {proj}_{ℎ} (H)$
16	8 15	eqssi	$⊢ ran {proj}_{ℎ} (H) = H$