Theorem rnmptssrn

Description: Inclusion relation for two ranges expressed in maps-to notation. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Hypotheses	rnmptssrn.b	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑉 )
	rnmptssrn.y	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ∃ 𝑦 ∈ 𝐶 𝐵 = 𝐷 )
Assertion	rnmptssrn	⊢ ( 𝜑 → ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ⊆ ran ( 𝑦 ∈ 𝐶 ↦ 𝐷 ) )

Proof

Step	Hyp	Ref	Expression
1		rnmptssrn.b	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑉 )
2		rnmptssrn.y	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ∃ 𝑦 ∈ 𝐶 𝐵 = 𝐷 )
3		eqid	⊢ ( 𝑦 ∈ 𝐶 ↦ 𝐷 ) = ( 𝑦 ∈ 𝐶 ↦ 𝐷 )
4	3 2 1	elrnmptd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ran ( 𝑦 ∈ 𝐶 ↦ 𝐷 ) )
5	4	ralrimiva	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 𝐵 ∈ ran ( 𝑦 ∈ 𝐶 ↦ 𝐷 ) )
6		eqid	⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
7	6	rnmptss	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ ran ( 𝑦 ∈ 𝐶 ↦ 𝐷 ) → ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ⊆ ran ( 𝑦 ∈ 𝐶 ↦ 𝐷 ) )
8	5 7	syl	⊢ ( 𝜑 → ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ⊆ ran ( 𝑦 ∈ 𝐶 ↦ 𝐷 ) )