Theorem 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	⊢ Ⅎ 𝑥 𝜑
	rnmptssbi.2	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
	rnmptssbi.3	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑉 )
Assertion	rnmptssbi	⊢ ( 𝜑 → ( ran 𝐹 ⊆ 𝐶 ↔ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		rnmptssbi.1	⊢ Ⅎ 𝑥 𝜑
2		rnmptssbi.2	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
3		rnmptssbi.3	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑉 )
4		nfmpt1	⊢ Ⅎ 𝑥 ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
5	2 4	nfcxfr	⊢ Ⅎ 𝑥 𝐹
6	5	nfrn	⊢ Ⅎ 𝑥 ran 𝐹
7		nfcv	⊢ Ⅎ 𝑥 𝐶
8	6 7	nfss	⊢ Ⅎ 𝑥 ran 𝐹 ⊆ 𝐶
9	1 8	nfan	⊢ Ⅎ 𝑥 ( 𝜑 ∧ ran 𝐹 ⊆ 𝐶 )
10		simplr	⊢ ( ( ( 𝜑 ∧ ran 𝐹 ⊆ 𝐶 ) ∧ 𝑥 ∈ 𝐴 ) → ran 𝐹 ⊆ 𝐶 )
11		simpr	⊢ ( ( ( 𝜑 ∧ ran 𝐹 ⊆ 𝐶 ) ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ 𝐴 )
12	3	adantlr	⊢ ( ( ( 𝜑 ∧ ran 𝐹 ⊆ 𝐶 ) ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑉 )
13	2 11 12	elrnmpt1d	⊢ ( ( ( 𝜑 ∧ ran 𝐹 ⊆ 𝐶 ) ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ran 𝐹 )
14	10 13	sseldd	⊢ ( ( ( 𝜑 ∧ ran 𝐹 ⊆ 𝐶 ) ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝐶 )
15	9 14	ralrimia	⊢ ( ( 𝜑 ∧ ran 𝐹 ⊆ 𝐶 ) → ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 )
16	2	rnmptss	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → ran 𝐹 ⊆ 𝐶 )
17	16	adantl	⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 ) → ran 𝐹 ⊆ 𝐶 )
18	15 17	impbida	⊢ ( 𝜑 → ( ran 𝐹 ⊆ 𝐶 ↔ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 ) )