rnmptssbi

Description: The range of a function given by the maps-to notation as a subset. (Contributed by Glauco Siliprandi, 2-Jan-2022)

	Ref	Expression
Hypotheses	rnmptssbi.1	$⊢ Ⅎ x φ$
	rnmptssbi.2	$⊢ F = (x \in A ⟼ B)$
	rnmptssbi.3	$⊢ (φ \land x \in A) \to B \in V$
Assertion	rnmptssbi	$⊢ φ \to (ran F \subseteq C \leftrightarrow \forall x \in A B \in C)$

Step	Hyp	Ref	Expression
1		rnmptssbi.1	$⊢ Ⅎ x φ$
2		rnmptssbi.2	$⊢ F = (x \in A ⟼ B)$
3		rnmptssbi.3	$⊢ (φ \land x \in A) \to B \in V$
4		nfmpt1	$⊢ \underline{Ⅎ} x (x \in A ⟼ B)$
5	2 4	nfcxfr	$⊢ \underline{Ⅎ} x F$
6	5	nfrn	$⊢ \underline{Ⅎ} x ran F$
7		nfcv	$⊢ \underline{Ⅎ} x C$
8	6 7	nfss	$⊢ Ⅎ x ran F \subseteq C$
9	1 8	nfan	$⊢ Ⅎ x (φ \land ran F \subseteq C)$
10		simplr	$⊢ ((φ \land ran F \subseteq C) \land x \in A) \to ran F \subseteq C$
11		simpr	$⊢ ((φ \land ran F \subseteq C) \land x \in A) \to x \in A$
12	3	adantlr	$⊢ ((φ \land ran F \subseteq C) \land x \in A) \to B \in V$
13	2 11 12	elrnmpt1d	$⊢ ((φ \land ran F \subseteq C) \land x \in A) \to B \in ran F$
14	10 13	sseldd	$⊢ ((φ \land ran F \subseteq C) \land x \in A) \to B \in C$
15	9 14	ralrimia	$⊢ (φ \land ran F \subseteq C) \to \forall x \in A B \in C$
16	2	rnmptss	$⊢ \forall x \in A B \in C \to ran F \subseteq C$
17	16	adantl	$⊢ (φ \land \forall x \in A B \in C) \to ran F \subseteq C$
18	15 17	impbida	$⊢ φ \to (ran F \subseteq C \leftrightarrow \forall x \in A B \in C)$

Metamath Proof Explorer